language-boogie-0.2: Interpreter and language infrastructure for Boogie.

Safe HaskellNone



Various normal forms of Boolean expressions



negationNF :: Expression -> ExpressionSource

Negation normal form of a Boolean expression: no negation above boolean connectives, quantifiers or relational operators; no boolean connectives except && and ||

prenexNF :: Expression -> ExpressionSource

Prenex normal form of a Boolean expression: all quantifiers are pushed to the outside and any two quantifiers of the same kind in a row are glued together. Requires expression to be in the negation normal form.

normalize :: Expression -> ExpressionSource

Negation and prenex normal form of a Boolean expression