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