Module Poly

module Poly: sig .. end

The basic data structure used in Cooper quantifier elimination
Author(s): Ruoyu Zhang

type psummand = Numeral.t * Var.t option 
psummand is a constant or a variable with coefficient
type poly = psummand list 
poly is a list of psummands
type preAtom = 
| GT of poly
| EQ of poly
| INEQ of poly
| DIVISIBLE of (Numeral.t * poly)
| INDIVISIBLE of (Numeral.t * poly)
For a polynomial p and integer i, a Presburger Atom could be p > 0, p = 0, p != 0, i | p, i !| p
type cformula = preAtom list 
cformula is a list of Presburger Atom conjuncted together
val pp_print_poly : Format.formatter -> poly -> unit
Print a polynomial
val pp_print_cformula : Format.formatter -> cformula -> unit
Print a cformula
val poly_is_constant : poly -> bool
Return true when the polynomial is a constant, false otherwise
val get_coe_in_poly : Var.t -> poly -> Numeral.t
Return the coefficient of a variable in a polynomial
val multiply_two_polys : poly -> poly -> poly
Multiply two polynomials, one of them must be constant
val add_two_polys : (Var.t -> Var.t -> int) -> poly -> poly -> poly -> poly
Add two polynomials with a ordering of varialbes and a accumulator
val negate_poly : poly -> poly
Negate a polynomial
val psummand_contains_variable : Var.t -> psummand -> bool
Return true when the psummand contains the variable, false otherwise
val cformula_contains_variable : Var.t -> cformula -> bool
Return true when the cformula contains the variable, false otherwise
val compare_variables : Var.t list -> Var.t -> Var.t -> int
Comparison of variables: variables to be eliminated earlier are smaller, compare as terms if none is to be eliminated