Connect++ 0.4.0
A fast, readable connection prover for first-order logic.
Loading...
Searching...
No Matches
StackItem.cpp
1/*
2
3Copyright © 2023-24 Sean Holden. All rights reserved.
4
5*/
6/*
7
8This file is part of Connect++.
9
10Connect++ is free software: you can redistribute it and/or modify it
11under the terms of the GNU General Public License as published by the
12Free Software Foundation, either version 3 of the License, or (at your
13option) any later version.
14
15Connect++ is distributed in the hope that it will be useful, but WITHOUT
16ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
17FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for
18more details.
19
20You should have received a copy of the GNU General Public License along
21with Connect++. If not, see <https://www.gnu.org/licenses/>.
22
23*/
24
25#include "StackItem.hpp"
26
27//----------------------------------------------------------------------
28ostream& operator<<(ostream& out, const StackItemType& si) {
29 switch (si) {
30 case StackItemType::Start:
31 out << "Start";
32 break;
33 case StackItemType::Axiom:
34 out << "Axiom";
35 break;
36 case StackItemType::Reduction:
37 out << "Reduction";
38 break;
39 case StackItemType::LeftBranch:
40 out << "Left Branch";
41 break;
42 case StackItemType::RightBranch:
43 out << "Right Branch";
44 break;
45 default:
46 break;
47 }
48 return out;
49}
50//----------------------------------------------------------------------
52 /*
53 * Implement the leanCop style restriction on backtracking.
54 */
55 actions.clear();
56}
57//----------------------------------------------------------------------
59 string result;
60 result += "Stack item: ";
61 switch (item_type) {
62 case StackItemType::Start:
63 result += "Start";
64 break;
65 case StackItemType::Axiom:
66 result += "Axiom";
67 break;
68 case StackItemType::Reduction:
69 result += "Reduction";
70 break;
71 case StackItemType::LeftBranch:
72 result += "Left Branch";
73 break;
74 case StackItemType::RightBranch:
75 result += "Right Branch";
76 break;
77 default:
78 break;
79 }
80 result += " with ";
81 result += to_string(actions.size()) += " options\n";
82 result += "C = ";
83 result += c.to_string() += "\n";
84 result += "P = ";
85 result += p.to_string() += "\n";
86 result += "L = ";
87 result += l.to_string() += "\n";
88 result += "Sub = ";
89 result += sub.to_string() += "\n";
90 result += "Depth: ";
91 result += std::to_string(depth);
92 return result;
93}
94//----------------------------------------------------------------------
95ostream& operator<<(ostream& out, const StackItem& si) {
96 out << si.to_string_unsubbed() << endl;
97 for (const InferenceItem& i : si.actions) {
98 out << i << endl;
99 }
100 return out;
101}
string to_string(bool=false) const
Convert to a string.
Definition Clause.cpp:202
string to_string(bool=false) const
Convert to a string.
Definition Lemmata.cpp:82
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.
Definition StackItem.hpp:51
void restrict_backtrack()
Adjust the collection of actions to limit backtracking.
Definition StackItem.cpp:51
SimplePath p
Each node in the proof tree is a tuple of clause, matrix, path, lemmata: this is the path.
Definition StackItem.hpp:65
vector< InferenceItem > actions
Actions available to try.
Definition StackItem.hpp:84
string to_string_unsubbed() const
Make a string representation.
Definition StackItem.cpp:58
Substitution sub
Some nodes in the proof tree have an associated substitution.
Definition StackItem.hpp:75
uint32_t depth
How deep in the proof tree are we?
Definition StackItem.hpp:88
Lemmata l
Each node in the proof tree is a tuple of clause, matrix, path, lemmata: this is the lemmata.
Definition StackItem.hpp:70
Clause c
Each node in the proof tree is a tuple of clause, matrix, path, lemmata: this is the clause.
Definition StackItem.hpp:60
StackItemType item_type
What type of StackItem is this?
Definition StackItem.hpp:55