Connect++ 0.6.0
A fast, readable connection prover for first-order logic.
Loading...
Searching...
No Matches
ClauseCopyCache.hpp
1/*
2
3Copyright © 2023-24 Sean Holden. All rights reserved.
4
5*/
6/*
7
8This file is part of Connect++.
9
10Connect++ is free software: you can redistribute it and/or modify it
11under the terms of the GNU General Public License as published by the
12Free Software Foundation, either version 3 of the License, or (at your
13option) any later version.
14
15Connect++ is distributed in the hope that it will be useful, but WITHOUT
16ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or
17FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for
18more details.
19
20You should have received a copy of the GNU General Public License along
21with Connect++. If not, see <https://www.gnu.org/licenses/>.
22
23*/
24
25#ifndef CLAUSECOPYCACHE_HPP
26#define CLAUSECOPYCACHE_HPP
27
28#include<iostream>
29#include<string>
30#include<vector>
31
32#include "Clause.hpp"
33
34using std::vector;
35using std::string;
36using std::ostream;
37using std::endl;
38using std::cout;
39
40class ClauseCopyCache {
41private:
47 vector<vector<Clause>> cache;
52 size_t size;
60 vector<size_t> number_of_copies_available;
66 vector<size_t> current_copy_number;
71 vector<size_t> stack;
72public:
88 ClauseCopyCache(size_t _size)
89 : size(_size)
90 , cache(_size, vector<Clause>())
91 , number_of_copies_available(_size, 0)
92 , current_copy_number(_size, 0)
93 , stack()
94 {}
99 void set_size(size_t);
111 void make_copy_with_new_variables(size_t, Clause&, VariableIndex&, TermIndex&);
116 void backtrack();
122 void clear();
123};
124
125#endif
ClauseCopyCache::set_size
void set_size(size_t)
You probably don't know the size at the point when this needs to be constructed.
Definition ClauseCopyCache.cpp:28
ClauseCopyCache::cache
vector< vector< Clause > > cache
Cache containing some number of copies (with unique variables, not used anywhere else) of clauses fro...
Definition ClauseCopyCache.hpp:47
ClauseCopyCache::stack
vector< size_t > stack
Each time you supply a copy, remember the action so that you can backtrack.
Definition ClauseCopyCache.hpp:71
ClauseCopyCache::clear
void clear()
We will sometimes need to clear the cache and start again because of reordering operations on the mat...
Definition ClauseCopyCache.cpp:54
ClauseCopyCache::make_copy_with_new_variables
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 ma...
Definition ClauseCopyCache.cpp:33
ClauseCopyCache::backtrack
void backtrack()
Backtracking is just looking at the last copy supplied and undoing that action.
Definition ClauseCopyCache.cpp:48
ClauseCopyCache::current_copy_number
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,...
Definition ClauseCopyCache.hpp:66
ClauseCopyCache::ClauseCopyCache
ClauseCopyCache()
You probably don't know the size at the point when this needs to be constructed.
Definition ClauseCopyCache.hpp:77
ClauseCopyCache::number_of_copies_available
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 avai...
Definition ClauseCopyCache.hpp:60
ClauseCopyCache::size
size_t size
Keep track of how many clauses there are in the matrix.
Definition ClauseCopyCache.hpp:52
ClauseCopyCache::ClauseCopyCache
ClauseCopyCache(size_t _size)
This is the only constructor that makes sense if you know the size.
Definition ClauseCopyCache.hpp:88
Clause
Representation of clauses.
Definition Clause.hpp:52
TermIndex
Look after terms, using hash consing to avoid storing copies of terms.
Definition TermIndex.hpp:54
VariableIndex
Storage of named variables, and management of new, anonymous and unique variables.
Definition VariableIndex.hpp:61