# Module `Poly`

Polynomials

The basic data structure used in Cooper quantifier elimination

author
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 : Stdlib.Format.formatter -> poly -> unit`

Print a polynomial

`val pp_print_cformula : Stdlib.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