module Language.SMTLib2.Connection
(SMTConnection()
,open
,close
,withConnection
,performSMT
,performSMTExitCleanly
) where
import Language.SMTLib2.Internals
import Control.Concurrent.MVar
import Control.Monad.Trans (MonadIO,liftIO)
import Control.Exception
import Prelude (($),IO,return)
data SMTConnection b = SMTConnection { backend :: MVar b
}
open :: (MonadIO m,SMTBackend b m) => b
-> m (SMTConnection b)
open solver = do
st <- liftIO $ newMVar solver
return (SMTConnection { backend = st })
close :: (MonadIO m,SMTBackend b m) => SMTConnection b -> m ()
close conn = do
st <- liftIO $ takeMVar (backend conn)
smtHandle st SMTExit
return ()
withConnection :: MonadIO m => SMTConnection b -> (b -> m (a,b)) -> m a
withConnection conn f = do
b <- liftIO $ takeMVar (backend conn)
(res,nb) <- f b
liftIO $ putMVar (backend conn) nb
return res
performSMT :: (MonadIO m,SMTBackend b m)
=> SMTConnection b
-> SMT' m a
-> m a
performSMT conn act = withConnection conn (runSMT act)
performSMTExitCleanly :: SMTBackend b IO
=> SMTConnection b
-> SMT' IO a
-> IO a
performSMTExitCleanly conn act = do
b <- takeMVar (backend conn)
catch (do
(res,nb) <- runSMT act b
putMVar (backend conn) nb
return res)
(\e -> do
smtHandle b SMTExit
throw (e :: SomeException))