This module provides a session monad to manage an interactive and incremental SMT solver session. Furthermore it includes abstractions for well-known SMT-LIB commands in Curry which are required during the interaction with an SMT solver.
Author: Jan Tikovsky, Marcellus Siegburg
Version: January 2018
getSess
:: SMTSess SMTSession
Get SMT session |
putSess
:: SMTSession -> SMTSess ()
Set an SMT session |
evalSess
:: SMTSess a -> SMT a
Evaluate multiple SMT sessions |
evalSessionsImpl
:: SMTSolver -> SMTOpts -> SMTSess a -> IO a
Evaluate SMT sessions by applying given solver and options |
evalSMT
:: SMT a -> SMTSession -> IO a
Evaluate an SMT action |
execSMT
:: SMT a -> SMTSession -> IO SMTSession
Execute an SMT action |
gets
:: (SMTSession -> a) -> SMT a
|
get
:: SMT SMTSession
Get SMT session |
put
:: SMTSession -> SMT ()
Set SMT session |
getStdin
:: SMT Handle
Get handle for stdin |
getStdout
:: SMT Handle
Get handle for stdout |
takeBuffer
:: SMT [Command]
Get buffered SMT commands and empty buffer |
getTrace
:: SMT [Command]
Get trace of SMT commands |
getGlobalCmds
:: SMT [Command]
Get global commands set in the SMT options |
isIncremental
:: SMT Bool
Check if incremental SMT solving is activated |
getGlobalDecls
:: SMT [Command]
Get global declarations |
modify
:: (SMTSession -> SMTSession) -> SMT ()
Modify an SMT session by applying the given function |
liftIOA
:: IO a -> SMTSess a
Lift an IO action directly to the SMT session monad |
liftSMT
:: SMT a -> SMTSess a
Lift an SMT action to the SMT session monad |
liftIO2SMT
:: IO a -> SMT a
Lift an IO action to the SMT monad |
evalSession
:: SMT a -> SMTSess a
Evaluate a singe SMT session (i.e. |
rsp2Msg
:: CmdResponse -> SMTError
Transform a command response to an error message |
res2Msgs
:: SMTResult -> [SMTError]
Transform a result to list of error messages |
declareVars
:: Int -> Sort -> SMT [Term]
Declare n fresh SMT variables of given sort |
checkSat
:: SMT SMTResult
Check for syntactic errors as well as for satisfiability of the assertions |
getModel
:: SMT (Either [SMTError] [ModelRsp])
Get a model for the current assertions on the solver stack |
getValues
:: [Term] -> SMT (Either [SMTError] [(Term,Term)])
Get bindings for given variables for the current assertions on the solver stack |
bufferGlobalDefs
:: SMT ()
Buffer global definitions in SMT session |
resetSession
:: SMT ()
Reset SMT session (by resetting the SMT solver stack) |
optReset
:: SMT ()
Optional reset of SMT session (in case of non-incremental solving) |
optTracing
:: [Command] -> SMT ()
Optional tracing of SMT-LIB commands in the given buffer |
closeSession
:: SMT ()
Close SMT session |
startSession
:: SMTSolver -> SMTOpts -> IO SMTSession
Low-level SMT solver interaction Start SMT solver process and initialize fresh SMT session |
termSession
:: SMTSession -> IO ()
Terminate SMT solver process |
dumpSession
:: SMTSession -> IO ()
Produce dump of SMT-LIB commands used during an SMT session |
bufferCmds
:: [Command] -> SMT ()
Buffer given SMT-LIB commands |
sendCmds
:: [Command] -> SMT ()
Send SMT-LIB commands to SMT solver |
getDelimited
:: SMT String
Get response string of an SMT solver |
info
:: String -> SMT ()
Write status information to the command line when quiet option is set to False |
rmvEchos
:: [Command] -> [Command]
Remove all Echo commands
|
An SMT solver session includes
Constructors:
SMTSession
:: (Handle,Handle,Handle) -> [Command] -> [Command] -> SMTOpts -> Int -> [Command] -> SMTSession
Fields:
Session monad maintaining session information during multiple SMT sessions
Constructors:
SMTSess
:: (SMTSession -> SMT (a,SMTSession)) -> SMTSess a
Fields:
runSMTSess
:: (SMTSession -> SMT (a,SMTSession))
SMT monad maintaining session information while performing SMT actions during a single SMT session
Constructors:
SMT
:: (SMTSession -> IO (a,SMTSession)) -> SMT a
Fields:
runSMT
:: (SMTSession -> IO (a,SMTSession))
High-level SMT solver interaction SMT solver result
Constructors:
Error
:: [SMTError] -> SMTResult
Unsat
:: SMTResult
Unknown
:: SMTResult
Sat
:: SMTResult
Model
:: [ModelRsp] -> SMTResult
Values
:: [ValuationPair] -> SMTResult
|
Get SMT session |
|
Set an SMT session |
|
Evaluate SMT sessions by applying given solver and options |
|
Evaluate an SMT action |
|
Execute an SMT action |
|
|
|
Get SMT session |
|
Set SMT session |
|
Get buffered SMT commands and empty buffer |
|
Get global commands set in the SMT options |
|
Check if incremental SMT solving is activated |
|
Get global declarations |
|
Modify an SMT session by applying the given function |
|
Lift an IO action to the SMT monad |
|
Evaluate a singe SMT session (i.e. lift SMT action to Session monad and thread session) |
|
Transform a command response to an error message |
|
Declare n fresh SMT variables of given sort |
|
Check for syntactic errors as well as for satisfiability of the assertions |
|
Get a model for the current assertions on the solver stack |
|
Get bindings for given variables for the current assertions on the solver stack |
|
Buffer global definitions in SMT session |
|
Reset SMT session (by resetting the SMT solver stack) |
|
Optional tracing of SMT-LIB commands in the given buffer |
|
Close SMT session |
|
Low-level SMT solver interaction Start SMT solver process and initialize fresh SMT session |
|
Terminate SMT solver process |
|
Produce dump of SMT-LIB commands used during an SMT session |
|
Buffer given SMT-LIB commands |
|
Get response string of an SMT solver |
|
Write status information to the command line when quiet option is set to False |