presburger-0.4: Cooper's decision procedure for Presburger arithmetic.




data Term Source

Terms of Presburger arithmetic. Term are created by using the Num class. WARNING: Presburger arithmetic only supports multiplication by a constant, trying to create invalid terms will result in a run-time error. A more type-safe alternative is to use the '(.*)' operator.


Eq Term 
Num Term 
Show Term 
PP Term 
Quant t => Quant (Term -> t) 

type Name = IntSource

We represent the names of variables in terms as integers.

split_term :: Name -> Term -> (Integer, Term)Source

split_term x (n * x + t1) = (n,t1) x does not occur in t1

is_constant :: Term -> Maybe IntegerSource

Check if a term is a constant (i.e., contains no variables). If so, then we return the constant, otherwise we return Nothing.

data Env Source