Safe Haskell | None |
---|---|
Language | Haskell98 |
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.
- data SMTConnection b
- open :: (MonadIO m, SMTBackend b m) => b -> m (SMTConnection b)
- close :: (MonadIO m, SMTBackend b m) => SMTConnection b -> m ()
- withConnection :: MonadIO m => SMTConnection b -> (b -> m (a, b)) -> m a
- performSMT :: (MonadIO m, SMTBackend b m) => SMTConnection b -> SMT' m a -> m a
- performSMTExitCleanly :: SMTBackend b IO => SMTConnection b -> SMT' IO a -> IO a
Documentation
data SMTConnection b Source
Represents a connection to an SMT solver. The SMT solver runs in a seperate thread and communication is handled via handles.
:: (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 () Source
Closes an open SMT connection. Do not use the connection afterwards.
withConnection :: MonadIO m => SMTConnection b -> (b -> m (a, b)) -> m a Source
:: (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 Source