Language.SMTLib2.Connection

This module can be used if the simple withSMTSolver-interface isn't sufficient, e.g. if you don't want to wrap your whole program into one big MonadSMT or you want to run multiple solvers side by side.

Documentation

data SMTConnection b

Represents a connection to an SMT solver. The SMT solver runs in a seperate thread and communication is handled via handles.

open

Arguments

:: (MonadIO m, SMTBackend b m)

=> b

The backend for the SMT solver.

-> m (SMTConnection b)

Create a new connection to a SMT solver by spawning a shell command. The solver must be able to read from stdin and write to stdout.

close :: (MonadIO m, SMTBackend b m) => SMTConnection b -> m ()

Closes an open SMT connection. Do not use the connection afterwards.

withConnection :: MonadIO m => SMTConnection b -> (b -> m (a, b)) -> m a

performSMT

Arguments

:: (MonadIO m, SMTBackend b m)

=> SMTConnection b

The connection to the SMT solver to use

-> SMT' m a

The action to perform

-> m a

Perform an action in the SMT solver associated with this connection and return the result.

performSMTExitCleanly :: SMTBackend b IO => SMTConnection b -> SMT' IO a -> IO a