Language.Hasmtlib.Type.SMT

This module provides a concrete implementation for MonadSMT with it's state SMT.

Type

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

• _sharingMode :: !SharingMode

  How to share common expressions

• _stableMap :: !(HashMap (StableName ()) (SomeKnownSMTSort Expr))

  Mapping between a StableName and it's Expr we may share

Instances

Default SMT

Defined in Language.Hasmtlib.Type.SMT

Methods

def :: SMT

RenderSeq SMT

Defined in Language.Hasmtlib.Type.SMT

Methods

renderSeq :: SMT -> Seq Builder

Sharing SMT

Defined in Language.Hasmtlib.Type.SMT

Associated Types

type SharingMonad SMT :: (Type -> Type) -> Constraint

Methods

stableMap :: Lens' SMT (HashMap (StableName ()) (SomeKnownSMTSort Expr))

assertSharedNode :: (MonadState SMT m, SharingMonad SMT m) => StableName () -> Expr 'BoolSort -> m ()

setSharingMode :: MonadState SMT m => SharingMode -> m ()

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 ()

Default (Debugger SMT)

Defined in Language.Hasmtlib.Solver.Common

Methods

def :: Debugger SMT

type SharingMonad SMT

Defined in Language.Hasmtlib.Type.SMT

type SharingMonad SMT = Monad

Lens

lastVarId :: Lens' SMT Int

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

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

mlogic :: Lens' SMT (Maybe String)

options :: Lens' SMT [SMTOption]

sharingMode :: Lens' SMT SharingMode

stableMap :: Lens' SMT (HashMap (StableName ()) (SomeKnownSMTSort Expr))

Rendering

renderSetLogic :: Builder -> Builder

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

renderAssert :: Expr BoolSort -> Builder

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