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