hasmtlib-2.6.3: A monad for interfacing with external SMT solvers
Safe HaskellSafe-Inferred
LanguageGHC2021

Language.Hasmtlib.Type.MonadSMT

Description

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.
Synopsis

MonadSMT

class MonadState s m => MonadSMT s m where Source #

A MonadState that holds an SMT-Problem.

Example

Expand
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) Source #

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

Construct a variable as expression.

Example

Expand
x <- var' (Proxy @RealType)

assert :: Expr BoolSort -> m () Source #

Assert a boolean expression.

Example

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

setOption :: SMTOption -> m () Source #

Set an SMT-Solver-Option.

Example

Expand
setOption $ Incremental True

setLogic :: String -> m () Source #

Set the logic for the SMT-Solver to use.

Example

Expand
setLogic "QF_LRA"

Instances

Instances details
MonadState OMT m => MonadSMT OMT m Source # 
Instance details

Defined in Language.Hasmtlib.Type.OMT

Methods

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

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

assert :: Expr 'BoolSort -> m () Source #

setOption :: SMTOption -> m () Source #

setLogic :: String -> m () Source #

(MonadState Pipe m, MonadIO m) => MonadSMT Pipe m Source # 
Instance details

Defined in Language.Hasmtlib.Type.Pipe

Methods

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

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

assert :: Expr 'BoolSort -> m () Source #

setOption :: SMTOption -> m () Source #

setLogic :: String -> m () Source #

MonadState SMT m => MonadSMT SMT m Source # 
Instance details

Defined in Language.Hasmtlib.Type.SMT

Methods

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

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

assert :: Expr 'BoolSort -> m () Source #

setOption :: SMTOption -> m () Source #

setLogic :: String -> m () Source #

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

Wrapper for var' which hides the Proxy.

Example

Expand
x <- var @BoolSort

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

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 Source #

Create a constant.

Examples

Expand
>>> 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 () Source #

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

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 Source #

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

Some solvers require to have SMTOption Incremental set first.

Example

Expand
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 () Source #

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

pop :: m () Source #

Pop the solvers context-stack by one.

checkSat :: m Result Source #

Run check-sat on the current problem.

getModel :: m Solution Source #

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

Example

Expand
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))) Source #

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

Example

Expand
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

Instances details
(MonadState Pipe m, MonadIO m) => MonadIncrSMT Pipe m Source # 
Instance details

Defined in Language.Hasmtlib.Type.Pipe

Methods

push :: m () Source #

pop :: m () Source #

checkSat :: m Result Source #

getModel :: m Solution Source #

getValue :: forall (t :: SMTSort). KnownSMTSort t => Expr t -> m (Maybe (Decoded (Expr t))) Source #

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

First run checkSat and then getModel on the current problem.

Example

Expand
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 Source #

A MonadSMT that addtionally allows optimization targets.

Example

Expand
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 () Source #

Minimizes a numerical expression within the OMT-Problem.

Example

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

will give x := -1 as solution.

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

Maximizes a numerical expression within the OMT-Problem.

Example

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

will give x := 0001 as solution.

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

Softly asserts a boolean expression.

May take a weight and an identifier for grouping.

Example

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

Instances

Instances details
MonadSMT OMT m => MonadOMT OMT m Source # 
Instance details

Defined in Language.Hasmtlib.Type.OMT

Methods

minimize :: forall (t :: SMTSort). (KnownSMTSort t, Num (Expr t)) => Expr t -> m () Source #

maximize :: forall (t :: SMTSort). (KnownSMTSort t, Num (Expr t)) => Expr t -> m () Source #

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

(MonadSMT Pipe m, MonadIO m) => MonadOMT Pipe m Source # 
Instance details

Defined in Language.Hasmtlib.Type.Pipe

Methods

minimize :: forall (t :: SMTSort). (KnownSMTSort t, Num (Expr t)) => Expr t -> m () Source #

maximize :: forall (t :: SMTSort). (KnownSMTSort t, Num (Expr t)) => Expr t -> m () Source #

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

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

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