sig
  type var = private { sv_var : Var.var; sv_offset : int; }
  type term = private { st_term : Term.term; st_offset : int; }
  type binding = private { sb_var : Subst.var; sb_term : Subst.term; }
  type subst = Subst.binding list
  module VarTable :
    sig
      type key = var
      type 'a t
      val create : int -> 'a t
      val clear : 'a t -> unit
      val copy : 'a t -> 'a t
      val add : 'a t -> key -> 'a -> 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 -> 'a -> unit
      val mem : 'a t -> key -> bool
      val iter : (key -> 'a -> unit) -> 'a t -> unit
      val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
      val length : 'a t -> int
    end
  type hash_subst = Subst.term Subst.VarTable.t
  exception SET_FAIL
  val input_literal_offset : int
  val context_literal_offset : int -> int
  val fresh_par_offset : int
  val empty : Subst.subst
  val make_var : Var.var -> int -> Subst.var
  val make_term : Term.term -> int -> Subst.term
  val make_binding : Subst.var -> Subst.term -> Subst.binding
  val get : Subst.subst -> Subst.var -> Subst.term option
  val get' : Subst.subst -> Var.var -> int -> Subst.term option
  val get_bound_vars : Subst.subst -> Subst.var list -> Subst.var list
  val set :
    recompute:bool ->
    ?p_preserving:bool ->
    Subst.subst -> Subst.var -> Subst.term -> Subst.subst
  val set' :
    recompute:bool ->
    ?p_preserving:bool ->
    Subst.subst -> Var.var -> int -> Term.term -> int -> Subst.subst
  val orient : Subst.binding -> Subst.binding
  val dereference' : Subst.hash_subst -> Subst.term -> Subst.term
  val first : Subst.subst -> Subst.binding
  val find : (Subst.binding -> bool) -> Subst.subst -> Subst.binding
  val find_all : (Subst.binding -> bool) -> Subst.subst -> Subst.subst
  val is_empty : Subst.subst -> bool
  val is_p_renaming : Subst.subst -> int -> bool
  val length : Subst.subst -> int
  val append : Subst.binding -> Subst.subst -> Subst.subst
  val map : (Subst.binding -> Subst.binding) -> Subst.subst -> Subst.subst
  val map' : (Subst.binding -> 'a) -> Subst.subst -> 'a list
  val partition :
    (Subst.binding -> bool) -> Subst.subst -> Subst.subst * Subst.subst
  val for_all : (Subst.binding -> bool) -> Subst.subst -> bool
  val exists : (Subst.binding -> bool) -> Subst.subst -> bool
  val fold : ('a -> Subst.binding -> 'a) -> 'a -> Subst.subst -> 'a
  val iter : (Subst.binding -> unit) -> Subst.subst -> unit
  module type T_Preserving =
    sig
      val set : Subst.subst -> Subst.var -> Subst.term -> Subst.subst
      val set' :
        Subst.subst -> Var.var -> int -> Term.term -> int -> Subst.subst
    end
  module PPreserving : T_Preserving
  module Preserving : T_Preserving
  module RPPreserving : T_Preserving
  module RPreserving : T_Preserving
  val normalize_term : Term.term -> Term.term
  val normalize_literal : Term.literal -> Term.literal
  val normalize_clause : Term.clause -> Term.clause
  val apply_to_term :
    ?insert_db:bool ->
    ?normalize:bool -> Subst.subst -> Term.term -> int -> Term.term
  val apply_to_literal :
    ?insert_db:bool ->
    ?normalize:bool -> Subst.subst -> Term.literal -> int -> Term.literal
  val apply_to_clause : Subst.subst -> Term.clause -> int -> Term.clause
  val apply_to_literals :
    Subst.subst -> (Term.literal * int) list -> Term.literal list
  val apply_to_literals_groups :
    Subst.subst -> (Term.literal * int) list list -> Term.literal list list
  val apply_to_literal_groups' :
    Subst.hash_subst ->
    (Term.literal * int) list list -> Term.literal list list
  val replace_offset : Subst.subst -> int -> int -> Subst.subst
  val replace_in_bound_terms :
    Subst.subst -> Term.term -> Term.term -> Subst.subst
  val reverse_bindings :
    Subst.subst -> Subst.var list -> Subst.var list -> Subst.subst
  val remove_context_var_renamings : Subst.subst -> Subst.subst
  val var_equal : Subst.var -> Subst.var -> bool
  val term_equal : Subst.term -> Subst.term -> bool
  val binding_equal : Subst.binding -> Subst.binding -> bool
  val subst_equal : Subst.subst -> Subst.subst -> bool
  val var_to_string : Subst.var -> string
  val term_to_string : Subst.term -> string
  val binding_to_string : Subst.binding -> string
  val subst_to_string : Subst.subst -> string
end