Language.Hasmtlib.Type.MonadSMT

This module provides MTL-Style-classes for building SMT-problems.

The following three classes form the core of this module:

1. MonadSMT for plain SMT-problems. Create variables using var and assert formulas via assert.
2. MonadIncrSMT for plain SMT-problems with addtional access to the external solvers incremental stack and it's operations.
3. MonadOMT for SMT-problems with optimization. Optimize via minimize and maximize and softly assert formulas via assertSoft.

MonadSMT

class MonadState s m => MonadSMT s m where

A MonadState that holds an SMT-Problem.

Example

problem :: MonadSMT s m => StateT s m (Expr IntSort)
problem = do
  setLogic "QF_LIA"
  x <- var @IntSort
  assert $ x + 2 === x * 2
  return x

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.

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

Construct a variable as expression.

Example

x <- var' (Proxy @RealType)

assert :: Expr BoolSort -> m ()

Assert a boolean expression.

Example

x <- var @IntType
assert $ x - 27 === 42

setOption :: SMTOption -> m ()

Set an SMT-Solver-Option.

Example

setOption $ Incremental True

setLogic :: String -> m ()

Set the logic for the SMT-Solver to use.

Example

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.

Example

x <- var @BoolSort

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.

Examples

>>> constant True
    Constant (BoolValue True)

>>> constant (10 :: Integer)
    Constant (IntValue 10)

>>> constant @RealSort 5
    Constant (RealValue 5.0)

>>> constant @(BvSort Unsigned 8) 14
    Constant (BvValue 00001110)

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 => KnownSMTSort t => Expr t -> m (Expr t)

Assign quantified variables to all quantified subexpressions of an expression.

Quantifies bottom-up.

This is intended for internal use. Usually before rendering an assert.

MonadIncrSMT

class MonadSMT s m => MonadIncrSMT s m where

A MonadSMT that addtionally allows incremental solving with access to a solvers incremental stack.

Some solvers require to have SMTOption Incremental set first.

Example

problem :: MonadIncrSMT s m => StateT s m ()
problem = do
  setOption $ Incremental True
  setLogic "QF_LIA"
  x <- var @IntSort
  push
  assert $ x + 2 === x * 2
  res <- checkSat
  case res of
    Sat -> do
      x' <- getValue x
      ...
    _ -> pop ...
  return ()

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.

Example

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

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.

Example

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.

Example

x <- var @BoolSort
assert $ x xor false
(res, sol) <- solve
case res of
  Sat -> do
    liftIO $ print $ decode sol x
  r -> print r

MonadOMT

class MonadSMT s m => MonadOMT s m where

A MonadSMT that addtionally allows optimization targets.

Example

problem :: MonadOMT s m => StateT s m (Expr (BvSort Unsigned 8))
problem = do
  setLogic "QF_BV"
  x <- var @(BvSort Unsigned 8)
  assertSoftWeighted (x <? maxBound) 2.0
  maximize x
  return x

Methods

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

Minimizes a numerical expression within the OMT-Problem.

Example

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.

Example

x <- var @(BvSort Signed 4)
assert $ x <? 2
maximize x

will give x := 0001 as solution.

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

Softly asserts a boolean expression.

May take a weight and an identifier for grouping.

Example

x <- var @BoolSort
assertSoft x (Just 0.5) (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.