SubstitutionStack Class Reference

As you build a proof you make substitutions that apply to the entire proof: if you backtrack during the search you need to remove the relevant substitutions. More...

#include <SubstitutionStack.hpp>

Collaboration diagram for SubstitutionStack:

Public Member Functions
	SubstitutionStack ()
	If you need a different initialization, you're probably doing something wrong.
	SubstitutionStack (const SubstitutionStack &)=delete
	As usual, you really don't want to be messing with this kind of thing, so let the compiler find your errors.
SubstitutionStack &	operator= (const SubstitutionStack &)=delete
void	push_all (Substitution &)
	Take all the substitutions provided and add the corresponding variables to the stack.
void	backtrack ()
	Remove variables from the stack, and remove substitutions as you go, as far back as the most recent backtrack point.
void	clear ()
	Reset everything.

Private Attributes
vector< Variable * >	stack
	Stack of pointers to Variables that have been substituted.
vector< size_t >	backtrack_points
	Indexes on the stack that can be backtracked to.
size_t	next_index
	Self-explanatory.

Friends
ostream &	operator<< (ostream &, const SubstitutionStack &)

Detailed Description

As you build a proof you make substitutions that apply to the entire proof: if you backtrack during the search you need to remove the relevant substitutions.

This class implements a stack that takes a Substitution applying possibly to multiple variables, and applies it while keeping track of backtracking information so that backtracking while removing substitutions is a single method call.

Definition at line 42 of file SubstitutionStack.hpp.

Constructor & Destructor Documentation

SubstitutionStack()

SubstitutionStack::SubstitutionStack ( )

inline

If you need a different initialization, you're probably doing something wrong.

Definition at line 65 of file SubstitutionStack.hpp.

: stack(), backtrack_points(), next_index(0) {}

Member Function Documentation

backtrack()

void SubstitutionStack::backtrack

(

)

Remove variables from the stack, and remove substitutions as you go, as far back as the most recent backtrack point.

Definition at line 36 of file SubstitutionStack.cpp.

                                  {
  size_t previous_index = backtrack_points.back();
  backtrack_points.pop_back();
  while (next_index > previous_index) {
    next_index--;
    stack.back()->remove_substitution();
    stack.pop_back();
  }
}

clear()

void SubstitutionStack::clear ( )

inline

Reset everything.

Definition at line 91 of file SubstitutionStack.hpp.

{ stack.clear(); backtrack_points.clear(); next_index = 0; }

push_all()

void SubstitutionStack::push_all

(

Substitution &

sub

)

Take all the substitutions provided and add the corresponding variables to the stack.

Also save the starting point as a backtrack point.

Parameters

sub	Reference to Substitution that has been applied.

Definition at line 28 of file SubstitutionStack.cpp.

                                                  {
  backtrack_points.push_back(next_index);
  for (SubPair& p : sub) {
    stack.push_back(p.first);
    next_index++;
  }
}

Friends And Related Symbol Documentation

operator<<

ostream & operator<< ( ostream & out, const SubstitutionStack & st )

friend

Definition at line 46 of file SubstitutionStack.cpp.

                                                               {
  out << st.stack.size();
  size_t bp_index = 0;
  for (size_t i = 0; i < st.stack.size(); i++) {
    if (i == st.backtrack_points[bp_index]) {
      out << "* ";
      bp_index++;
    }
    else
      out << "  ";
    out << st.stack[i]->to_string() << " -> "
        << st.stack[i]->get_subbed_term() << endl;
  }
  return out;
}

Member Data Documentation

backtrack_points

vector<size_t> SubstitutionStack::backtrack_points

private

Indexes on the stack that can be backtracked to.

When you backtrack you undo every substitution back to the most recent index.

Definition at line 55 of file SubstitutionStack.hpp.

next_index

size_t SubstitutionStack::next_index

private

Self-explanatory.

Definition at line 59 of file SubstitutionStack.hpp.

stack

vector<Variable*> SubstitutionStack::stack

private

Stack of pointers to Variables that have been substituted.

Definition at line 48 of file SubstitutionStack.hpp.

---

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

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