what4-1.1: Solver-agnostic symbolic values support for issuing queries
Copyright(c) Galois Inc 2018-2020
LicenseBSD3
MaintainerRob Dockins <rdockins@galois.com>
Safe HaskellNone
LanguageHaskell2010

What4.Protocol.Online

Description

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

Synopsis

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

Instances details
OnlineSolver Connection Source # 
Instance details

Defined in What4.Solver.Yices

OnlineSolver (Writer Z3) Source # 
Instance details

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)) Source #

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

OnlineSolver (Writer STP) Source # 
Instance details

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)) Source #

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

OnlineSolver (Writer CVC4) Source # 
Instance details

Defined in What4.Solver.CVC4

OnlineSolver (Writer Boolector) Source # 
Instance details

Defined in What4.Solver.Boolector

data AnOnlineSolver Source #

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

Constructors

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

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.

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 #

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.