Up  

Class type Term_indexing.predicate_index


class type ['a] predicate_index = object .. end
The interface for a predicate term indexing module.

To be used for exactly one predicate/function symbol, not for several at once. Thus adding f(x) and g(x) is not allowed.

Insertion of variants of already inserted terms is allowed and must keep the data attached to all variants intact. For an explanation for p_preserving and i_preserving see Subst.

Access

method add : ?no_duplicates:bool -> term -> 'a -> unit
add term with attached 'data to the index.

if no_duplicates (false by default) then each term may be stored only once, i.e. if a term is added more than once only the first entry is stored with its data, the others are silently dropped.

method remove : term -> 'a option -> bool
removes the entry associated with term. if data is given, then additionally data must be attached the removed variant.

returns false if no such entry exists.

method clear : unit
removes all entries.
method size : int
the number of elements stored in the index.

Traversal

method iter : (term -> 'a -> unit) -> unit
like List.iter. function style iterator over all term/data pairs stored in the index.
method fold : 'b. ('b -> term -> 'a -> 'b) -> 'b -> 'b
like List.fold.
method get_generalization_iterator : p_preserving:bool -> term -> 'a iterator
object style iterator over all terms (i.e. the attached data) which are generalizations of the term.
method get_shielding_iterator : term -> term -> 'a iterator
object style iterator over all terms (i.e. the attached data) which shield the first term from the second term.

Find All

method find_all_variants : term -> 'a list
returns the data attached to all (universal- and parameter-preserving) variant terms of term (used for testing only).
method find_all_generalizations : p_preserving:bool -> term -> 'a list
returns the data attached to all terms more general than term.
method find_all_unifiable : p_preserving:bool -> term -> 'a list
returns the data attached to all terms unifiable with term.
method find_all_unifiable_subst : p_preserving:bool -> term -> ('a * Subst.subst) list
method find_all_instances : p_preserving:bool -> term -> 'a list
returns the data attached to all terms which are instances of term.
method find_all_shielding : term -> term -> 'a list
returns the data attached to all terms which strongly shield the first from the second term (see Term_indexing.predicate_index.find_strongly_shielding). Note: if the second term is part of the index is counts as a shielding term, while the first term does not.

Find First

method find : term -> 'a option
returns the data attached to term.
method find_generalization : p_preserving:bool -> term -> 'a option
returns the data attached to a term more general than term.
method find_unifiable : p_preserving:bool -> term -> 'a option
returns the data attached to a term unifiable with term.
method find_instance : p_preserving:bool -> term -> 'a option
returns the data attached to a term which is an instance of term.
method find_strongly_shielding : term -> term -> 'a option
find_strongly_shielding term1 term2

First part of the productivity check (see the Model Evolution paper for details).

returns None, if term2 is not strongly shielded from term1 by the index, i.e. there is no true instance of term2 which is more general than term1.

otherwise, returns a shielding entry.

Note: if the second term is part of the index it counts as a shielding term, while the first term does not.

method find_shielding : term -> term -> 'a option
find_shielding index term1 term2 Second part of the productivity check.

returns all index elements that shield term2 from term1, i.e. which have a p-preserving instance which is also a true instance of term2 and more general than term1.

Note: if the second term is part of the index it counts as a shielding term, while the first term does not.

Representation

method to_string : string
string representation of the index.