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.
void	set_size (size_t _s)
	Set the number of clauses we need cached copies for.
void	reset (const Matrix &, VariableIndex &, TermIndex &)
	This is for any actual initialisation, when you either (1) intially know what you're dealing with, or (2) need to restart after something like a re-ordering of the matrix.
void	make_copy_with_new_variables (size_t, Clause &, const Matrix &, 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	show_counts () const
	Mostly for development. See how many copies you actually ended up with.

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 >	next_copy_index
	Index of the next available copy of each clause.
vector< size_t >	stack
	Each time you supply a copy, remember the action so that you can backtrack.

Friends
ostream &	operator<< (ostream &out, const ClauseCopyCache &_cache)

Detailed Description

Definition at line 40 of file ClauseCopyCache.hpp.

Constructor & Destructor Documentation

ClauseCopyCache()

ClauseCopyCache::ClauseCopyCache ( )

inline

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

Definition at line 75 of file ClauseCopyCache.hpp.

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

Member Function Documentation

backtrack()

void ClauseCopyCache::backtrack

(

)

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

Definition at line 61 of file ClauseCopyCache.cpp.

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

make_copy_with_new_variables()

void ClauseCopyCache::make_copy_with_new_variables	(	size_t	_index,
		Clause &	_clause,
		const Matrix &	_m,
		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.
_m	Reference to the actual matrix.
_vi	Reference to the variable index.
_ti	Reference to the term index.

Definition at line 46 of file ClauseCopyCache.cpp.

                                            {
    _clause = (cache[_index])[next_copy_index[_index]++]; 
    stack.push_back(_index); 
    if (next_copy_index[_index] == number_of_copies_available[_index]) {
        number_of_copies_available[_index] += params::clause_copy_cache_increment;
        Clause new_c;
        for (size_t i = 0; i < params::clause_copy_cache_increment; i++) {
            _m.make_copy_with_new_unique_vars(_index, new_c, _vi, _ti);
            cache[_index].push_back(new_c);
        }
    }
} 

reset()

void ClauseCopyCache::reset	(	const Matrix &	_m,
		VariableIndex &	_vi,
		TermIndex &	_ti )

This is for any actual initialisation, when you either (1) intially know what you're dealing with, or (2) need to restart after something like a re-ordering of the matrix.

Parameters

_m	Reference to the actual matrix.
_vi	Reference to variable index.
_ti	Reference to term index.

Definition at line 28 of file ClauseCopyCache.cpp.

                                                                                {
    if (params::clause_copy_cache_start_size < 1) {
        cerr << "params::clause_copy_cache_start_size must be at least 1" << endl;
        exit(EXIT_FAILURE);
    }
    cache = vector<vector<Clause>>(size, vector<Clause>());
    Clause new_c;
    for (size_t i = 0; i < size; i++) {
        for (size_t j = 0; j < params::clause_copy_cache_start_size; j++) {
          _m.make_copy_with_new_unique_vars(i, new_c, _vi, _ti);
          cache[i].push_back(new_c);
        }
    }
    number_of_copies_available = vector<size_t>(size, params::clause_copy_cache_start_size);
    next_copy_index = vector<size_t>(size, 0);
    stack.clear();
}

set_size()

void ClauseCopyCache::set_size ( size_t _s )

inline

Set the number of clauses we need cached copies for.

Definition at line 85 of file ClauseCopyCache.hpp.

{ size = _s; }

show_counts()

void ClauseCopyCache::show_counts

(

)

const

Mostly for development. See how many copies you actually ended up with.

Definition at line 67 of file ClauseCopyCache.cpp.

                                        {
    cout << "|";
    for (size_t count : number_of_copies_available) {
        cout << count << "|";
    }
    cout << endl;
}

Friends And Related Symbol Documentation

operator<<

ostream & operator<< ( ostream & out, const ClauseCopyCache & _cache )

friend

Definition at line 75 of file ClauseCopyCache.cpp.

                                                                 {
    size_t i = 0;
    for (const vector<Clause>& vc : _cache.cache) {
        out << "---------------------------------------------------------------" << endl;
        out << "Cached clauses for clause: " << i << endl;
        out << "Copies available: " << _cache.number_of_copies_available[i] << endl;
        out << "---------------------------------------------------------------" << endl;
        size_t j = 0;
        for (const Clause& c : vc) {
            out << c;
            if (j++ == _cache.next_copy_index[i]) {
                out << " <-";
            }
            out << endl;
        }
        i++;
    }
    return out;
}

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.

next_copy_index

vector<size_t> ClauseCopyCache::next_copy_index

private

Index of the next available copy of each clause.

Definition at line 64 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 69 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