Documentation

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

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