Connect++ 0.6.1
A fast, readable connection prover for first-order logic.
Loading...
Searching...
No Matches
StackItem.hpp
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#ifndef STACKITEM_HPP
26#define STACKITEM_HPP
27
28#include<iostream>
29
30#include "SimplePath.hpp"
31#include "Lemmata.hpp"
32#include "Matrix.hpp"
33
34using std::ostream;
35
42enum class StackItemType {
43 Start, Axiom, Reduction, LeftBranch, RightBranch, Lemmata
44};
45
46ostream& operator<<(ostream&, const StackItemType&);
47
54struct StackItem {
58StackItemType item_type;
98uint32_t depth;
112//----------------------------------------------------------------------
113// Generation of lemmas.
114//----------------------------------------------------------------------
128//----------------------------------------------------------------------
129// Generation of reductions.
130//----------------------------------------------------------------------
144//----------------------------------------------------------------------
145// Generation of extensions.
146//----------------------------------------------------------------------
165//----------------------------------------------------------------------
166// Methods.
167//----------------------------------------------------------------------
168StackItem() {};
169
170StackItem(StackItemType sit,
171 const Clause& _c,
172 const SimplePath& _p,
173 const Lemmata& _l,
174 uint32_t _d)
175: item_type(sit)
176, c(_c)
177, p(_p)
178, l(_l)
179, sub()
180, depth(_d)
181, this_action()
183{
185}
189inline void set_this_action(const InferenceItem& inf_i) {
190 this_action = inf_i;
191}
195inline void set_bt_restriction_index(size_t i) {
197}
202void stack_item_setup();
207void initialize(Matrix&);
234void restrict_backtrack();
242string to_string_unsubbed() const;
243};
244
245ostream& operator<<(ostream&, const StackItem&);
246
247#endif
Representation of clauses.
Definition Clause.hpp:52
Representation of the lemma list.
Definition Lemmata.hpp:49
Basic representation of literals, bundling together (pointers to) a Predicate, a collection of argume...
Definition Literal.hpp:50
Representation of the Matrix within a proof.
Definition Matrix.hpp:74
Simple representation of the path within a proof tree.
General representation of a substitution.
Wrap up various applications of unificiation into a single class: all the unification you need to do ...
Definition Unifier.hpp:89
Full representation of inferences, beyond just the name.
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
void set_bt_restriction_index(size_t i)
Basic set method.
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...
size_t bt_restriction_index
Pointer that allows a right branch to know where to delete alternatives for restricted backtracking.
bool reduction_no_more_results
Make it easy to know when there are no more possibilities.
void set_this_action(const InferenceItem &inf_i)
Basic set method.
bool reduction_backtrack_restricted
Setting this to true stops any further possibilities from being generated.
InferenceItem this_action
Action that got you to this clause, path etc.
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