presburger-1.3.1: A decision procedure for quantifier-free linear arithmetic.

Safe Haskell | Trustworthy
Language | Haskell98

Data.Integer.SAT

Contents

- Iterators
- Debug
- For QuickCheck

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
  - = PTrue
  - | PFalse
  - | Prop :|| Prop
  - | Prop :&& Prop
  - | Not Prop
  - | Expr :== Expr
  - | Expr :/= Expr
  - | Expr :< Expr
  - | Expr :> Expr
  - | Expr :<= Expr
  - | Expr :>= Expr
- data Expr
  - = Expr :+ Expr
  - | Expr :- Expr
  - | Integer :* Expr
  - | Negate Expr
  - | Var Name
  - | K Integer
  - | If Prop Expr Expr
  - | Div Expr Integer
  - | Mod Expr Integer
- data BoundType
  - = Lower
  - | Upper
- 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

data PropSet Source

A collection of propositions.

Instances

Show PropSet Source |

noProps :: PropSet Source

An empty 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 (?).

assert :: Prop -> PropSet -> PropSet Source

Add a new proposition to an existing collection.

data Prop Source

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 |

Instances

Read Prop Source |
Show Prop Source |

data Expr Source

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

Instances

Read Expr Source |
Show Expr Source |

data BoundType Source

Constructors

Lower |
Upper |

Instances

Show BoundType Source |

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.

data Name Source

Instances

Eq Name Source |
Ord Name Source |
Read Name Source |
Show Name Source |

toName :: Int -> Name Source

fromName :: Name -> Maybe Int Source

# 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

allInerts :: PropSet -> [Inerts] Source

ppInerts :: Inerts -> Doc Source

# For QuickCheck

iPickBounded :: BoundType -> [Bound] -> Maybe Integer Source

data Bound Source

Constructors

Bound Integer Term | The integer is strictly positive

Instances

Show Bound Source |

tConst :: Integer -> Term Source

A constant term.