ClauseCopyCache.hpp

/*
 
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/>. 
 
*/
 
#ifndef CLAUSECOPYCACHE_HPP
#define CLAUSECOPYCACHE_HPP
 
#include<iostream>
#include<string>
#include<vector>
 
#include "Matrix.hpp"
 
using std::vector;
using std::string;
using std::ostream;
using std::endl;
using std::cout;
 
class ClauseCopyCache {
private:
    vector<vector<Clause>> cache;
    size_t size;
    vector<size_t> number_of_copies_available;
    vector<size_t> next_copy_index;
    vector<size_t> stack;
public:
    ClauseCopyCache()
    : size(0)
    , cache()
    , number_of_copies_available()
    , next_copy_index()
    , stack()
    {}
    inline void set_size(size_t _s) { size = _s; }
    void reset(const Matrix&, VariableIndex&, TermIndex&);
    void make_copy_with_new_variables(size_t, Clause&, const Matrix&, VariableIndex&, TermIndex&);
    void backtrack();
    void show_counts() const;
 
    friend ostream& operator<<(ostream&, const ClauseCopyCache&);
};
 
#endif