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

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

What4.Solver.Adapter

Description

Synopsis

- data SolverAdapter (st :: Type -> Type) = SolverAdapter {
  - solver_adapter_name :: !String
  - solver_adapter_config_options :: ![ConfigDesc]
  - 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)
  - solver_adapter_write_smt2 :: !(forall t fs. ExprBuilder t st fs -> Handle -> [BoolExpr t] -> IO ())
  }
- defaultWriteSMTLIB2Features :: ProblemFeatures
- defaultSolverAdapter :: ConfigOption (BaseStringType Unicode)
- solverAdapterOptions :: forall (st :: Type -> Type). [SolverAdapter st] -> IO ([ConfigDesc], IO (SolverAdapter st))
- data LogData = LogData {
  - logCallbackVerbose :: Int -> String -> IO ()
  - logVerbosity :: Int
  - logReason :: String
  - logHandle :: Maybe Handle
  }
- logCallback :: LogData -> String -> IO ()
- defaultLogData :: LogData
- smokeTest :: forall t (st :: Type -> Type) fs. ExprBuilder t st fs -> SolverAdapter st -> IO (Maybe SomeException)

# Documentation

data SolverAdapter (st :: Type -> Type) Source #

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

Instances details

Show (SolverAdapter st) Source # |
Instance details Defined in What4.Solver.Adapter Methods showsPrec :: Int -> SolverAdapter st -> ShowS Source # show :: SolverAdapter st -> String Source # showList :: [SolverAdapter st] -> ShowS Source #
Eq (SolverAdapter st) Source # |
Instance details Defined in What4.Solver.Adapter Methods (==) :: SolverAdapter st -> SolverAdapter st -> Bool Source # (/=) :: SolverAdapter st -> SolverAdapter st -> Bool Source #
Ord (SolverAdapter st) Source # |

Instance details

Defined in What4.Solver.Adapter

Methods

compare :: SolverAdapter st -> SolverAdapter st -> Ordering Source #

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

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

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

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

max :: SolverAdapter st -> SolverAdapter st -> SolverAdapter st Source #

min :: SolverAdapter st -> SolverAdapter st -> SolverAdapter st Source #

defaultWriteSMTLIB2Features :: ProblemFeatures Source #

Default featues to use for writing SMTLIB2 files.

defaultSolverAdapter :: ConfigOption (BaseStringType Unicode) Source #

solverAdapterOptions :: forall (st :: Type -> Type). [SolverAdapter st] -> IO ([ConfigDesc], IO (SolverAdapter st)) Source #

data LogData Source #

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

defaultLogData :: LogData Source #

smokeTest :: forall t (st :: Type -> Type) fs. ExprBuilder t st fs -> SolverAdapter st -> IO (Maybe SomeException) Source #

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