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

Safe HaskellTrustworthy
LanguageHaskell98

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

Documentation

data PropSet Source #

A collection of propositions.

Instances
Show PropSet Source # 
Instance details

Defined in Data.Integer.SAT

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 # 
Instance details

Defined in Data.Integer.SAT

Show Prop Source # 
Instance details

Defined in Data.Integer.SAT

Methods

showsPrec :: Int -> Prop -> ShowS #

show :: Prop -> String #

showList :: [Prop] -> ShowS #

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 # 
Instance details

Defined in Data.Integer.SAT

Show Expr Source # 
Instance details

Defined in Data.Integer.SAT

Methods

showsPrec :: Int -> Expr -> ShowS #

show :: Expr -> String #

showList :: [Expr] -> ShowS #

data BoundType Source #

Constructors

Lower 
Upper 
Instances
Show BoundType Source # 
Instance details

Defined in Data.Integer.SAT

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 # 
Instance details

Defined in Data.Integer.SAT

Methods

(==) :: Name -> Name -> Bool #

(/=) :: Name -> Name -> Bool #

Ord Name Source # 
Instance details

Defined in Data.Integer.SAT

Methods

compare :: Name -> Name -> Ordering #

(<) :: Name -> Name -> Bool #

(<=) :: Name -> Name -> Bool #

(>) :: Name -> Name -> Bool #

(>=) :: Name -> Name -> Bool #

max :: Name -> Name -> Name #

min :: Name -> Name -> Name #

Read Name Source # 
Instance details

Defined in Data.Integer.SAT

Show Name Source # 
Instance details

Defined in Data.Integer.SAT

Methods

showsPrec :: Int -> Name -> ShowS #

show :: Name -> String #

showList :: [Name] -> ShowS #

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

allInerts :: PropSet -> [Inerts] Source #

ppInerts :: Inerts -> Doc Source #

For QuickCheck

data Bound Source #

Constructors

Bound Integer Term

The integer is strictly positive

Instances
Show Bound Source # 
Instance details

Defined in Data.Integer.SAT

Methods

showsPrec :: Int -> Bound -> ShowS #

show :: Bound -> String #

showList :: [Bound] -> ShowS #

tConst :: Integer -> Term Source #

A constant term.