Language.Hasmtlib.Type.MonadSMT

Documentation

class MonadState s m => MonadSMT s m where

A MonadState that holds an SMT-Problem.

Methods

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

Construct a variable.

x :: SMTVar RealType <- smtvar' (Proxy @RealType)

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

Construct a variable as expression.

x :: Expr RealType <- var' (Proxy @RealType)

assert :: Expr BoolSort -> m ()

Assert a boolean expression.

x :: Expr IntType <- var @IntType
assert $ x + 5 === 42

setOption :: SMTOption -> m ()

Set an SMT-Solver-Option.

setOption $ Incremental True

setLogic :: String -> m ()

Set the logic for the SMT-Solver to use.

setLogic QF_LRA

Instances

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

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

var :: forall t s m. (KnownSMTSort t, MonadSMT s m) => m (Expr t)

Wrapper for var' which hides the Proxy.

smtvar :: forall t s m. (KnownSMTSort t, MonadSMT s m) => m (SMTVar t)

Wrapper for smtvar' which hides the Proxy. | This is mainly intended for internal use. | In the API use var instead.

constant :: KnownSMTSort t => HaskellType t -> Expr t

Create a constant.

>>> constant True
    Constant (BoolValue True)

>>> let x :: Integer = 10 ; constant x
    Constant (IntValue 10)

>>> constant @IntType 5
    Constant (IntValue 5)

>>> constant @(BvType 8) 5
    Constant (BvValue 0000101)

quantify :: MonadSMT s m => Expr t -> m (Expr t)

Assign quantified variables to all quantified subexpressions of an expression. This shall only be used internally. Usually before rendering an assert.

class MonadSMT s m => MonadIncrSMT s m | m -> s where

A MonadSMT that allows incremental solving.

Methods

push :: m ()

Push a new context (one) to the solvers context-stack.

pop :: m ()

Pop the solvers context-stack by one.

checkSat :: m Result

Run check-sat on the current problem.

getModel :: m Solution

Run get-model on the current problem. This can be used to decode temporary models within the SMT-Problem.

x <- var RealSort
y <- var RealSort
assert $ x >? y && y <? (-1)
res <- checkSat
case checkSat of
  Unsat -> print "Unsat. Cannot get model."
  r     -> do
    model <- getModel
    liftIO $ print $ decode model x

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

Evaluate any expressions value in the solvers model. Requires a Sat or Unknown check-sat response beforehand.

x <- var @RealSort
assert $ x >? 10
res <- checkSat
case checkSat of
  Unsat -> print "Unsat. Cannot get value for x."
  r     -> do
    x' <- getValue x
    liftIO $ print $ show r ++ ": x = " ++ show x'

Instances

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

solve :: (MonadIncrSMT s m, MonadIO m) => m (Result, Solution)

First run checkSat and then getModel on the current problem.