Language.Hasmtlib.Type.SMT

Documentation

data SMT

The state of the SMT-problem.

Constructors

SMT

Fields

• _lastVarId :: !Int

  Last Id assigned to a new var

• _vars :: !(Seq (SomeKnownSMTSort SMTVar))

  All constructed variables

• _formulas :: !(Seq (Expr BoolSort))

  All asserted formulas

• _mlogic :: Maybe String

  Logic for the SMT-Solver

• _options :: [SMTOption]

  All manually configured SMT-Solver-Options

Instances

Default SMT

Defined in Language.Hasmtlib.Type.SMT

Methods

def :: SMT

MonadState SMT m => MonadSMT SMT m

Defined in Language.Hasmtlib.Type.SMT

Methods

smtvar' :: forall (t :: SMTSort). KnownSMTSort t => Proxy t -> m (SMTVar t)

var' :: forall (t :: SMTSort). KnownSMTSort t => Proxy t -> m (Expr t)

assert :: Expr 'BoolSort -> m ()

setOption :: SMTOption -> m ()

setLogic :: String -> m ()

vars :: Lens' SMT (Seq (SomeKnownSMTSort SMTVar))

options :: Lens' SMT [SMTOption]

mlogic :: Lens' SMT (Maybe String)

lastVarId :: Lens' SMT Int

formulas :: Lens' SMT (Seq (Expr 'BoolSort))

renderSMT :: SMT -> Seq Builder

Render a SMT-Problem to SMTLib2-Syntax. Each element of the returned Sequence is a line.

renderSetLogic :: Builder -> Builder

renderDeclareVar :: forall t. KnownSMTSort t => SMTVar t -> Builder

renderAssert :: Expr BoolSort -> Builder

renderVars :: Seq (SomeKnownSMTSort SMTVar) -> Seq Builder