sig
  type term = Term.term
  type literal = Term.literal
  exception ITERATOR_EMPTY
  val index_offset : int
  val query_offset : int
  class virtual ['a] data :
    object
      method virtual is_equal : 'a -> 'a -> bool
      method virtual to_string : 'a -> string
    end
  class virtual ['a] iterator :
    object method virtual is_empty : bool method virtual next : 'a end
  class type ['a] predicate_index =
    object
      method add : ?no_duplicates:bool -> Term_indexing.term -> 'a -> unit
      method clear : unit
      method find : Term_indexing.term -> 'a option
      method find_all_generalizations :
        p_preserving:bool -> Term_indexing.term -> 'a list
      method find_all_instances :
        p_preserving:bool -> Term_indexing.term -> 'a list
      method find_all_shielding :
        Term_indexing.term -> Term_indexing.term -> 'a list
      method find_all_unifiable :
        p_preserving:bool -> Term_indexing.term -> 'a list
      method find_all_unifiable_subst :
        p_preserving:bool -> Term_indexing.term -> ('a * Subst.subst) list
      method find_all_variants : Term_indexing.term -> 'a list
      method find_generalization :
        p_preserving:bool -> Term_indexing.term -> 'a option
      method find_instance :
        p_preserving:bool -> Term_indexing.term -> 'a option
      method find_shielding :
        Term_indexing.term -> Term_indexing.term -> 'a option
      method find_strongly_shielding :
        Term_indexing.term -> Term_indexing.term -> 'a option
      method find_unifiable :
        p_preserving:bool -> Term_indexing.term -> 'a option
      method fold : ('b -> Term_indexing.term -> 'a -> 'b) -> 'b -> 'b
      method get_generalization_iterator :
        p_preserving:bool -> Term_indexing.term -> 'a Term_indexing.iterator
      method get_shielding_iterator :
        Term_indexing.term -> Term_indexing.term -> 'a Term_indexing.iterator
      method iter : (Term_indexing.term -> 'a -> unit) -> unit
      method remove : Term_indexing.term -> 'a option -> bool
      method size : int
      method to_string : string
    end
  class ['a] index :
    'a Term_indexing.data ->
    ('a Term_indexing.data -> 'a Term_indexing.predicate_index) ->
    object
      method find : Term_indexing.literal -> 'a Term_indexing.predicate_index
      method fold :
        ('b ->
         Term_indexing.literal -> 'a Term_indexing.predicate_index -> 'b) ->
        'b -> 'b
      method is_empty : bool
      method iter :
        (Term_indexing.literal -> 'a Term_indexing.predicate_index -> unit) ->
        unit
    end
end