A | |
| add [Term_indexing.predicate_index] |
add
term with attached 'data to the index.
|
| addClause [Problem.problem] | |
| addClauses [Problem.problem] |
adds clauses (preserving their order) to front of current clauses
|
| addToInitialInterpretation [Problem.problem] |
adds literals (preserving their order) to the initial interpretation.
|
| apply_assert [Log.log] | apply_assert selected
registers an Assert application in the current choice point.
|
| apply_split_left [Log.log] | apply_split_left choice_point selected
registers a Left Split creating a new choice_point.
|
| apply_split_right [Log.log] | apply_split_right selected
registers a Right Split application in the current choice point.
|
| apply_split_unit [Log.log] | apply_split_unit selected
registers a Unit Split application in the current choice point.
|
| argument_to_string [Flags.flag_type] |
string representation of an argument.
|
B | |
| backtrack [Log.log] |
backtracks to the currently active choice point.
|
| backtrack [Bound.bound] |
retracts information invalidated by backtracking (
State).
|
C | |
| clear [Term_indexing.predicate_index] |
removes all entries.
|
| close [Log.log] | close closing_context_unifier registers a Close application.
|
| compare_complexity [Bound.bound] |
usual comparison.
|
| complexity_to_string [Bound.bound] |
the deepening bound as a string.
|
| containsEquality [Problem.problem] |
does the clause set contain
Symbol.equality?
|
| current_bound [Bound.bound] |
the current deepening bound.
|
D | |
| description [Flags.flag_type] |
e.g.
|
| dropped_choice_point [Bound.bound] |
the oldest choice point of an ignored literal in the current derivation branch,
if any have been ignored yet.
|
E | |
| exceeds [Bound.bound] |
returns true, if the candidate exceeds the current deepening bound.
|
| exceeds_current [Bound.bound] |
returns true, if registering this candidate would have an impact
wrt.
|
F | |
| finalize [Log.log] |
finalizes the derivation log.
|
| find [Term_indexing.predicate_index] |
returns the data attached to
term.
|
| find [Term_indexing.index] | |
| find_all_generalizations [Term_indexing.predicate_index] |
returns the data attached to all terms more general than
term.
|
| find_all_instances [Term_indexing.predicate_index] |
returns the data attached to all terms which are instances of
term.
|
| find_all_shielding [Term_indexing.predicate_index] |
returns the data attached to all terms which strongly shield
the first from the second term
(see
Term_indexing.predicate_index.find_strongly_shielding).
|
| find_all_unifiable [Term_indexing.predicate_index] |
returns the data attached to all terms unifiable with
term.
|
| find_all_unifiable_subst [Term_indexing.predicate_index] | |
| find_all_variants [Term_indexing.predicate_index] |
returns the data attached to all
(universal- and parameter-preserving) variant terms of
term
(used for testing only).
|
| find_generalization [Term_indexing.predicate_index] |
returns the data attached to a term more general than
term.
|
| find_instance [Term_indexing.predicate_index] |
returns the data attached to a term which is an instance of
term.
|
| find_shielding [Term_indexing.predicate_index] | find_shielding index term1 term2
Second part of the productivity check.
|
| find_strongly_shielding [Term_indexing.predicate_index] | find_strongly_shielding term1 term2
|
| find_unifiable [Term_indexing.predicate_index] |
returns the data attached to a term unifiable with
term.
|
| fold [Term_indexing.predicate_index] |
like
List.fold.
|
| fold [Term_indexing.index] | |
G | |
| getClauses [Problem.problem] |
returns the clause set.
|
| getConstantSymbols [Problem.problem] |
returns the constant symbols contained in the clause set
|
| getFunctionArities [Problem.problem] |
returns the function symbols grouped by arity.
|
| getFunctionSymbols [Problem.problem] |
returns the function symbols contained in the clause set
|
| getInitialInterpretation [Problem.problem] |
returns the initial interpretation.
|
| getMaxClauseLength [Problem.problem] |
returns the length of the longest clause.
|
| getPredicateArities [Problem.problem] |
returns the predicate symbols (except for
Symbol.equality) grouped by arity.
|
| getPredicateSymbols [Problem.problem] |
returns the predicate symbols contained in the clause set
(except for
Symbol.equality).
|
| get_complexity [Bound.bound] |
the complexity value of a literal.
|
| get_complexity_subst [Bound.bound] | get_complexity_subst literal subst offset
returns the complexity of the literal assembled by applying
subst with offset to literal.
|
| get_generalization_iterator [Term_indexing.predicate_index] |
object style iterator over all terms (i.e.
|
| get_shielding_iterator [Term_indexing.predicate_index] |
object style iterator over all terms (i.e.
|
H | |
| has_min_exceeding [Bound.bound] |
restarting will increase the depth bound by 1.
|
I | |
| id [Flags.flag_type] |
the flag id.
|
| incomplete [Log.log] |
registers a branch as 'closed' because of being incomplete (see
Bound).
|
| incomplete [Bound.bound] |
marks the derivation as incomplete, i.e.
|
| isBS [Problem.problem] |
is the clause set free of function symbols (Bernays-Schoenfinkle) ?
|
| isHorn [Problem.problem] |
is the clause set Horn?
|
| is_default [Flags.flag_type] |
false iff the value was specified by a command line flag
|
| is_derivation_incomplete [Bound.bound] |
an incomplete branch is part of the derivation and has been skipped.
|
| is_empty [Term_indexing.index] | |
| is_empty [Term_indexing.iterator] |
are more elements left?
|
| is_equal [Term_indexing.data] | |
| iter [Term_indexing.predicate_index] |
like
List.iter.
|
| iter [Term_indexing.index] | |
J | |
| jump [Log.log] |
registers a branch as 'closed' because of a jump (see
Jumping).
|
L | |
| long_name [Flags.flag_type] |
e.g.
|
N | |
| next [Term_indexing.iterator] |
advances to and returns the next element.
|
O | |
| opt_to_string [Flags.flag_type] |
string representation of the valid arguments.
|
P | |
| print_statistic [Bound.bound] |
string representation of the current bound, restarts, and skipped incomplete branches
(ala
Print.print_label).
|
R | |
| register [Bound.bound] |
like
Bound.bound.exceeds,
and additionally registers the candidate as dropped.
|
| register_subst [Bound.bound] | |
| remove [Term_indexing.predicate_index] |
removes the entry associated with
term.
|
| restart [Bound.bound] |
cleans all stored data and increases the depth bound (if
keep_bound is false, which is the default).
|
S | |
| set [Flags.flag_type] |
performs a validity check and updates the flag's value
resp.
|
| set_opt [Flags.flag_type] |
changes the value according to the argument.
|
| short_name [Flags.flag_type] |
e.g.
|
| signature [Flags.flag_type] |
the range of valid values.
|
| size [Term_indexing.predicate_index] |
the number of elements stored in the index.
|
T | |
| to_string [Term_indexing.predicate_index] |
string representation of the index.
|
| to_string [Term_indexing.data] | |
V | |
| value [Flags.flag_type] |
e.g.
|
| value_to_string [Flags.flag_type] |
string representation of a value.
|