module RealQuantElim: sig .. end
Simplify existentially quantified conjunction of polynomial inequalities.
val case_str : (Poly.polynomial * Formula.sign_op) list -> string
val cases_str : string -> (Poly.polynomial * Formula.sign_op) list list -> string
val simplify : string list ->
(Poly.polynomial * Formula.sign_op) list ->
(Poly.polynomial * Formula.sign_op) list list
val simplify_sat : string list ->
(Poly.polynomial * Formula.sign_op) list ->
(Poly.polynomial * Formula.sign_op) list list
val sat : (Poly.polynomial * Formula.sign_op) list -> bool