module SignTable: sig .. end
Handling sign tables for quantifier elimination.
val poly_sign_op_cmp : OrderedPoly.polynomial * Formula.sign_op ->
OrderedPoly.polynomial * Formula.sign_op -> int
exception Contradicting_sign_ops
Exception raised when contraditing ops are given to join_sign_ops.
val join_sign_ops : Formula.sign_op -> Formula.sign_op -> Formula.sign_op
Given two sign_ops x and y return a sign op for "x and y".
val sign_op_str : Formula.sign_op -> string
Print a sign_op as string.
val check_sign : float -> Formula.sign_op -> bool
Check if given float has sign as required by the sign_op.
val neg_sign_op : Formula.sign_op -> Formula.sign_op
Negate a sign_op.
val int_case_str : (OrderedPoly.polynomial * int) list -> string
Print a case, i.e. a list of polynomials and their signs, as string.
val case_str : (OrderedPoly.polynomial * Formula.sign_op) list -> string
val log_no_cases : ?upto:int -> (OrderedPoly.polynomial * Formula.sign_op) list -> int
Estimate the (base-3) logarithm of the number of cases needed for pset.
val build_cases : (OrderedPoly.polynomial * Formula.sign_op) list ->
(OrderedPoly.polynomial * int) list list * OrderedPoly.polynomial array
Build array of polynomials and cases to check given set of polynomials.
val solve : (OrderedPoly.polynomial * int) list list * OrderedPoly.polynomial array ->
(OrderedPoly.polynomial * Formula.sign_op) list ->
(OrderedPoly.polynomial * Formula.sign_op) list list
Given cases and polynomial array as constructed by build_cases and
requirement list for some polynomials, return all satisfying cases.