hermod-recon-framework
Safe HaskellSafe-Inferred
LanguageHaskell2010

Hermod.ReCon.Presburger.Formula

Synopsis

Documentation

data BinRel Source #

Binary comparison relation on an ordered type.

Constructors

Eq 
Lt 
Lte 
Gt 
Gte 

Instances

Instances details
Show BinRel Source # 
Instance details

Defined in Hermod.ReCon.Common.Types

Methods

showsPrec :: Int -> BinRel -> ShowS Source #

show :: BinRel -> String Source #

showList :: [BinRel] -> ShowS Source #

Eq BinRel Source # 
Instance details

Defined in Hermod.ReCon.Common.Types

Methods

(==) :: BinRel -> BinRel -> Bool Source #

(/=) :: BinRel -> BinRel -> Bool Source #

Ord BinRel Source # 
Instance details

Defined in Hermod.ReCon.Common.Types

Methods

compare :: BinRel -> BinRel -> Ordering Source #

(<) :: BinRel -> BinRel -> Bool Source #

(<=) :: BinRel -> BinRel -> Bool Source #

(>) :: BinRel -> BinRel -> Bool Source #

(>=) :: BinRel -> BinRel -> Bool Source #

max :: BinRel -> BinRel -> BinRel Source #

min :: BinRel -> BinRel -> BinRel Source #

data Formula Source #

Formulae of Presburger arithmetic — the first-order theory of the integers under addition (+), integer constants, and the standard comparison relations (=, <, ≤, >, ≥), extended with the divisibility predicate d | t ("d divides t").

Quantifiers range over ℤ only. There are no free variables: every well-formed formula is a closed sentence whose truth value is decidable via Cooper's quantifier-elimination procedure (decide).

Constructors

Or Formula Formula

φ ∨ ψ

And Formula Formula

φ ∧ ψ

Not Formula

¬ φ

Implies Formula Formula

φ ⇒ ψ

Top

T

Bottom

⊥

IntForall VariableIdentifier Formula

∀x : ℤ. φ

IntExists VariableIdentifier Formula

∃x : ℤ. φ

IntBinRel BinRel IntTerm IntTerm

i = i | i | i ≤ i | i i | i ≥ i

IntDiv NatValue IntTerm

ℕ⁺ | i (divisibility relation, first argument is a non-zero ℕ)

Instances

Instances details
Show Formula Source # 
Instance details

Defined in Hermod.ReCon.Presburger.Formula

Methods

showsPrec :: Int -> Formula -> ShowS Source #

show :: Formula -> String Source #

showList :: [Formula] -> ShowS Source #

Eq Formula Source # 
Instance details

Defined in Hermod.ReCon.Presburger.Formula

Methods

(==) :: Formula -> Formula -> Bool Source #

(/=) :: Formula -> Formula -> Bool Source #

Ord Formula Source # 
Instance details

Defined in Hermod.ReCon.Presburger.Formula

Methods

compare :: Formula -> Formula -> Ordering Source #

(<) :: Formula -> Formula -> Bool Source #

(<=) :: Formula -> Formula -> Bool Source #

(>) :: Formula -> Formula -> Bool Source #

(>=) :: Formula -> Formula -> Bool Source #

max :: Formula -> Formula -> Formula Source #

min :: Formula -> Formula -> Formula Source #

unfoldImplies :: Formula -> Formula -> Formula Source #