sig
  type comparator = Eq | Neq | Le | Lt
  type combinator = And | Or | Imp | Not
  type t =
      Lit of Literal.LT.t
    | Comb of Smt.Formula.combinator * Smt.Formula.t list
  val f_true : Smt.Formula.t
  val f_false : Smt.Formula.t
  val make_lit : Smt.Formula.comparator -> Smt.Term.t list -> Smt.Formula.t
  val make : Smt.Formula.combinator -> Smt.Formula.t list -> Smt.Formula.t
  val make_cnf : Smt.Formula.t -> Literal.LT.t list list
  val print : Format.formatter -> Smt.Formula.t -> unit
end