sig
  module T :
    sig
      type symbol = Symbol.t
      type var = Var.t
      type sort = Type.t
      type attr
      type lambda_node = private L of sort list * t
      and lambda = private (lambda_node, unit) Hashcons.hash_consed
      and t_node = private
          FreeVar of var
        | BoundVar of int
        | Leaf of symbol
        | Node of symbol * t list
        | Let of lambda * t list
        | Exists of lambda
        | Forall of lambda
        | Annot of t * attr
      and t_prop = private { bound_vars : int list; }
      and t = private (t_node, t_prop) Hashcons.hash_consed
      and flat = private
          Var of var
        | Const of symbol
        | App of symbol * t list
        | Attr of t * attr
      val compare : t -> t -> int
      val equal : t -> t -> bool
      val hash : t -> int
      val tag : t -> int
      val mk_lambda : var list -> t -> lambda
      val eval_lambda : lambda -> t list -> t
      val partial_eval_lambda : lambda -> t list -> lambda
      val mk_term : t_node -> t
      val mk_var : var -> t
      val mk_const : symbol -> t
      val mk_app : symbol -> t list -> t
      val mk_let : (var * t) list -> t -> t
      val mk_let_elim : (var * t) list -> t -> t
      val mk_exists : var list -> t -> t
      val mk_forall : var list -> t -> t
      val mk_annot : t -> attr -> t
      val node_of_t : t -> t_node
      val node_of_lambda : lambda -> lambda_node
      val sorts_of_lambda : lambda -> sort list
      val tag_of_t : t -> int
      val eval_t :
        ?fail_on_quantifiers:bool -> (flat -> 'a list -> 'a) -> t -> 'a
      val map : (int -> t -> t) -> t -> t
      val destruct : t -> flat
      val has_quantifier : t -> bool
      val instantiate : lambda -> t list -> t
      val construct : flat -> t
      val import : t -> t
      val import_lambda : lambda -> lambda
      val pp_print_term : ?db:int -> Format.formatter -> t -> unit
      val pp_print_lambda_w :
        (?arity:int -> Format.formatter -> symbol -> unit) ->
        (Format.formatter -> var -> unit) ->
        (Format.formatter -> sort -> unit) ->
        ?db:int -> Format.formatter -> lambda -> unit
      val pp_print_term_w :
        (?arity:int -> Format.formatter -> symbol -> unit) ->
        (Format.formatter -> var -> unit) ->
        (Format.formatter -> sort -> unit) ->
        ?db:int -> Format.formatter -> t -> unit
      val print_term : ?db:int -> t -> unit
      val pp_print_lambda : ?db:int -> Format.formatter -> lambda -> unit
      val print_lambda : ?db:int -> lambda -> unit
      val stats : unit -> int * int * int * int * int * int
    end
  type t = Term.T.t
  type lambda = Term.T.lambda
  val compare : Term.t -> Term.t -> int
  val equal : Term.t -> Term.t -> bool
  val hash : Term.t -> int
  val tag : Term.t -> int
  module TermHashtbl :
    sig
      type key = t
      type 'a t
      val create : int -> 'a t
      val clear : 'a t -> unit
      val reset : 'a t -> unit
      val copy : 'a t -> 'a t
      val add : 'a t -> key -> '-> unit
      val remove : 'a t -> key -> unit
      val find : 'a t -> key -> 'a
      val find_all : 'a t -> key -> 'a list
      val replace : 'a t -> key -> '-> unit
      val mem : 'a t -> key -> bool
      val iter : (key -> '-> unit) -> 'a t -> unit
      val filter_map_inplace : (key -> '-> 'a option) -> 'a t -> unit
      val fold : (key -> '-> '-> 'b) -> 'a t -> '-> 'b
      val length : 'a t -> int
      val stats : 'a t -> Hashtbl.statistics
    end
  module TermSet :
    sig
      type elt = t
      type t
      val empty : t
      val is_empty : t -> bool
      val mem : elt -> t -> bool
      val add : elt -> t -> t
      val singleton : elt -> t
      val remove : elt -> t -> t
      val union : t -> t -> t
      val inter : t -> t -> t
      val diff : t -> t -> t
      val compare : t -> t -> int
      val equal : t -> t -> bool
      val subset : t -> t -> bool
      val iter : (elt -> unit) -> t -> unit
      val map : (elt -> elt) -> t -> t
      val fold : (elt -> '-> 'a) -> t -> '-> 'a
      val for_all : (elt -> bool) -> t -> bool
      val exists : (elt -> bool) -> t -> bool
      val filter : (elt -> bool) -> t -> t
      val partition : (elt -> bool) -> t -> t * t
      val cardinal : t -> int
      val elements : t -> elt list
      val min_elt : t -> elt
      val max_elt : t -> elt
      val choose : t -> elt
      val split : elt -> t -> t * bool * t
      val find : elt -> t -> elt
      val of_list : elt list -> t
    end
  module TermMap :
    sig
      type key = t
      type +'a t
      val empty : 'a t
      val is_empty : 'a t -> bool
      val mem : key -> 'a t -> bool
      val add : key -> '-> 'a t -> 'a t
      val singleton : key -> '-> 'a t
      val remove : key -> 'a t -> 'a t
      val merge :
        (key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
      val union : (key -> '-> '-> 'a option) -> 'a t -> 'a t -> 'a t
      val compare : ('-> '-> int) -> 'a t -> 'a t -> int
      val equal : ('-> '-> bool) -> 'a t -> 'a t -> bool
      val iter : (key -> '-> unit) -> 'a t -> unit
      val fold : (key -> '-> '-> 'b) -> 'a t -> '-> 'b
      val for_all : (key -> '-> bool) -> 'a t -> bool
      val exists : (key -> '-> bool) -> 'a t -> bool
      val filter : (key -> '-> bool) -> 'a t -> 'a t
      val partition : (key -> '-> bool) -> 'a t -> 'a t * 'a t
      val cardinal : 'a t -> int
      val bindings : 'a t -> (key * 'a) list
      val min_binding : 'a t -> key * 'a
      val max_binding : 'a t -> key * 'a
      val choose : 'a t -> key * 'a
      val split : key -> 'a t -> 'a t * 'a option * 'a t
      val find : key -> 'a t -> 'a
      val map : ('-> 'b) -> 'a t -> 'b t
      val mapi : (key -> '-> 'b) -> 'a t -> 'b t
    end
  val mk_term : Term.T.t_node -> Term.t
  val mk_lambda : Var.t list -> Term.t -> Term.lambda
  val import : Term.t -> Term.t
  val import_lambda : Term.lambda -> Term.lambda
  val is_lambda_identity : Term.lambda -> bool
  val mk_true : unit -> Term.t
  val mk_false : unit -> Term.t
  val mk_not : Term.t -> Term.t
  val mk_implies : Term.t list -> Term.t
  val mk_and : Term.t list -> Term.t
  val mk_or : Term.t list -> Term.t
  val mk_xor : Term.t list -> Term.t
  val mk_eq : Term.t list -> Term.t
  val mk_distinct : Term.t list -> Term.t
  val mk_ite : Term.t -> Term.t -> Term.t -> Term.t
  val mk_num : Numeral.t -> Term.t
  val mk_num_of_int : int -> Term.t
  val mk_constr : string -> Term.t
  val mk_dec : Decimal.t -> Term.t
  val mk_minus : Term.t list -> Term.t
  val mk_plus : Term.t list -> Term.t
  val mk_times : Term.t list -> Term.t
  val mk_div : Term.t list -> Term.t
  val mk_intdiv : Term.t list -> Term.t
  val mk_mod : Term.t -> Term.t -> Term.t
  val mk_abs : Term.t -> Term.t
  val mk_leq : Term.t list -> Term.t
  val mk_lt : Term.t list -> Term.t
  val mk_geq : Term.t list -> Term.t
  val mk_gt : Term.t list -> Term.t
  val mk_to_real : Term.t -> Term.t
  val mk_to_int : Term.t -> Term.t
  val mk_is_int : Term.t -> Term.t
  val mk_divisible : Numeral.t -> Term.t -> Term.t
  val mk_select : Term.t -> Term.t -> Term.t
  val mk_store : Term.t -> Term.t -> Term.t -> Term.t
  val mk_named : Term.t -> int * Term.t
  val mk_named_unsafe : Term.t -> string -> int -> Term.t
  val mk_uf : UfSymbol.t -> Term.t list -> Term.t
  val mk_var : Var.t -> Term.t
  val mk_let : (Var.t * Term.t) list -> Term.t -> Term.t
  val mk_exists : ?fundef:bool -> Var.t list -> Term.t -> Term.t
  val mk_forall : ?fundef:bool -> Var.t list -> Term.t -> Term.t
  val t_true : Term.t
  val t_false : Term.t
  module Abbrev :
    sig
      val ( ?%@ ) : int -> Term.t
      val ( !@ ) : Term.t -> Term.t
      val ( =>@ ) : Term.t -> Term.t -> Term.t
      val ( &@ ) : Term.t -> Term.t -> Term.t
      val ( |@ ) : Term.t -> Term.t -> Term.t
      val ( =@ ) : Term.t -> Term.t -> Term.t
      val ( ~@ ) : Term.t -> Term.t
      val ( -@ ) : Term.t -> Term.t -> Term.t
      val ( +@ ) : Term.t -> Term.t -> Term.t
      val ( *@ ) : Term.t -> Term.t -> Term.t
      val ( //@ ) : Term.t -> Term.t -> Term.t
      val ( /%@ ) : Term.t -> Term.t -> Term.t
      val ( <=@ ) : Term.t -> Term.t -> Term.t
      val ( <@ ) : Term.t -> Term.t -> Term.t
      val ( >=@ ) : Term.t -> Term.t -> Term.t
      val ( >@ ) : Term.t -> Term.t -> Term.t
    end
  val mk_bool : bool -> Term.t
  val mk_const_of_symbol_node : Symbol.symbol -> Term.t
  val mk_const : Symbol.t -> Term.t
  val mk_app_of_symbol_node : Symbol.symbol -> Term.t list -> Term.t
  val mk_app : Symbol.t -> Term.t list -> Term.t
  val mk_succ : Term.t -> Term.t
  val mk_pred : Term.t -> Term.t
  val negate : Term.t -> Term.t
  val mk_minus_simplify : Term.t -> Term.t
  val negate_simplify : Term.t -> Term.t
  val unnegate : Term.t -> Term.t
  val type_of_term : Term.t -> Type.t
  val node_of_term : Term.t -> Term.T.t_node
  val destruct : Term.t -> Term.T.flat
  val has_quantifier : Term.t -> bool
  val construct : Term.T.flat -> Term.t
  val is_atom : Term.t -> bool
  val is_negated : Term.t -> bool
  val is_free_var : Term.t -> bool
  val free_var_of_term : Term.t -> Var.t
  val is_bound_var : Term.t -> bool
  val is_leaf : Term.t -> bool
  val leaf_of_term : Term.t -> Symbol.t
  val is_node : Term.t -> bool
  val node_symbol_of_term : Term.t -> Symbol.t
  val node_args_of_term : Term.t -> Term.t list
  val is_let : Term.t -> bool
  val is_exists : Term.t -> bool
  val is_forall : Term.t -> bool
  val is_named : Term.t -> bool
  val term_of_named : Term.t -> Term.t
  val name_of_named : Term.t -> int
  val is_numeral : Term.t -> bool
  val numeral_of_term : Term.t -> Numeral.t
  val is_decimal : Term.t -> bool
  val decimal_of_term : Term.t -> Decimal.t
  val is_bool : Term.t -> bool
  val bool_of_term : Term.t -> bool
  val is_select : Term.t -> bool
  val is_store : Term.t -> bool
  val indexes_and_var_of_select : Term.t -> Var.t * Term.t list
  val array_and_indexes_of_select : Term.t -> Term.t * Term.t list
  val var_of_select_store : Term.t -> Var.t
  val pp_print_term : Format.formatter -> Term.t -> unit
  val print_term : Term.t -> unit
  val string_of_term : Term.t -> string
  val pp_print_lambda : Format.formatter -> Term.lambda -> unit
  val print_lambda : Term.lambda -> unit
  val string_of_lambda : Term.lambda -> string
  val eval_t :
    ?fail_on_quantifiers:bool ->
    (Term.T.flat -> 'a list -> 'a) -> Term.t -> 'a
  val eval_lambda : Term.lambda -> Term.t list -> Term.t
  val partial_eval_lambda : Term.lambda -> Term.t list -> Term.lambda
  val map : (int -> Term.T.t -> Term.T.t) -> Term.t -> Term.t
  val apply_subst : (Var.t * Term.t) list -> Term.t -> Term.t
  val map_state_vars : (StateVar.t -> StateVar.t) -> Term.t -> Term.t
  val map_vars : (Var.t -> Var.t) -> Term.t -> Term.t
  val mod_to_divisible : Term.t -> Term.t
  val divisible_to_mod : Term.t -> Term.t
  val nums_to_pos_nums : Term.t -> Term.t
  val bump_state : Numeral.t -> Term.t -> Term.t
  val bump_and_apply_k : (Term.t -> unit) -> Numeral.t -> Term.t -> unit
  val state_vars_of_term : Term.t -> StateVar.StateVarSet.t
  val vars_of_term : Term.t -> Var.VarSet.t
  val state_vars_at_offset_of_term :
    Numeral.t -> Term.t -> StateVar.StateVarSet.t
  val vars_at_offset_of_term : Numeral.t -> Term.t -> Var.VarSet.t
  val var_offsets_of_term : Term.t -> Numeral.t option * Numeral.t option
  val select_symbols_of_term : Term.t -> Symbol.SymbolSet.t
  val select_terms : Term.t -> Term.TermSet.t
  val convert_select : Term.t -> Term.t
  val partial_selects : Term.t -> Term.t * UfSymbol.t list
  val reinterpret_select : Term.t -> Term.t
  val indexes_of_state_var : StateVar.t -> Term.t -> Term.t list list
  val stats : unit -> int * int * int * int * int * int
end