What4.Solver.Adapter

Documentation

data SolverAdapter st

The main interface for interacting with a solver in an "offline" fashion, which means that a new solver process is started for each query.

Constructors

SolverAdapter

Fields

• solver_adapter_name :: !String
• solver_adapter_config_options :: ![ConfigDesc]

  Configuration options relevant to this solver adapter

• solver_adapter_check_sat :: !(forall t fs a. ExprBuilder t st fs -> LogData -> [BoolExpr t] -> (SatResult (GroundEvalFn t, Maybe (ExprRangeBindings t)) () -> IO a) -> IO a)

  Operation to check the satisfiability of a formula. The final argument is a callback that calculates the ultimate result from a SatResult and operations for finding model values in the event of a SAT result. Note: the evaluation functions may cease to be avaliable after the callback completes, so any necessary information should be extracted from them before returning.

• solver_adapter_write_smt2 :: !(forall t fs. ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ())

  Write an SMTLib2 problem instance onto the given handle, incorporating any solver-specific tweaks appropriate to this solver

Instances

Eq (SolverAdapter st)

Defined in What4.Solver.Adapter

Methods

(==) :: SolverAdapter st -> SolverAdapter st -> Bool

(/=) :: SolverAdapter st -> SolverAdapter st -> Bool

Ord (SolverAdapter st)

Defined in What4.Solver.Adapter

Methods

compare :: SolverAdapter st -> SolverAdapter st -> Ordering

(<) :: SolverAdapter st -> SolverAdapter st -> Bool

(<=) :: SolverAdapter st -> SolverAdapter st -> Bool

(>) :: SolverAdapter st -> SolverAdapter st -> Bool

(>=) :: SolverAdapter st -> SolverAdapter st -> Bool

max :: SolverAdapter st -> SolverAdapter st -> SolverAdapter st

min :: SolverAdapter st -> SolverAdapter st -> SolverAdapter st

Show (SolverAdapter st)

Defined in What4.Solver.Adapter

Methods

showsPrec :: Int -> SolverAdapter st -> ShowS

show :: SolverAdapter st -> String

showList :: [SolverAdapter st] -> ShowS

defaultWriteSMTLIB2Features :: ProblemFeatures

Default featues to use for writing SMTLIB2 files.

defaultSolverAdapter :: ConfigOption (BaseStringType Unicode)

solverAdapterOptions :: [SolverAdapter st] -> IO ([ConfigDesc], IO (SolverAdapter st))

data LogData

A collection of operations for producing output from solvers. Solvers can produce messages at varying verbosity levels that might be appropriate for user output by using the logCallbackVerbose operation. If a logHandle is provided, the entire interaction sequence with the solver will be mirrored into that handle.

Constructors

LogData

Fields

• logCallbackVerbose :: Int -> String -> IO ()

  takes a verbosity and a message to log

• logVerbosity :: Int

  the default verbosity; typical default is 2

• logReason :: String

  the reason for performing the operation

• logHandle :: Maybe Handle

  handle on which to mirror solver input/responses

logCallback :: LogData -> String -> IO ()

defaultLogData :: LogData

smokeTest :: ExprBuilder t st fs -> SolverAdapter st -> IO (Maybe SomeException)

Test the ability to interact with a solver by peforming a check-sat query on a trivially unsatisfiable problem.