25#include "VariableIndex.hpp"
28VariableIndex::VariableIndex()
33, first_anon_variable(0)
34, highest_anon_variable(0)
35, all_names_added(false)
39VariableIndex::~VariableIndex() {
40 for (
size_t i = 0; i <
vars.size(); i++)
50 vars.push_back(new_var);
58 cerr <<
"You can't add any more named variables." << endl;
69 for (
size_t i = 0; i <
vars.size(); i++)
70 vars[i]->remove_substitution();
90 vars.push_back(new_var);
96 string name(params::unique_var_prefix);
104 istringstream st(var_name);
113 cerr <<
"That anonymous variable doesn't exist" << endl;
120 cerr <<
"That named variable doesn't exist" << endl;
140 cerr <<
"There's nowhere left to backtrack to." << endl;
159 out <<
"Variable Index" << endl;
160 out <<
"--------------" << endl;
169 out <<
" <- Backtrack point";
Basic representation of variables.
void remove_substitution()
Self-explanatory, but be careful!
Storage of named variables, and management of new, anonymous and unique variables.
Variable * add_unique_var()
Add a unique variable when converting to CNF.
void reset()
Get rid of all the markers used for backtracking.
ID next_unique_index
When converting to CNF you need new, unique variables, but they need to be treated separately from an...
vector< ID > backtrack_points
Backtrack points stored as indices in the vars vector.
void clear_substitutions()
Undo all substitutions made, to anything, ever.
Variable * add_named_var(const string &)
Add a variable with the specified name to the index.
ID next_index
Keep track of automatically generated Variable indices.
ID add_named_backtrack_point()
Same as add_backtrack_point, but return an identifier allowing multiple levels of backtracking using ...
ID first_anon_variable
Set after you've added all the named variables for the problem.
void set_all_names_added()
Call this to indicate that only anonymous variables can now be created.
ID highest_anon_variable
Keep track of how many anonymous Variables you currently have available.
void backtrack_to_named_point(ID)
Backtrack, possibly multiple times, to the specified point.
vector< Variable * > vars
All the variables made, named, unique and anonymous.
Variable * add_anon_var()
Add an anonymous variable.
void backtrack()
Backtrack to the last marker.
void add_backtrack_point()
Add a backtrack point.
unordered_map< string, Variable * > name_index
Fast lookup of Variables by name.
bool all_names_added
Set after you've added all the named variables for the problem.
Variable * find_variable(const string &)
Look up a variable by name.