1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
|
/***********************************************************************
CryptoMiniSat -- Copyright (c) 2009 Mate Soos
This program 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.
This program 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 this program. If not, see <http://www.gnu.org/licenses/>.
************************************************************************/
#ifndef CLAUSEALLOCATOR_H
#define CLAUSEALLOCATOR_H
#ifdef _MSC_VER
#include <msvc/stdint.h>
#else
#include <stdint.h>
#endif //_MSC_VER
#include <stdlib.h>
#include "Vec.h"
#include <map>
#include <vector>
#include "ClauseOffset.h"
#include "Watched.h"
#define NUM_BITS_OUTER_OFFSET 4
#define BASE_DATA_TYPE char
namespace CMSat {
using std::map;
using std::vector;
class Clause;
class XorClause;
class Solver;
/**
@brief Allocates memory for (xor) clauses
This class allocates memory in large chunks, then distributes it to clauses when
needed. When instructed, it consolidates the unused space (i.e. clauses free()-ed).
Essentially, it is a stack-like allocator for clauses. It is useful to have
this, because this way, we can address clauses according to their number,
which is 32-bit, instead of their address, which might be 64-bit
*/
class ClauseAllocator {
public:
ClauseAllocator();
~ClauseAllocator();
template<class T>
Clause* Clause_new(const T& ps, const bool learnt = false);
template<class T>
XorClause* XorClause_new(const T& ps, const bool xorEqualFalse);
Clause* Clause_new(Clause& c);
ClauseOffset getOffset(const Clause* ptr) const;
/**
@brief Returns the pointer of a clause given its offset
Takes the "dataStart" of the correct stack, and adds the offset,
returning the thus created pointer. Used a LOT in propagation, thus this
is very important to be fast (therefore, it is an inlined method)
*/
inline Clause* getPointer(const uint32_t offset) const
{
return (Clause*)(dataStarts[offset&((1 << NUM_BITS_OUTER_OFFSET) - 1)]
+(offset >> NUM_BITS_OUTER_OFFSET));
}
void clauseFree(Clause* c);
void consolidate(Solver* solver, const bool force = false) throw (std::bad_alloc);
uint32_t getNewClauseNum();
private:
uint32_t getOuterOffset(const Clause* c) const;
uint32_t getInterOffset(const Clause* c, const uint32_t outerOffset) const;
ClauseOffset combineOuterInterOffsets(const uint32_t outerOffset, const uint32_t interOffset) const;
void updateAllOffsetsAndPointers(Solver* solver);
template<class T>
void updatePointers(vec<T*>& toUpdate);
void updatePointers(vector<Clause*>& toUpdate);
void updatePointers(vector<XorClause*>& toUpdate);
void updatePointers(vector<std::pair<Clause*, uint32_t> >& toUpdate);
void updateOffsets(vec<vec<Watched> >& watches);
void checkGoodPropBy(const Solver* solver);
void releaseClauseNum(const uint32_t num);
vec<BASE_DATA_TYPE*> dataStarts; ///<Stacks start at these positions
vec<size_t> sizes; ///<The number of 32-bit datapieces currently used in each stack
/**
@brief Clauses in the stack had this size when they were allocated
This my NOT be their current size: the clauses may be shrinked during
the running of the solver. Therefore, it is imperative that their orignal
size is saved. This way, we can later move clauses around.
*/
vec<vec<uint32_t> > origClauseSizes;
vec<size_t> maxSizes; ///<The number of 32-bit datapieces allocated in each stack
/**
@brief The estimated used size of the stack
This is incremented by clauseSize each time a clause is allocated, and
decremetented by clauseSize each time a clause is deallocated. The
problem is, that clauses can shrink, and thus this value will be an
overestimation almost all the time
*/
vec<size_t> currentlyUsedSizes;
void* allocEnough(const uint32_t size) throw (std::bad_alloc);
/**
@brief The clause's data is replaced by this to aid updating
We need to update the pointer or offset that points to the clause
The best way to do that is to simply fill the original place of the clause
with the pointer/offset of the new location.
*/
struct NewPointerAndOffset
{
uint32_t newOffset; ///<The new offset where the clause now resides
Clause* newPointer; ///<The new place
};
vector<Clause*> otherClauses;
vector<Clause*> threeLongClauses;
Clause* getClause();
void putClausesIntoDatastruct(std::vector<Clause*>& clauses);
};
}
#endif //CLAUSEALLOCATOR_H
|
