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

#include <StackItem.hpp>

Collaboration diagram for StackItem:

[legend]

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

void	set_this_action (const InferenceItem &inf_i)
	Basic set method.

void	set_bt_restriction_index (size_t i)
	Basic set method.

void	stack_item_setup ()
	Basic setup collected in a method to avoid repeating it in the various constructors.

void	initialize (Matrix &)
	Call this after the constructor but before you want to use the enumeration of possible actions.

InferenceItem	next_lemma ()
	Generate the next lemma.

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.

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	restrict_backtrack ()
	Adjust the collection of actions to limit backtracking.

InferenceItem	get_next_inference (Matrix &, Unifier &)
	Get the next inference to try.

string	to_string_unsubbed () const
	Make a string representation.

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.

Literal	lit
	First literal of clause c.

Literal	neg_lit
	Negation of lit.

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, lemmas: this is the lemmas.

size_t	lemma_size
	Length of current lemmas.

Substitution	sub
	Some nodes in the proof tree have an associated substitution.

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.

size_t	lemma_current_lemma_index
	Which possible lemma will we consider next?

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

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

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.

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

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

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.

Definition at line 54 of file StackItem.hpp.

Constructor & Destructor Documentation

◆ StackItem() [1/2]

StackItem::StackItem ( )

inline

Definition at line 168 of file StackItem.hpp.

168{};

◆ StackItem() [2/2]

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

inline

Definition at line 170 of file StackItem.hpp.

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

Member Function Documentation

◆ get_next_inference()

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

Get the next inference to try.

Definition at line 159 of file StackItem.cpp.

                                                                    {
  InferenceItem result;
  if (!(lemma_backtrack_restricted || lemma_no_more_results)) {
    result = next_lemma();
    if (result.T == InferenceItemType::Lemma) {
      return result;
    }
  } 
  if (!(reduction_backtrack_restricted || reduction_no_more_results)) {
    result = next_reduction(_u);
    if (result.T == InferenceItemType::Reduction) {
      return result;
    }
  }
  if (!(extension_backtrack_restricted || extension_no_more_results)) {
    result = next_extension(_m, _u);
    if (result.T == InferenceItemType::Extension) {
      return result;
    }
  }
  return result;
}

◆ initialize()

void StackItem::initialize ( Matrix & _m )

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

Definition at line 138 of file StackItem.cpp.

                                     {
  if (params::use_lemmata) {
    lemma_no_more_results = false;
  } 
 
  reduction_no_more_results = false; 
 
  extension_no_more_results = false;
  extension_i = neg_lit.get_pred_as_index();  
  extension_current_index_entry = _m.get_index_entry_size(extension_i);
}

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

                                                               {
    // Default constructor makes InferenceItemType::None.
    if (extension_backtrack_restricted || extension_no_more_results) {
        return InferenceItem();
    }
    UnificationOutcome outcome = UnificationOutcome::ConflictFail;
    while (outcome != UnificationOutcome::Succeed && 
           extension_current_index_entry > 0) {
        size_t new_index = --extension_current_index_entry;
        outcome = _u(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); 
            _u.backtrack();
            // DON'T store the substitution. You're avoiding making a copy of a clause 
            // here. Later you will make one, and then you need to find the relevant 
            // substitution.
            return InferenceItem(InferenceItemType::Extension, 
                        lit, 0,
                        p.first, p.second, extension_i, new_index);
        }   
        _u.backtrack();
    }
    extension_no_more_results = true;
    return InferenceItem();
}

◆ next_lemma()

InferenceItem StackItem::next_lemma ( )

Generate the next lemma.

This is slightly different to the others as you only ever need one.

Definition at line 70 of file StackItem.cpp.

                                    {
    // Default constructor makes InferenceItemType::None.
    if (lemma_backtrack_restricted || lemma_no_more_results) {
      return InferenceItem();
    }
    while (lemma_current_lemma_index > 0) {
        Literal& lit2 = l.examine_literal(--lemma_current_lemma_index);
        if (lit.subbed_equal(&lit2)) {
            lemma_no_more_results = true;
            return InferenceItem(InferenceItemType::Lemma, lit, 0,
                        lemma_current_lemma_index);
        }   
    }
    lemma_no_more_results = true;
    return InferenceItem();
}

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

                                                   {
    // Default constructor makes InferenceItemType::None.
    if (reduction_backtrack_restricted || reduction_no_more_results) {
        return InferenceItem();
    }
    UnificationOutcome outcome = UnificationOutcome::ConflictFail;
    while (outcome != UnificationOutcome::Succeed && 
           reduction_current_path_index > 0) {
        const Literal& lit2 = p.examine_literal(--reduction_current_path_index);
        if (!neg_lit.is_compatible_with(&lit2)) {
            continue;
        }
        outcome = _u(neg_lit, lit2);
        if (outcome == UnificationOutcome::Succeed) {
            InferenceItem result = InferenceItem(InferenceItemType::Reduction, lit, 0,
                        0, 0, _u.get_substitution(), reduction_current_path_index);
            _u.backtrack();
            return result;
        }   
        _u.backtrack();
    }
    reduction_no_more_results = true;
    return InferenceItem();
}

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

                                   {
  /*
  * Implement the leanCop style restriction on backtracking.
  */
  lemma_backtrack_restricted = true; 
  reduction_backtrack_restricted = true; 
  extension_backtrack_restricted = true; 
}

◆ set_bt_restriction_index()

void StackItem::set_bt_restriction_index ( size_t i )

inline

Basic set method.

Definition at line 195 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 189 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();
  lemma_size = l.size();
  lit = c.get_literal(0);
  neg_lit = lit;
  neg_lit.invert();
 
  lemma_current_lemma_index = lemma_size;
  lemma_backtrack_restricted = false;
  lemma_no_more_results = true;
 
  reduction_current_path_index = path_length;
  reduction_backtrack_restricted = false;
  reduction_no_more_results = true;
 
  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 182 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 += "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

◆ 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 111 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 63 of file StackItem.hpp.

◆ depth

uint32_t StackItem::depth

How deep in the proof tree are we?

Definition at line 98 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 160 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 155 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 151 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 164 of file StackItem.hpp.

◆ item_type

StackItemType StackItem::item_type

What type of StackItem is this?

Definition at line 58 of file StackItem.hpp.

◆ l

Lemmata StackItem::l

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

Definition at line 85 of file StackItem.hpp.

◆ lemma_backtrack_restricted

bool StackItem::lemma_backtrack_restricted

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

Definition at line 123 of file StackItem.hpp.

◆ lemma_current_lemma_index

size_t StackItem::lemma_current_lemma_index

Which possible lemma will we consider next?

Definition at line 118 of file StackItem.hpp.

◆ lemma_no_more_results

bool StackItem::lemma_no_more_results

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

Definition at line 127 of file StackItem.hpp.

◆ lemma_size

size_t StackItem::lemma_size

Length of current lemmas.

Definition at line 89 of file StackItem.hpp.

◆ lit

Literal StackItem::lit

First literal of clause c.

Definition at line 67 of file StackItem.hpp.

◆ neg_lit

Literal StackItem::neg_lit

Negation of lit.

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

◆ path_length

size_t StackItem::path_length

Length of current path.

Definition at line 80 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 139 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 134 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 143 of file StackItem.hpp.

◆ sub

Substitution StackItem::sub

Some nodes in the proof tree have an associated substitution.

Definition at line 94 of file StackItem.hpp.

◆ this_action

InferenceItem StackItem::this_action

Action that got you to this clause, path etc.

Definition at line 102 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

Public Member Functions

Public Attributes

Detailed Description

Constructor & Destructor Documentation

◆ StackItem() [1/2]

◆ StackItem() [2/2]

Member Function Documentation

◆ get_next_inference()

◆ initialize()

◆ next_extension()

◆ next_lemma()

◆ next_reduction()

◆ restrict_backtrack()

◆ set_bt_restriction_index()

◆ set_this_action()

◆ stack_item_setup()

◆ to_string_unsubbed()

Member Data Documentation

◆ bt_restriction_index

◆ c

◆ depth

◆ extension_backtrack_restricted

◆ extension_current_index_entry

◆ extension_i

◆ extension_no_more_results

◆ item_type

◆ l

◆ lemma_backtrack_restricted

◆ lemma_current_lemma_index

◆ lemma_no_more_results

◆ lemma_size

◆ lit

◆ neg_lit

◆ p

◆ path_length

◆ reduction_backtrack_restricted

◆ reduction_current_path_index

◆ reduction_no_more_results

◆ sub

◆ this_action