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

• _pipeSharingMode :: !SharingMode

  How to share common expressions

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

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

• _incrSharedAuxs :: !(Seq (Seq (StableName ())))

  Index of each Seq (StableName ()) is incremental stack height where StableName representing auxiliary var that has been shared

• _pipeSolver :: !Solver

  Active pipe to the backend

• _isDebugging :: !Bool

  Flag if pipe shall debug

Instances

Sharing Pipe

Defined in Language.Hasmtlib.Type.Pipe

Associated Types

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

Methods

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

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

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

WithSolver Pipe

Defined in Language.Hasmtlib.Type.Solver

Methods

withSolver :: Solver -> Bool -> 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 ()

type SharingMonad Pipe

Defined in Language.Hasmtlib.Type.Pipe

type SharingMonad Pipe = MonadIO

pipeStableMap :: Lens' Pipe (HashMap (StableName ()) (SomeKnownSMTSort Expr))

pipeSolver :: Lens' Pipe Solver

pipeSharingMode :: Lens' Pipe SharingMode

mPipeLogic :: Lens' Pipe (Maybe String)

lastPipeVarId :: Lens' Pipe Int

isDebugging :: Lens' Pipe Bool

incrSharedAuxs :: Lens' Pipe (Seq (Seq (StableName ())))