Safe Haskell | Trustworthy |
---|---|
Language | Haskell98 |
This module implements a decision procedure for quantifier-free linear arithmetic. The algorithm is based on the following paper:
An Online Proof-Producing Decision Procedure for Mixed-Integer Linear Arithmetic by Sergey Berezin, Vijay Ganesh, and David L. Dill
- data PropSet
- noProps :: PropSet
- checkSat :: PropSet -> Maybe [(Int, Integer)]
- assert :: Prop -> PropSet -> PropSet
- data Prop
- data Expr
- data BoundType
- getExprBound :: BoundType -> Expr -> PropSet -> Maybe Integer
- getExprRange :: Expr -> PropSet -> Maybe [Integer]
- data Name
- toName :: Int -> Name
- fromName :: Name -> Maybe Int
- allSolutions :: PropSet -> [Solutions]
- slnCurrent :: Solutions -> [(Int, Integer)]
- slnNextVal :: Solutions -> Maybe Solutions
- slnNextVar :: Solutions -> Maybe Solutions
- slnEnumerate :: Solutions -> [Solutions]
- dotPropSet :: PropSet -> Doc
- sizePropSet :: PropSet -> (Integer, Integer, Integer)
- allInerts :: PropSet -> [Inerts]
- ppInerts :: Inerts -> Doc
- iPickBounded :: BoundType -> [Bound] -> Maybe Integer
- data Bound = Bound Integer Term
- tConst :: Integer -> Term
Documentation
checkSat :: PropSet -> Maybe [(Int, Integer)] Source
Extract a model from a consistent set of propositions.
Returns Nothing
if the assertions have no model.
If a variable does not appear in the assignment, then it is 0 (?).
The type of proposition.
The type of integer expressions. Variable names must be non-negative.
getExprBound :: BoundType -> Expr -> PropSet -> Maybe Integer Source
Computes bounds on the expression that are compatible with the model.
Returns Nothing
if the bound is not known.
getExprRange :: Expr -> PropSet -> Maybe [Integer] Source
Compute the range of possible values for an expression.
Returns Nothing
if the bound is not known.
Iterators
allSolutions :: PropSet -> [Solutions] Source
slnCurrent :: Solutions -> [(Int, Integer)] Source
slnNextVal :: Solutions -> Maybe Solutions Source
slnNextVar :: Solutions -> Maybe Solutions Source
slnEnumerate :: Solutions -> [Solutions] Source
Debug
dotPropSet :: PropSet -> Doc Source