ClauseCopyCache.cpp

/*
 
Copyright © 2023-25 Sean Holden. All rights reserved.
 
*/
/*
 
This file is part of Connect++.
 
Connect++ is free software: you can redistribute it and/or modify it 
under the terms of the GNU General Public License as published by the 
Free Software Foundation, either version 3 of the License, or (at your 
option) any later version.
 
Connect++ is distributed in the hope that it will be useful, but WITHOUT 
ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or 
FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for 
more details.
 
You should have received a copy of the GNU General Public License along 
with Connect++. If not, see <https://www.gnu.org/licenses/>. 
 
*/
 
#include "ClauseCopyCache.hpp"
 
//---------------------------------------------------------------------------
void ClauseCopyCache::reset(const Matrix& _m, VariableIndex& _vi, TermIndex& _ti) {
    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();
}
//---------------------------------------------------------------------------
void ClauseCopyCache::make_copy_with_new_variables(size_t _index, 
                            Clause& _clause, const Matrix& _m, VariableIndex& _vi, 
                            TermIndex& _ti) {
    _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);
        }
    }
} 
//---------------------------------------------------------------------------
void ClauseCopyCache::backtrack() {
    size_t i = stack.back();
    stack.pop_back();
    next_copy_index[i]--;
}
//---------------------------------------------------------------------------
void ClauseCopyCache::show_counts() const {
    cout << "|";
    for (size_t count : number_of_copies_available) {
        cout << count << "|";
    }
    cout << endl;
}
//---------------------------------------------------------------------------
ostream& operator<<(ostream& out, const ClauseCopyCache& _cache) {
    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;
}