Language.SMTLib2.Internals.Monad

Documentation

newtype SMT b a

The SMT monad is used to perform communication with the SMT solver. The type of solver is given by the b parameter.

Constructors

SMT

Fields

• runSMT :: StateT (SMTState b) (SMTMonad b) a

Instances

Backend b => Monad (SMT b)

Methods

(>>=) :: SMT b a -> (a -> SMT b b) -> SMT b b

(>>) :: SMT b a -> SMT b b -> SMT b b

return :: a -> SMT b a

fail :: String -> SMT b a

Backend b => Functor (SMT b)

Methods

fmap :: (a -> b) -> SMT b a -> SMT b b

(<$) :: a -> SMT b b -> SMT b a

Backend b => Applicative (SMT b)

Methods

pure :: a -> SMT b a

(<*>) :: SMT b (a -> b) -> SMT b a -> SMT b b

(*>) :: SMT b a -> SMT b b -> SMT b b

(<*) :: SMT b a -> SMT b b -> SMT b a

(Backend b, MonadIO (SMTMonad b)) => MonadIO (SMT b)

Methods

liftIO :: IO a -> SMT b a

Backend b => MonadState (SMTState b) (SMT b)

Methods

get :: SMT b (SMTState b)

put :: SMTState b -> SMT b ()

state :: (SMTState b -> (a, SMTState b)) -> SMT b a

Backend b => Embed (SMT b) (Expr b)

Associated Types

type EmVar (SMT b :: * -> *) (Expr b :: Type -> *) :: Type -> *

type EmQVar (SMT b :: * -> *) (Expr b :: Type -> *) :: Type -> *

type EmFun (SMT b :: * -> *) (Expr b :: Type -> *) :: ([Type], Type) -> *

type EmFunArg (SMT b :: * -> *) (Expr b :: Type -> *) :: Type -> *

type EmLVar (SMT b :: * -> *) (Expr b :: Type -> *) :: Type -> *

Methods

embed :: SMT b (EmbedExpr (SMT b) (Expr b) tp) -> SMT b (Expr b tp)

embedQuantifier :: Quantifier -> List Type Repr arg -> (forall m e. (Embed m e, Monad m) => List Type (EmQVar m e) arg -> m (e BoolType)) -> SMT b (Expr b BoolType)

embedTypeOf :: SMT b (Expr b tp -> Repr tp)

type EmVar (SMT b) (Expr b)

type EmVar (SMT b) (Expr b) = Var b

type EmQVar (SMT b) (Expr b)

type EmQVar (SMT b) (Expr b) = QVar b

type EmFun (SMT b) (Expr b)

type EmFun (SMT b) (Expr b) = Fun b

type EmFunArg (SMT b) (Expr b)

type EmFunArg (SMT b) (Expr b) = FunArg b

type EmLVar (SMT b) (Expr b)

type EmLVar (SMT b) (Expr b) = LVar b

data SMTState b

Constructors

SMTState

Fields

• backend :: !b
• datatypes :: !(Set String)

Instances

Backend b => MonadState (SMTState b) (SMT b)

Methods

get :: SMT b (SMTState b)

put :: SMTState b -> SMT b ()

state :: (SMTState b -> (a, SMTState b)) -> SMT b a

withBackend

Arguments

:: Backend b

=> SMTMonad b b

An action that creates a fresh backend.

-> SMT b a

The SMT action to perform.

-> SMTMonad b a

Execute an SMT action on a given backend.

withBackendExitCleanly :: (Backend b, SMTMonad b ~ IO) => IO b -> SMT b a -> IO a

Like withBackend but specialized to the IO monad so exeptions can be handled by gracefully exiting the solver.

liftSMT :: Backend b => SMTMonad b a -> SMT b a

embedSMT :: Backend b => (b -> SMTMonad b (a, b)) -> SMT b a

embedSMT' :: Backend b => (b -> SMTMonad b b) -> SMT b ()

registerDatatype :: (Backend b, IsDatatype dt) => Datatype dt -> SMT b ()

defineVar' :: Backend b => Expr b t -> SMT b (Var b t)

defineVarNamed' :: Backend b => String -> Expr b t -> SMT b (Var b t)

declareVar' :: Backend b => Repr t -> SMT b (Var b t)

declareVarNamed' :: Backend b => Repr t -> String -> SMT b (Var b t)