Safe Haskell | Safe-Inferred |
---|---|
Language | GHC2021 |
Language.Hasmtlib.Type.MonadSMT
Contents
Description
This module provides MTL-Style-classes for building SMT-problems.
The following three classes form the core of this module:
MonadSMT
for plain SMT-problems. Create variables usingvar
and assert formulas viaassert
.MonadIncrSMT
for plain SMT-problems with addtional access to the external solvers incremental stack and it's operations.MonadOMT
for SMT-problems with optimization. Optimize viaminimize
andmaximize
and softly assert formulas viaassertSoft
.
Synopsis
- class MonadState s m => MonadSMT s m where
- var :: forall t s m. (KnownSMTSort t, MonadSMT s m) => m (Expr t)
- smtvar :: forall t s m. (KnownSMTSort t, MonadSMT s m) => m (SMTVar t)
- constant :: KnownSMTSort t => HaskellType t -> Expr t
- assertMaybe :: MonadSMT s m => Maybe (Expr BoolSort) -> m ()
- quantify :: MonadSMT s m => KnownSMTSort t => Expr t -> m (Expr t)
- class MonadSMT s m => MonadIncrSMT s m where
- solve :: (MonadIncrSMT s m, MonadIO m) => m (Result, Solution)
- class MonadSMT s m => MonadOMT s m where
- assertSoftWeighted :: MonadOMT s m => Expr BoolSort -> Double -> m ()
MonadSMT
class MonadState s m => MonadSMT s m where Source #
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) 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
x <- var' (Proxy @RealType)
assert :: Expr BoolSort -> m () Source #
Assert a boolean expression.
Example
x <- var @IntType assert $ x - 27 === 42
setOption :: SMTOption -> m () Source #
Set an SMT-Solver-Option.
Example
setOption $ Incremental True
setLogic :: String -> m () Source #
Set the logic for the SMT-Solver to use.
Example
setLogic "QF_LRA"
Instances
MonadState OMT m => MonadSMT OMT m Source # | |
Defined in Language.Hasmtlib.Type.OMT | |
(MonadState Pipe m, MonadIO m) => MonadSMT Pipe m Source # | |
Defined in Language.Hasmtlib.Type.Pipe | |
MonadState SMT m => MonadSMT SMT m Source # | |
Defined in Language.Hasmtlib.Type.SMT |
constant :: KnownSMTSort t => HaskellType t -> Expr t Source #
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)
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
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 a new context (one) to the solvers context-stack.
Pop the solvers context-stack by one.
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
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 #
Instances
(MonadState Pipe m, MonadIO m) => MonadIncrSMT Pipe m Source # | |
MonadOMT
class MonadSMT s m => MonadOMT s m where Source #
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 () Source #
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 () Source #
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 () Source #
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")
assertSoftWeighted :: MonadOMT s m => Expr BoolSort -> Double -> m () Source #
Like assertSoft
but forces a weight and omits the group-id.