sig
  type error =
      DuplicateTypeName of Hstring.t
    | DuplicateSymb of Hstring.t
    | UnknownType of Hstring.t
    | UnknownSymb of Hstring.t
  exception Error of Smt.error
  module Type :
    sig
      type t = Hstring.t
      val type_int : Smt.Type.t
      val type_real : Smt.Type.t
      val type_bool : Smt.Type.t
      val type_proc : Smt.Type.t
      val declare : Hstring.t -> Hstring.t list -> unit
      val all_constructors : unit -> Hstring.t list
      val constructors : Smt.Type.t -> Hstring.t list
    end
  module Symbol :
    sig
      type t = Hstring.t
      val declare : Hstring.t -> Smt.Type.t list -> Smt.Type.t -> unit
      val type_of : Smt.Symbol.t -> Smt.Type.t list * Smt.Type.t
      val has_abstract_type : Smt.Symbol.t -> bool
      val has_type_proc : Smt.Symbol.t -> bool
      val declared : Smt.Symbol.t -> bool
    end
  module Variant :
    sig
      val init : (Smt.Symbol.t * Smt.Type.t) list -> unit
      val close : unit -> unit
      val assign_constr : Smt.Symbol.t -> Hstring.t -> unit
      val assign_var : Smt.Symbol.t -> Smt.Symbol.t -> unit
      val print : unit -> unit
      val get_variants : Smt.Symbol.t -> Hstring.HSet.t
    end
  module rec Term :
    sig
      type t
      type operator = Plus | Minus | Mult | Div | Modulo
      val make_int : Num.num -> Smt.Term.t
      val make_real : Num.num -> Smt.Term.t
      val make_app : Smt.Symbol.t -> Smt.Term.t list -> Smt.Term.t
      val make_arith :
        Smt.Term.operator -> Smt.Term.t -> Smt.Term.t -> Smt.Term.t
      val make_ite : Smt.Formula.t -> Smt.Term.t -> Smt.Term.t -> Smt.Term.t
      val is_int : Smt.Term.t -> bool
      val is_real : Smt.Term.t -> bool
      val t_true : Smt.Term.t
      val t_false : Smt.Term.t
    end
  and Formula :
    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
  exception Unsat of int list
  val set_cc : bool -> unit
  module type Solver =
    sig
      type state
      val get_time : unit -> float
      val get_calls : unit -> int
      val clear : unit -> unit
      val assume : ?profiling:bool -> id:int -> Smt.Formula.t -> unit
      val check : ?profiling:bool -> unit -> unit
      val save_state : unit -> Smt.Solver.state
      val restore_state : Smt.Solver.state -> unit
      val entails : ?profiling:bool -> id:int -> Smt.Formula.t -> bool
    end
  module Make : functor (Dummy : sig  end) -> Solver
end