ClauseCopyCache Class Reference

Collaboration diagram for ClauseCopyCache:

Public Member Functions
	ClauseCopyCache ()
	You probably don't know the size at the point when this needs to be constructed.
	ClauseCopyCache (size_t _size)
	This is the only constructor that makes sense if you know the size.
void	set_size (size_t)
	You probably don't know the size at the point when this needs to be constructed.
void	make_copy_with_new_variables (size_t, Clause &, VariableIndex &, TermIndex &)
	If there is a copy cached, replace the parameter with it. Otherwise, use the parameter to actually make a copy, then add it to the cache and return it in the same way.
void	backtrack ()
	Backtracking is just looking at the last copy supplied and undoing that action.
void	clear ()
	We will sometimes need to clear the cache and start again because of reordering operations on the matrix.

Private Attributes
vector< vector< Clause > >	cache
	Cache containing some number of copies (with unique variables, not used anywhere else) of clauses from the matrix.
size_t	size
	Keep track of how many clauses there are in the matrix.
vector< size_t >	number_of_copies_available
	How many copies of each clause, in total, are currently available? At any given time some may be available immediately. Anything beyond this requires an actual new copy to be made.
vector< size_t >	current_copy_number
	When 0, there are no copies available. When 1, the last copy we used is the one at index 0, and so on.
vector< size_t >	stack
	Each time you supply a copy, remember the action so that you can backtrack.

Detailed Description

Definition at line 40 of file ClauseCopyCache.hpp.

Constructor & Destructor Documentation

ClauseCopyCache() [1/2]

ClauseCopyCache::ClauseCopyCache ( )

inline

You probably don't know the size at the point when this needs to be constructed.

Definition at line 77 of file ClauseCopyCache.hpp.

    : size(0)
    , cache()
    , number_of_copies_available()
    , current_copy_number()
    , stack()
    {}

ClauseCopyCache() [2/2]

ClauseCopyCache::ClauseCopyCache ( size_t _size )

inline

This is the only constructor that makes sense if you know the size.

Definition at line 88 of file ClauseCopyCache.hpp.

    : size(_size)
    , cache(_size, vector<Clause>())
    , number_of_copies_available(_size, 0)
    , current_copy_number(_size, 0)
    , stack()
    {}

Member Function Documentation

backtrack()

void ClauseCopyCache::backtrack

(

)

Backtracking is just looking at the last copy supplied and undoing that action.

Definition at line 48 of file ClauseCopyCache.cpp.

                                {
    size_t i = stack.back();
    stack.pop_back();
    current_copy_number[i]--;
}

clear()

void ClauseCopyCache::clear

(

)

We will sometimes need to clear the cache and start again because of reordering operations on the matrix.

Definition at line 54 of file ClauseCopyCache.cpp.

                            {
    cache = vector<vector<Clause>>(size, vector<Clause>());
    number_of_copies_available = vector<size_t>(size, 0);
    current_copy_number = vector<size_t>(size, 0);
    stack.clear();
}

make_copy_with_new_variables()

void ClauseCopyCache::make_copy_with_new_variables	(	size_t	_index,
		Clause &	_clause,
		VariableIndex &	_vi,
		TermIndex &	_ti )

If there is a copy cached, replace the parameter with it. Otherwise, use the parameter to actually make a copy, then add it to the cache and return it in the same way.

Parameters

_index	Index of the clause in the matrix.
_clause	Clause you want a copy of.
_vi	Reference to the variable index.
_ti	Reference to the term index.

Definition at line 33 of file ClauseCopyCache.cpp.

                                                                        {
    size_t n = current_copy_number[_index];
    if (n < number_of_copies_available[_index]) {
        _clause = (cache[_index])[n];
    }
    else {
        // _clause = Make an actual copy
        cache[_index].push_back(_clause);
        number_of_copies_available[_index]++;
    }
    current_copy_number[_index]++;
    stack.push_back(_index);
}

set_size()

void ClauseCopyCache::set_size

(

size_t

_size

)

You probably don't know the size at the point when this needs to be constructed.

Definition at line 28 of file ClauseCopyCache.cpp.

                                           {
    size = _size;
    clear();
}

Member Data Documentation

cache

vector<vector<Clause> > ClauseCopyCache::cache

private

Cache containing some number of copies (with unique variables, not used anywhere else) of clauses from the matrix.

Definition at line 47 of file ClauseCopyCache.hpp.

current_copy_number

vector<size_t> ClauseCopyCache::current_copy_number

private

When 0, there are no copies available. When 1, the last copy we used is the one at index 0, and so on.

Definition at line 66 of file ClauseCopyCache.hpp.

number_of_copies_available

vector<size_t> ClauseCopyCache::number_of_copies_available

private

How many copies of each clause, in total, are currently available? At any given time some may be available immediately. Anything beyond this requires an actual new copy to be made.

Definition at line 60 of file ClauseCopyCache.hpp.

size

size_t ClauseCopyCache::size

private

Keep track of how many clauses there are in the matrix.

Definition at line 52 of file ClauseCopyCache.hpp.

stack

vector<size_t> ClauseCopyCache::stack

private

Each time you supply a copy, remember the action so that you can backtrack.

Definition at line 71 of file ClauseCopyCache.hpp.

---

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

• /Users/sbh11/Desktop/connection-prover/c++/connect++/source/ClauseCopyCache.hpp
• /Users/sbh11/Desktop/connection-prover/c++/connect++/source/ClauseCopyCache.cpp