25#include "StackItem.hpp"
28ostream& operator<<(ostream& out,
const StackItemType& si) {
30 case StackItemType::Start:
33 case StackItemType::Axiom:
36 case StackItemType::Reduction:
39 case StackItemType::LeftBranch:
42 case StackItemType::RightBranch:
43 out <<
"Right Branch";
92 UnificationOutcome outcome = UnificationOutcome::ConflictFail;
93 while (outcome != UnificationOutcome::Succeed &&
100 if (outcome == UnificationOutcome::Succeed) {
117 UnificationOutcome outcome = UnificationOutcome::ConflictFail;
118 while (outcome != UnificationOutcome::Succeed &&
122 if (outcome == UnificationOutcome::Succeed) {
139 if (params::use_lemmata) {
163 if (result.
T == InferenceItemType::Lemma) {
169 if (result.
T == InferenceItemType::Reduction) {
175 if (result.
T == InferenceItemType::Extension) {
184 result +=
"Stack item: ";
186 case StackItemType::Start:
189 case StackItemType::Axiom:
192 case StackItemType::Reduction:
193 result +=
"Reduction";
195 case StackItemType::LeftBranch:
196 result +=
"Left Branch";
198 case StackItemType::RightBranch:
199 result +=
"Right Branch";
214 result += std::to_string(
depth);
218ostream& operator<<(ostream& out,
const StackItem& si) {
Literal get_literal(LitNum) const
Get and return the specified Literal.
string to_string(bool=false) const
Convert to a string.
size_t size()
Self-explanatory.
string to_string(bool=false) const
Convert to a string.
Literal & examine_literal(size_t i)
Access individual literals.
Basic representation of literals, bundling together (pointers to) a Predicate, a collection of argume...
bool is_compatible_with(const Literal *) const
Literals can only be unified if the polarity and actual predicate are the same.
size_t get_pred_as_index() const
Turn a Literal into an array index.
bool subbed_equal(Literal *) const
Equality, taking account of substitutions.
void invert()
Basic manipulation - entirely self-explanatory.
Representation of the Matrix within a proof.
const Literal & inspect_index_literal(size_t i, size_t j)
Straightforward get method.
MatrixPairType get_index_entry(size_t _i, size_t _j) const
The ExtensionEnumerator needs to know this.
size_t get_index_entry_size(size_t _i) const
The ExtensionEnumerator needs to know this.
string to_string(bool=false) const
Convert the path to a string.
uint32_t length() const
Straightforward get method.
const Literal & examine_literal(size_t i) const
Access individual literals.
string to_string(bool=false) const
Make a string representation.
Wrap up various applications of unificiation into a single class: all the unification you need to do ...
void backtrack()
Apply the backtracking process to the substitution that has been constructed.
Substitution get_substitution() const
Trivial get methods for the result.
Full representation of inferences, beyond just the name.
InferenceItemType T
What kind of inference is this?
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.
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...
bool reduction_no_more_results
Make it easy to know when there are no more possibilities.
bool reduction_backtrack_restricted
Setting this to true stops any further possibilities from being generated.
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.