Copyright	(c) Galois Inc 2018-2020
License	BSD3
Maintainer	Rob Dockins <rdockins@galois.com>
Safe Haskell	None
Language	Haskell2010

What4.Protocol.Online

Description

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 = 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
}
data ErrorBehavior
- = ImmediateExit
- | ContinueOnError
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.

Methods

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

OnlineSolver Connection Source #
Instance details Defined in What4.Solver.Yices Methods startSolverProcess :: ProblemFeatures -> Maybe Handle -> ExprBuilder scope st fs -> IO (SolverProcess scope Connection) Source # shutdownSolverProcess :: SolverProcess scope Connection -> IO (ExitCode, Text) Source #
OnlineSolver (Writer Z3) Source #
Instance details Defined in What4.Solver.Z3 Methods startSolverProcess :: ProblemFeatures -> Maybe Handle -> ExprBuilder scope st fs -> IO (SolverProcess scope (Writer Z3)) Source # shutdownSolverProcess :: SolverProcess scope (Writer Z3) -> IO (ExitCode, Text) Source #
OnlineSolver (Writer STP) Source #
Instance details Defined in What4.Solver.STP Methods startSolverProcess :: ProblemFeatures -> Maybe Handle -> ExprBuilder scope st fs -> IO (SolverProcess scope (Writer STP)) Source # shutdownSolverProcess :: SolverProcess scope (Writer STP) -> IO (ExitCode, Text) Source #
OnlineSolver (Writer CVC4) Source #
Instance details Defined in What4.Solver.CVC4 Methods startSolverProcess :: ProblemFeatures -> Maybe Handle -> ExprBuilder scope st fs -> IO (SolverProcess scope (Writer CVC4)) Source # shutdownSolverProcess :: SolverProcess scope (Writer CVC4) -> IO (ExitCode, Text) Source #
OnlineSolver (Writer Boolector) Source #
Instance details Defined in What4.Solver.Boolector Methods startSolverProcess :: ProblemFeatures -> Maybe Handle -> ExprBuilder scope st fs -> IO (SolverProcess scope (Writer Boolector)) Source # shutdownSolverProcess :: SolverProcess scope (Writer Boolector) -> IO (ExitCode, Text) Source #

data AnOnlineSolver Source #

Simple data-type encapsulating some implementation of an online solver.

Constructors

OnlineSolver s => AnOnlineSolver (Proxy s)

data SolverProcess scope solver Source #

A live connection to a running solver process.

Constructors

SolverProcess

Fields

solverConn :: !(WriterConn scope solver)
Writer for sending commands to the solver
solverCleanupCallback :: IO ExitCode
Callback for regular code paths to gracefully close associated pipes and wait for the process to shutdown
solverHandle :: !ProcessHandle
Handle to the solver process
solverStdin :: !(OutputStream Text)
Standard in for the solver process.
solverResponse :: !(InputStream Text)
Wrap the solver's stdout, for easier parsing of responses.
solverErrorBehavior :: !ErrorBehavior
Indicate this solver's behavior following an error response
solverStderr :: !HandleReader
Standard error for the solver process
solverEvalFuns :: !(SMTEvalFunctions solver)
The functions used to parse values out of models.
solverLogFn :: SolverEvent -> IO ()
solverName :: String
solverEarlyUnsat :: IORef (Maybe Int)
Some solvers will enter an UNSAT state early, if they can easily determine that context is unsatisfiable. If this IORef contains an integer value, it indicates how many "pop" operations need to be performed to return to a potentially satisfiable state. A Just 0 state indicates the special case that the top-level context is unsatisfiable, and must be "reset".
solverSupportsResetAssertions :: Bool
Some solvers do not have support for the SMTLib2.6 operation (reset-assertions), or an equivalent. For these solvers, we instead make sure to always have at least one assertion frame pushed, and pop all outstanding frames (and push a new top-level one) as a way to mimic the reset behavior.

data ErrorBehavior Source #

This datatype describes how a solver will behave following an error.

Constructors

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 top-level 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 check-sat 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 check-sat 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 check-with-assumptions 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.