SubstitutionStack.hpp

/*
 
Copyright © 2023-24 Sean Holden. All rights reserved.
 
*/
/*
 
This file is part of Connect++.
 
Connect++ is free software: you can redistribute it and/or modify it 
under the terms of the GNU General Public License as published by the 
Free Software Foundation, either version 3 of the License, or (at your 
option) any later version.
 
Connect++ is distributed in the hope that it will be useful, but WITHOUT 
ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or 
FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for 
more details.
 
You should have received a copy of the GNU General Public License along 
with Connect++. If not, see <https://www.gnu.org/licenses/>. 
 
*/
 
#ifndef SUBSTITUTIONSTACK_HPP
#define SUBSTITUTIONSTACK_HPP
 
#include<iostream>
 
#include "Substitution.hpp"
 
class SubstitutionStack {
private:
  vector<Variable*> stack;
  vector<size_t> backtrack_points;
  size_t next_index;
public:
  SubstitutionStack() : stack(), backtrack_points(), next_index(0) {}
  SubstitutionStack(const SubstitutionStack&) = delete;
  SubstitutionStack& operator=(const SubstitutionStack&) = delete;
  void push_all(Substitution&);
  void backtrack();
  void clear() { stack.clear(); backtrack_points.clear(); next_index = 0; }
 
  friend ostream& operator<<(ostream&, const SubstitutionStack&);
};
 
#endif