Connect++ 0.5.0
A fast, readable connection prover for first-order logic.
Loading...
Searching...
No Matches
StackItem.hpp
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#ifndef STACKITEM_HPP
26#define STACKITEM_HPP
27
28#include<iostream>
29
30#include "SimplePath.hpp"
31#include "Lemmata.hpp"
32
33using std::ostream;
34
41enum class StackItemType {
42 Start, Axiom, Reduction, LeftBranch, RightBranch, Lemmata
43};
44
45ostream& operator<<(ostream&, const StackItemType&);
46
51struct StackItem {
55 StackItemType item_type;
60 Clause c;
65 SimplePath p;
70 Lemmata l;
75 Substitution sub;
84 vector<InferenceItem> actions;
88 uint32_t depth;
92 InferenceItem this_action;
101 size_t bt_restriction_index;
102 //----------------------------------------------------------------------
103 // Many constructors - mostly you're just using StackItems as
104 // storage and there isn't much to do with the contents.
105 //----------------------------------------------------------------------
106 StackItem() = delete;
107 StackItem(StackItemType sit)
108 : item_type(sit)
109 , c()
110 , p()
111 , l()
112 , sub()
113 , actions()
114 , depth(0)
115 , this_action()
116 , bt_restriction_index(0)
117 {};
118 StackItem(StackItemType sit, const Clause& _c, const SimplePath& _p)
119 : item_type(sit)
120 , c(_c)
121 , p(_p)
122 , l()
123 , sub()
124 , actions()
125 , depth(0)
126 , this_action()
127 , bt_restriction_index(0)
128 {};
129 StackItem(StackItemType sit, const Clause& _c, const SimplePath& _p, const Lemmata& _l)
130 : item_type(sit)
131 , c(_c)
132 , p(_p)
133 , l(_l)
134 , sub()
135 , actions()
136 , depth(0)
137 , this_action()
138 , bt_restriction_index(0)
139 {};
140 StackItem(StackItemType sit, const Clause& _c, const SimplePath& _p, uint32_t _d)
141 : item_type(sit)
142 , c(_c)
143 , p(_p)
144 , l()
145 , sub()
146 , actions()
147 , depth(_d)
148 , this_action()
149 , bt_restriction_index(0)
150 {};
151 StackItem(StackItemType sit,
152 const Clause& _c,
153 const SimplePath& _p,
154 const Lemmata& _l,
155 uint32_t _d)
156 : item_type(sit)
157 , c(_c)
158 , p(_p)
159 , l(_l)
160 , sub()
161 , actions()
162 , depth(_d)
163 , this_action()
164 , bt_restriction_index(0)
165 {};
166 StackItem(StackItemType sit, const Clause& _c, const SimplePath& _p,
167 const Substitution& _sub , uint32_t _d)
168 : item_type(sit)
169 , c(_c)
170 , p(_p)
171 , l()
172 , sub(_sub)
173 , actions()
174 , depth(_d)
175 , this_action()
176 , bt_restriction_index(0)
177 {};
178 StackItem(StackItemType sit, const Clause& _c, const SimplePath& _p, const Lemmata& _l,
179 const Substitution& _sub , uint32_t _d)
180 : item_type(sit)
181 , c(_c)
182 , p(_p)
183 , l(_l)
184 , sub(_sub)
185 , actions()
186 , depth(_d)
187 , this_action()
188 , bt_restriction_index(0)
189 {};
197 void restrict_backtrack();
201 string to_string_unsubbed() const;
208 void clear() { actions.clear(); }
212 inline void set_this_action(const InferenceItem& inf_i) {
213 this_action = inf_i;
214 }
218 inline void set_bt_restriction_index(size_t i) {
219 bt_restriction_index = i;
220 }
221};
222
223ostream& operator<<(ostream&, const StackItem&);
224
225#endif
Clause
Representation of clauses.
Definition Clause.hpp:52
Lemmata
Representation of the lemma list.
Definition Lemmata.hpp:49
SimplePath
Simple representation of the path within a proof tree.
Definition SimplePath.hpp:55
Substitution
General representation of a substitution.
Definition Substitution.hpp:57
InferenceItem
Full representation of inferences, beyond just the name.
Definition InferenceItem.hpp:61
StackItem
Stack items: each contains its own stack of possible next inferences.
Definition StackItem.hpp:51
StackItem::restrict_backtrack
void restrict_backtrack()
Adjust the collection of actions to limit backtracking.
Definition StackItem.cpp:51
StackItem::clear
void clear()
Delete all the remaining possible actions.
Definition StackItem.hpp:208
StackItem::p
SimplePath p
Each node in the proof tree is a tuple of clause, matrix, path, lemmata: this is the path.
Definition StackItem.hpp:65
StackItem::actions
vector< InferenceItem > actions
Actions available to try.
Definition StackItem.hpp:84
StackItem::to_string_unsubbed
string to_string_unsubbed() const
Make a string representation.
Definition StackItem.cpp:58
StackItem::sub
Substitution sub
Some nodes in the proof tree have an associated substitution.
Definition StackItem.hpp:75
StackItem::set_bt_restriction_index
void set_bt_restriction_index(size_t i)
Basic set method.
Definition StackItem.hpp:218
StackItem::depth
uint32_t depth
How deep in the proof tree are we?
Definition StackItem.hpp:88
StackItem::bt_restriction_index
size_t bt_restriction_index
Pointer that allows a right branch to know where to delete alternatives for restricted backtracking.
Definition StackItem.hpp:101
StackItem::set_this_action
void set_this_action(const InferenceItem &inf_i)
Basic set method.
Definition StackItem.hpp:212
StackItem::this_action
InferenceItem this_action
Action that got you to this clause, path etc.
Definition StackItem.hpp:92
StackItem::l
Lemmata l
Each node in the proof tree is a tuple of clause, matrix, path, lemmata: this is the lemmata.
Definition StackItem.hpp:70
StackItem::c
Clause c
Each node in the proof tree is a tuple of clause, matrix, path, lemmata: this is the clause.
Definition StackItem.hpp:60
StackItem::item_type
StackItemType item_type
What type of StackItem is this?
Definition StackItem.hpp:55