Language.Hasmtlib.Solver.Common

Documentation

newtype ProcessSolver

A newtype-wrapper for Config which configures a solver via external process.

Constructors

ProcessSolver

Fields

• conf :: Config

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

Creates a Solver from a ProcessSolver

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

Creates a debugging Solver from a ProcessSolver

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

Creates an interactive session with a solver by creating and returning an alive process-handle Handle.

data Debugger s

A type holding actions for debugging states.

Constructors

Debugger

Fields

• debugState :: s -> IO ()
• debugProblem :: Seq Builder -> IO ()
• debugResultResponse :: ByteString -> IO ()
• debugModelResponse :: ByteString -> IO ()

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.