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