Module Discrimination_tree (.ml)

module Discrimination_tree: sig .. end

type term = Term.term 

type literal = Term.literal 

type clause = Term.clause 

type 'a data = 'a Term_indexing.data 

type 'a predicate_index = 'a Term_indexing.predicate_index 

type 'a index = 'a Term_indexing.index 

val create_predicate_index : bool -> 'a data -> 'a predicate_index

creates a Term_indexing.predicate_index using discrimination trees.

val create_index : bool -> 'a data -> 'a index

create_index productivity data creates a Term_indexing.index using discrimination trees.

as a memory optimization productivity must be true if the checks related to productiviy checks are to be supported. otherwise those checks will fail (Term_indexing.predicate_index.get_shielding_iterator. Term_indexing.predicate_index.find_all_shielding, Term_indexing.predicate_index.find_strongly_shielding, Term_indexing.predicate_index.find_shielding).

val create_int_index : bool -> int index

creates a term index specialized to contain ints as values.

val create_term_index : bool -> term index

creates a term index specialized to contain terms as values.

uses Term.term_equal for comparison.

val create_literal_index : bool -> literal index

creates a term index specialized to contain literals as values.

uses Term.literal_equal for comparison.

val create_clause_index : bool -> clause index

creates a term index specialized to contain clauses as values.

uses Term.clause_equal for clause comparison.

val create_literal_clause_index : bool ->
       (literal * clause)
       index

creates a term index specialized to contain (literal, clause) pairs as values.

uses Term.literal_equal and Term.clause_equal for clause comparison.