Language.Hasmtlib.Type.Pipe

This module provides an IO-Pipe to external SMT-Solvers and ships with implementations for MonadSMT, MonadOMT and MonadIncrSMT.

The Pipe is based on a Solver from Tweag's package smtlib-backends and in reality is just an IO-Handle.

Type

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

• _mPipeDebugger :: Maybe (Debugger Pipe)

  Debugger for communication with the external solver

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

(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

Lens

lastPipeVarId :: Lens' Pipe Int

mPipeLogic :: Lens' Pipe (Maybe String)

pipeSharingMode :: Lens' Pipe SharingMode

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

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

pipeSolver :: Lens' Pipe Solver