Module Solver.SMTLIB.Session

This module provides operations for an interactive communication with SMT solvers - which implement the SMT-LIB interface - via stdin and stdout. Currently only the Z3 SMT solver is supported.

Author: Jan Tikovsky, Marcellus Siegburg

Version: January 2018

Summary of exported operations:

defSMTOpts
                  ::  SMTOpts

default options for SMT solving

evalSessions
                  ::  SMTSolver -> SMTOpts -> SMTSess a -> IO a

Evaluate SMT sessions by applying given solver and options

setSMTOpts
                  ::  SMTOpts -> SMTSess ()

Set options for SMT solving

freshSMTVars
                  ::  Int -> Sort -> SMTSess [Term]

Get n fresh variables of given sort

solveSMT
                  ::  [Command] -> SMTSess (Either [SMTError] [ModelRsp])

Solve the SMT problem specified by the given SMT-LIB commands and try to find a binding for all variables used

solveSMTVars
                  ::  [Term] -> [Command] -> SMTSess (Either [SMTError] [(Term,Term)])

Solve the SMT problem specified by the given SMT-LIB commands and try to find a binding for all given variables

Exported operations:

defSMTOpts :: SMTOpts

default options for SMT solving

Further infos:

solution complete, i.e., able to compute all solutions

evalSessions :: SMTSolver -> SMTOpts -> SMTSess a -> IO a

Evaluate SMT sessions by applying given solver and options

setSMTOpts :: SMTOpts -> SMTSess ()

Set options for SMT solving

freshSMTVars :: Int -> Sort -> SMTSess [Term]

Get n fresh variables of given sort

solveSMT :: [Command] -> SMTSess (Either [SMTError] [ModelRsp])

Solve the SMT problem specified by the given SMT-LIB commands and try to find a binding for all variables used

solveSMTVars :: [Term] -> [Command] -> SMTSess (Either [SMTError] [(Term,Term)])

Solve the SMT problem specified by the given SMT-LIB commands and try to find a binding for all given variables