Index of types

A
apply_to_flag [Flags]	for reasons of the type system it is not possible to pass the function contained in this type directly to `Flags.process_flag`.
arities [Problem]	mapping from arity to symbols.
arities [Finite_domain]
B
binding [Unification]
binding [Subst]	a binding of a `Subst.var` to a `Subst.term`.
bound [Selection_split]
bound [Selection_assert]
bound [Selection]
bound [Problem_literals]
bound [Lemma_propositional]
bound [Jumping]
bound [Context_unifier_space]
bound [Context_unifier_search]
bound [Context_unifier_check]
bound [Context]
C
candidate_type [Context_unifier]	when a literal is added to the context all or only specific context unifiers can be computed.
candidates [Selection_split]
candidates [Selection_assert]
candidates [Lemma_propositional]
choice_point [State_backtrack]
choice_point [State]	see module description.
choice_point [Selection_types]
choice_point [Selection_split]
choice_point [Selection]
choice_point [Problem_literals]
choice_point [Log]
choice_point [Lemma_propositional]
choice_point [Lemma_lifted]
choice_point [Lemma_grounded]
choice_point [Jumping]
choice_point [Context_unifier]
choice_point [Context]
choice_point [Bound]
clause [Unification]
clause [Term_attributes]
clause [Term]	a clause: a list, not a set as in theory.
clause [State_backtrack]
clause [State]
clause [Sort_inference]
clause [Selection]
clause [Read_tptp]
clause [Read_tme]
clause [Read_darwin]
clause [Problem]
clause [Preprocessing_unit]
clause [Preprocessing_split_nonground]
clause [Preprocessing_split_ground]
clause [Preprocessing_resolution]
clause [Preprocessing_pure]
clause [Preprocessing_equality]
clause [Lemma_propositional]
clause [Lemma_lifted]
clause [Lemma_grounded]
clause [Finite_domain]
clause [Equality]
clause [Discrimination_tree]
clause [Context_unifier_space]
clause [Context_unifier_check]
clause [Context_unifier]
clause [Context]
complexity [Bound]	the complexity (of a literal), i.e.
config [Statistic]
config [State_backtrack]
config [State]
config [Selection_split]
config [Selection_assert]
config [Selection]
config [Problem_literals]
config [Log]
config [Lemma_propositional]
config [Jumping]
config [Context_unifier_space]
config [Context_unifier_search]
config [Context_unifier_check]
config [Context]
config [Config]
config [Bound]
context [State_backtrack]
context [Selection_split]
context [Selection_assert]
context [Selection]
context [Problem_literals]
context [Log]
context [Lemma_propositional]
context [Lemma_lifted]
context [Lemma_grounded]
context [Context_unifier_search]
context [Context]
context_partner [Problem_literals]
context_partner [Context_unifier_search]
context_partner [Context_unifier]	a context literal paired to an input clause literal.
context_partners [Context_unifier_search]
context_partners [Context_unifier_check]
context_partners [Context_unifier]	the context literals paired with an input clause, i.e.
context_unifier_space [Problem_literals]
context_unifier_space [Context_unifier_space]
context_unifier_space [Context_unifier_search]
context_unifier_space [Context_unifier_check]
context_unifier_space [Context_unifier]	represents an input clause and its relationship with the context, i.e.
counter [Counter]
counter [Context]
D
data [Heap.MinMaxHeap]
data [Heap.Heap]
data [Discrimination_tree]
E
element [Context]	a context literal with some information
entry [Zip_wrapper]	an entry/zipped file in a zip file/archive
explanation [State_backtrack]
explanation [State]	the explanation of a choice point are the choice points it depends on.
explanation [Lemma_propositional]
F
finite_domain [Finite_domain]	finite domain data type
finite_domain [Context]
flag [Flags]	unifies the different flag types.
flag_id [Flags]	a flag is identified by its id.
flag_type_backtracking [Flags]
flag_type_bool [Flags]
flag_type_equality [Flags]
flag_type_float [Flags]
flag_type_input_format [Flags]
flag_type_int [Flags]
flag_type_iterative_deepening [Flags]
flag_type_lemma [Flags]
flag_type_neg_assert_candidates [Flags]
flag_type_preprocess_split [Flags]
flag_type_print_fd_problem [Flags]
flag_type_restart [Flags]
flag_type_string [Flags]
flag_type_unit [Flags]
flags [Flags]	the result of the evaluation of the command line.
flags [Config]
func [Term]	a functional term, e.g.
G
guiding_path [Selection]
guiding_path [Jumping]	replaying this guiding path in order recreates the search space remaining from the corresponding jump.
guiding_step [Jumping]	a recorded step of a guiding path
H
hash_subst [Subst]	a substitution as a mapping from variables to bindings.
I
in_file [Zip_wrapper]	a zip file/archive
index [Discrimination_tree]
input_partner [Problem_literals]
input_partner [Context_unifier]	a literal of an input clause, with some properties and the results of its unification with all context literals.
J
jumping [Jumping]	initiates jumps, and record guiding paths.
L
lemmas_propositional [Lemma_propositional]
literal [Unification]
literal [Term_indexing]
literal [Term_attributes]
literal [Term]	a literal is a signed term - the term is interpreted as a predicate.
literal [State_backtrack]
literal [State]
literal [Selection_types]
literal [Selection_split]
literal [Selection_lookahead]
literal [Selection_assert]
literal [Selection]
literal [Read_darwin]
literal [Problem_literals]
literal [Problem]
literal [Preprocessing_pure]
literal [Log]
literal [Lemma_propositional]
literal [Lemma_lifted]
literal [Lemma_grounded]
literal [Lemma]
literal [Jumping]
literal [Discrimination_tree]
literal [Context_unifier_space]
literal [Context_unifier_check]
literal [Context_unifier]
literal [Context]
literal [Config]
literal [Bound]
literal_info [State]	the information associated with a context literal needed for backtracking, dependency analysis, lemma generation, ...
literal_type [State]	inference rule which produced the context literal.
O
opt_backtracking [Flags]	the valid arguments for the backtracking flag.
opt_equality [Flags]	the valid arguments for the equality flag, i.e.
opt_input_format [Flags]	the supported input formats.
opt_iterative_deepening [Flags]	the valid arguments for the iterative deepening flag.
opt_lemma [Flags]	lemma computation.
opt_neg_assert_candidates [Flags]	how to handle negative assert candidates.
opt_preprocess_split [Flags]	preprocessing of input clauses by splitting into smaller clauses.
opt_print_fd_problem [Flags]	printing of finite domain problems for each domain size.
opt_restart [Flags]	the valid arguments for the restarting strategies flag.
P
predicate_index [Discrimination_tree]
problem [Finite_domain]
problem [Context]
problem [Config]
problem_literals [Selection_split]
problem_literals [Selection_assert]
problem_literals [Problem_literals]
problem_literals [Context_unifier_space]
propositional_lemmas [Lemma_propositional]
pureness [Term_attributes]	a term is universal, if it contains no parameters,, mixed, if it contains parameters and variables,, parametric, if it contains parameters but no variables.
R
raw_context_unifier [State_backtrack]
raw_context_unifier [Selection_types]
raw_context_unifier [Selection_split]
raw_context_unifier [Selection_lookahead]
raw_context_unifier [Selection_assert]
raw_context_unifier [Log]
raw_context_unifier [Lemma_propositional]
raw_context_unifier [Context_unifier_space]
raw_context_unifier [Context_unifier_check]
raw_context_unifier [Context_unifier]	the minimal information needed to recompute a context unifier.
raw_context_unifier [Admissible]
S
selected [Selection_types]	a selected candidate
selected [Selection_split]
selected [Selection_assert]
selected [Selection]
selected [Log]
selected [Lemma_propositional]
selection [Selection]	the Selection data structure
selection_lookahead [Selection_lookahead]
sort [Symbol]	each symbol has a sort.
sorts [Sort_inference]	the sorts of a clause set.
sorts [Finite_domain]
space_registry [Selection_split]
space_registry [Lemma_propositional]
space_registry [Context_unifier_space]	used to create `context_unifier_space` values.
stack [Stack]	the stack
stack [Context_unifier]
state [State_backtrack]
state [State]	manages a derivation branch, i.e.
state [Selection_split]
state [Selection_assert]
state [Selection]
state [Problem_literals]
state [Log]
state [Lemma_propositional]
state [Lemma_lifted]
state [Lemma_grounded]
state [Jumping]
state [Context_unifier_space]
state [Context_unifier]
state [Context]
statistic [Statistic]
statistic [Selection_split]
statistic [Selection_assert]
statistic [Selection]
statistic [Problem_literals]
statistic [Jumping]
statistic [Context_unifier_space]
statistic [Context]
subst [Unification]
subst [Term_attributes]
subst [Subst]	a substitution is a set of bindings.
subst [State]
subst [Problem_literals]
subst [Lemma_lifted]
subst [Lemma_grounded]
subst [Context_unifier_search]
subst [Context_unifier_check]
subst [Context_unifier]
subst [Bound]
subst [Admissible]
symbol [Term]
symbol [Symbol]	a symbol
symbol [Sort_inference]
symbol [Problem]
symbol [Finite_domain]
symbol [Equality]
symbol [Context]
T
t [Heap.OrderedType]
t [Heap.MinMaxHeap]	the heap
t [Heap.Heap]	the heap
term [Unification]
term [Term_indexing]
term [Term_attributes]
term [Term]	a term can be a variable, a constant or a function.
term [Subst]	associates a `Term.term` with an offset.
term [Read_darwin]
term [Finite_domain]
term [Discrimination_tree]
term [Context]
V
var [Var]	a universal variable or a parameter
var [Term]
var [Subst]	associates a `Var.var` with an offset.
var [Read_darwin]
var [Context_unifier_check]
var [Context_unifier]
var [Context]