Connect++ 0.6.1
A fast, readable connection prover for first-order logic.
Loading...
Searching...
No Matches
StackItem.cpp
1/*
2
3Copyright © 2023-25 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//----------------------------------------------------------------------
69//----------------------------------------------------------------------
71 // Default constructor makes InferenceItemType::None.
73 return InferenceItem();
74 }
75 while (lemma_current_lemma_index > 0) {
77 if (lit.subbed_equal(&lit2)) {
79 return InferenceItem(InferenceItemType::Lemma, lit, 0,
81 }
82 }
84 return InferenceItem();
85}
86//----------------------------------------------------------------------
88 // Default constructor makes InferenceItemType::None.
90 return InferenceItem();
91 }
92 UnificationOutcome outcome = UnificationOutcome::ConflictFail;
93 while (outcome != UnificationOutcome::Succeed &&
96 if (!neg_lit.is_compatible_with(&lit2)) {
97 continue;
98 }
99 outcome = _u(neg_lit, lit2);
100 if (outcome == UnificationOutcome::Succeed) {
101 InferenceItem result = InferenceItem(InferenceItemType::Reduction, lit, 0,
103 _u.backtrack();
104 return result;
105 }
106 _u.backtrack();
107 }
109 return InferenceItem();
110}
111//----------------------------------------------------------------------
113 // Default constructor makes InferenceItemType::None.
115 return InferenceItem();
116 }
117 UnificationOutcome outcome = UnificationOutcome::ConflictFail;
118 while (outcome != UnificationOutcome::Succeed &&
120 size_t new_index = --extension_current_index_entry;
121 outcome = _u(neg_lit, _m.inspect_index_literal(extension_i, new_index));
122 if (outcome == UnificationOutcome::Succeed) {
123 const MatrixPairType p = _m.get_index_entry(extension_i, new_index);
124 _u.backtrack();
125 // DON'T store the substitution. You're avoiding making a copy of a clause
126 // here. Later you will make one, and then you need to find the relevant
127 // substitution.
128 return InferenceItem(InferenceItemType::Extension,
129 lit, 0,
130 p.first, p.second, extension_i, new_index);
131 }
132 _u.backtrack();
133 }
135 return InferenceItem();
136}
137//----------------------------------------------------------------------
139 if (params::use_lemmata) {
140 lemma_no_more_results = false;
141 }
142
144
148}
149//----------------------------------------------------------------------
151 /*
152 * Implement the leanCop style restriction on backtracking.
153 */
157}
158//----------------------------------------------------------------------
160 InferenceItem result;
162 result = next_lemma();
163 if (result.T == InferenceItemType::Lemma) {
164 return result;
165 }
166 }
168 result = next_reduction(_u);
169 if (result.T == InferenceItemType::Reduction) {
170 return result;
171 }
172 }
174 result = next_extension(_m, _u);
175 if (result.T == InferenceItemType::Extension) {
176 return result;
177 }
178 }
179 return result;
180}
181//----------------------------------------------------------------------
183 string result;
184 result += "Stack item: ";
185 switch (item_type) {
186 case StackItemType::Start:
187 result += "Start";
188 break;
189 case StackItemType::Axiom:
190 result += "Axiom";
191 break;
192 case StackItemType::Reduction:
193 result += "Reduction";
194 break;
195 case StackItemType::LeftBranch:
196 result += "Left Branch";
197 break;
198 case StackItemType::RightBranch:
199 result += "Right Branch";
200 break;
201 default:
202 break;
203 }
204 result += " with ";
205 result += "C = ";
206 result += c.to_string() += "\n";
207 result += "P = ";
208 result += p.to_string() += "\n";
209 result += "L = ";
210 result += l.to_string() += "\n";
211 result += "Sub = ";
212 result += sub.to_string() += "\n";
213 result += "Depth: ";
214 result += std::to_string(depth);
215 return result;
216}
217//----------------------------------------------------------------------
218ostream& operator<<(ostream& out, const StackItem& si) {
219 out << si.to_string_unsubbed() << endl;
220 return out;
221}
Literal get_literal(LitNum) const
Get and return the specified Literal.
Definition Clause.cpp:213
string to_string(bool=false) const
Convert to a string.
Definition Clause.cpp:257
size_t size()
Self-explanatory.
Definition Lemmata.hpp:64
string to_string(bool=false) const
Convert to a string.
Definition Lemmata.cpp:82
Literal & examine_literal(size_t i)
Access individual literals.
Definition Lemmata.hpp:78
Basic representation of literals, bundling together (pointers to) a Predicate, a collection of argume...
Definition Literal.hpp:50
bool is_compatible_with(const Literal *) const
Literals can only be unified if the polarity and actual predicate are the same.
Definition Literal.cpp:84
size_t get_pred_as_index() const
Turn a Literal into an array index.
Definition Literal.hpp:126
bool subbed_equal(Literal *) const
Equality, taking account of substitutions.
Definition Literal.cpp:152
void invert()
Basic manipulation - entirely self-explanatory.
Definition Literal.hpp:107
Representation of the Matrix within a proof.
Definition Matrix.hpp:74
const Literal & inspect_index_literal(size_t i, size_t j)
Straightforward get method.
Definition Matrix.hpp:265
MatrixPairType get_index_entry(size_t _i, size_t _j) const
The ExtensionEnumerator needs to know this.
Definition Matrix.hpp:235
size_t get_index_entry_size(size_t _i) const
The ExtensionEnumerator needs to know this.
Definition Matrix.hpp:229
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 ...
Definition Unifier.hpp:89
void backtrack()
Apply the backtracking process to the substitution that has been constructed.
Definition Unifier.cpp:195
Substitution get_substitution() const
Trivial get methods for the result.
Definition Unifier.hpp:122
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.
Definition StackItem.hpp:54
size_t reduction_current_path_index
Which possible reduction will we consider next?
Literal neg_lit
Negation of lit.
Definition StackItem.hpp:71
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.
Definition StackItem.hpp:76
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.
Definition StackItem.hpp:94
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.
Definition StackItem.hpp:89
uint32_t depth
How deep in the proof tree are we?
Definition StackItem.hpp:98
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.
Definition StackItem.cpp:70
Literal lit
First literal of clause c.
Definition StackItem.hpp:67
Lemmata l
Each node in the proof tree is a tuple of clause, matrix, path, lemmas: this is the lemmas.
Definition StackItem.hpp:85
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...
Definition StackItem.cpp:87
Clause c
Each node in the proof tree is a tuple of clause, matrix, path, lemmata: this is the clause.
Definition StackItem.hpp:63
StackItemType item_type
What type of StackItem is this?
Definition StackItem.hpp:58
void stack_item_setup()
Basic setup collected in a method to avoid repeating it in the various constructors.
Definition StackItem.cpp:51
size_t path_length
Length of current path.
Definition StackItem.hpp:80