StackItem Struct Reference

Stack items: each contains its own stack of possible next inferences. More...

#include <StackItem.hpp>

Collaboration diagram for StackItem:

Public Member Functions
	StackItem (StackItemType sit)
	StackItem (StackItemType sit, const Clause &_c, const SimplePath &_p)
	StackItem (StackItemType sit, const Clause &_c, const SimplePath &_p, const Lemmata &_l)
	StackItem (StackItemType sit, const Clause &_c, const SimplePath &_p, uint32_t _d)
	StackItem (StackItemType sit, const Clause &_c, const SimplePath &_p, const Lemmata &_l, uint32_t _d)
	StackItem (StackItemType sit, const Clause &_c, const SimplePath &_p, const Substitution &_sub, uint32_t _d)
	StackItem (StackItemType sit, const Clause &_c, const SimplePath &_p, const Lemmata &_l, const Substitution &_sub, uint32_t _d)
void	restrict_backtrack ()
	Adjust the collection of actions to limit backtracking.
string	to_string_unsubbed () const
	Make a string representation.
void	clear ()
	Delete all the remaining possible actions.
void	set_this_action (const InferenceItem &inf_i)
	Basic set method.
void	set_bt_restriction_index (size_t i)
	Basic set method.

Public Attributes
StackItemType	item_type
	What type of StackItem is this?
Clause	c
	Each node in the proof tree is a tuple of clause, matrix, path, lemmata: this is the clause.
SimplePath	p
	Each node in the proof tree is a tuple of clause, matrix, path, lemmata: this is the path.
Lemmata	l
	Each node in the proof tree is a tuple of clause, matrix, path, lemmata: this is the lemmata.
Substitution	sub
	Some nodes in the proof tree have an associated substitution.
vector< InferenceItem >	actions
	Actions available to try.
uint32_t	depth
	How deep in the proof tree are we?
InferenceItem	this_action
	Action that got you to this clause, path etc.
size_t	bt_restriction_index
	Pointer that allows a right branch to know where to delete alternatives for restricted backtracking.

Detailed Description

Stack items: each contains its own stack of possible next inferences.

Member Function Documentation

clear()

void StackItem::clear ( )

inline

Delete all the remaining possible actions.

Possibly the most aggressive backtracking restriction heuristic available.

restrict_backtrack()

void StackItem::restrict_backtrack

(

)

Adjust the collection of actions to limit backtracking.

Of course, you might want to modify how this works if you want to do something more sophisticated. At present you have either the leanCop style, or the most aggressive style possible.

Member Data Documentation

actions

vector<InferenceItem> StackItem::actions

Actions available to try.

These are all the actions that can be used to extend the proof further from this point onward. They are tried in order. Reordering here is an obvious approach to making a heuristic, and deletion corresponds to restriction of backtracking.

bt_restriction_index

size_t StackItem::bt_restriction_index

Pointer that allows a right branch to know where to delete alternatives for restricted backtracking.

DO NOT try to do this by storing a pointer to the StackItem. As the vector can have its storage reallocated in the background, you end up with all manner of segfaultyness.

---

The documentation for this struct was generated from the following files:

• StackItem.hpp
• StackItem.cpp