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

Data.Integer.Presburger.Utils

Synopsis

Documentation

lcms :: Integral a => [a] -> aSource

groupEither :: [Either a b] -> ([a], [b])Source

mapEither :: (a -> Either x y) -> [a] -> ([x], [y])Source

extended_gcd :: Integral a => a -> a -> (a, a, a)Source

let (p,q,r) = extended_gcd x y in (x * p + y * q = r) && (gcd x y = r)

divides :: Integral a => a -> a -> BoolSource

class PP a whereSource

Methods

pp :: a -> DocSource

Instances

PP Env 
PP Term 
PP Conn 
PP Formula 
SignPP p => PP (NormProp p) 
SignPP p => PP (Prop p) 
PP p => PP (Form p)