what4-1.5.1: Solver-agnostic symbolic values support for issuing queries

Copyright | (c) Galois Inc 2018-2020
License | BSD3
Maintainer | Rob Dockins <rdockins@galois.com>
Safe Haskell | Safe-Inferred
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 = forall s.OnlineSolver s => AnOnlineSolver (Proxy s)
- data SolverProcess scope solver = SolverProcess {
  - solverConn :: !(WriterConn scope solver)
  - solverCleanupCallback :: IO ExitCode
  - solverHandle :: !ProcessHandle
  - solverErrorBehavior :: !ErrorBehavior
  - solverStderr :: !HandleReader
  - solverEvalFuns :: !(SMTEvalFunctions solver)
  - solverLogFn :: SolverEvent -> IO ()
  - solverName :: String
  - solverEarlyUnsat :: IORef (Maybe Int)
  - solverSupportsResetAssertions :: Bool
  - solverGoalTimeout :: SolverGoalTimeout
  }
- solverStdin :: SolverProcess t solver -> OutputStream Text
- solverResponse :: SolverProcess t solver -> InputStream Text
- newtype SolverGoalTimeout = SolverGoalTimeout {
  - getGoalTimeoutInMilliSeconds :: Integer
  }
- getGoalTimeoutInSeconds :: SolverGoalTimeout -> Integer
- withLocalGoalTimeout :: SolverProcess t s -> (WriterConn t s -> IO (SatResult () ())) -> IO (Either SomeException (SatResult () ()))
- data ErrorBehavior
  - = ImmediateExit
  - | ContinueOnError
- killSolver :: SolverProcess t solver -> IO ()
- push :: SMTReadWriter solver => SolverProcess scope solver -> IO ()
- pop :: SMTReadWriter solver => SolverProcess scope solver -> IO ()
- tryPop :: 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
- inNewFrame2Open :: SMTReadWriter solver => SolverProcess scope solver -> IO ()
- inNewFrame2Close :: SMTReadWriter solver => SolverProcess scope solver -> IO ()
- 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]
- getAbducts :: SMTReadWriter solver => SolverProcess scope solver -> Int -> Text -> BoolExpr scope -> IO [String]
- 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

Instances details

OnlineSolver Connection Source # |
Instance details Defined in What4.Solver.Yices Methods startSolverProcess :: forall scope (st :: Type -> Type) fs. ProblemFeatures -> Maybe Handle -> ExprBuilder scope st fs -> IO (SolverProcess scope Connection) Source # shutdownSolverProcess :: SolverProcess scope Connection -> IO (ExitCode, Text) Source #
OnlineSolver (Writer Boolector) Source # |
Instance details 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)) Source # shutdownSolverProcess :: SolverProcess scope (Writer Boolector) -> IO (ExitCode, Text) Source #
OnlineSolver (Writer CVC4) Source # |
Instance details 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)) Source # shutdownSolverProcess :: SolverProcess scope (Writer CVC4) -> IO (ExitCode, Text) Source #
OnlineSolver (Writer CVC5) Source # |
Instance details Defined in What4.Solver.CVC5 Methods startSolverProcess :: forall scope (st :: Type -> Type) fs. ProblemFeatures -> Maybe Handle -> ExprBuilder scope st fs -> IO (SolverProcess scope (Writer CVC5)) Source # shutdownSolverProcess :: SolverProcess scope (Writer CVC5) -> 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 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 #

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

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

Standard input stream for the solver process.

solverResponse :: SolverProcess t solver -> InputStream Text Source #

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

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

Constructors

SolverGoalTimeout |

Fields

- getGoalTimeoutInMilliSeconds :: Integer

#### Instances

Instances details

Show SolverGoalTimeout Source # |
Instance details Defined in What4.Protocol.Online Methods showsPrec :: Int -> SolverGoalTimeout -> ShowS Source # show :: SolverGoalTimeout -> String Source # showList :: [SolverGoalTimeout] -> ShowS Source #
Pretty SolverGoalTimeout Source # |
Instance details Defined in What4.Protocol.Online Methods pretty :: SolverGoalTimeout -> Doc ann Source # prettyList :: [SolverGoalTimeout] -> Doc ann Source #

getGoalTimeoutInSeconds :: SolverGoalTimeout -> Integer Source #

Get the SolverGoalTimeout raw numeric value in units of seconds.

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

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

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

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

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.

inNewFrame2Open :: SMTReadWriter solver => SolverProcess scope solver -> IO () Source #

Open a second solver assumption frame. For abduction, we want the final assertion to be a in a new frame, so that it can be closed before asking for abducts. The following two commands allow frame 2 to be pushed and popped independently of other commands

inNewFrame2Close :: SMTReadWriter solver => SolverProcess scope solver -> IO () Source #

Close a second solver assumption 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 evaluation 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.

getAbducts :: SMTReadWriter solver => SolverProcess scope solver -> Int -> Text -> BoolExpr scope -> IO [String] Source #

`get-abuct nm t` queries the solver for the first abduct, which is returned as an SMT function definition named `nm`. The remaining abducts are obtained from the solver by successive invocations of the `get-abduct-next` command, which return SMT functions bound to the same `nm` as the first. The name `nm` is bound within the current assertion frame. Note that this is an unstable API; we expect that the return type will change to a parsed expression in the future

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.