Documentation

Parse a Presburger arithmetic formula.

Precedence table (outermost / lowest binding first):

  ∀x. φ   ∃x. φ     quantifiers
  φ ⇒ ψ             implication (right-associative)
  φ ∨ ψ             disjunction (right-associative)
  φ ∧ ψ             conjunction (right-associative)
  ¬ φ               negation    (prefix, binds to single atom)
  ⊥  ⊤  (φ)  d∣t  t rel t     atoms

Note: to combine a quantifier with a connective write φ ∧ (∀x. ψ) — quantifiers inside sub-formulas must be parenthesised.

Full IntTerm: atoms joined by + and -.