Language.Hasmtlib.Solver.Common

Documentation

solver :: (RenderSeq s, MonadIO m) => Config -> Solver s m

Creates a Solver from a Config.

debug :: (RenderSeq s, MonadIO m) => Config -> Debugger s -> Solver s m

Creates a debugging Solver from a Config.

interactiveSolver :: MonadIO m => Config -> m (Solver, Handle)

Creates an interactive session with a solver by creating and returning an alive process-handle Handle. Queues commands by default, see Queuing.

data Debugger s

A type holding actions for debugging states.

Constructors

Debugger

Fields

• debugState :: s -> IO ()

  Debug the entire state

• debugProblem :: Seq Builder -> IO ()

  Debug the linewise-rendered problem

• debugResultResponse :: ByteString -> IO ()

  Debug the solvers raw response for (check-sat)

• debugModelResponse :: ByteString -> IO ()

  Debug the solvers raw response for (get-model)

Instances

Default (Debugger OMT)

Defined in Language.Hasmtlib.Solver.Common

Methods

def :: Debugger OMT

Default (Debugger SMT)

Defined in Language.Hasmtlib.Solver.Common

Methods

def :: Debugger SMT

processSolver :: (RenderSeq s, MonadIO m) => Config -> Maybe (Debugger s) -> Solver s m

A Solver which holds an external process with a SMT-Solver. This will:

1. Encode the SMT-problem,
2. Start a new external process for the SMT-Solver,
3. Send the problem to the SMT-Solver,
4. Wait for an answer and parse it and
5. close the process and clean up all resources.