Copyright  (c) Galois Inc 20182020 

License  BSD3 
Maintainer  Rob Dockins <rdockins@galois.com> 
Safe Haskell  None 
Language  Haskell2010 
This module defines an API for interacting with solvers that support online interaction modes.
Synopsis
 class SMTReadWriter solver => OnlineSolver solver where
 startSolverProcess :: forall scope st fs. ProblemFeatures > Maybe Handle > ExprBuilder scope st fs > IO (SolverProcess scope solver)
 shutdownSolverProcess :: forall scope. SolverProcess scope solver > IO (ExitCode, Text)
 data AnOnlineSolver = forall s.OnlineSolver s => AnOnlineSolver (Proxy s)
 data SolverProcess scope solver = SolverProcess {
 solverConn :: !(WriterConn scope solver)
 solverCleanupCallback :: IO ExitCode
 solverHandle :: !ProcessHandle
 solverStdin :: !(OutputStream Text)
 solverResponse :: !(InputStream Text)
 solverErrorBehavior :: !ErrorBehavior
 solverStderr :: !HandleReader
 solverEvalFuns :: !(SMTEvalFunctions solver)
 solverLogFn :: SolverEvent > IO ()
 solverName :: String
 solverEarlyUnsat :: IORef (Maybe Int)
 solverSupportsResetAssertions :: Bool
 solverGoalTimeout :: SolverGoalTimeout
 newtype SolverGoalTimeout = SolverGoalTimeout {}
 getGoalTimeoutInSeconds :: SolverGoalTimeout > Integer
 data ErrorBehavior
 killSolver :: SolverProcess t solver > IO ()
 push :: SMTReadWriter solver => SolverProcess scope solver > IO ()
 pop :: SMTReadWriter solver => SolverProcess scope solver > IO ()
 reset :: SMTReadWriter solver => SolverProcess scope solver > IO ()
 inNewFrame :: (MonadIO m, MonadMask m, SMTReadWriter solver) => SolverProcess scope solver > m a > m a
 inNewFrameWithVars :: (MonadIO m, MonadMask m, SMTReadWriter solver) => SolverProcess scope solver > [Some (ExprBoundVar scope)] > m a > m a
 check :: SMTReadWriter solver => SolverProcess scope solver > String > IO (SatResult () ())
 checkAndGetModel :: SMTReadWriter solver => SolverProcess scope solver > String > IO (SatResult (GroundEvalFn scope) ())
 checkWithAssumptions :: SMTReadWriter solver => SolverProcess scope solver > String > [BoolExpr scope] > IO ([Text], SatResult () ())
 checkWithAssumptionsAndModel :: SMTReadWriter solver => SolverProcess scope solver > String > [BoolExpr scope] > IO (SatResult (GroundEvalFn scope) ())
 getModel :: SMTReadWriter solver => SolverProcess scope solver > IO (GroundEvalFn scope)
 getUnsatCore :: SMTReadWriter solver => SolverProcess scope solver > IO [Text]
 getUnsatAssumptions :: SMTReadWriter solver => SolverProcess scope solver > IO [(Bool, Text)]
 getSatResult :: SMTReadWriter s => SolverProcess t s > IO (SatResult () ())
 checkSatisfiable :: SMTReadWriter solver => SolverProcess scope solver > String > BoolExpr scope > IO (SatResult () ())
 checkSatisfiableWithModel :: SMTReadWriter solver => SolverProcess scope solver > String > BoolExpr scope > (SatResult (GroundEvalFn scope) () > IO a) > IO a
Documentation
class SMTReadWriter solver => OnlineSolver solver where Source #
This class provides an API for starting and shutting down connections to various different solvers that support online interaction modes.
startSolverProcess :: forall scope st fs. ProblemFeatures > Maybe Handle > ExprBuilder scope st fs > IO (SolverProcess scope solver) Source #
Start a new solver process attached to the given ExprBuilder
.
shutdownSolverProcess :: forall scope. SolverProcess scope solver > IO (ExitCode, Text) Source #
Shut down a solver process. The process will be asked to shut down in
a "polite" way, e.g., by sending an (exit)
message, or by closing
the process's stdin
. Use killProcess
instead to shutdown a process
via a signal.
Instances
data AnOnlineSolver Source #
Simple datatype encapsulating some implementation of an online solver.
forall s.OnlineSolver s => AnOnlineSolver (Proxy s) 
data SolverProcess scope solver Source #
A live connection to a running solver process.
This data structure should be used in a singlethreaded manner or with external synchronization to ensure that only a single thread has access at a time. Unsynchronized multithreaded use will lead to race conditions and very strange results.
SolverProcess  

newtype SolverGoalTimeout Source #
The amount of time that a solver is allowed to attempt to satisfy any particular goal.
The timeout value may be retrieved with
getGoalTimeoutInMilliSeconds
or getGoalTimeoutInSeconds
.
getGoalTimeoutInSeconds :: SolverGoalTimeout > Integer Source #
Get the SolverGoalTimeout raw numeric value in units of seconds.
data ErrorBehavior Source #
This datatype describes how a solver will behave following an error.
ImmediateExit  This indicates the solver will immediately exit following an error 
ContinueOnError  This indicates the solver will remain live and respond to further commmands following an error 
killSolver :: SolverProcess t solver > IO () Source #
An impolite way to shut down a solver. Prefer to use
shutdownSolverProcess
, unless the solver is unresponsive
or in some unrecoverable error state.
push :: SMTReadWriter solver => SolverProcess scope solver > IO () Source #
Push a new solver assumption frame.
pop :: SMTReadWriter solver => SolverProcess scope solver > IO () Source #
Pop a previous solver assumption frame.
reset :: SMTReadWriter solver => SolverProcess scope solver > IO () Source #
Pop all assumption frames and remove all toplevel asserts from the global scope. Forget all declarations except those in scope at the top level.
inNewFrame :: (MonadIO m, MonadMask m, SMTReadWriter solver) => SolverProcess scope solver > m a > m a Source #
Perform an action in the scope of a solver assumption frame.
inNewFrameWithVars :: (MonadIO m, MonadMask m, SMTReadWriter solver) => SolverProcess scope solver > [Some (ExprBoundVar scope)] > m a > m a Source #
Perform an action in the scope of a solver assumption frame, where the given bound variables are considered free within that frame.
check :: SMTReadWriter solver => SolverProcess scope solver > String > IO (SatResult () ()) Source #
Send a check command to the solver, and get the SatResult without asking a model.
checkAndGetModel :: SMTReadWriter solver => SolverProcess scope solver > String > IO (SatResult (GroundEvalFn scope) ()) Source #
Send a check command to the solver and get the model in the case of a SAT result.
checkWithAssumptions :: SMTReadWriter solver => SolverProcess scope solver > String > [BoolExpr scope] > IO ([Text], SatResult () ()) Source #
checkWithAssumptionsAndModel :: SMTReadWriter solver => SolverProcess scope solver > String > [BoolExpr scope] > IO (SatResult (GroundEvalFn scope) ()) Source #
getModel :: SMTReadWriter solver => SolverProcess scope solver > IO (GroundEvalFn scope) Source #
Following a successful checksat command, build a ground evaulation function that will evaluate terms in the context of the current model.
getUnsatCore :: SMTReadWriter solver => SolverProcess scope solver > IO [Text] Source #
After an unsatisfiable checksat command, compute a set of the named assertions that (together with all the unnamed assertions) form an unsatisfiable core. Note: the returned unsatisfiable core might not be minimal.
getUnsatAssumptions :: SMTReadWriter solver => SolverProcess scope solver > IO [(Bool, Text)] Source #
After an unsatisfiable checkwithassumptions command, compute a set of the supplied
assumptions that (together with previous assertions) form an unsatisfiable core.
Note: the returned unsatisfiable set might not be minimal. The boolean value
returned along with the name indicates if the assumption was negated or not:
True
indidcates a positive atom, and False
represents a negated atom.
getSatResult :: SMTReadWriter s => SolverProcess t s > IO (SatResult () ()) Source #
Get the sat result from a previous SAT command.
checkSatisfiable :: SMTReadWriter solver => SolverProcess scope solver > String > BoolExpr scope > IO (SatResult () ()) Source #
Check if the given formula is satisfiable in the current solver state, without requesting a model. This is done in a fresh frame, which is exited after the check call.
checkSatisfiableWithModel :: SMTReadWriter solver => SolverProcess scope solver > String > BoolExpr scope > (SatResult (GroundEvalFn scope) () > IO a) > IO a Source #
Check if the formula is satisifiable in the current solver state. This is done in a fresh frame, which is exited after the continuation complets. The evaluation function can be used to query the model. The model is valid only in the given continuation.