Module Poly

Polynomials

The basic data structure used in Cooper quantifier elimination

exception Not_in_LIA
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 =
  1. | GT of poly
  2. | EQ of poly
  3. | INEQ of poly
  4. | DIVISIBLE of Numeral.t * poly
  5. | 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