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

#include <StackItem.hpp>

Collaboration diagram for StackItem:

[legend]

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.

Definition at line 51 of file StackItem.hpp.

Constructor & Destructor Documentation

◆ StackItem() [1/7]

StackItem::StackItem ( StackItemType sit )

inline

Definition at line 107 of file StackItem.hpp.

  : item_type(sit)
  , c()
  , p()
  , l()
  , sub()
  , actions()
  , depth(0)
  , this_action()
  , bt_restriction_index(0)
  {};

◆ StackItem() [2/7]

StackItem::StackItem	(	StackItemType	sit,
		const Clause &	_c,
		const SimplePath &	_p )

inline

Definition at line 118 of file StackItem.hpp.

  : item_type(sit)
  , c(_c)
  , p(_p)
  , l()
  , sub()
  , actions()
  , depth(0)
  , this_action()
  , bt_restriction_index(0)
  {};

◆ StackItem() [3/7]

StackItem::StackItem	(	StackItemType	sit,
		const Clause &	_c,
		const SimplePath &	_p,
		const Lemmata &	_l )

inline

Definition at line 129 of file StackItem.hpp.

  : item_type(sit)
  , c(_c)
  , p(_p)
  , l(_l)
  , sub()
  , actions()
  , depth(0)
  , this_action()
  , bt_restriction_index(0)
  {};

◆ StackItem() [4/7]

StackItem::StackItem	(	StackItemType	sit,
		const Clause &	_c,
		const SimplePath &	_p,
		uint32_t	_d )

inline

Definition at line 140 of file StackItem.hpp.

  : item_type(sit)
  , c(_c)
  , p(_p)
  , l()
  , sub()
  , actions()
  , depth(_d)
  , this_action()
  , bt_restriction_index(0)
  {};

◆ StackItem() [5/7]

StackItem::StackItem	(	StackItemType	sit,
		const Clause &	_c,
		const SimplePath &	_p,
		const Lemmata &	_l,
		uint32_t	_d )

inline

Definition at line 151 of file StackItem.hpp.

  : item_type(sit)
  , c(_c)
  , p(_p)
  , l(_l)
  , sub()
  , actions()
  , depth(_d)
  , this_action()
  , bt_restriction_index(0)
  {};

◆ StackItem() [6/7]

StackItem::StackItem	(	StackItemType	sit,
		const Clause &	_c,
		const SimplePath &	_p,
		const Substitution &	_sub,
		uint32_t	_d )

inline

Definition at line 166 of file StackItem.hpp.

  : item_type(sit)
  , c(_c)
  , p(_p)
  , l()
  , sub(_sub)
  , actions()
  , depth(_d)
  , this_action()
  , bt_restriction_index(0)
  {};

◆ StackItem() [7/7]

StackItem::StackItem	(	StackItemType	sit,
		const Clause &	_c,
		const SimplePath &	_p,
		const Lemmata &	_l,
		const Substitution &	_sub,
		uint32_t	_d )

inline

Definition at line 178 of file StackItem.hpp.

  : item_type(sit)
  , c(_c)
  , p(_p)
  , l(_l)
  , sub(_sub)
  , actions()
  , depth(_d)
  , this_action()
  , bt_restriction_index(0)
  {};

Member Function Documentation

◆ clear()

void StackItem::clear ( )

inline

Delete all the remaining possible actions.

Possibly the most aggressive backtracking restriction heuristic available.

Definition at line 208 of file StackItem.hpp.

208{ actions.clear(); }

◆ 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 the leanCop style.

Definition at line 51 of file StackItem.cpp.

                                   {
  /*
  * Implement the leanCop style restriction on backtracking.
  */
  actions.clear();
}

◆ set_bt_restriction_index()

void StackItem::set_bt_restriction_index ( size_t i )

inline

Basic set method.

Definition at line 218 of file StackItem.hpp.

                                                 {
    bt_restriction_index = i;
  }

◆ set_this_action()

void StackItem::set_this_action ( const InferenceItem & inf_i )

inline

Basic set method.

Definition at line 212 of file StackItem.hpp.

                                                          {
    this_action = inf_i;
  }

◆ to_string_unsubbed()

string StackItem::to_string_unsubbed ( ) const

Make a string representation.

Definition at line 58 of file StackItem.cpp.

                                           {
  string result;
  result += "Stack item: ";
  switch (item_type) {
    case StackItemType::Start:
      result += "Start";
      break;
    case StackItemType::Axiom:
      result += "Axiom";
      break;
    case StackItemType::Reduction:
      result += "Reduction";
      break;
    case StackItemType::LeftBranch:
      result += "Left Branch";
      break;
    case StackItemType::RightBranch:
      result += "Right Branch";
      break;
    default:
      break;
  }
  result += " with ";
  result  += to_string(actions.size()) += " options\n";
  result += "C = ";
  result += c.to_string() += "\n";
  result += "P = ";
  result += p.to_string() += "\n";
  result += "L = ";
  result += l.to_string() += "\n";
  result += "Sub = ";
  result += sub.to_string() += "\n";
  result += "Depth: ";
  result += std::to_string(depth);
  return result;
}

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.

Definition at line 84 of file StackItem.hpp.

◆ 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.

Definition at line 101 of file StackItem.hpp.

◆ c

Clause StackItem::c

Each node in the proof tree is a tuple of clause, matrix, path, lemmata: this is the clause.

Definition at line 60 of file StackItem.hpp.

◆ depth

uint32_t StackItem::depth

How deep in the proof tree are we?

Definition at line 88 of file StackItem.hpp.

◆ item_type

StackItemType StackItem::item_type

What type of StackItem is this?

Definition at line 55 of file StackItem.hpp.

◆ l

Lemmata StackItem::l

Each node in the proof tree is a tuple of clause, matrix, path, lemmata: this is the lemmata.

Definition at line 70 of file StackItem.hpp.

◆ p

SimplePath StackItem::p

Each node in the proof tree is a tuple of clause, matrix, path, lemmata: this is the path.

Definition at line 65 of file StackItem.hpp.

◆ sub

Substitution StackItem::sub

Some nodes in the proof tree have an associated substitution.

Definition at line 75 of file StackItem.hpp.

◆ this_action

InferenceItem StackItem::this_action

Action that got you to this clause, path etc.

Definition at line 92 of file StackItem.hpp.

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

/Users/sbh11/Desktop/connection-prover/c++/connect++/v0.5.0/source/StackItem.hpp
/Users/sbh11/Desktop/connection-prover/c++/connect++/v0.5.0/source/StackItem.cpp

Public Member Functions

Public Attributes

Detailed Description

Constructor & Destructor Documentation

◆ StackItem() [1/7]

◆ StackItem() [2/7]

◆ StackItem() [3/7]

◆ StackItem() [4/7]

◆ StackItem() [5/7]

◆ StackItem() [6/7]

◆ StackItem() [7/7]

Member Function Documentation

◆ clear()

◆ restrict_backtrack()

◆ set_bt_restriction_index()

◆ set_this_action()

◆ to_string_unsubbed()

Member Data Documentation

◆ actions

◆ bt_restriction_index

◆ c

◆ depth

◆ item_type

◆ l

◆ p

◆ sub

◆ this_action