Module Presburger

Conversions from and to Presburger arithmetic formulas

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