Documentation

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.

Instances

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

type Name = Int Source

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 Integer Source

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

(.*) :: Integer -> Term -> Term Source

var :: Name -> Term Source

num :: Integer -> Term Source

data Env Source

Instances

PP Env

env_empty :: Env Source

env_extend :: Name -> Integer -> Env -> Env Source

eval_term :: Term -> Env -> Integer Source

subst_term :: Name -> Integer -> Term -> Term Source

var_name :: Name -> String Source