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

Data.Integer.Presburger.Prop

Synopsis

# Documentation

data Prop p Source

Possibly negated propositions. For example, we would express t1 not equal to t2 like this: `Prop { negated = True, prop = Bin Equal t1 t2 }`

Constructors

 Prop Fieldsnegated :: !Bool prop :: !p

Instances

 SignPP p => PP (Prop p)

data NormProp p Source

A proposition normalized with respect to a particular variable.

Constructors

 Ind (Prop PosP) Independent of variable. Norm (Prop p) Depends on variable.

Instances

 SignPP p => PP (NormProp p)

data RelOp Source

Basic binary relations.

Constructors

 Equal LessThan LessThanEqual

Instances

 Eq RelOp SignPP RelOp

data PosP Source

Basic propositions.

Constructors

 Bin !RelOp Term Term Divides !Integer Term FF

Instances

 SignPP PosP

data VarP Source

Propositions specialized to say something about a particular variable.

Constructors

 NBin !RelOp Term x `op` t NDivides !Integer Term n | x + t

Instances

 SignPP VarP

data CVarP Source

Propositions specialized for a variable with a coefficient. For example: 4 * x = t `CVarP { coeff = 4, pprop = NBin Equal t }`

Constructors

 CVarP Fieldscoeff :: !Integer pprop :: !VarP

Instances

 SignPP CVarP

Rewrite a propositions as a predicate about a specific variable.

Eliminate variable coefficients by scaling the properties appropriately.

Evaluate a proposition for a sufficiently small value of the variable, if possible. Otherwise, substitute the given term.

Evaluate a proposition for a sufficiently large value of the variable, if possible. Otherwise, substitute the given term.

Evaluate a proposition with a given term for the variable.

The meanings of atomic propositions

Replace a variable with a constant, in a property.

class SignPP t whereSource

Methods

pp_neg :: Bool -> t -> DocSource

Instances

 SignPP CVarP SignPP VarP SignPP PosP SignPP RelOp