What4.Protocol.Online

This module defines an API for interacting with solvers that support online interaction modes.

Documentation

class SMTReadWriter solver => OnlineSolver solver where

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)

Start a new solver process attached to the given ExprBuilder.

shutdownSolverProcess :: forall scope. SolverProcess scope solver -> IO (ExitCode, Text)

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

Defined in What4.Solver.Yices

Methods

startSolverProcess :: forall scope (st :: Type -> Type) fs. ProblemFeatures -> Maybe Handle -> ExprBuilder scope st fs -> IO (SolverProcess scope Connection)

shutdownSolverProcess :: SolverProcess scope Connection -> IO (ExitCode, Text)

OnlineSolver (Writer Z3)

Defined in What4.Solver.Z3

Methods

startSolverProcess :: forall scope (st :: Type -> Type) fs. ProblemFeatures -> Maybe Handle -> ExprBuilder scope st fs -> IO (SolverProcess scope (Writer Z3))

shutdownSolverProcess :: SolverProcess scope (Writer Z3) -> IO (ExitCode, Text)

OnlineSolver (Writer STP)

Defined in What4.Solver.STP

Methods

startSolverProcess :: forall scope (st :: Type -> Type) fs. ProblemFeatures -> Maybe Handle -> ExprBuilder scope st fs -> IO (SolverProcess scope (Writer STP))

shutdownSolverProcess :: SolverProcess scope (Writer STP) -> IO (ExitCode, Text)

OnlineSolver (Writer CVC4)

Defined in What4.Solver.CVC4

Methods

startSolverProcess :: forall scope (st :: Type -> Type) fs. ProblemFeatures -> Maybe Handle -> ExprBuilder scope st fs -> IO (SolverProcess scope (Writer CVC4))

shutdownSolverProcess :: SolverProcess scope (Writer CVC4) -> IO (ExitCode, Text)

OnlineSolver (Writer Boolector)

Defined in What4.Solver.Boolector

Methods

startSolverProcess :: forall scope (st :: Type -> Type) fs. ProblemFeatures -> Maybe Handle -> ExprBuilder scope st fs -> IO (SolverProcess scope (Writer Boolector))

shutdownSolverProcess :: SolverProcess scope (Writer Boolector) -> IO (ExitCode, Text)

data AnOnlineSolver

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

Constructors

forall s.OnlineSolver s => AnOnlineSolver (Proxy s)

data SolverProcess scope solver

A live connection to a running solver process.

This data structure should be used in a single-threaded 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.

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

• 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.

• solverGoalTimeout :: SolverGoalTimeout

  The amount of time (in seconds) that a solver should spend trying to satisfy any particular goal before giving up. A value of zero indicates no time limit.

  Note that it is not sufficient to set just this value to control timeouts; this value is used as a reference for common code (e.g. SMTLIB2) to determine the timeout for the associated timer. When initialized, this field of the SolverProcess is initialized from a solver-specific timeout configuration (e.g. z3Timeout); the latter is the definitive reference for the timeout, and solver-specific code will likely use the the latter rather than this common field.

solverStdin :: SolverProcess t solver -> OutputStream Text

Standard input stream for the solver process.

solverResponse :: SolverProcess t solver -> InputStream Text

The solver's stdout, for easier parsing of responses.

newtype SolverGoalTimeout

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.

Constructors

SolverGoalTimeout

Fields

• getGoalTimeoutInMilliSeconds :: Integer

Instances

Show SolverGoalTimeout

Defined in What4.Protocol.Online

Methods

showsPrec :: Int -> SolverGoalTimeout -> ShowS

show :: SolverGoalTimeout -> String

showList :: [SolverGoalTimeout] -> ShowS

Pretty SolverGoalTimeout

Defined in What4.Protocol.Online

Methods

pretty :: SolverGoalTimeout -> Doc ann

prettyList :: [SolverGoalTimeout] -> Doc ann

getGoalTimeoutInSeconds :: SolverGoalTimeout -> Integer

Get the SolverGoalTimeout raw numeric value in units of seconds.

withLocalGoalTimeout :: SolverProcess t s -> (WriterConn t s -> IO (SatResult () ())) -> IO (Either SomeException (SatResult () ()))

If the solver cannot voluntarily limit itself to the requested timeout period, this runs a local async process with a slightly longer time period that will forcibly terminate the solver process if it expires while the solver process is still running.

Note that this will require re-establishment of the solver process and any associated context for any subsequent solver goal evaluation.

data ErrorBehavior

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 ()

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 ()

Push a new solver assumption frame.

pop :: SMTReadWriter solver => SolverProcess scope solver -> IO ()

Pop a previous solver assumption frame.

tryPop :: SMTReadWriter solver => SolverProcess scope solver -> IO ()

Pop a previous solver assumption frame, but allow this to fail if the solver has exited.

reset :: SMTReadWriter solver => SolverProcess scope solver -> IO ()

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

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

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 () ())

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) ())

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 () ())

checkWithAssumptionsAndModel :: SMTReadWriter solver => SolverProcess scope solver -> String -> [BoolExpr scope] -> IO (SatResult (GroundEvalFn scope) ())

getModel :: SMTReadWriter solver => SolverProcess scope solver -> IO (GroundEvalFn scope)

Following a successful check-sat command, build a ground evaluation function that will evaluate terms in the context of the current model.

getUnsatCore :: SMTReadWriter solver => SolverProcess scope solver -> IO [Text]

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)]

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 () ())

Get the sat result from a previous SAT command.

checkSatisfiable :: SMTReadWriter solver => SolverProcess scope solver -> String -> BoolExpr scope -> IO (SatResult () ())

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

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.