sig
  type psummand = Numeral.t * Var.t option
  type poly = Poly.psummand list
  type preAtom =
      GT of Poly.poly
    | EQ of Poly.poly
    | INEQ of Poly.poly
    | DIVISIBLE of (Numeral.t * Poly.poly)
    | INDIVISIBLE of (Numeral.t * Poly.poly)
  type cformula = Poly.preAtom list
  val pp_print_poly : Format.formatter -> Poly.poly -> unit
  val pp_print_cformula : Format.formatter -> Poly.cformula -> unit
  val poly_is_constant : Poly.poly -> bool
  val get_coe_in_poly : Var.t -> Poly.poly -> Numeral.t
  val multiply_two_polys : Poly.poly -> Poly.poly -> Poly.poly
  val add_two_polys :
    (Var.t -> Var.t -> int) ->
    Poly.poly -> Poly.poly -> Poly.poly -> Poly.poly
  val negate_poly : Poly.poly -> Poly.poly
  val psummand_contains_variable : Var.t -> Poly.psummand -> bool
  val cformula_contains_variable : Var.t -> Poly.cformula -> bool
  val compare_variables : Var.t list -> Var.t -> Var.t -> int
end