25#include "VariableIndex.hpp"
28VariableIndex::VariableIndex()
34, first_anon_variable(0)
35, highest_anon_variable(0)
36, all_names_added(false)
40VariableIndex::~VariableIndex() {
41 for (
size_t i = 0; i <
vars.size(); i++)
53 vars.push_back(new_var);
61 cerr <<
"You can't add any more named variables." << endl;
72 for (
size_t i = 0; i <
vars.size(); i++)
73 vars[i]->remove_substitution();
93 vars.push_back(new_var);
99 string name(params::unique_var_prefix);
106 string name(params::unique_var_prefix);
117 istringstream st(var_name);
126 cerr <<
"That anonymous variable doesn't exist" << endl;
133 cerr <<
"That named variable doesn't exist" << endl;
153 cerr <<
"There's nowhere left to backtrack to." << endl;
172 out <<
"Variable Index" << endl;
173 out <<
"--------------" << endl;
182 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 * > cached_vars
All the cached variables made.
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.
Variable * add_cached_var()
Cached variables are dealt with separately as there's no need to keep track of them like the others.
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.