30#include "SimplePath.hpp"
42enum class StackItemType {
43 Start, Axiom, Reduction, LeftBranch, RightBranch,
Lemmata
46ostream& operator<<(ostream&,
const StackItemType&);
245ostream& operator<<(ostream&,
const StackItem&);
Representation of clauses.
Representation of the lemma list.
Basic representation of literals, bundling together (pointers to) a Predicate, a collection of argume...
Representation of the Matrix within a proof.
Simple representation of the path within a proof tree.
General representation of a substitution.
Wrap up various applications of unificiation into a single class: all the unification you need to do ...
Full representation of inferences, beyond just the name.
Stack items: each contains its own material for generating possible next inferences.
size_t reduction_current_path_index
Which possible reduction will we consider next?
Literal neg_lit
Negation of lit.
size_t extension_current_index_entry
Which possible extension will we consider next?
bool extension_no_more_results
Make it easy to know when there are no more possibilities.
InferenceItem get_next_inference(Matrix &, Unifier &)
Get the next inference to try.
void restrict_backtrack()
Adjust the collection of actions to limit backtracking.
SimplePath p
Each node in the proof tree is a tuple of clause, matrix, path, lemmata: this is the path.
string to_string_unsubbed() const
Make a string representation.
size_t lemma_current_lemma_index
Which possible lemma will we consider next?
size_t extension_i
Index computed for neg_lit telling us where to find the information we need in the matrix index.
bool extension_backtrack_restricted
Setting this to true stops any further possibilities from being generated.
Substitution sub
Some nodes in the proof tree have an associated substitution.
void initialize(Matrix &)
Call this after the constructor but before you want to use the enumeration of possible actions.
bool lemma_no_more_results
Make it easy to know when there are no more possibilities.
size_t lemma_size
Length of current lemmas.
void set_bt_restriction_index(size_t i)
Basic set method.
uint32_t depth
How deep in the proof tree are we?
InferenceItem next_extension(Matrix &, Unifier &)
Find the next possible extension or indicate there is none. The state of the object keeps track of wh...
size_t bt_restriction_index
Pointer that allows a right branch to know where to delete alternatives for restricted backtracking.
bool reduction_no_more_results
Make it easy to know when there are no more possibilities.
void set_this_action(const InferenceItem &inf_i)
Basic set method.
bool reduction_backtrack_restricted
Setting this to true stops any further possibilities from being generated.
InferenceItem this_action
Action that got you to this clause, path etc.
InferenceItem next_lemma()
Generate the next lemma.
Literal lit
First literal of clause c.
Lemmata l
Each node in the proof tree is a tuple of clause, matrix, path, lemmas: this is the lemmas.
bool lemma_backtrack_restricted
Setting this to true stops any further possibilities from being generated.
InferenceItem next_reduction(Unifier &)
Find the next possible reduction or indicate there is none. The state of the object keeps track of wh...
Clause c
Each node in the proof tree is a tuple of clause, matrix, path, lemmata: this is the clause.
StackItemType item_type
What type of StackItem is this?
void stack_item_setup()
Basic setup collected in a method to avoid repeating it in the various constructors.
size_t path_length
Length of current path.