ClauseCopyCache.cpp

/*
 
Copyright © 2023-24 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::set_size(size_t _size) {
    size = _size;
    clear();
}
//---------------------------------------------------------------------------
void ClauseCopyCache::make_copy_with_new_variables(
    size_t _index, Clause& _clause, VariableIndex& _vi, TermIndex& _ti) {
    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);
}
//---------------------------------------------------------------------------
void ClauseCopyCache::backtrack() {
    size_t i = stack.back();
    stack.pop_back();
    current_copy_number[i]--;
}
//---------------------------------------------------------------------------
void ClauseCopyCache::clear() {
    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();
}