Index of values

returns the active choice point, i.e.

string representation of the active choice point.

adds a split candidate to the repository.

add no_duplicates candidate_literal candidate_context_unifier adds a candidate_literal with its context unifier to the lookahead set.

adds an assert candidate to the repository.

to be called when a new element is added to the context.

add problem_literals context_literal candidate_type checks the new context_literal against all stored problem literals, and calls Context_unifier_search.Search.search_context_unifiers for each match.

adds an element.

adds an element.

add context literal generation is_fd_incomplete adds a new literal to the context, for generation see Context.element.

add_constant sorts constant existing registers the new constant symbol.

add a lemma to the current clause set.

add_lemma lemmas_propositional lemma global adds the lemma.

adds the binding to the substitution without doing any of the consistency checks that Subst.set does perform.

apply_propagation state context_literal context_unifier clause clause_index utility_function context_literals is similar to State.apply_split_right, but applies an assert or unit split.

apply_split_left state context_literal context_unifier clause clause_vars clause_index utility_function creates a new choice point initiated by a left split on the new context_literal.

apply_split_right state context_literal context_unifier clause clause_index utility_function explanation is similar to State.apply_split_left, but applies a right split.

see Subst.apply_to_term.

see Subst.apply_to_term.

like Subst.apply_to_literals, but using a hash_subst.

like Subst.apply_to_term.

like Subst.apply_to_literals, but for lists of literals.

apply_to_term subst term offset applies subst to term with offset and returns a new term.

are the clauses free of function symbols?

is the clause set?

are two terms variants modulo skolem constants? That is, is there a bijective mapping of the skolem constants of one literal to the skolem constants of the other literal, and the literals are universal- and parameter-preverving variants?

see Term.are_terms_variants.

are the two terms unifiable?

are two terms (universal- and parameter-preserving) variants?

the symbol arity.

like List.exists for an array.

like List.find for an array.

array_fold2 f init array1 array2 like List.fold_left2 for arrays.

like List.for_all for an array.

like List.for_all2 for an array.

array_iter2 f array1 array2 like List.iter2 for arrays.

pseudo assert literal for use as the assert gap in a context unifier, contains Term.assert_literal, always valid choice point.

marks an assert gap in a context unifier (Context_unifier).

used as the gap marker in an 'assert context unifier'.

backtrack state config closing_context_unifier (retract, explanation, lemma) backtracks state based on the given closing context unifier.

backtrack candidates retracted explanation returns the candidate store to the one associated to the current active state.

removes invalid candidates.

returns the candidate store to the one associated to the current active state.

backtrack selection retracted_split explanation removes candidates based on invalid states.

removes all information based on retracted context literals.

backtracks to the most recent valid choice point

DEPENDENCY: Problem_literals.backtrack must have been executed before, dependent on resolve information managed there.

removes context elements added in invalid choice points, and undoes the corresponding compacting of the context.

backtrack_incomplete state rectract backtracks state to the choice point before retract.

removes all literal_info entries which have been retracted, i.e.

the chosen backtracking method.

depends the first choice point on the second int the sense that, if the second is retracted in backtracking, is the first retrackted as well?

are the two bindings identical?

extended string representation of the derivation branch, including validity and dependency information.

check literal returns true, if the literal is contradictory with the lookahead set.

check_assert config bound context subst context_unifier_space context_partners is_element_incomplete returns the raw_context_unifier representation of the assert literal, if subst is a valid 'assert context unifier'.

returns a raw_context_unifier, assumes that subst has an empty remainder.

check_contradictory context literal checks if literal is contradictory with the context.

registers all candidates which exceed the depth bound and are currently applicable Bound.

registers all candidates which exceed the depth bound and are currently applicable Bound.

check_productive context producer produced checks if producer is producing the negation of produced in the context (that is producer is the context literal and produced the remainder literal of the context unifier to check).

check_split config bound subst context_unifier_space context_partners is_element_incomplete returns the raw_context_unifier representation of the context unifier subst between the input clause context_unifier_space and the context literals context_partners.

check_subsumed context literal checks if literal is (p-preservingly) subsumed by the context.

are two choice points equal?

string representation of a choice point, e.g.

are two clauses equal? order of literals does matter.

are two clauses equal? order of literals does not matter.

Example: { +p(f(a), _0), -q(b) }

empties the stack

Var.clone_renumbered var id creates a variable of the same type (i.e.

pseudo-context literal to regress, used to mark the regression task of the closing clause.

cmp_pureness_universality pureness1 pureness2 returns -1, if pureness1 is universal but pureness2 is not,, 1, if pureness2 is universal but pureness1 is not,, 0, otherwise

cmp_pureness_universality pureness1 pureness2 returns -1, 0, or 1 and prefers first, terms with as few parameters as possible, and second, terms with as much universal variables as possible.

apply compact.

total order.

total order by id.

compares the age of two choice points.

a total ordering on context unifiers based on the clause and context literal ids.

Pervasives.compare specialized for integers.

see Term.compare_terms.

total order by name.

a quick non-total order on terms.

compute_deferred problem_literals candidate_type computes all context unifiers with the context based on candidate_type, where candidate_type must be Assert or Split.

compute_for_element problem_literals context_element candidate_type computes all context unifiers with the context based on candidate_type, where candidate_type must be Assert or Split which are created by context_element.

maps each clause / context literal pairing to true, if it corresponds to a remainder literal, false otherwise.

Computes and returns short resolvents for the clause set.

a clause is condensed if it subsumes no proper subset of itself, i.e.

returns the constants partitioned by sorts.

is a clause empty, or contains only false?

does the clause set contain a (dis)equality literal?

context_literal_offset input_clause_literal_index computes the offset of the context literal paired with the input literal at position input_clause_literal_index of the clause.

same as raw_context_unifier_to_string

creates a new derivation branch.

create null_element creates an empty stack.

creates an empty candidate repository.

create limit database creates a lookahead where at most limit candidates are stored in the index.

creates an empty candidate repository.

create ... input_clauses lemmas initial_interpretation guiding_path creates a new selection over the given input clauses and lemmas.

creation of the problem_literals data structure within a given environment.

create equality bool clauses initial_interpretation creates an instance of class type problem.

provides various ways to print the current derivation.

create config state context candidates process_close_candidate process_assert_candidate space_registry creates a lemmas_propositional structure.

creates an empty heap.

creates an empty heap.

create file_name creates a default configuration.

create print problem domain_size creates a finite domain representation based on problem, and infers the problem sorts.

creates a fresh counter initialized with 0.

create a space_registry

creates the context and fixes the indexing method based.

create ~flags ~horn ~equality ~start_time ~fof ~theorem creates a new configuration initialized with flags.

creates a bound object with the initial bound given in Config.deepening_bound.

creates a bound object specialized for the BS class (function free terms) using term depth as the complexity.

creates a term index specialized to contain clauses as values.

creates a unique fresh connection symbol of the given arity.

create_context_partner cp_element cp_p_preserving cp_element

create_context_unifier rcu_space rcu_context_partners rcu_exceeding_complexity

returns the constant symbol which is the transformation of the given constant/function symbol.

Symbol.create_function name arity registers a function symbol and returns it.

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

create_input_partner ip_index ip_literal ip_vars ip_context_partners

creates a term index specialized to contain ints as values.

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

creates a term index specialized to contain literals as values.

creates a literal_info value.

creation of a parametric variable by id.

Symbol.create_predicate name arity registers a predicate symbol and returns it.

creates a Term_indexing.predicate_index using discrimination trees.

create the schema term for a symbol.

create the schema term for a term.

creates a unique fresh skolem symbol.

create: space_registry problem_literals clause process_close_candidate process_assert_candidate process_split_candidate is_assert_incomplete is_split_incomplete is_lemma

create_space cus_id cus_clause cus_vars cus_shared_vars cus_local_vars cus_input_partners cus_input_partners_ordering cus_process_close_candidate cus_process_assert_candidate cus_process_split_candidate cus_is_element_incomplete_assert cus_is_element_incomplete_split cus_lemma

creates a function that increments the utility value of the context_unifier_space.

creates a term index specialized to contain terms as values.

creation of a universal variable by id.

create_with start_value creates a new counter with start_value.

the most recent (youngest) context element used to compute the context unifier.

compile the (slow) debug version which performs additional consistency checks, i.e.

decrements the counter by 1.

decrease the utility value of clauses and lemmas after each decay_clause_utility backtrack operations.

divide the clause utility by decay_clause_utility_ratio on decay.

the initial bound for the iterative deepening.

returns +v or -v, depending on Config.plus_v.

depth of a literal, i.e.

depth_of_literal_subst subst literal offset is like Term_attributes.depth_of_literal, but variables in literal are replaced by their bindings in subst

dereferences term in the substitution.

the negated equality symbol

lists_shared equal list1 list2.

the same element?

returns the element for a literal, if the literal is in the context.

empty substitution.

true, as zip support is available.

see module description above.

the same symbol?

the equality symbol

how should equality be handled?

creates a configuration based on the command line options.

like List.exists

string representation of an explanation, e.g.

compute assert and close candidates for the new context element and propagate them

extend_partial_context_unifier partial_context_unifier input_partner context_partner extends the partial_context_unifier with the partial context unifier between input_partner and context_partner.

the false literal (sign is true).

instantiate the total axioms for arities for which only 1 symbol exist.

use static symmetry reduction

use canonicity axioms in conjunction with static symmetry reduction.

add definitions for equalities.

replace Symbol.equality by -Symbol.diff.

use term definitions for flattening of deep terms.

find a binding satisfying the predicate

find stack check finds the element specified by check.

find all bindings satisfying the predicate

find_all_subsuming context literal returns all (also compacted) context elements that (p-preservingly) subsume literal

find_all_unifiable context literal returns all (also compacted) context elements that unify with literal

finds entry with given file name in zipped file/archive

finds the maximum list element according to the given comparision function.

is not guided path recorded? i.e.

search for finite domain models.

add functionality axioms for each function symbol in finite domain mode.

get any binding in the substitution.

like List.fold

visits each stack element in order from bottom to top, i.e.

like List.for_all

to make a context unifier admissible it might be necessary to bind universal variables to new/fresh parameters.

from_file file_name creates a context from a file.

depth of the dependency tree of the context literals needed to compute this context unifier, i.e.

get subst var returns the term bound to var, or None if var is unbound.

get' subst var offset wrapper for Subst.get.

returns all symbols of the given arity

returns the axioms for the given domain size, that is for totality and equality.

computes the equality axioms needed for the clause set.

get_bound_vars subst vars returns for each var in vars the subst_vars contained in the term bound to var,, or var itself if it is unbound.

returns the current derivation branch, i.e.

computed assert candidates within the deepening bound.

computed split candidates (remainders) within the deeping bound.

the context literals of the context partners in the same order as paired to the clause in its initial order.

the choice point in which this unifier has been computed

returns the i.th domain element.

returns all domain elements for the given domain size.

computes and returns the explanation of a set of context literals.

returns the i.th domain element.

returns the relation symbol of the given arity.

returns the maker symbol of the given domain size.

candidates ignored because of productivity.

returns the flattened problem.

returns a unique id for a context_unifier_space.

executed jumps (Jumping).

get_lemma uip state context closing_context_unifier closing_clause context_literals retracted_choice_point

get_lemma uip state context closing_context_unifier closing_clause context_literals retracted_choice_point

get all stored (non-local) lemmas.

returns all global (see ) clauses.

returns the information associated with this context literal.

the sort of the top symbol

returns the original problem.

pureness of a term.

returns the sorts of the problem.

reverse function to Symbol.create_fd_symbol.

the sort of the top symbol

the next candidate to be chosen will lead to the computation of a closing context unifier (Selection_lookahead).

see Term.hash_of_clause.

see Term.hash_of_term.

the hash value of a term.

a good hash value for a variable.

the symbol' uniqe id.

the id of the choice point as used by State.compare_age

retrieval of a variable's id.

if used with the id of a choice point this give the same representation as using State.choice_point_to_string directly.

is the derivation still replaying the initial guiding path?

increments the counter by 1.

increments the counter by the given positive value.

register that this clause has been learned as a lemma.

the offset of an index literal.

infers the sorts for the clause set.

marks an assert gap for a literal of the initial interpretation of a context.

a literal of the input clause.

see Term.insert_term.

inserts the literal into the database if it is not already contained.

an invalid choice point.

invalidates a choice point.

is the clause free of function symbols? (Bernays-Schoenfinkle class)

is the clause Horn?

is this choice point invalid?

is this choice point valid?

a connection symbol?

a connection predicate?

does the clause contain exactly one positive literal?

see Selection_assert.is_element_incomplete.

is_element_incomplete candidates context_element returns true if applicable exceeding candidates computed by this context_element have been dropped when the restart mode Config.restart is Flags.opt_restart.RS_Delayed.

is this the empty substitution?

empty stack?

no elements?

no elements?

a finite domain element?

a finite domain element symbol?

see Term.is_fd_term

a finite domain relation predicate?

a finite domain relation symbol?

a finite domain marker predicate?

a finite domain marker symbol?

a finite domain function symbol?

a term built over the input signature and additional finite domain symbols? I.e.

is the original problem fof or cnf?

is the index full, i.e.

a function symbol (sort = Function)?

is the problem (after transformations) horn?

a symbol from the input signature? Same as is_predicate || is_function.

see Term.is_input_term

a term built over the input signature?

see Term.is_literal_var.

see Unification.is_term_instance.

see Term.is_term_var.

is the term mixed?

returns true if the first element has been added later to the context.

is this subset p-preserving on the given offset? I.e.

is this a parametric variable?

is the term parametric?

is_permanently_blocking blocking blocked checks if the candidate represented by blocked is always present as long as the candidate represented by blocking is present.

a predicate symbol (sort = Predicate)?

is the literal propositional, i.e.

has the raw_context_unifier become invalid after backtracking?

is_remainder subst element offset checks if the substitution maps a parameter contained in element with the given offset to a non-parameter.

checks if the substitution maps a parameter to a non-parameter.

is this a schema term?

a skolem symbol?

a skolem free literal?

a skolem free term?

is the given clause subsumed by the context?

is the clause a tautology?

is the first term a (proper or improper) generalization of the second?

is the term ground?

is the first term a (proper or improper) instance of the second?

faster shortcut for Term_attributes.is_parametric (Term_attributes.get_pureness term).

is the term of type Var?

for a fof problems, does it contain a conjecture?

is the literal true in the current context?

is this a universal variable?

is the term universal?

does the context contain only universal (i.e.

like List.iter

visits each stack element in order from bottom to top, i.e.

iterates over all elements (in unsorted order).

iterates over all elements (in unsorted order).

iter_stop apply stop like iter, but stop the traversal if stop is true on a stack element.

the chosen iterative deepening method.

must be called upon each left split decision.

do jumps in the search space Jumping.

Check after each jump_check_every_splits if a jump should be done (also based on the used time and the time limit).

a jump must at least skip over this many choice points.

for purposes of determining if a jump should be done the remaining time ration is assumed to be this fraction higher than it actually is (based on the given timeout and the used time).

the length of lables used in printing of configuration and statistic entries.

left_pad string width ensures that string has at least width by adding whitespace on its left side.

returns the left split literal used to create this choice point.

compute and store lemmas.

forget lemmas when there are more than lemma_max lemmas.

for lifted lemmas stop the computation of a lemma if more then lemma_max_constraints constraints are generated.

when forgetting lemmas keep at least lemma_min lemmas.

apply parametric propagation on lemmas/clauses learnt at least n times.

used to denote the pseudo-predicate standing for the closed clause, when computing a lemma.

use the UIP in lemma generation as described in Lemma.

the number of bindings in the substitution.

list_add equal list element adds element to list if it is not already contained.

returns the first n elements of the list, or all, if the lists is shorter than n

mapping of a list to the same type of list.

list_remove_first predicate list returns list without the first element meeting the predicate.

are the two lists equal? That is, they are of same length and elements at the same element are equal with respect to the given comparison predicate.

merges the two lists.

lists_shared equal lists finds all elements which are in more than one list.

lists_unordered_equal equal list1 list2.

see Term.term_contains_var.

see Term.term_contains_var.

are two literals equal?

Example: -p(a, _0)

apply the close look-ahaed also to Assert candidates exceeding the current deepening bound.

make_admissible config database raw_context_unifier subst remainder_flags makes the context unifier raw_context_unifier admissible.

create a Subst.binding.

create a Subst.term.

create a Subst.var.

like List.map, but the result must be a substitution.

clones the stack.

like List.map, but the result may be any list.

mapping_extend mapping key_equal value_equal key value.

like Unification.match_terms over literals.

match_substs subsuming_offset subst1 subst2 merges subst1 and subst2.

match_terms term1 offset1 term2 offset2 returns a most general substitution which applied to term1 offset1 produces term2.

returns the maximum element.

how many evaluated assert candidates (context unifiers) may be stored? this is the size of a cache of best candidates, worse candidates are forgotten until needed, then recomputed.

how many assert candidates (within the current bound) should be stored in the lookahead?

how many assert candidates exceeding the current bound should be stored in the lookahead?

how many partial context unifiers are explicitely cached in Context_unifier.context_partner.cp_partial_context_unifier?

returns the biggest partition in Sort_inference.constants_partition.

Pervasives.max specialized for integers.

how many assert candidates (context unifiers) may be stored after being computed before being evaluated? might save on computation if a closing context unifier is found before the candidates need to be evaluated.

like Const.max_unprocessed_assert_candidates for split candidates.

merge_substs subst1 subst2 merges subst1 and subst2 by adding all bindings into one substitution.

returns the minimum element.

returns the minimum element.

the -v context literal.

pseudo minus_v literal for use in a context unifier, contains Term.minus_v, always valid choice point.

allow context literals containing universal and parametric variables.

returns the most recently added context literal.

the symbol's unique name.

how to handle negative Assert candidate literals in the Horn case.

increments the counter by 1 and returns its new value.

see Subst.normalize_term.

see Subst.normalize_term.

returns the normalized version of the term.

used for initialization.

for initialization usage, invalid choice point.

to be used for default initialization.

used for initialization.

to be used for default initialization.

opens zip file/archive with given file name

orients bindings by imposing a total order: by offset: <, by universal < parametric, by var id: <

outputs a string to the output channel followed by a new line.

like List.partition

the +v context literal.

should +v be used instead of -v as the initial context literal?

pseudo plus_v literal for use in a context unifier, contains Term.plus_v, always valid choice point.

removes and returns the top element of the stack.

string representation of the statistics (Print.print_label).

prints the sorts.

string representation of the configuration (ala Print.print_label).

print_DIG context out problem prints the context in the DIG model representation, i.e.

print each computed applicable assert candidate.

print the configuration settings.

prints the (not compacted) context literals, one literal per line.

print the corresponding context unifier when an application of Assert, Split, or Close is printed.

print Assert, Split, and Close applications when they are applied during the derivation, plus stuff like the depth bound, backtracking, and restarts.

print the added equality axioms, if any.

print the axiomation in finite domain mode (Finite_domain).

print the generated problem in finite domain mode (Finite_domain).

formatted printing of a label and its value.

print the lemmas generated and kept over restarts.

print level.

string representation of the maximimal context size during the derivation (ala Print.print_label).

print a found model as a DIG.

like Config.print_model_DIG, but to the file with the given name.

print a found model as a context.

like Config.print_model_context, but to the file with the given name.

print the multiplication tables of a found finite domain model.

print a model in TPTP format

like Config.print_model_tptp, but to the file with the given name.

print the multiplication tables of a finite domain model.

print each computed applicable split candidate.

formatted printing of an integer Statistic entry and its value.

formatted printing of an integer Statistic entry and its value.

formatted printing of a float Statistic entry and its value.

print a statistics after the derivation.

print the model represented by the context.

returns the problem clause set to solve.

the file name of the problem.

applies a function to the Flags.flag_type subtype contained in the flag.

only consider productive remainders.

pushs an element onto the stack.

the offset of a query literal.

string representation of the literal pairing of the context unifier.

reads and uncompresses a zipped entry

recomputes the full context unifier in the ME paper sense.

recomputes the substitution of the raw_context_unifier.

register_input_partner problem_literals input_partner context_unifier_space registers the context_unifier_space as containing the literal input_partner, so that if a context literal unifies with this literal context_unifier_space is searched for new context unifiers.

register_literal problem_literals literal index retrieves (or implicitly creates) the input_partner representing the problem literal used at the index position in a clause.

transforms a relational term into all the functional term represented by it.

textual representation of (the remainder of) the context unifier as a clause.

removes all renamings of context variables that are not bound by/in a term bound by another variable.

removes duplicate literals.

removes the maximum element and returns it.

removes the minimum element and returns it.

removes the minimum element and returns it.

removes the top element of the stack.

removes variants from a literal set

replace_offset subst old_term new_term replaces in all terms bound in subst all occurences of old_term by new_term.

replace_offset subst old_offset new_offset replaces all occurences of old_offset in subst by new_offset.

see Term.replace_term_in_term.

replace_in_term_term term sub_term replace_term builds a new term from term by replacing every occurrence of sub_term in term by replace_term.

see Term.replace_terms_in_term.

like Term.replace_term_in_term, but for a number of terms simultaneously.

see Term.replace_vars_in_term.

replace_vars_in_term term map like Term.replace_terms_in_term, but a variable is replaced by a term by the function map.

reinitializes with state, bound, and the internal statistics.

requests a Term.term.Const term from a database.

requests a Term.term.Func term.

requests a Term.literal.

requests a negation of a literal.

see Term.request_skolemized_literal.

requests the skolemization of a literal from the database.

see Term.request_universal_clause.

see Term.request_universal_term.

requests the universal version of a term from the database, i.e.

requests a Term.term.Var term from a database.

apply resolve.

the maximum length of a resolvent computed by Preprocessing_resolution.compute_resolvents.

the maximum number of resolvents computed by Preprocessing_resolution.compute_resolvents.

the chosen restarting strategy.

reverse_var_to_par subst vars_to_reverse pars_to_keep reverses one by one the bindings of the variables in vars_to_reverse, if the variable is bound to a parameter, no variable in vars_to_keep is bound to the same parameter as the variable - this would also reverse the parameters binding and let it be bound to a universal variable, thus loosing p_preserving bindings.

analog to left_pad.

returns the right split literals applied in this choice point in order of application.

returns the root choice point.

search_context_unifiers config bound context space fixed_index active_partner subst searchs for all context unifiers of the clause space with the current context and the new context literal active_partner, which is paired to the clause literal with ip_index = fixed_index.

selects (priority based) a split literal from the repository, and blocks it from further selection (until backtracking).

selects (priority based) an assert literal from the repository, and blocks it from further selection (until backtracking).

selects a literal to be added to the context.

selects a right split literal and blocks it from further selection (until backtracking).

set subst var term.

set value sets the counter to value.

wrapper for Subst.set

replaces the current derivation branch with this choice point list.

set the input_partner as resolved by the context_partner.

performs unit simplification.

removes pure clauses.

performs trivial simplificiations based on equality and returns the simplified clauses.

accepts a list of literal lists, where each literal is the class of all regressed instances of the same context literal.

the stack size

the number of candidates to chose from.

the number of candidates to chose from.

number of elements.

number of elements.

the symbol's sort

sorts the stack.

sorts a clause with Term.compare_literals.

string representation of a sort.

performs non-ground clause splitting and returns the split clauses.

performs ground clause splitting and returns the split clauses.

ensures that independently of all flags the same derivation is produced.

returns the (wall clock) time when the derivation was started.

are the two substitutions identical?

returns the triangular form, i.e.

apply subsume.

does the first clause subsume the second one? that is, exists a subsitution that applied to the second clause yields the first clause (if seen as sets)?

term_contains_term term contained is the term contained contained in the term term?

is the variable contained in the term?

are two terms equal?

are the two terms identical?

should term indexing be applied for context checks?

Example: +p(a, _0).

system cpu timeout in seconds.

system cpu timeout in seconds.

converts a string to a Term.clause.

converts a string to a Term.clause.

to_clauses string converts string into a Term.clause list

to_clauses_from_file file_name reads the tptp file file_name into a Term.clause list.

to_clauses_from_file file_name reads the tme file file_name into a Term.clause list.

to_clauses_from_file file_name reads the file file_name and converts it into a Term.clause list

to_clauses_from_file file_name reads the tptp file file_name into a Term.clause list.

to_clauses_from_file file_name reads the tme file file_name into a Term.clause list.

to_clauses_from_file file_name reads the file file_name and converts it into a Term.clause list

converts a string to a Term.literal.

the string representation of var with id is _id for a universal variable, =id for a parameter and a * as an additional prefix for an indicator variable.

print a symbol.

string representation of the heap as an array

converts a string to a Term.term.

performs all transformations necessary to output a term as a tptp term.

converts a string to a Var.var.

returns the top element of the stack.

see Term.top_symbol_term.

returns the top symbol of the term.

tptp_clause_to_tptp_string label clause transforms a clause into a tptp string representation.

get the i.th finite domain element in tptp format: "1"

replaces all variables in a term by constants, so that instead of Darwin's _0 the output is a tptp conform X0.

the true literal (sign is true).

unifies constraints of universal literals with offsets.

like , but returns a hash_subst.

like Unification.unify_terms over literals.

like unify_literals, but extends the given substitution.

match_substs subsuming_offset subst1 subst2 merges subst1 and subst2.

a pre-check to unify_subst which only unifies top symbols of terms.

unify_terms term1 offset1 term2 offset2 returns a most general substitution which applied to term1 offset1 or term2 offset2 produces the same term.

like unify_terms, but extends the given substitution.

undoes the effects of the calls to Problem_literals.register_input_partner with this space.

adds symbol to arities, that is to list of symbols with the same arity while keeping arities in increasing order.

dummy parameter contained in plus_v and minus_v, to be used together with v_term.

dummy term to bind plus_v oder minus_v to in a context unifier, see implementation of Context_unifier.extend_partial_context_unifier.

a valid choice_point.

returns the current value of the counter.

are the two variables identical?

see Term.vars_of_literal.

see Term.vars_of_term.

returns the variables of the term (without duplicates).

the current system version, e.g.

weight of a clause, i.e.

weight of a literal, i.e.

weight_of_literal_subst subst literal offset is like Term_attributes.weight_of_literal, but variables in literal are replaced by their bindings in subst

if zip support is enabled (Zip_wrapper.enabled), and a zipped input file has been given, its name is provided here.