sig
  type comparator = Eq | Neq | Le | Lt
  type combinator = And | Or | Imp | Not
  type literal
  type t
  val f_true : Smt_sig.S.Formula.t
  val f_false : Smt_sig.S.Formula.t
  val make_lit :
    Smt_sig.S.Formula.comparator ->
    Smt_sig.S.Term.t list -> Smt_sig.S.Formula.t
  val make :
    Smt_sig.S.Formula.combinator ->
    Smt_sig.S.Formula.t list -> Smt_sig.S.Formula.t
  val make_cnf : Smt_sig.S.Formula.t -> Smt_sig.S.Formula.literal list list
  val print : Format.formatter -> Smt_sig.S.Formula.t -> unit
end