sig
  val poly_sign_op_cmp :
    OrderedPoly.polynomial * Formula.sign_op ->
    OrderedPoly.polynomial * Formula.sign_op -> int
  exception Contradicting_sign_ops
  val join_sign_ops : Formula.sign_op -> Formula.sign_op -> Formula.sign_op
  val sign_op_str : Formula.sign_op -> string
  val check_sign : float -> Formula.sign_op -> bool
  val neg_sign_op : Formula.sign_op -> Formula.sign_op
  val int_case_str : (OrderedPoly.polynomial * int) list -> string
  val case_str : (OrderedPoly.polynomial * Formula.sign_op) list -> string
  val log_no_cases :
    ?upto:int -> (OrderedPoly.polynomial * Formula.sign_op) list -> int
  val build_cases :
    (OrderedPoly.polynomial * Formula.sign_op) list ->
    (OrderedPoly.polynomial * int) list list * OrderedPoly.polynomial array
  val solve :
    (OrderedPoly.polynomial * int) list list * OrderedPoly.polynomial array ->
    (OrderedPoly.polynomial * Formula.sign_op) list ->
    (OrderedPoly.polynomial * Formula.sign_op) list list
end