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>

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.

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.

Member Function Documentation

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.

---

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

• SubstitutionStack.hpp
• SubstitutionStack.cpp