Linear arithmetic expression over integers.

Literals of Presburger arithmetic.

Quantifier-free formula of Presburger arithmetic.

d | e means e can be divided by d.

A Model is a map from variables to values.

project x φ returns (ψ, lift) such that:

• ⊢_LIA ∀y1, …, yn. (∃x. φ) ↔ ψ where {y1, …, yn} = FV(φ) \ {x}, and
• if M ⊧_LIA ψ then lift M ⊧_LIA φ.

projectN {x1,…,xm} φ returns (ψ, lift) such that:

• ⊢_LIA ∀y1, …, yn. (∃x1, …, xm. φ) ↔ ψ where {y1, …, yn} = FV(φ) \ {x1,…,xm}, and
• if M ⊧_LIA ψ then lift M ⊧_LIA φ.

projectCases x φ returns [(ψ_1, lift_1), …, (ψ_m, lift_m)] such that:

• ⊢_LIA ∀y1, …, yn. (∃x. φ) ↔ (ψ_1 ∨ … ∨ φ_m) where {y1, …, yn} = FV(φ) \ {x}, and
• if M ⊧_LIA ψ_i then lift_i M ⊧_LIA φ.

projectCasesN {x1,…,xm} φ returns [(ψ_1, lift_1), …, (ψ_n, lift_n)] such that:

• ⊢_LIA ∀y1, …, yp. (∃x. φ) ↔ (ψ_1 ∨ … ∨ φ_n) where {y1, …, yp} = FV(φ) \ {x1,…,xm}, and
• if M ⊧_LIA ψ_i then lift_i M ⊧_LIA φ.

Eliminate quantifiers and returns equivalent quantifier-free formula.

eliminateQuantifiers φ returns (ψ, lift) such that:

• ψ is a quantifier-free formula and LIA ⊢ ∀y1, …, yn. φ ↔ ψ where {y1, …, yn} = FV(φ) ⊇ FV(ψ), and
• if M ⊧_LIA ψ then lift M ⊧_LIA φ.

φ may or may not be a closed formula.

solve {x1,…,xn} φ returns Just M that M ⊧_LIA φ when such M exists, returns Nothing otherwise.

FV(φ) must be a subset of {x1,…,xn}.

solveQFFormula {x1,…,xn} φ returns Just M that M ⊧_LIA φ when such M exists, returns Nothing otherwise.

FV(φ) must be a subset of {x1,…,xn}.

solveFormula {x1,…,xm} φ

• returns Sat M such that M ⊧_LIA φ when such M exists,
• returns Unsat when such M does not exists, and
• returns Unknown when φ is beyond LIA.

solveQFLIRAConj {x1,…,xn} φ I returns Just M that M ⊧_LIRA φ when such M exists, returns Nothing otherwise.

• FV(φ) must be a subset of {x1,…,xn}.
• I is a set of integer variables and must be a subset of {x1,…,xn}.