Language.Hasmtlib.Type.Pipe

Documentation

data Pipe

A pipe to the solver. If Solver is Queuing then all commands that do not expect an answer are sent to the queue. All commands that expect an answer have the queue to be sent to the solver before sending the command itself. If Solver is not Queuing, all commands are sent to the solver immediately.

Constructors

Pipe

Fields

• _lastPipeVarId :: !Int

  Last Id assigned to a new var

• _mPipeLogic :: Maybe String

  Logic for the SMT-Solver

• _pipe :: !Solver

  Active pipe to the backend

Instances

WithSolver Pipe

Defined in Language.Hasmtlib.Type.Solver

Methods

withSolver :: Solver -> Pipe

(MonadState Pipe m, MonadIO m) => MonadIncrSMT Pipe m

Defined in Language.Hasmtlib.Type.Pipe

Methods

push :: m ()

pop :: m ()

checkSat :: m Result

getModel :: m Solution

getValue :: forall (t :: SMTSort). KnownSMTSort t => Expr t -> m (Maybe (Decoded (Expr t)))

(MonadSMT Pipe m, MonadIO m) => MonadOMT Pipe m

Defined in Language.Hasmtlib.Type.Pipe

Methods

minimize :: forall (t :: SMTSort). (KnownSMTSort t, Num (Expr t)) => Expr t -> m ()

maximize :: forall (t :: SMTSort). (KnownSMTSort t, Num (Expr t)) => Expr t -> m ()

assertSoft :: Expr 'BoolSort -> Maybe Double -> Maybe String -> m ()

(MonadState Pipe m, MonadIO m) => MonadSMT Pipe m

Defined in Language.Hasmtlib.Type.Pipe

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

pipe :: Lens' Pipe Solver

mPipeLogic :: Lens' Pipe (Maybe String)

lastPipeVarId :: Lens' Pipe Int

Orphan instances

(MonadState Pipe m, MonadIO m) => MonadIncrSMT Pipe m

Methods

push :: m ()

pop :: m ()

checkSat :: m Result

getModel :: m Solution

getValue :: forall (t :: SMTSort). KnownSMTSort t => Expr t -> m (Maybe (Decoded (Expr t)))