Connect++ 0.6.1
A fast, readable connection prover for first-order logic.
Loading...
Searching...
No Matches
Public Member Functions | Private Member Functions | Private Attributes | Friends | List of all members
Stack Class Reference

If you implement the stacks used by the prover as a vector<StackItem> then every time you move down the stack a StackItem destructor is called. This ends up eating about 1/6th of the runtime, and is completely unnecessary. More...

#include <Stack.hpp>

Collaboration diagram for Stack:
Collaboration graph
[legend]

Public Member Functions

 Stack ()
 The constructor is straightforward - just make some initial space in the vector.
 
void clear ()
 Exact analogue of the same function for vector<>.
 
bool empty () const
 Exact analogue of the same function for vector<>.
 
size_t size () const
 Exact analogue of the same function for vector<>.
 
void push_back (const StackItem &_item)
 Exact analogue of the same function for vector<>.
 
StackItem & back ()
 Exact analogue of the same function for vector<>.
 
void pop_back ()
 Exact analogue of the same function for vector<>. BUT - importantly - avoid calling the StackItem destructor.
 
StackItem & operator[] (size_t _i)
 Exact analogue of the same function for vector<>.
 
void emplace_back (StackItemType sit, const Clause &_c, const SimplePath &_p, const Lemmata &_l, uint32_t _d)
 (Almost!) exact analogue of the same function for vector<>.
 
void emplace_back (StackItemType sit, const Clause &_c, const SimplePath &_p, const Lemmata &_l, const Substitution &_sub, uint32_t _d)
 (Almost!) exact analogue of the same function for vector<>.
 

Private Member Functions

void extend (size_t _n)
 Make extra space later if needed.
 

Private Attributes

StackItem * stack
 The idea is to store the stack here, but to never actually remove anything from it, so we avoid calling the destructor for StackItem.
 
size_t next_item_index
 Keep track of where the next empty space is.
 
size_t capacity
 Keep track of how much space we have. If we need more then extend as needed.
 

Friends

ostream & operator<< (ostream &out, Stack &_s)
 

Detailed Description

If you implement the stacks used by the prover as a vector<StackItem> then every time you move down the stack a StackItem destructor is called. This ends up eating about 1/6th of the runtime, and is completely unnecessary.

This class just wraps a stack up in such a way that StackItems get left in place when moving down the stack, and overwritten when moving up. A bunch of space is initialised at the outset and extended whenever necessary.

Definition at line 40 of file Stack.hpp.

Constructor & Destructor Documentation

◆ Stack()

Stack::Stack ( )
inline

The constructor is straightforward - just make some initial space in the vector.

Definition at line 75 of file Stack.hpp.

75 : stack(), next_item_index(0), capacity(params::stack_start_size) {
76 stack = new StackItem [params::stack_start_size];
77 };
Stack::next_item_index
size_t next_item_index
Keep track of where the next empty space is.
Definition Stack.hpp:50
Stack::stack
StackItem * stack
The idea is to store the stack here, but to never actually remove anything from it,...
Definition Stack.hpp:46
Stack::capacity
size_t capacity
Keep track of how much space we have. If we need more then extend as needed.
Definition Stack.hpp:55
StackItem
Stack items: each contains its own material for generating possible next inferences.
Definition StackItem.hpp:54

◆ ~Stack()

Stack::~Stack ( )
inline

Definition at line 78 of file Stack.hpp.

78{ delete [] stack; }

Member Function Documentation

◆ back()

StackItem & Stack::back ( )
inline

Exact analogue of the same function for vector<>.

Definition at line 109 of file Stack.hpp.

109 {
110 return stack[next_item_index - 1];
111 }

◆ clear()

void Stack::clear ( )
inline

Exact analogue of the same function for vector<>.

Definition at line 82 of file Stack.hpp.

82 {
83 next_item_index = 0;
84 }

◆ emplace_back() [1/2]

void Stack::emplace_back ( StackItemType sit,
const Clause & _c,
const SimplePath & _p,
const Lemmata & _l,
const Substitution & _sub,
uint32_t _d )
inline

(Almost!) exact analogue of the same function for vector<>.

Strictly speaking it doesn't do exactly the same thing, because we only want to copy into existing storage, without risking actually constructing (and destructing) a StackItem.

Definition at line 158 of file Stack.hpp.

163 {
164 if (next_item_index == capacity) {
165 extend(params::stack_increment);
166 }
167 StackItem* si = stack + next_item_index;
168 si->item_type = sit;
169 si->c = _c;
170 si->p = _p;
171 si->l = _l;
172 si->sub = _sub;
173 si->depth = _d;
174 si->bt_restriction_index = 0;
175 si->stack_item_setup();
176 next_item_index++;
177 }
Stack::extend
void extend(size_t _n)
Make extra space later if needed.
Definition Stack.hpp:59
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:76
StackItem::sub
Substitution sub
Some nodes in the proof tree have an associated substitution.
Definition StackItem.hpp:94
StackItem::depth
uint32_t depth
How deep in the proof tree are we?
Definition StackItem.hpp:98
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:111
StackItem::l
Lemmata l
Each node in the proof tree is a tuple of clause, matrix, path, lemmas: this is the lemmas.
Definition StackItem.hpp:85
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:63
StackItem::item_type
StackItemType item_type
What type of StackItem is this?
Definition StackItem.hpp:58
StackItem::stack_item_setup
void stack_item_setup()
Basic setup collected in a method to avoid repeating it in the various constructors.
Definition StackItem.cpp:51

◆ emplace_back() [2/2]

void Stack::emplace_back ( StackItemType sit,
const Clause & _c,
const SimplePath & _p,
const Lemmata & _l,
uint32_t _d )
inline

(Almost!) exact analogue of the same function for vector<>.

Strictly speaking it doesn't do exactly the same thing, because we only want to copy into existing storage, without risking actually constructing (and destructing) a StackItem.

Definition at line 132 of file Stack.hpp.

136 {
137 if (next_item_index == capacity) {
138 extend(params::stack_increment);
139 }
140 StackItem* si = stack + next_item_index;
141 si->item_type = sit;
142 si->c = _c;
143 si->p = _p;
144 si->l = _l;
145 si->sub.clear();
146 si->depth = _d;
147 si->bt_restriction_index = 0;
148 si->stack_item_setup();
149 next_item_index++;
150 }
Substitution::clear
void clear()
Clear a substitution.
Definition Substitution.hpp:85

◆ empty()

bool Stack::empty ( ) const
inline

Exact analogue of the same function for vector<>.

Definition at line 88 of file Stack.hpp.

88 {
89 return next_item_index == 0;
90 }

◆ extend()

void Stack::extend ( size_t _n)
inlineprivate

Make extra space later if needed.

Definition at line 59 of file Stack.hpp.

59 {
60 size_t old_capacity = capacity;
61 // _n == 0 is interpreted as "double the capacity".
62 _n == 0 ? capacity *= 2 : capacity += _n;
63 StackItem* old_stack = stack;
64 stack = new StackItem [capacity];
65 for (size_t i = 0; i < old_capacity; i++) {
66 stack[i] = old_stack[i];
67 }
68 delete [] old_stack;
69 }

◆ operator[]()

StackItem & Stack::operator[] ( size_t _i)
inline

Exact analogue of the same function for vector<>.

Definition at line 122 of file Stack.hpp.

122 {
123 return stack[_i];
124 }

◆ pop_back()

void Stack::pop_back ( )
inline

Exact analogue of the same function for vector<>. BUT - importantly - avoid calling the StackItem destructor.

Definition at line 116 of file Stack.hpp.

116 {
117 next_item_index--;
118 }

◆ push_back()

void Stack::push_back ( const StackItem & _item)
inline

Exact analogue of the same function for vector<>.

Definition at line 100 of file Stack.hpp.

100 {
101 if (next_item_index == capacity) {
102 extend(params::stack_increment);
103 }
104 stack[next_item_index++] = _item;
105 }

◆ size()

size_t Stack::size ( ) const
inline

Exact analogue of the same function for vector<>.

Definition at line 94 of file Stack.hpp.

94 {
95 return next_item_index;
96 }

Friends And Related Symbol Documentation

◆ operator<<

ostream & operator<< ( ostream & out,
Stack & _s )
friend

Definition at line 27 of file Stack.cpp.

27 {
28 for (size_t i = 0; i < _s.capacity; i++) {
29 out << _s[i] << endl;
30 }
31 return out;
32}

Member Data Documentation

◆ capacity

size_t Stack::capacity
private

Keep track of how much space we have. If we need more then extend as needed.

Definition at line 55 of file Stack.hpp.

◆ next_item_index

size_t Stack::next_item_index
private

Keep track of where the next empty space is.

Definition at line 50 of file Stack.hpp.

◆ stack

StackItem* Stack::stack
private

The idea is to store the stack here, but to never actually remove anything from it, so we avoid calling the destructor for StackItem.

Definition at line 46 of file Stack.hpp.

The documentation for this class was generated from the following file: