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 :: MonadIO m => ProcessSolver -> Solver SMT m

Creates a Solver from a ProcessSolver

debug :: MonadIO m => ProcessSolver -> Solver SMT 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

A type holding actions to execute for debugging SMT solving.

Constructors

Debugger

Fields

• debugSMT :: SMT -> IO ()
• debugProblem :: Seq Builder -> IO ()
• debugResultResponse :: ByteString -> IO ()
• debugModelResponse :: ByteString -> IO ()

Instances

Default Debugger

Defined in Language.Hasmtlib.Solver.Common

Methods

def :: Debugger

processSolver :: MonadIO m => Config -> Maybe Debugger -> Solver SMT 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.