sig
  module type S =
    sig
      type error =
          DuplicateTypeName of Hstring.t
        | DuplicateSymb of Hstring.t
        | UnknownType of Hstring.t
        | UnknownSymb of Hstring.t
      exception Error of Smt_sig.S.error
      val report : Format.formatter -> Smt_sig.S.error -> unit
      type check_strategy = Lazy | Eager
      module Type :
        sig
          type t = Hstring.t
          val type_int : Smt_sig.S.Type.t
          val type_real : Smt_sig.S.Type.t
          val type_bool : Smt_sig.S.Type.t
          val type_proc : Smt_sig.S.Type.t
          val declare : Hstring.t -> Hstring.t list -> unit
          val all_constructors : unit -> Hstring.t list
          val constructors : Smt_sig.S.Type.t -> Hstring.t list
          val declared_types : unit -> Smt_sig.S.Type.t list
        end
      module Symbol :
        sig
          type t = Hstring.t
          val declare :
            Hstring.t -> Smt_sig.S.Type.t list -> Smt_sig.S.Type.t -> unit
          val type_of :
            Smt_sig.S.Symbol.t -> Smt_sig.S.Type.t list * Smt_sig.S.Type.t
          val has_abstract_type : Smt_sig.S.Symbol.t -> bool
          val has_infinite_type : Smt_sig.S.Symbol.t -> bool
          val has_type_proc : Smt_sig.S.Symbol.t -> bool
          val declared : Smt_sig.S.Symbol.t -> bool
        end
      module Variant :
        sig
          val init : (Smt_sig.S.Symbol.t * Smt_sig.S.Type.t) list -> unit
          val close : unit -> unit
          val assign_constr : Smt_sig.S.Symbol.t -> Hstring.t -> unit
          val assign_var : Smt_sig.S.Symbol.t -> Smt_sig.S.Symbol.t -> unit
          val print : unit -> unit
          val get_variants : Smt_sig.S.Symbol.t -> Hstring.HSet.t
        end
      module Term :
        sig
          type t
          type operator = Plus | Minus | Mult | Div | Modulo
          val make_int : Num.num -> Smt_sig.S.Term.t
          val make_real : Num.num -> Smt_sig.S.Term.t
          val make_app :
            Smt_sig.S.Symbol.t -> Smt_sig.S.Term.t list -> Smt_sig.S.Term.t
          val make_arith :
            Smt_sig.S.Term.operator ->
            Smt_sig.S.Term.t -> Smt_sig.S.Term.t -> Smt_sig.S.Term.t
          val is_int : Smt_sig.S.Term.t -> bool
          val is_real : Smt_sig.S.Term.t -> bool
          val t_true : Smt_sig.S.Term.t
          val t_false : Smt_sig.S.Term.t
        end
      module Formula :
        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
      exception Unsat of int list
      val set_cc : bool -> unit
      val set_arith : bool -> unit
      val set_sum : bool -> unit
      module type Solver =
        sig
          val check_strategy : Smt_sig.S.check_strategy
          val get_time : unit -> float
          val get_calls : unit -> int
          val clear : unit -> unit
          val assume : id:int -> Smt_sig.S.Formula.t -> unit
          val check : unit -> unit
          val entails : Smt_sig.S.Formula.t -> bool
          val push : unit -> unit
          val pop : unit -> unit
        end
      module Make :
        functor (Options : sig val profiling : bool end) -> Solver
    end
end