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

Data.Integer.Presburger.ModArith

Synopsis

Documentation

is_nat :: Term -> FormulaSource

is_reminder :: Integer -> Term -> FormulaSource

div_mod_is :: Term -> Integer -> Term -> Term -> FormulaSource

divMod t d == (q,r)

mod_is :: Term -> Integer -> Term -> FormulaSource

mod t d == r

bin_op_mod :: Integer -> (Term -> Term -> Term) -> Term -> Term -> Term -> FormulaSource

add_mod, mul_mod, sub_mod :: Integer -> Term -> Term -> Term -> FormulaSource