Module Presburger

module Presburger: sig .. end
Conversions from and to Presburger arithmetic formulas
Author(s): Ruoyu Zhang

exception Not_in_LIA
Formula is not in linear integer arithmetic
val to_presburger : Var.t list -> Term.t -> Poly.cformula
Normalize the term into a Presburger formula
val term_of_poly : Poly.poly -> Term.t
Convert a polynomial to a term
val term_of_cformula : Poly.cformula -> Term.t list
Convert a presburger formula to a term