Skip to content

Commit ac301bc

Browse files
muhosmuhos
committed
fixed incremental solving allocation
1 parent 367f0ce commit ac301bc

9 files changed

Lines changed: 79 additions & 49 deletions

File tree

‎.gitignore‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,7 @@ src/cpu/version.h
88
src/gpu/version.hpp
99
src/cpu/Makefile
1010
src/gpu/Makefile
11+
src_backup
1112
build
1213
.vscode
1314
*.cnf

‎src/gpu/assume.cpp‎

Lines changed: 17 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -48,13 +48,8 @@ uint32 Solver::iadd() {
4848
LOG2(3, " adding new variable %d (%d unassigned)..", v, inf.unassigned);
4949
const uint32 lit = V2L(v);
5050
inf.maxDualVars = lit + 2;
51+
// Expanding non-SP structures.
5152
wt.expand(lit + 2);
52-
ivalue.expand(lit + 2, UNDEFINED);
53-
ilevel.expand(v + 1, UNDEFINED);
54-
iphase.expand(v + 1, opts.polarity);
55-
isource.expand(v + 1, NOREF);
56-
ivstate.expand(v + 1);
57-
ivstate[v] = VSTATE();
5853
ifrozen.expand(v + 1, 0);
5954
bumps.expand(v + 1, 0);
6055
activity.expand(v + 1, 0.0);
@@ -71,11 +66,20 @@ uint32 Solver::iadd() {
7166
if (opts.proof_en)
7267
proof.init(sp);
7368
}
74-
sp->value = ivalue;
75-
sp->level = ilevel;
76-
sp->source = isource;
77-
sp->vstate = ivstate;
78-
sp->psaved = iphase;
69+
if (!sp->selfallocated) {
70+
// Build mode: expanding SP structures the rebind.
71+
ivalue.expand(lit + 2, UNDEFINED);
72+
ilevel.expand(v + 1, UNDEFINED);
73+
iphase.expand(v + 1, opts.polarity);
74+
isource.expand(v + 1, NOREF);
75+
ivstate.expand(v + 1);
76+
ivstate[v] = VSTATE();
77+
sp->value = ivalue;
78+
sp->level = ilevel;
79+
sp->source = isource;
80+
sp->vstate = ivstate;
81+
sp->psaved = iphase;
82+
}
7983
return v;
8084
}
8185

@@ -105,7 +109,7 @@ bool Solver::itoClause(Lits_t& c, Lits_t& org) {
105109
uint32 mvar = ABS(mlit);
106110
mlit = V2DEC(mvar, sign);
107111
PRINT2(3, 5, "%d ", SIGN(mlit) ? -int(mvar) : int(mvar));
108-
LIT_ST val = ivalue[mlit];
112+
LIT_ST val = sp->value[mlit];
109113
if (UNASSIGNED(val))
110114
c.push(mlit);
111115
else if (val)
@@ -130,7 +134,7 @@ bool Solver::itoClause(Lits_t& c, Lits_t& org) {
130134
} else if (newsize == 1) {
131135
const uint32 unit = *c;
132136
CHECKLIT(unit);
133-
LIT_ST val = ivalue[unit];
137+
LIT_ST val = sp->value[unit];
134138
if (UNASSIGNED(val))
135139
enqueueUnit(unit), formula.units++;
136140
else if (!val) {

‎src/gpu/malloc.hpp‎

Lines changed: 8 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -28,16 +28,20 @@ namespace ParaFROST {
2828

2929
class MEMOUTEXCEPTION {};
3030

31+
inline std::size_t align_up(const size_t& n, const size_t& a) {
32+
return (n + (a - 1)) & ~(a - 1);
33+
}
34+
3135
template <class T>
32-
T* pfmalloc(size_t numElements) {
36+
T* pfmalloc(const size_t& numElements) {
3337
if (!numElements) LOGERROR("catched zero-memory size at %s", __func__);
3438
T* _mem = (T*)std::malloc(numElements * sizeof(T));
3539
if (_mem == NULL) throw MEMOUTEXCEPTION();
3640
return _mem;
3741
}
3842

3943
template <class T>
40-
T* pfcalloc(size_t numElements) {
44+
T* pfcalloc(const size_t& numElements) {
4145
if (!numElements) LOGERROR("catched zero-memory size at %s", __func__);
4246
T* _mem = (T*)std::calloc(numElements, sizeof(T));
4347
if (_mem == NULL) throw MEMOUTEXCEPTION();
@@ -50,15 +54,15 @@ namespace ParaFROST {
5054
#endif
5155

5256
template <class T>
53-
void pfralloc(T*& mem, size_t bytes) {
57+
void pfralloc(T*& mem, const size_t& bytes) {
5458
if (!bytes) LOGERROR("catched zero-memory size at %s", __func__);
5559
T* _mem = (T*)std::realloc(mem, bytes);
5660
if (_mem == NULL) throw MEMOUTEXCEPTION();
5761
mem = _mem;
5862
}
5963

6064
template <class T>
61-
void pfshrinkAlloc(T*& mem, size_t bytes) {
65+
void pfshrinkAlloc(T*& mem, const size_t& bytes) {
6266
if (!bytes) LOGERROR("catched zero-memory size at %s", __func__);
6367
T* _mem = NULL;
6468
_mem = (T*)std::realloc(_mem, bytes);

‎src/gpu/solver.cpp‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -122,8 +122,7 @@ void Solver::allocSolver()
122122
assert(sp == NULL);
123123
const uint32 maxSize = inf.maxVar + 1;
124124
const C_REF initcap = inf.orgCls * sizeof(CLAUSE) + maxSize;
125-
sp = new SP(maxSize);
126-
sp->initSaved(opts.polarity);
125+
sp = new SP(maxSize, opts.polarity);
127126
cm.init(initcap);
128127
wt.resize(inf.maxDualVars);
129128
trail.reserve(inf.maxVar);

‎src/gpu/solver.hpp‎

Lines changed: 14 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -64,7 +64,9 @@ namespace ParaFROST {
6464
LAST last;
6565
STATS stats;
6666
SLEEP sleep;
67-
BCNF orgs, learnts, reduced;
67+
BCNF orgs;
68+
BCNF learnts;
69+
BCNF reduced;
6870
VMAP vmap;
6971
Lits_t learntC;
7072
CLAUSE subbin;
@@ -79,22 +81,28 @@ namespace ParaFROST {
7981
Vec<WOL> wot;
8082
Vec<BOL> bot;
8183
Vec1D lbdlevels;
82-
uVec1D vorg, vhist;
84+
uVec1D vorg;
85+
uVec1D vhist;
8386
uVec1D eligible;
8487
uVec1D probes;
8588
uVec1D dlevels;
8689
uVec1D trail;
87-
uVec1D analyzed, minimized;
90+
uVec1D analyzed;
91+
uVec1D minimized;
8892
LBDREST lbdrest;
8993
LUBYREST lubyrest;
9094
RANDOM random;
9195
WALK tracker;
9296
uint64 bumped;
93-
C_REF conflict, ignore;
97+
C_REF conflict;
98+
C_REF ignore;
9499
size_t solLineLen;
95100
string solLine;
96101
CNFState cnfstate;
97-
bool intr, stable, probed, incremental;
102+
bool intr;
103+
bool stable;
104+
bool probed;
105+
bool incremental;
98106

99107
public:
100108
OPTION opts;
@@ -816,6 +824,7 @@ namespace ParaFROST {
816824
Vec<C_REF> isource;
817825
Vec1D ilevel;
818826
Lits_t assumptions, iconflict;
827+
819828
public:
820829
void* termCallbackState;
821830
void* learnCallbackState;

‎src/gpu/solverinc.cpp‎

Lines changed: 15 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -44,28 +44,30 @@ void Solver::iallocSpace()
4444
if (sp->size() == size_t(inf.maxVar) + 1) return; // avoid allocation if 'maxVar' didn't change
4545
assert(inf.maxVar);
4646
LOGN2(2, " Allocating fixed memory for %d variables..", inf.maxVar);
47+
const size_t newsize = size_t(inf.maxVar) + 1;
4748
assert(inf.orgVars == inf.maxVar);
48-
assert(vorg.size() == inf.maxVar + 1);
49-
assert(V2L(inf.maxVar + 1) == inf.maxDualVars);
50-
assert(model.lits.size() == inf.maxVar + 1);
51-
assert(ilevel.size() == ivstate.size());
52-
assert(ilevel.size() == inf.maxVar + 1);
49+
assert(vorg.size() == newsize);
50+
assert(V2L(newsize) == inf.maxDualVars);
51+
assert(model.lits.size() == newsize);
5352
assert(imarks.empty());
5453
inf.orgCls = orgs.size();
5554
vorg[0] = 0;
5655
model.lits[0] = 0;
5756
model.init(vorg);
58-
SP* newSP = new SP(inf.maxVar + 1);
57+
// Fixed mode: SP grows its own memory.
58+
SP* newSP = new SP(newsize, opts.polarity);
5959
newSP->copyFrom(sp);
60-
delete sp;
61-
sp = newSP;
60+
if (!newSP->selfallocated) {
61+
ilevel.clear(true);
62+
ivalue.clear(true);
63+
iphase.clear(true);
64+
isource.clear(true);
65+
ivstate.clear(true);
66+
newSP->selfallocated = true;
67+
}
68+
delete sp, sp = newSP;
6269
if (opts.proof_en)
6370
proof.init(sp, vorg);
64-
ilevel.clear(true);
65-
ivalue.clear(true);
66-
iphase.clear(true);
67-
isource.clear(true);
68-
ivstate.clear(true);
6971
LOGDONE(2, 5);
7072
LOGMEMCALL(this, 2);
7173
}

‎src/gpu/space.hpp‎

Lines changed: 19 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -56,9 +56,10 @@ namespace ParaFROST {
5656
uint32 trailpivot;
5757
uint32 simplified;
5858
uint32 propagated;
59+
bool selfallocated;
5960
//================
60-
SP() { RESETSTRUCT(this); }
61-
SP(const uint32& size)
61+
SP () { RESETSTRUCT(this); }
62+
explicit SP (const size_t& size, const LIT_ST& pol)
6263
{
6364
RESETSTRUCT(this);
6465
assert(sizeof(C_REF) == sizeof(uint64));
@@ -69,7 +70,7 @@ namespace ParaFROST {
6970
_sz = size;
7071
_cap = vec1Bytes + vec4Bytes + vec8Bytes;
7172
assert(_cap);
72-
pfralloc(_mem, _cap);
73+
pfralloc(_mem, align_up(_cap, 64));
7374
assert(_mem != NULL);
7475
memset(_mem, 0, _cap);
7576
// 8-byte arrays
@@ -93,22 +94,24 @@ namespace ParaFROST {
9394
memset(marks, UNDEFINED, _sz);
9495
memset(ptarget, UNDEFINED, _sz);
9596
memset(pbest, UNDEFINED, _sz);
97+
memset(psaved, pol, _sz);
9698
forall_space(v) {
9799
level[v] = UNDEFINED;
98100
source[v] = NOREF;
99101
}
102+
selfallocated = true;
100103
}
101104
size_t size () const { return _sz; }
102105
size_t capacity () const { return _cap; }
103-
void initSaved (const LIT_ST& pol) {
104-
memset(psaved, pol, _sz);
105-
}
106+
// Assume memory is already allocated and initialized properly.
106107
void copyFrom (SP* src)
107108
{
109+
assert(src->size() <= _sz);
110+
selfallocated = src->selfallocated;
108111
propagated = src->propagated;
109112
trailpivot = src->trailpivot;
110113
simplified = src->simplified;
111-
forall_space(v) {
114+
for (size_t v = 1; v < src->size(); v++) {
112115
const uint32 p = V2L(v), n = NEG(p);
113116
value[p] = src->value[p];
114117
value[n] = src->value[n];
@@ -118,6 +121,14 @@ namespace ParaFROST {
118121
psaved[v] = src->psaved[v];
119122
}
120123
}
124+
void printPhases () {
125+
LOGN1(" Phases->[");
126+
forall_space(v) {
127+
PRINT("%5d:%d ", v, psaved[v]);
128+
breakline(v);
129+
}
130+
putc(']', stdout), PUTCH('\n');
131+
}
121132
void printStates () {
122133
LOGN1(" States->[");
123134
forall_space(v) {
@@ -144,7 +155,7 @@ namespace ParaFROST {
144155
putc(']', stdout), PUTCH('\n');
145156
}
146157
void clearSubsume() { forall_space(v) vstate[v].subsume = 0; }
147-
void destroy () { if (_mem != NULL) std::free(_mem); }
158+
void destroy () { if (_mem != NULL) std::free(_mem); _mem = NULL; }
148159
~SP () { destroy(); }
149160
};
150161
}

‎src/gpu/vector.hpp‎

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -159,12 +159,12 @@ namespace ParaFROST {
159159
cap = sz;
160160
}
161161
}
162-
__forceinline void copyFrom (Vec<T, S>& copy) {
162+
__forceinline void copyFrom (const Vec<T, S>& copy) {
163163
resize(copy.size());
164-
std::memcpy(_mem, copy, sz * sizeof(T));
164+
std::memcpy(_mem, copy.data(), sz * sizeof(T));
165165
}
166166
template<class SS = uint32>
167-
__forceinline void copyFrom (T* copy, const SS& copy_sz) {
167+
__forceinline void copyFrom (const T* copy, const SS& copy_sz) {
168168
assert(copy_sz <= sz);
169169
std::memcpy(_mem, copy, sz * sizeof(T));
170170
}

‎src/gpu/vmap.cpp‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -112,7 +112,7 @@ void Solver::map(const bool& sigmified)
112112
vmap.mapShrinkVars(activity);
113113
vsids.rebuild(tmp);
114114
// map search space
115-
SP* newSP = new SP(vmap.size());
115+
SP* newSP = new SP(vmap.size(), opts.polarity);
116116
vmap.mapSP(newSP);
117117
delete sp;
118118
sp = newSP;

0 commit comments

Comments
 (0)