| Safe Haskell | Trustworthy |
|---|---|
| Language | Haskell98 |
Data.Integer.SAT
Contents
Description
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
Synopsis
- 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
A collection of propositions.
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.
Constructors
| PTrue | |
| PFalse | |
| Prop :|| Prop infixr 2 | |
| Prop :&& Prop infixr 3 | |
| Not Prop | |
| Expr :== Expr infix 4 | |
| Expr :/= Expr infix 4 | |
| Expr :< Expr infix 4 | |
| Expr :> Expr infix 4 | |
| Expr :<= Expr infix 4 | |
| Expr :>= Expr infix 4 |
The type of integer expressions. Variable names must be non-negative.
Constructors
| Expr :+ Expr infixl 6 | Addition |
| Expr :- Expr infixl 6 | Subtraction |
| Integer :* Expr infixl 7 | Multiplication by a constant |
| Negate Expr | Negation |
| Var Name | Variable |
| K Integer | Constant |
| If Prop Expr Expr | A conditional expression |
| Div Expr Integer | Division, rounds down |
| Mod Expr Integer | Non-negative remainder |
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 #
sizePropSet :: PropSet -> (Integer, Integer, Integer) Source #
For QuickCheck
iPickBounded :: BoundType -> [Bound] -> Maybe Integer Source #
Constructors
| Bound Integer Term | The integer is strictly positive |