StackItem Struct Reference

Stack items: each contains its own material for generating possible next inferences. More...

#include <StackItem.hpp>

Collaboration diagram for StackItem:

Public Member Functions
void	stack_item_setup ()
	Basic setup collected in a method to avoid repeating it in the various constructors.
void	reduction_initialize (Unifier &)
	Make sure you do this!
void	reduction_move_to_next_result (Unifier &)
	Before you do anything else, set up the first result.
bool	reduction_is_empty () const
	Have we exhaused all possible reductions?
void	reduction_restrict_backtrack ()
	Indicate that we don't want any further possibilities.
InferenceItem	next_reduction (Unifier &)
	Find the next possible reduction or indicate there is none. The state of the object keeps track of where we are.
void	all_reductions (vector< InferenceItem > &, Unifier &)
	Generate all possible reductions in one go, should you need to.
void	extension_initialize (Matrix &, Unifier &)
	Make sure you do this!
void	extension_move_to_next_result (Matrix &, Unifier &)
	Before you do anything else, set up the first result.
bool	extension_is_empty () const
	Have we exhaused all possible extensions?
void	extension_restrict_backtrack ()
	Indicate that we don't want any further possibilities.
InferenceItem	next_extension (Matrix &, Unifier &)
	Find the next possible extension or indicate there is none. The state of the object keeps track of where we are.
void	all_extensions (vector< InferenceItem > &, Matrix &, Unifier &)
	Generate all possible extensions in one go, should you need to.
	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	initialize (Matrix &, Unifier &)
	Call this after the constructor but before you want to use the enumeration of possible actions.
void	restrict_backtrack ()
	Adjust the collection of actions to limit backtracking.
void	add_all_extensions_to_actions (Matrix &, Unifier &)
	You may really want to generate all the extensions at once.
void	add_all_reductions_to_actions (Unifier &)
	You may really want to generate all the reductions at once.
bool	no_more_inferences ()
	Is there anything left to do?
InferenceItem	get_next_inference (Matrix &, Unifier &)
	Get the next inference to try.
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.
size_t	path_length
	Length of current 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.
Literal	reduction_lit
	Literal of interest.
Literal	reduction_neg_lit
	Negation of literal of interest.
LitNum	reduction_ind
	Index of literal of interest.
size_t	reduction_current_path_index
	Which possible reduction will we consider next?
bool	reduction_backtrack_restricted
	Setting this to true stops any further possibilities from being generated.
InferenceItem	reduction_next_result
	We always want to know the next available result, and especially need to try to find it so that we actually know when there are none left.
bool	reduction_no_more_results
	Make it easy to know when there are no more possibilities.
Literal	extension_lit
	Literal of interest.
Literal	extension_neg_lit
	Negation of literal of interest.
LitNum	extension_ind
	Index of literal of interest.
size_t	extension_i
	Index computed for neg_lit telling us where to find the information we need in the matrix index.
size_t	extension_index_entry_size
	Size of matrix index entry.
size_t	extension_current_index_entry
	Which possible extension will we consider next?
bool	extension_backtrack_restricted
	Setting this to true stops any further possibilities from being generated.
InferenceItem	extension_next_result
	We always want to know the next available result, and especially need to try to find it so that we actually know when there are none left.
bool	extension_no_more_results
	Make it easy to know when there are no more possibilities.

Detailed Description

Stack items: each contains its own material for generating possible next inferences.

Note: this is really performance critical. It probably looks as though there's a lot of unnecessary stuff here, but that's generally so that it can be computed once and stored.

Definition at line 56 of file StackItem.hpp.

Constructor & Destructor Documentation

StackItem() [1/7]

StackItem::StackItem ( StackItemType sit )

inline

Definition at line 270 of file StackItem.hpp.

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

StackItem() [2/7]

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

inline

Definition at line 282 of file StackItem.hpp.

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

StackItem() [3/7]

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

inline

Definition at line 296 of file StackItem.hpp.

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

StackItem() [4/7]

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

inline

Definition at line 311 of file StackItem.hpp.

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

StackItem() [5/7]

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

inline

Definition at line 326 of file StackItem.hpp.

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

StackItem() [6/7]

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

inline

Definition at line 342 of file StackItem.hpp.

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

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 358 of file StackItem.hpp.

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

Member Function Documentation

add_all_extensions_to_actions()

void StackItem::add_all_extensions_to_actions	(	Matrix &	_m,
		Unifier &	_u )

You may really want to generate all the extensions at once.

Definition at line 178 of file StackItem.cpp.

                                                                     {
  all_extensions(actions, _m, _u);
}

add_all_reductions_to_actions()

void StackItem::add_all_reductions_to_actions

(

Unifier &

_u

)

You may really want to generate all the reductions at once.

Definition at line 182 of file StackItem.cpp.

                                                         {
  all_reductions(actions, _u);
}

all_extensions()

void StackItem::all_extensions	(	vector< InferenceItem > &	extensions,
		Matrix &	_m,
		Unifier &	_u )

Generate all possible extensions in one go, should you need to.

Definition at line 156 of file StackItem.cpp.

                                                                  {
    while (!extension_no_more_results) {
        extensions.push_back(extension_next_result);
        extension_move_to_next_result(_m, _u);
    }
}

all_reductions()

void StackItem::all_reductions	(	vector< InferenceItem > &	reductions,
		Unifier &	_u )

Generate all possible reductions in one go, should you need to.

Definition at line 109 of file StackItem.cpp.

                                                      {
    while (!reduction_no_more_results) {
        reductions.push_back(reduction_next_result);
        reduction_move_to_next_result(_u);
    }
}

clear()

void StackItem::clear ( )

inline

Delete all the remaining possible actions.

Possibly the most aggressive backtracking restriction heuristic available.

Definition at line 415 of file StackItem.hpp.

{ actions.clear(); }

extension_initialize()

void StackItem::extension_initialize	(	Matrix &	_m,
		Unifier &	_u )

Make sure you do this!

Definition at line 117 of file StackItem.cpp.

                                                            {
    extension_no_more_results = false;
    extension_i = extension_neg_lit.get_pred_as_index();  
    extension_index_entry_size = _m.get_index_entry_size(extension_i);
    extension_move_to_next_result(_m, _u);
}

extension_is_empty()

bool StackItem::extension_is_empty ( ) const

inline

Have we exhaused all possible extensions?

Definition at line 244 of file StackItem.hpp.

                                       { 
    return (extension_backtrack_restricted || extension_no_more_results); 
}

extension_move_to_next_result()

void StackItem::extension_move_to_next_result	(	Matrix &	_m,
		Unifier &	_u )

Before you do anything else, set up the first result.

This is necessary because we always want to have the next available, or know that there isn't one.

Definition at line 124 of file StackItem.cpp.

                                                                     {
    if (extension_no_more_results) {
        return;
    }
    UnificationOutcome outcome = UnificationOutcome::ConflictFail;
    while (outcome != UnificationOutcome::Succeed && 
           extension_current_index_entry < extension_index_entry_size) {
        size_t new_index = extension_index_entry_size - 1 - extension_current_index_entry++;
        outcome = _u(extension_neg_lit, _m.inspect_index_literal(extension_i, new_index));
        if (outcome == UnificationOutcome::Succeed) {
            const MatrixPairType p = _m.get_index_entry(extension_i, new_index); 
            extension_next_result = InferenceItem(InferenceItemType::Extension, 
                        extension_lit, extension_ind,
                        p.first, p.second, extension_i, new_index);
            _u.backtrack();
            return;
        }   
        _u.backtrack();
    }
    extension_no_more_results = true;
}

extension_restrict_backtrack()

void StackItem::extension_restrict_backtrack ( )

inline

Indicate that we don't want any further possibilities.

Definition at line 250 of file StackItem.hpp.

                                           { 
    extension_backtrack_restricted = true; 
}

get_next_inference()

InferenceItem StackItem::get_next_inference	(	Matrix &	_m,
		Unifier &	_u )

Get the next inference to try.

Definition at line 190 of file StackItem.cpp.

                                                                    {
  InferenceItem result;
  if (actions.size() > 0) { 
    result = actions.back();
    actions.pop_back();
    return result;
  }
  if (!reduction_is_empty()) {
    return next_reduction(_u);
  }
  if (!extension_is_empty()) {
    return next_extension(_m, _u);
  }
  return result;
}

initialize()

void StackItem::initialize	(	Matrix &	_m,
		Unifier &	_u )

Call this after the constructor but before you want to use the enumeration of possible actions.

Definition at line 164 of file StackItem.cpp.

                                                  {
  reduction_initialize(_u);
  extension_initialize(_m, _u);
}

next_extension()

InferenceItem StackItem::next_extension	(	Matrix &	_m,
		Unifier &	_u )

Find the next possible extension or indicate there is none. The state of the object keeps track of where we are.

Definition at line 146 of file StackItem.cpp.

                                                               {
    // Default constructor makes InferenceItemType::None.
    InferenceItem result;
    if (extension_backtrack_restricted || extension_no_more_results) 
        return result;
    result = extension_next_result;
    extension_move_to_next_result(_m, _u);
    return result;
}

next_reduction()

InferenceItem StackItem::next_reduction

(

Unifier &

_u

)

Find the next possible reduction or indicate there is none. The state of the object keeps track of where we are.

Definition at line 99 of file StackItem.cpp.

                                                   {
    // Default constructor makes InferenceItemType::None.
    InferenceItem result;
    if (reduction_backtrack_restricted || reduction_no_more_results) 
        return result;
    result = reduction_next_result;
    reduction_move_to_next_result(_u);
    return result;
}

no_more_inferences()

bool StackItem::no_more_inferences

(

)

Is there anything left to do?

Definition at line 186 of file StackItem.cpp.

                                   { 
    return actions.empty() && reduction_is_empty() && extension_is_empty();
}

reduction_initialize()

void StackItem::reduction_initialize

(

Unifier &

_u

)

Make sure you do this!

Definition at line 71 of file StackItem.cpp.

                                                {
    reduction_no_more_results = false; 
    reduction_move_to_next_result(_u);
}

reduction_is_empty()

bool StackItem::reduction_is_empty ( ) const

inline

Have we exhaused all possible reductions?

Definition at line 210 of file StackItem.hpp.

                                       { 
    return (reduction_backtrack_restricted || reduction_no_more_results); 
}

reduction_move_to_next_result()

void StackItem::reduction_move_to_next_result

(

Unifier &

_u

)

Before you do anything else, set up the first result.

This is necessary because we always want to have the next available, or know that there isn't one.

Definition at line 76 of file StackItem.cpp.

                                                         {
    // Default constructor makes InferenceItemType::None.
    if (reduction_no_more_results)
        return;
    UnificationOutcome outcome = UnificationOutcome::ConflictFail;
    while (outcome != UnificationOutcome::Succeed && 
           reduction_current_path_index < path_length) {
        const Literal& lit2 = p.examine_literal(path_length - 1 - reduction_current_path_index++);
        if (!reduction_neg_lit.is_compatible_with(&lit2)) {
            continue;
        }
        outcome = _u(reduction_neg_lit, lit2);
        if (outcome == UnificationOutcome::Succeed) {
            reduction_next_result = InferenceItem(InferenceItemType::Reduction, reduction_lit, reduction_ind,
                        0, 0, _u.get_substitution(), path_length - reduction_current_path_index);
            _u.backtrack();
            return;
        }   
        _u.backtrack();
    }
    reduction_no_more_results = true;
}

reduction_restrict_backtrack()

void StackItem::reduction_restrict_backtrack ( )

inline

Indicate that we don't want any further possibilities.

Definition at line 216 of file StackItem.hpp.

                                           { 
    reduction_backtrack_restricted = true; 
}

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 169 of file StackItem.cpp.

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

set_bt_restriction_index()

void StackItem::set_bt_restriction_index ( size_t i )

inline

Basic set method.

Definition at line 425 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 419 of file StackItem.hpp.

                                                          {
    this_action = inf_i;
  }

stack_item_setup()

void StackItem::stack_item_setup

(

)

Basic setup collected in a method to avoid repeating it in the various constructors.

Definition at line 51 of file StackItem.cpp.

                                 {
  path_length = p.length();
  reduction_lit = c.get_literal(0);
  reduction_neg_lit = reduction_lit;
  reduction_neg_lit.invert();
  reduction_ind = 0;
  reduction_current_path_index = 0;
  reduction_backtrack_restricted = false;
  reduction_no_more_results = true;
 
  extension_lit = c.get_literal(0);
  extension_neg_lit = extension_lit;
  extension_neg_lit.invert();
  extension_ind = 0;extension_i = 0;
  extension_index_entry_size = 0;
  extension_current_index_entry = 0;
  extension_backtrack_restricted = false;
  extension_no_more_results = true;
}

to_string_unsubbed()

string StackItem::to_string_unsubbed

(

)

const

Make a string representation.

Definition at line 206 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 lemmas 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.

At some point, remove this and do it in the same way as reductions and extensions.

Definition at line 96 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 113 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 65 of file StackItem.hpp.

depth

uint32_t StackItem::depth

How deep in the proof tree are we?

Definition at line 100 of file StackItem.hpp.

extension_backtrack_restricted

bool StackItem::extension_backtrack_restricted

Setting this to true stops any further possibilities from being generated.

Definition at line 180 of file StackItem.hpp.

extension_current_index_entry

size_t StackItem::extension_current_index_entry

Which possible extension will we consider next?

Definition at line 175 of file StackItem.hpp.

extension_i

size_t StackItem::extension_i

Index computed for neg_lit telling us where to find the information we need in the matrix index.

Definition at line 167 of file StackItem.hpp.

extension_ind

LitNum StackItem::extension_ind

Index of literal of interest.

Definition at line 162 of file StackItem.hpp.

extension_index_entry_size

size_t StackItem::extension_index_entry_size

Size of matrix index entry.

Definition at line 171 of file StackItem.hpp.

extension_lit

Literal StackItem::extension_lit

Literal of interest.

Definition at line 154 of file StackItem.hpp.

extension_neg_lit

Literal StackItem::extension_neg_lit

Negation of literal of interest.

Definition at line 158 of file StackItem.hpp.

extension_next_result

InferenceItem StackItem::extension_next_result

We always want to know the next available result, and especially need to try to find it so that we actually know when there are none left.

Definition at line 186 of file StackItem.hpp.

extension_no_more_results

bool StackItem::extension_no_more_results

Make it easy to know when there are no more possibilities.

Definition at line 190 of file StackItem.hpp.

item_type

StackItemType StackItem::item_type

What type of StackItem is this?

Definition at line 60 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 79 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 70 of file StackItem.hpp.

path_length

size_t StackItem::path_length

Length of current path.

Definition at line 74 of file StackItem.hpp.

reduction_backtrack_restricted

bool StackItem::reduction_backtrack_restricted

Setting this to true stops any further possibilities from being generated.

Definition at line 137 of file StackItem.hpp.

reduction_current_path_index

size_t StackItem::reduction_current_path_index

Which possible reduction will we consider next?

Definition at line 132 of file StackItem.hpp.

reduction_ind

LitNum StackItem::reduction_ind

Index of literal of interest.

Definition at line 128 of file StackItem.hpp.

reduction_lit

Literal StackItem::reduction_lit

Literal of interest.

Definition at line 120 of file StackItem.hpp.

reduction_neg_lit

Literal StackItem::reduction_neg_lit

Negation of literal of interest.

Definition at line 124 of file StackItem.hpp.

reduction_next_result

InferenceItem StackItem::reduction_next_result

We always want to know the next available result, and especially need to try to find it so that we actually know when there are none left.

Definition at line 143 of file StackItem.hpp.

reduction_no_more_results

bool StackItem::reduction_no_more_results

Make it easy to know when there are no more possibilities.

Definition at line 147 of file StackItem.hpp.

sub

Substitution StackItem::sub

Some nodes in the proof tree have an associated substitution.

Definition at line 84 of file StackItem.hpp.

this_action

InferenceItem StackItem::this_action

Action that got you to this clause, path etc.

Definition at line 104 of file StackItem.hpp.

---

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

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