Storage of named variables, and management of new, anonymous and unique variables. More...

#include <VariableIndex.hpp>

Collaboration diagram for VariableIndex:

[legend]

Public Member Functions
	VariableIndex (const VariableIndex &)=delete
	Copying this would be a very silly idea, so explicitly disallow it.

	VariableIndex (const VariableIndex &&)=delete

VariableIndex &	operator= (const VariableIndex &)=delete

VariableIndex &	operator= (const VariableIndex &&)=delete

ID	get_next_index () const
	Straightforward access function.

ID	get_first_anon_variable () const
	Straightforward access function.

ID	get_highest_anon_variable () const
	Straightforward access function.

bool	get_all_names_added () const
	Straightforward access function.

size_t	get_num_backtracks () const
	Straightforward access function.

Variable *	add_named_var (const string &)
	Add a variable with the specified name to the index.

Variable *	add_anon_var ()
	Add an anonymous variable.

Variable *	add_unique_var ()
	Add a unique variable when converting to CNF.

Variable *	add_cached_var ()
	Cached variables are dealt with separately as there's no need to keep track of them like the others.

Variable *	find_variable (const string &)
	Look up a variable by name.

void	set_all_names_added ()
	Call this to indicate that only anonymous variables can now be created.

void	clear_substitutions ()
	Undo all substitutions made, to anything, ever.

void	add_backtrack_point ()
	Add a backtrack point.

ID	add_named_backtrack_point ()
	Same as add_backtrack_point, but return an identifier allowing multiple levels of backtracking using backtrack_to_named_point.

void	backtrack ()
	Backtrack to the last marker.

void	backtrack_to_named_point (ID)
	Backtrack, possibly multiple times, to the specified point.

void	reset ()
	Get rid of all the markers used for backtracking.

Private Attributes
vector< Variable * >	vars
	All the variables made, named, unique and anonymous.

vector< Variable * >	cached_vars
	All the cached variables made.

unordered_map< string, Variable * >	name_index
	Fast lookup of Variables by name.

ID	next_index
	Keep track of automatically generated Variable indices.

ID	next_unique_index
	When converting to CNF you need new, unique variables, but they need to be treated separately from anonymous variables.

ID	first_anon_variable
	Set after you've added all the named variables for the problem.

ID	highest_anon_variable
	Keep track of how many anonymous Variables you currently have available.

bool	all_names_added
	Set after you've added all the named variables for the problem.

vector< ID >	backtrack_points
	Backtrack points stored as indices in the vars vector.

Friends
ostream &	operator<< (ostream &out, const VariableIndex &vi)

Detailed Description

Storage of named variables, and management of new, anonymous and unique variables.

Variables are only stored once, and I want backtracking to be easy while recycling old anonymous variables. You should only add named variables once, at the beginning of the process.

You should only make variables using this index. If you do then it takes care of allocation/deallocation for you.

Definition at line 61 of file VariableIndex.hpp.

Constructor & Destructor Documentation

◆ VariableIndex() [1/2]

VariableIndex::VariableIndex ( )

Definition at line 28 of file VariableIndex.cpp.

: vars()
, cached_vars()
, name_index()
, next_index(0)
, next_unique_index(0)
, first_anon_variable(0)
, highest_anon_variable(0)
, all_names_added(false)
, backtrack_points()
{}

◆ ~VariableIndex()

VariableIndex::~VariableIndex ( )

Definition at line 40 of file VariableIndex.cpp.

                              {
    for (size_t i = 0; i < vars.size(); i++)
        delete vars[i];
    for (size_t i = 0; i < cached_vars.size(); i++)
        delete cached_vars[i];
}

◆ VariableIndex() [2/2]

VariableIndex::VariableIndex ( const VariableIndex & )

delete

Copying this would be a very silly idea, so explicitly disallow it.

As usual, let the compiler be your friend.

Member Function Documentation

◆ add_anon_var()

Variable * VariableIndex::add_anon_var ( )

Add an anonymous variable.

Anonymous variables are recycled after backtracking. Also denies addition of new named variables if you didn't do that yourself. Anonymous variables do get names of the form "_next_index" but are not currently included in the map as they can be found by other means if you absolutely need to, which you shouldn't.

Definition at line 76 of file VariableIndex.cpp.

                                      {
    if (!all_names_added) {
        set_all_names_added();
    }
    Variable* new_var = nullptr;
    // You can recycle an anonymous variable that was used 
    // earlier then freed up under backtracking.
    if (next_index <= highest_anon_variable) {
        new_var = vars[next_index++];
        new_var->remove_substitution();
    }
    // You need to actually generate a new anonymous variable.
    else {
        highest_anon_variable = next_index;
        string name("_");
        name += to_string(next_index);
        new_var = new Variable(next_index++, name);
        vars.push_back(new_var);
    }
    return new_var;
}

◆ add_backtrack_point()

void VariableIndex::add_backtrack_point ( )

Add a backtrack point.

This is straightforward. All we have to do is remember a starting point so that all anonymous variables after that can easily be reused.

It is the responsibility of the user to insert and maintain an initial backtrack point at the first anonymous variable.

Definition at line 138 of file VariableIndex.cpp.

                                        {
    backtrack_points.push_back(next_index);
}

◆ add_cached_var()

Variable * VariableIndex::add_cached_var ( )

Cached variables are dealt with separately as there's no need to keep track of them like the others.

Definition at line 105 of file VariableIndex.cpp.

                                        {
    string name(params::unique_var_prefix);
    name += to_string(next_unique_index);
    next_unique_index++;
    Variable* new_var = new Variable(0, name);
    cached_vars.push_back(new_var);
    name_index.insert(MapType(name, new_var));
    return new_var;
}

◆ add_named_backtrack_point()

ID VariableIndex::add_named_backtrack_point ( )

Same as add_backtrack_point, but return an identifier allowing multiple levels of backtracking using backtrack_to_named_point.

Definition at line 142 of file VariableIndex.cpp.

                                            {
    backtrack_points.push_back(next_index);
    return next_index;
}

◆ add_named_var()

Variable * VariableIndex::add_named_var ( const string & name )

Add a variable with the specified name to the index.

Only allow a named variable to be added once, and before any anonymous variables. If you add something twice you'll just get a pointer to the first copy.

Parameters

name	Name of Variable to add.

Definition at line 47 of file VariableIndex.cpp.

                                                         {
    Variable* new_var = nullptr;
    if (!all_names_added) {
        auto i = name_index.find(name);
        if (i == name_index.end()) {
            new_var = new Variable(next_index++, name);
            vars.push_back(new_var);
            name_index.insert(MapType(name, new_var));
        }
        else {
            new_var = i->second;
        }
    }
    else {
        cerr << "You can't add any more named variables." << endl;
    }
    return new_var;
}

◆ add_unique_var()

Variable * VariableIndex::add_unique_var ( )

Add a unique variable when converting to CNF.

These are also used to cache copies of clauses.

Does not immediately deny addition of further named variables.

Definition at line 98 of file VariableIndex.cpp.

                                        {
    string name(params::unique_var_prefix);
    name += to_string(next_unique_index);
    next_unique_index++;
    return add_named_var(name);
}

◆ backtrack()

void VariableIndex::backtrack ( )

Backtrack to the last marker.

This is straightforward. Substitutions do not have to be undone here as that will happen if a variable is reused.

Definition at line 147 of file VariableIndex.cpp.

                              {
    if (backtrack_points.size() > 0) {
        next_index = backtrack_points.back();
        backtrack_points.pop_back();
    }
    else
        cerr << "There's nowhere left to backtrack to." << endl;
}

◆ backtrack_to_named_point()

void VariableIndex::backtrack_to_named_point ( ID id )

Backtrack, possibly multiple times, to the specified point.

Definition at line 156 of file VariableIndex.cpp.

                                                  {
    while (backtrack_points.back() != id) {
        backtrack_points.pop_back();
    }
    next_index = id;
    backtrack_points.pop_back();
}

◆ clear_substitutions()

void VariableIndex::clear_substitutions ( )

Undo all substitutions made, to anything, ever.

Definition at line 71 of file VariableIndex.cpp.

                                        {
  for (size_t i = 0; i < vars.size(); i++)
    vars[i]->remove_substitution();
}

◆ find_variable()

Variable * VariableIndex::find_variable ( const string & var_name )

Look up a variable by name.

Parameters

var_name Name of Variable to find.

Definition at line 115 of file VariableIndex.cpp.

                                                             {
    Variable* var = nullptr;
    istringstream st(var_name);
    char c;
    st >> c;
    if (c == '_') {
        ID id;
        st >> id;
        if (id < next_index)
            var = vars[id];
        else
            cerr << "That anonymous variable doesn't exist" << endl;
    }
    else {
        auto i = name_index.find(var_name);
        if (i != name_index.end())
            var = i->second;
        else
            cerr << "That named variable doesn't exist" << endl;
    }
    return var;
}