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";
60 result +=
"Stack item: ";
62 case StackItemType::Start:
65 case StackItemType::Axiom:
68 case StackItemType::Reduction:
69 result +=
"Reduction";
71 case StackItemType::LeftBranch:
72 result +=
"Left Branch";
74 case StackItemType::RightBranch:
75 result +=
"Right Branch";
81 result += to_string(
actions.size()) +=
" options\n";
91 result += std::to_string(
depth);
95ostream& operator<<(ostream& out,
const StackItem& si) {
string to_string(bool=false) const
Convert to a string.
string to_string(bool=false) const
Convert to a string.
string to_string(bool=false) const
Convert the path to a string.
string to_string(bool=false) const
Make a string representation.
Full representation of inferences, beyond just the name.
Stack items: each contains its own stack of possible next inferences.
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.
vector< InferenceItem > actions
Actions available to try.
string to_string_unsubbed() const
Make a string representation.
Substitution sub
Some nodes in the proof tree have an associated substitution.
uint32_t depth
How deep in the proof tree are we?
Lemmata l
Each node in the proof tree is a tuple of clause, matrix, path, lemmata: this is the lemmata.
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?