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]