Language.Hasmtlib.Solver.Common

This module handles common IO interaction with external SMT-Solvers via external processes.

It is built on top of Tweag's package smtlib-backends.

Although there already are several concrete solvers like Z3 in Language.Hasmtlib.Solver.Z3, you may use this module to create your own solver bindings.

Construction

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,
5. close the process and clean up all resources and
6. return the decoded solution.

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

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

Debugging

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

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

Creates a debugging Solver from a Config.

def :: Default a => a

The default value for this type.