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. This is mainly intended for internal use. In the API use var' instead.

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 OMT m => MonadSMT OMT m

Defined in Language.Hasmtlib.Type.OMT

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

assertMaybe :: MonadSMT s m => Maybe (Expr BoolSort) -> m ()

Maybe assert a boolean expression. Asserts given expression if Maybe is a Just. Does nothing otherwise.

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
assert $ x >? y && y <? (-1)
res <- checkSat
case res 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 res 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.

class MonadSMT s m => MonadOMT s m where

A MonadState that holds an OMT-Problem. An OMT-Problem is a 'SMT-Problem' with additional optimization targets.

Methods

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

Minimizes a numerical expression within the OMT-Problem.

For example, below minimization:

x <- var @IntSort
assert $ x >? -2
minimize x

will give x := -1 as solution.

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

Maximizes a numerical expression within the OMT-Problem.

For example, below maximization:

x <- var @(BvSort 8)
maximize x

will give x := 11111111 as solution.

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

Asserts a soft boolean expression. May take a weight and an identifier for grouping.

For example, below a soft constraint with weight 2.0 and identifier "myId" for grouping:

x <- var @BoolSort
assertSoft x (Just 2.0) (Just "myId")

Omitting the weight will default it to 1.0.

x <- var BoolSort
y <- var BoolSort
assertSoft x
assertSoft y (Just "myId")

Instances

MonadSMT OMT m => MonadOMT OMT m

Defined in Language.Hasmtlib.Type.OMT

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

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

assertSoftWeighted :: MonadOMT s m => Expr BoolSort -> Double -> m ()

Like assertSoft but forces a weight and omits the group-id.