This module provides operations for an interactive communication with SMT solvers  which implement the SMTLIB interface  via stdin and stdout. Currently only the Z3 SMT solver is supported.
Author: Jan Tikovsky, Marcellus Siegburg
Version: January 2018
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 SMTLIB 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 SMTLIB commands and try to find a binding for all given variables 
default options for SMT solving

Evaluate SMT sessions by applying given solver and options 
Set options for SMT solving 
Get n fresh variables of given sort 