sig
  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
end