ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
rrrBddManager.h
Go to the documentation of this file.
1#pragma once
2
3#include <cstdlib>
4#include <limits>
5#include <vector>
6#include <iostream>
7#include <iomanip>
8#include <cmath>
9
10ABC_NAMESPACE_CXX_HEADER_START
11
12namespace rrr {
13namespace NewBdd {
14
15 typedef unsigned short var;
16 typedef int bvar;
17 typedef unsigned lit;
18 typedef unsigned short ref;
19 typedef unsigned long long size;
20 typedef unsigned edge;
21 typedef unsigned uniq;
22 typedef unsigned cac;
23 static inline var VarMax() { return std::numeric_limits<var>::max(); }
24 static inline bvar BvarMax() { return std::numeric_limits<bvar>::max(); }
25 static inline lit LitMax() { return std::numeric_limits<lit>::max(); }
26 static inline ref RefMax() { return std::numeric_limits<ref>::max(); }
27 static inline size SizeMax() { return std::numeric_limits<size>::max(); }
28 static inline uniq UniqHash(lit Arg0, lit Arg1) { return Arg0 + 4256249 * Arg1; }
29 static inline cac CacHash(lit Arg0, lit Arg1) { return Arg0 + 4256249 * Arg1; }
30
31 static inline void fatal_error(const char* message) {
32 std::cerr << message << std::endl;
33 std::abort();
34 }
35
36 class Cache {
37 private:
38 cac nSize;
39 cac nMax;
40 cac Mask;
41 size nLookups;
42 size nHits;
43 size nThold;
44 double HitRate;
45 int nVerbose;
46 std::vector<lit> vCache;
47
48 public:
49 Cache(int nCacheSizeLog, int nCacheMaxLog, int nVerbose): nVerbose(nVerbose) {
50 if(nCacheMaxLog < nCacheSizeLog)
51 fatal_error("nCacheMax must not be smaller than nCacheSize");
52 nMax = (cac)1 << nCacheMaxLog;
53 if(!(nMax << 1))
54 fatal_error("Memout (nCacheMax) in init");
55 nSize = (cac)1 << nCacheSizeLog;
56 if(nVerbose)
57 std::cout << "Allocating " << nSize << " cache entries" << std::endl;
58 vCache.resize(nSize * 3);
59 Mask = nSize - 1;
60 nLookups = 0;
61 nHits = 0;
62 nThold = (nSize == nMax)? SizeMax(): nSize;
63 HitRate = 1;
64 }
65 ~Cache() {
66 if(nVerbose)
67 std::cout << "Free " << nSize << " cache entries" << std::endl;
68 }
69 inline lit Lookup(lit x, lit y) {
70 nLookups++;
71 if(nLookups > nThold) {
72 double NewHitRate = (double)nHits / nLookups;
73 if(nVerbose >= 2)
74 std::cout << "Cache Hits: " << std::setw(10) << nHits << ", "
75 << "Lookups: " << std::setw(10) << nLookups << ", "
76 << "Rate: " << std::setw(10) << NewHitRate
77 << std::endl;
78 if(NewHitRate > HitRate)
79 Resize();
80 if(nSize == nMax)
81 nThold = SizeMax();
82 else {
83 nThold <<= 1;
84 if(!nThold)
85 nThold = SizeMax();
86 }
87 HitRate = NewHitRate;
88 }
89 cac i = (CacHash(x, y) & Mask) * 3;
90 if(vCache[i] == x && vCache[i + 1] == y) {
91 if(nVerbose >= 3)
92 std::cout << "Cache hit: "
93 << "x = " << std::setw(10) << x << ", "
94 << "y = " << std::setw(10) << y << ", "
95 << "z = " << std::setw(10) << vCache[i + 2] << ", "
96 << "hash = " << std::hex << (CacHash(x, y) & Mask) << std::dec
97 << std::endl;
98 nHits++;
99 return vCache[i + 2];
100 }
101 return LitMax();
102 }
103 inline void Insert(lit x, lit y, lit z) {
104 cac i = (CacHash(x, y) & Mask) * 3;
105 vCache[i] = x;
106 vCache[i + 1] = y;
107 vCache[i + 2] = z;
108 if(nVerbose >= 3)
109 std::cout << "Cache ent: "
110 << "x = " << std::setw(10) << x << ", "
111 << "y = " << std::setw(10) << y << ", "
112 << "z = " << std::setw(10) << z << ", "
113 << "hash = " << std::hex << (CacHash(x, y) & Mask) << std::dec
114 << std::endl;
115 }
116 inline void Clear() {
117 std::fill(vCache.begin(), vCache.end(), 0);
118 }
119 void Resize() {
120 cac nSizeOld = nSize;
121 nSize <<= 1;
122 if(nVerbose >= 2)
123 std::cout << "Reallocating " << nSize << " cache entries" << std::endl;
124 vCache.resize(nSize * 3);
125 Mask = nSize - 1;
126 for(cac j = 0; j < nSizeOld; j++) {
127 cac i = j * 3;
128 if(vCache[i] || vCache[i + 1]) {
129 cac hash = (CacHash(vCache[i], vCache[i + 1]) & Mask) * 3;
130 vCache[hash] = vCache[i];
131 vCache[hash + 1] = vCache[i + 1];
132 vCache[hash + 2] = vCache[i + 2];
133 if(nVerbose >= 3)
134 std::cout << "Cache mov: "
135 << "x = " << std::setw(10) << vCache[i] << ", "
136 << "y = " << std::setw(10) << vCache[i + 1] << ", "
137 << "z = " << std::setw(10) << vCache[i + 2] << ", "
138 << "hash = " << std::hex << (CacHash(vCache[i], vCache[i + 1]) & Mask) << std::dec
139 << std::endl;
140 }
141 }
142 }
143 };
144
145 struct Param {
146 int nObjsAllocLog;
147 int nObjsMaxLog;
148 int nUniqueSizeLog;
149 double UniqueDensity;
150 int nCacheSizeLog;
151 int nCacheMaxLog;
152 int nCacheVerbose;
153 bool fCountOnes;
154 int nGbc;
155 bvar nReo;
156 double MaxGrowth;
157 bool fReoVerbose;
158 int nVerbose;
159 std::vector<var> *pVar2Level;
160 Param() {
161 nObjsAllocLog = 20;
162 nObjsMaxLog = 25;
163 nUniqueSizeLog = 10;
164 UniqueDensity = 4;
165 nCacheSizeLog = 15;
166 nCacheMaxLog = 20;
167 nCacheVerbose = 0;
168 fCountOnes = false;
169 nGbc = 0;
170 nReo = BvarMax();
171 MaxGrowth = 1.2;
172 fReoVerbose = false;
173 nVerbose = 0;
174 pVar2Level = NULL;
175 }
176 };
177
178 class Man {
179 private:
180 var nVars;
181 bvar nObjs;
182 bvar nObjsAlloc;
183 bvar nObjsMax;
184 unsigned long long nCreatedTotal;
185 bvar RemovedHead;
186 int nGbc;
187 bvar nReo;
188 double MaxGrowth;
189 bool fReoVerbose;
190 int nVerbose;
191 std::vector<var> vVars;
192 std::vector<var> Var2Level;
193 std::vector<var> Level2Var;
194 std::vector<lit> vObjs;
195 std::vector<bvar> vNexts;
196 std::vector<bool> vMarks;
197 std::vector<ref> vRefs;
198 std::vector<edge> vEdges;
199 std::vector<double> vOneCounts;
200 std::vector<uniq> vUniqueMasks;
201 std::vector<bvar> vUniqueCounts;
202 std::vector<bvar> vUniqueTholds;
203 std::vector<std::vector<bvar> > vvUnique;
204 Cache *cache;
205
206 public:
207 inline lit Bvar2Lit(bvar a) const { return (lit)a << 1; }
208 inline lit Bvar2Lit(bvar a, bool c) const { return ((lit)a << 1) ^ (lit)c; }
209 inline bvar Lit2Bvar(lit x) const { return (bvar)(x >> 1); }
210 inline var VarOfBvar(bvar a) const { return vVars[a]; }
211 inline lit ThenOfBvar(bvar a) const { return vObjs[Bvar2Lit(a)]; }
212 inline lit ElseOfBvar(bvar a) const { return vObjs[Bvar2Lit(a, true)]; }
213 inline ref RefOfBvar(bvar a) const { return vRefs[a]; }
214 inline lit Const0() const { return (lit)0; }
215 inline lit Const1() const { return (lit)1; }
216 inline bool IsConst0(lit x) const { return x == Const0(); }
217 inline bool IsConst1(lit x) const { return x == Const1(); }
218 inline lit IthVar(var v) const { return Bvar2Lit((bvar)v + 1); }
219 inline lit LitRegular(lit x) const { return x & ~(lit)1; }
220 inline lit LitIrregular(lit x) const { return x | (lit)1; }
221 inline lit LitNot(lit x) const { return x ^ (lit)1; }
222 inline lit LitNotCond(lit x, bool c) const { return x ^ (lit)c; }
223 inline bool LitIsCompl(lit x) const { return x & (lit)1; }
224 inline bool LitIsEq(lit x, lit y) const { return x == y; }
225 inline var Var(lit x) const { return vVars[Lit2Bvar(x)]; }
226 inline var Level(lit x) const { return Var2Level[Var(x)]; }
227 inline lit Then(lit x) const { return LitNotCond(vObjs[LitRegular(x)], LitIsCompl(x)); }
228 inline lit Else(lit x) const { return LitNotCond(vObjs[LitIrregular(x)], LitIsCompl(x)); }
229 inline ref Ref(lit x) const { return vRefs[Lit2Bvar(x)]; }
230 inline double OneCount(lit x) const {
231 if(vOneCounts.empty())
232 fatal_error("fCountOnes was not set");
233 if(LitIsCompl(x))
234 return std::pow(2.0, nVars) - vOneCounts[Lit2Bvar(x)];
235 return vOneCounts[Lit2Bvar(x)];
236 }
237
238 public:
239 inline void IncRef(lit x) { if(!vRefs.empty() && Ref(x) != RefMax()) vRefs[Lit2Bvar(x)]++; }
240 inline void DecRef(lit x) { if(!vRefs.empty() && Ref(x) != RefMax()) vRefs[Lit2Bvar(x)]--; }
241
242 private:
243 inline bool Mark(lit x) const { return vMarks[Lit2Bvar(x)]; }
244 inline edge Edge(lit x) const { return vEdges[Lit2Bvar(x)]; }
245 inline void SetMark(lit x) { vMarks[Lit2Bvar(x)] = true; }
246 inline void ResetMark(lit x) { vMarks[Lit2Bvar(x)] = false; }
247 inline void IncEdge(lit x) { vEdges[Lit2Bvar(x)]++; }
248 inline void DecEdge(lit x) { vEdges[Lit2Bvar(x)]--; }
249 inline bool MarkOfBvar(bvar a) const { return vMarks[a]; }
250 inline edge EdgeOfBvar(bvar a) const { return vEdges[a]; }
251 inline void SetVarOfBvar(bvar a, var v) { vVars[a] = v; }
252 inline void SetThenOfBvar(bvar a, lit x) { vObjs[Bvar2Lit(a)] = x; }
253 inline void SetElseOfBvar(bvar a, lit x) { vObjs[Bvar2Lit(a, true)] = x; }
254 inline void SetMarkOfBvar(bvar a) { vMarks[a] = true; }
255 inline void ResetMarkOfBvar(bvar a) { vMarks[a] = false; }
256 inline void RemoveBvar(bvar a) {
257 var v = VarOfBvar(a);
258 SetVarOfBvar(a, VarMax());
259 std::vector<bvar>::iterator q = vvUnique[v].begin() + (UniqHash(ThenOfBvar(a), ElseOfBvar(a)) & vUniqueMasks[v]);
260 for(; *q; q = vNexts.begin() + *q)
261 if(*q == a)
262 break;
263 bvar next = vNexts[*q];
264 vNexts[*q] = RemovedHead;
265 RemovedHead = *q;
266 *q = next;
267 vUniqueCounts[v]--;
268 }
269
270 private:
271 void SetMark_rec(lit x) {
272 if(x < 2 || Mark(x))
273 return;
274 SetMark(x);
275 SetMark_rec(Then(x));
276 SetMark_rec(Else(x));
277 }
278 void ResetMark_rec(lit x) {
279 if(x < 2 || !Mark(x))
280 return;
281 ResetMark(x);
282 ResetMark_rec(Then(x));
283 ResetMark_rec(Else(x));
284 }
285 bvar CountNodes_rec(lit x) {
286 if(x < 2 || Mark(x))
287 return 0;
288 SetMark(x);
289 return 1 + CountNodes_rec(Then(x)) + CountNodes_rec(Else(x));
290 }
291 void CountEdges_rec(lit x) {
292 if(x < 2)
293 return;
294 IncEdge(x);
295 if(Mark(x))
296 return;
297 SetMark(x);
298 CountEdges_rec(Then(x));
299 CountEdges_rec(Else(x));
300 }
301 void CountEdges() {
302 vEdges.resize(nObjsAlloc);
303 for(bvar a = (bvar)nVars + 1; a < nObjs; a++)
304 if(RefOfBvar(a))
305 CountEdges_rec(Bvar2Lit(a));
306 for(bvar a = 1; a <= (bvar)nVars; a++)
307 vEdges[a]++;
308 for(bvar a = (bvar)nVars + 1; a < nObjs; a++)
309 if(RefOfBvar(a))
310 ResetMark_rec(Bvar2Lit(a));
311 }
312
313 public:
314 bool Resize() {
315 if(nObjsAlloc == nObjsMax)
316 return false;
317 lit nObjsAllocLit = (lit)nObjsAlloc << 1;
318 if(nObjsAllocLit > (lit)BvarMax())
319 nObjsAlloc = BvarMax();
320 else
321 nObjsAlloc = (bvar)nObjsAllocLit;
322 if(nVerbose >= 2)
323 std::cout << "Reallocating " << nObjsAlloc << " nodes" << std::endl;
324 vVars.resize(nObjsAlloc);
325 vObjs.resize((lit)nObjsAlloc * 2);
326 vNexts.resize(nObjsAlloc);
327 vMarks.resize(nObjsAlloc);
328 if(!vRefs.empty())
329 vRefs.resize(nObjsAlloc);
330 if(!vEdges.empty())
331 vEdges.resize(nObjsAlloc);
332 if(!vOneCounts.empty())
333 vOneCounts.resize(nObjsAlloc);
334 return true;
335 }
336 void ResizeUnique(var v) {
337 uniq nUniqueSize, nUniqueSizeOld;
338 nUniqueSize = nUniqueSizeOld = vvUnique[v].size();
339 nUniqueSize <<= 1;
340 if(!nUniqueSize) {
341 vUniqueTholds[v] = BvarMax();
342 return;
343 }
344 if(nVerbose >= 2)
345 std::cout << "Reallocating " << nUniqueSize << " unique table entries for Var " << v << std::endl;
346 vvUnique[v].resize(nUniqueSize);
347 vUniqueMasks[v] = nUniqueSize - 1;
348 for(uniq i = 0; i < nUniqueSizeOld; i++) {
349 std::vector<bvar>::iterator q, tail, tail1, tail2;
350 q = tail1 = vvUnique[v].begin() + i;
351 tail2 = q + nUniqueSizeOld;
352 while(*q) {
353 uniq hash = UniqHash(ThenOfBvar(*q), ElseOfBvar(*q)) & vUniqueMasks[v];
354 if(hash == i)
355 tail = tail1;
356 else
357 tail = tail2;
358 if(tail != q)
359 *tail = *q, *q = 0;
360 q = vNexts.begin() + *tail;
361 if(tail == tail1)
362 tail1 = q;
363 else
364 tail2 = q;
365 }
366 }
367 vUniqueTholds[v] <<= 1;
368 if((lit)vUniqueTholds[v] > (lit)BvarMax())
369 vUniqueTholds[v] = BvarMax();
370 }
371 bool Gbc() {
372 if(nVerbose >= 2)
373 std::cout << "Garbage collect" << std::endl;
374 if(!vEdges.empty()) {
375 for(bvar a = (bvar)nVars + 1; a < nObjs; a++)
376 if(!EdgeOfBvar(a) && VarOfBvar(a) != VarMax())
377 RemoveBvar(a);
378 } else {
379 for(bvar a = (bvar)nVars + 1; a < nObjs; a++)
380 if(RefOfBvar(a))
381 SetMark_rec(Bvar2Lit(a));
382 for(bvar a = (bvar)nVars + 1; a < nObjs; a++)
383 if(!MarkOfBvar(a) && VarOfBvar(a) != VarMax())
384 RemoveBvar(a);
385 for(bvar a = (bvar)nVars + 1; a < nObjs; a++)
386 if(RefOfBvar(a))
387 ResetMark_rec(Bvar2Lit(a));
388 }
389 cache->Clear();
390 return RemovedHead;
391 }
392
393 private:
394 inline lit UniqueCreateInt(var v, lit x1, lit x0) {
395 std::vector<bvar>::iterator p, q;
396 p = q = vvUnique[v].begin() + (UniqHash(x1, x0) & vUniqueMasks[v]);
397 for(; *q; q = vNexts.begin() + *q)
398 if(VarOfBvar(*q) == v && ThenOfBvar(*q) == x1 && ElseOfBvar(*q) == x0)
399 return Bvar2Lit(*q);
400 nCreatedTotal++;
401 bvar next = *p;
402 if(nObjs < nObjsAlloc)
403 *p = nObjs++;
404 else if(RemovedHead)
405 *p = RemovedHead, RemovedHead = vNexts[*p];
406 else
407 return LitMax();
408 SetVarOfBvar(*p, v);
409 SetThenOfBvar(*p, x1);
410 SetElseOfBvar(*p, x0);
411 vNexts[*p] = next;
412 if(!vOneCounts.empty())
413 vOneCounts[*p] = OneCount(x1) / 2 + OneCount(x0) / 2;
414 if(nVerbose >= 3) {
415 std::cout << "Create node " << std::setw(10) << *p << ": "
416 << "Var = " << std::setw(6) << v << ", "
417 << "Then = " << std::setw(10) << x1 << ", "
418 << "Else = " << std::setw(10) << x0;
419 if(!vOneCounts.empty())
420 std::cout << ", Ones = " << std::setw(10) << vOneCounts[*q];
421 std::cout << std::endl;
422 }
423 vUniqueCounts[v]++;
424 if(vUniqueCounts[v] > vUniqueTholds[v]) {
425 bvar a = *p;
426 ResizeUnique(v);
427 return Bvar2Lit(a);
428 }
429 return Bvar2Lit(*p);
430 }
431 inline lit UniqueCreate(var v, lit x1, lit x0) {
432 if(x1 == x0)
433 return x1;
434 lit x;
435 while(true) {
436 if(!LitIsCompl(x0))
437 x = UniqueCreateInt(v, x1, x0);
438 else
439 x = UniqueCreateInt(v, LitNot(x1), LitNot(x0));
440 if(x == LitMax()) {
441 bool fRemoved = false;
442 if(nGbc > 1)
443 fRemoved = Gbc();
444 if(!Resize() && !fRemoved && (nGbc != 1 || !Gbc()))
445 fatal_error("Memout (node)");
446 } else
447 break;
448 }
449 return LitIsCompl(x0)? LitNot(x): x;
450 }
451 lit And_rec(lit x, lit y) {
452 if(x == 0 || y == 1)
453 return x;
454 if(x == 1 || y == 0)
455 return y;
456 if(Lit2Bvar(x) == Lit2Bvar(y))
457 return (x == y)? x: 0;
458 if(x > y)
459 std::swap(x, y);
460 lit z = cache->Lookup(x, y);
461 if(z != LitMax())
462 return z;
463 var v;
464 lit x0, x1, y0, y1;
465 if(Level(x) < Level(y))
466 v = Var(x), x1 = Then(x), x0 = Else(x), y0 = y1 = y;
467 else if(Level(x) > Level(y))
468 v = Var(y), x0 = x1 = x, y1 = Then(y), y0 = Else(y);
469 else
470 v = Var(x), x1 = Then(x), x0 = Else(x), y1 = Then(y), y0 = Else(y);
471 lit z1 = And_rec(x1, y1);
472 IncRef(z1);
473 lit z0 = And_rec(x0, y0);
474 IncRef(z0);
475 z = UniqueCreate(v, z1, z0);
476 DecRef(z1);
477 DecRef(z0);
478 cache->Insert(x, y, z);
479 return z;
480 }
481
482 private:
483 bvar Swap(var i) {
484 var v1 = Level2Var[i];
485 var v2 = Level2Var[i + 1];
486 bvar f = 0;
487 bvar diff = 0;
488 for(std::vector<bvar>::iterator p = vvUnique[v1].begin(); p != vvUnique[v1].end(); p++) {
489 std::vector<bvar>::iterator q = p;
490 while(*q) {
491 if(!EdgeOfBvar(*q)) {
492 SetVarOfBvar(*q, VarMax());
493 bvar next = vNexts[*q];
494 vNexts[*q] = RemovedHead;
495 RemovedHead = *q;
496 *q = next;
497 vUniqueCounts[v1]--;
498 continue;
499 }
500 lit f1 = ThenOfBvar(*q);
501 lit f0 = ElseOfBvar(*q);
502 if(Var(f1) == v2 || Var(f0) == v2) {
503 DecEdge(f1);
504 if(Var(f1) == v2 && !Edge(f1))
505 DecEdge(Then(f1)), DecEdge(Else(f1)), diff--;
506 DecEdge(f0);
507 if(Var(f0) == v2 && !Edge(f0))
508 DecEdge(Then(f0)), DecEdge(Else(f0)), diff--;
509 bvar next = vNexts[*q];
510 vNexts[*q] = f;
511 f = *q;
512 *q = next;
513 vUniqueCounts[v1]--;
514 continue;
515 }
516 q = vNexts.begin() + *q;
517 }
518 }
519 while(f) {
520 lit f1 = ThenOfBvar(f);
521 lit f0 = ElseOfBvar(f);
522 lit f00, f01, f10, f11;
523 if(Var(f1) == v2)
524 f11 = Then(f1), f10 = Else(f1);
525 else
526 f10 = f11 = f1;
527 if(Var(f0) == v2)
528 f01 = Then(f0), f00 = Else(f0);
529 else
530 f00 = f01 = f0;
531 if(f11 == f01)
532 f1 = f11;
533 else {
534 f1 = UniqueCreate(v1, f11, f01);
535 if(!Edge(f1))
536 IncEdge(f11), IncEdge(f01), diff++;
537 }
538 IncEdge(f1);
539 IncRef(f1);
540 if(f10 == f00)
541 f0 = f10;
542 else {
543 f0 = UniqueCreate(v1, f10, f00);
544 if(!Edge(f0))
545 IncEdge(f10), IncEdge(f00), diff++;
546 }
547 IncEdge(f0);
548 DecRef(f1);
549 SetVarOfBvar(f, v2);
550 SetThenOfBvar(f, f1);
551 SetElseOfBvar(f, f0);
552 std::vector<bvar>::iterator q = vvUnique[v2].begin() + (UniqHash(f1, f0) & vUniqueMasks[v2]);
553 lit next = vNexts[f];
554 vNexts[f] = *q;
555 *q = f;
556 vUniqueCounts[v2]++;
557 f = next;
558 }
559 Var2Level[v1] = i + 1;
560 Var2Level[v2] = i;
561 Level2Var[i] = v2;
562 Level2Var[i + 1] = v1;
563 return diff;
564 }
565 void Sift() {
566 bvar count = CountNodes();
567 std::vector<var> sift_order(nVars);
568 for(var v = 0; v < nVars; v++)
569 sift_order[v] = v;
570 for(var i = 0; i < nVars; i++) {
571 var max_j = i;
572 for(var j = i + 1; j < nVars; j++)
573 if(vUniqueCounts[sift_order[j]] > vUniqueCounts[sift_order[max_j]])
574 max_j = j;
575 if(max_j != i)
576 std::swap(sift_order[max_j], sift_order[i]);
577 }
578 for(var v = 0; v < nVars; v++) {
579 bvar lev = Var2Level[sift_order[v]];
580 bool UpFirst = lev < (bvar)(nVars / 2);
581 bvar min_lev = lev;
582 bvar min_diff = 0;
583 bvar diff = 0;
584 bvar thold = count * (MaxGrowth - 1);
585 if(fReoVerbose)
586 std::cout << "Sift " << sift_order[v] << " : Level = " << lev << " Count = " << count << " Thold = " << thold << std::endl;
587 if(UpFirst) {
588 lev--;
589 for(; lev >= 0; lev--) {
590 diff += Swap(lev);
591 if(fReoVerbose)
592 std::cout << "\tSwap " << lev << " : Diff = " << diff << " Thold = " << thold << std::endl;
593 if(diff < min_diff)
594 min_lev = lev, min_diff = diff, thold = (count + diff) * (MaxGrowth - 1);
595 else if(diff > thold) {
596 lev--;
597 break;
598 }
599 }
600 lev++;
601 }
602 for(; lev < (bvar)nVars - 1; lev++) {
603 diff += Swap(lev);
604 if(fReoVerbose)
605 std::cout << "\tSwap " << lev << " : Diff = " << diff << " Thold = " << thold << std::endl;
606 if(diff <= min_diff)
607 min_lev = lev + 1, min_diff = diff, thold = (count + diff) * (MaxGrowth - 1);
608 else if(diff > thold) {
609 lev++;
610 break;
611 }
612 }
613 lev--;
614 if(UpFirst) {
615 for(; lev >= min_lev; lev--) {
616 diff += Swap(lev);
617 if(fReoVerbose)
618 std::cout << "\tSwap " << lev << " : Diff = " << diff << " Thold = " << thold << std::endl;
619 }
620 } else {
621 for(; lev >= 0; lev--) {
622 diff += Swap(lev);
623 if(fReoVerbose)
624 std::cout << "\tSwap " << lev << " : Diff = " << diff << " Thold = " << thold << std::endl;
625 if(diff <= min_diff)
626 min_lev = lev, min_diff = diff, thold = (count + diff) * (MaxGrowth - 1);
627 else if(diff > thold) {
628 lev--;
629 break;
630 }
631 }
632 lev++;
633 for(; lev < min_lev; lev++) {
634 diff += Swap(lev);
635 if(fReoVerbose)
636 std::cout << "\tSwap " << lev << " : Diff = " << diff << " Thold = " << thold << std::endl;
637 }
638 }
639 count += min_diff;
640 if(fReoVerbose)
641 std::cout << "Sifted " << sift_order[v] << " : Level = " << min_lev << " Count = " << count << " Thold = " << thold << std::endl;
642 }
643 }
644
645 public:
646 Man(int nVars_, Param p) {
647 nCreatedTotal = 0;
648 nVerbose = p.nVerbose;
649 // parameter sanity check
650 if(p.nObjsMaxLog < p.nObjsAllocLog)
651 fatal_error("nObjsMax must not be smaller than nObjsAlloc");
652 if(nVars_ >= (int)VarMax())
653 fatal_error("Memout (nVars) in init");
654 nVars = nVars_;
655 lit nObjsMaxLit = (lit)1 << p.nObjsMaxLog;
656 if(!nObjsMaxLit)
657 fatal_error("Memout (nObjsMax) in init");
658 if(nObjsMaxLit > (lit)BvarMax())
659 nObjsMax = BvarMax();
660 else
661 nObjsMax = (bvar)nObjsMaxLit;
662 lit nObjsAllocLit = (lit)1 << p.nObjsAllocLog;
663 if(!nObjsAllocLit)
664 fatal_error("Memout (nObjsAlloc) in init");
665 if(nObjsAllocLit > (lit)BvarMax())
666 nObjsAlloc = BvarMax();
667 else
668 nObjsAlloc = (bvar)nObjsAllocLit;
669 if(nObjsAlloc <= (bvar)nVars)
670 fatal_error("nObjsAlloc must be larger than nVars");
671 uniq nUniqueSize = (uniq)1 << p.nUniqueSizeLog;
672 if(!nUniqueSize)
673 fatal_error("Memout (nUniqueSize) in init");
674 // allocation
675 if(nVerbose)
676 std::cout << "Allocating " << nObjsAlloc << " nodes and " << nVars << " x " << nUniqueSize << " unique table entries" << std::endl;
677 vVars.resize(nObjsAlloc);
678 vObjs.resize((lit)nObjsAlloc * 2);
679 vNexts.resize(nObjsAlloc);
680 vMarks.resize(nObjsAlloc);
681 vvUnique.resize(nVars);
682 vUniqueMasks.resize(nVars);
683 vUniqueCounts.resize(nVars);
684 vUniqueTholds.resize(nVars);
685 for(var v = 0; v < nVars; v++) {
686 vvUnique[v].resize(nUniqueSize);
687 vUniqueMasks[v] = nUniqueSize - 1;
688 if((lit)(nUniqueSize * p.UniqueDensity) > (lit)BvarMax())
689 vUniqueTholds[v] = BvarMax();
690 else
691 vUniqueTholds[v] = (bvar)(nUniqueSize * p.UniqueDensity);
692 }
693 if(p.fCountOnes) {
694 if(nVars > 1023)
695 fatal_error("nVars must be less than 1024 to count ones");
696 vOneCounts.resize(nObjsAlloc);
697 }
698 // set up cache
699 cache = new Cache(p.nCacheSizeLog, p.nCacheMaxLog, p.nCacheVerbose);
700 // create nodes for variables
701 nObjs = 1;
702 vVars[0] = VarMax();
703 for(var v = 0; v < nVars; v++)
704 UniqueCreateInt(v, 1, 0);
705 // set up variable order
706 Var2Level.resize(nVars);
707 Level2Var.resize(nVars);
708 for(var v = 0; v < nVars; v++) {
709 if(p.pVar2Level)
710 Var2Level[v] = (*p.pVar2Level)[v];
711 else
712 Var2Level[v] = v;
713 Level2Var[Var2Level[v]] = v;
714 }
715 // set other parameters
716 RemovedHead = 0;
717 nGbc = p.nGbc;
718 nReo = p.nReo;
719 MaxGrowth = p.MaxGrowth;
720 fReoVerbose = p.fReoVerbose;
721 if(nGbc || nReo != BvarMax())
722 vRefs.resize(nObjsAlloc);
723 }
724 ~Man() {
725 if(nVerbose) {
726 std::cout << "Free " << nObjsAlloc << " nodes (" << nObjs << " live nodes)" << std::endl;
727 std::cout << "Free {";
728 std::string delim;
729 for(var v = 0; v < nVars; v++) {
730 std::cout << delim << vvUnique[v].size();
731 delim = ", ";
732 }
733 std::cout << "} unique table entries" << std::endl;
734 if(!vRefs.empty())
735 std::cout << "Free " << vRefs.size() << " refs" << std::endl;
736 }
737 delete cache;
738 }
739 void Reorder() {
740 if(nVerbose >= 2)
741 std::cout << "Reorder" << std::endl;
742 int nGbc_ = nGbc;
743 nGbc = 0;
744 CountEdges();
745 Sift();
746 vEdges.clear();
747 cache->Clear();
748 nGbc = nGbc_;
749 }
750 inline lit And(lit x, lit y) {
751 if(nObjs > nReo) {
752 Reorder();
753 while(nReo < nObjs) {
754 nReo <<= 1;
755 if((lit)nReo > (lit)BvarMax())
756 nReo = BvarMax();
757 }
758 }
759 return And_rec(x, y);
760 }
761 inline lit Or(lit x, lit y) {
762 return LitNot(And(LitNot(x), LitNot(y)));
763 }
764
765 public:
766 void SetRef(std::vector<lit> const &vLits) {
767 vRefs.clear();
768 vRefs.resize(nObjsAlloc);
769 for(size_t i = 0; i < vLits.size(); i++)
770 IncRef(vLits[i]);
771 }
772 void RemoveRefIfUnused() {
773 if(!nGbc && nReo == BvarMax())
774 vRefs.clear();
775 }
776 void TurnOnReo(int nReo_ = 0, std::vector<lit> const *vLits = NULL) {
777 if(nReo_)
778 nReo = nReo_;
779 else
780 nReo = nObjs << 1;
781 if((lit)nReo > (lit)BvarMax())
782 nReo = BvarMax();
783 if(vRefs.empty()) {
784 if(vLits)
785 SetRef(*vLits);
786 else
787 vRefs.resize(nObjsAlloc);
788 }
789 }
790 void TurnOffReo() {
791 nReo = BvarMax();
792 }
793 var GetNumVars() const {
794 return nVars;
795 }
796 void GetOrdering(std::vector<int> &Var2Level_) {
797 Var2Level_.resize(nVars);
798 for(var v = 0; v < nVars; v++)
799 Var2Level_[v] = Var2Level[v];
800 }
801 bvar CountNodes() {
802 bvar count = 1;
803 if(!vEdges.empty()) {
804 for(bvar a = 1; a < nObjs; a++)
805 if(EdgeOfBvar(a))
806 count++;
807 return count;
808 }
809 for(bvar a = 1; a <= (bvar)nVars; a++) {
810 count++;
811 SetMarkOfBvar(a);
812 }
813 for(bvar a = (bvar)nVars + 1; a < nObjs; a++)
814 if(RefOfBvar(a))
815 count += CountNodes_rec(Bvar2Lit(a));
816 for(bvar a = 1; a <= (bvar)nVars; a++)
817 ResetMarkOfBvar(a);
818 for(bvar a = (bvar)nVars + 1; a < nObjs; a++)
819 if(RefOfBvar(a))
820 ResetMark_rec(Bvar2Lit(a));
821 return count;
822 }
823 bvar CountNodes(std::vector<lit> const &vLits) {
824 bvar count = 1;
825 for(size_t i = 0; i < vLits.size(); i++)
826 count += CountNodes_rec(vLits[i]);
827 for(size_t i = 0; i < vLits.size(); i++)
828 ResetMark_rec(vLits[i]);
829 return count;
830 }
831 void PrintStats() {
832 bvar nRemoved = 0;
833 bvar a = RemovedHead;
834 while(a)
835 a = vNexts[a], nRemoved++;
836 bvar nLive = 1;
837 for(var v = 0; v < nVars; v++)
838 nLive += vUniqueCounts[v];
839 std::cout << "ref: " << std::setw(10) << (vRefs.empty()? 0: CountNodes()) << ", "
840 << "used: " << std::setw(10) << nObjs << ", "
841 << "live: " << std::setw(10) << nLive << ", "
842 << "dead: " << std::setw(10) << nRemoved << ", "
843 << "alloc: " << std::setw(10) << nObjsAlloc
844 << std::endl;
845 }
846 unsigned long long GetNumTotalCreatedNodes() {
847 return nCreatedTotal;
848 }
849 };
850
851}
852}
853
854ABC_NAMESPACE_CXX_HEADER_END
ABC_NAMESPACE_CXX_HEADER_START
#define ABC_NAMESPACE_CXX_HEADER_START
Definition abc_namespaces.h:52
ABC_NAMESPACE_CXX_HEADER_END
#define ABC_NAMESPACE_CXX_HEADER_END
Definition abc_namespaces.h:53
rrr::NewBdd::Cache::Insert
void Insert(lit x, lit y, lit z)
Definition rrrBddManager.h:103
rrr::NewBdd::Cache::Cache
Cache(int nCacheSizeLog, int nCacheMaxLog, int nVerbose)
Definition rrrBddManager.h:49
rrr::NewBdd::Cache::Lookup
lit Lookup(lit x, lit y)
Definition rrrBddManager.h:69
rrr::NewBdd::Man::Const0
lit Const0() const
Definition rrrBddManager.h:214
rrr::NewBdd::Man::CountNodes
bvar CountNodes(std::vector< lit > const &vLits)
Definition rrrBddManager.h:823
rrr::NewBdd::Man::RefOfBvar
ref RefOfBvar(bvar a) const
Definition rrrBddManager.h:213
rrr::NewBdd::Man::IsConst0
bool IsConst0(lit x) const
Definition rrrBddManager.h:216
rrr::NewBdd::Man::Lit2Bvar
bvar Lit2Bvar(lit x) const
Definition rrrBddManager.h:209
rrr::NewBdd::Man::GetNumVars
var GetNumVars() const
Definition rrrBddManager.h:793
rrr::NewBdd::Man::Man
Man(int nVars_, Param p)
Definition rrrBddManager.h:646
rrr::NewBdd::Man::LitNot
lit LitNot(lit x) const
Definition rrrBddManager.h:221
rrr::NewBdd::Man::SetRef
void SetRef(std::vector< lit > const &vLits)
Definition rrrBddManager.h:766
rrr::NewBdd::Man::LitIsEq
bool LitIsEq(lit x, lit y) const
Definition rrrBddManager.h:224
rrr::NewBdd::Man::GetOrdering
void GetOrdering(std::vector< int > &Var2Level_)
Definition rrrBddManager.h:796
rrr::NewBdd::Man::Then
lit Then(lit x) const
Definition rrrBddManager.h:227
rrr::NewBdd::Man::LitNotCond
lit LitNotCond(lit x, bool c) const
Definition rrrBddManager.h:222
rrr::NewBdd::Man::IthVar
lit IthVar(var v) const
Definition rrrBddManager.h:218
rrr::NewBdd::Man::ResizeUnique
void ResizeUnique(var v)
Definition rrrBddManager.h:336
rrr::NewBdd::Man::LitRegular
lit LitRegular(lit x) const
Definition rrrBddManager.h:219
rrr::NewBdd::Man::Bvar2Lit
lit Bvar2Lit(bvar a, bool c) const
Definition rrrBddManager.h:208
rrr::NewBdd::Man::Else
lit Else(lit x) const
Definition rrrBddManager.h:228
rrr::NewBdd::Man::IsConst1
bool IsConst1(lit x) const
Definition rrrBddManager.h:217
rrr::NewBdd::Man::Bvar2Lit
lit Bvar2Lit(bvar a) const
Definition rrrBddManager.h:207
rrr::NewBdd::Man::ElseOfBvar
lit ElseOfBvar(bvar a) const
Definition rrrBddManager.h:212
rrr::NewBdd::Man::Level
var Level(lit x) const
Definition rrrBddManager.h:226
rrr::NewBdd::Man::IncRef
void IncRef(lit x)
Definition rrrBddManager.h:239
rrr::NewBdd::Man::Or
lit Or(lit x, lit y)
Definition rrrBddManager.h:761
rrr::NewBdd::Man::LitIsCompl
bool LitIsCompl(lit x) const
Definition rrrBddManager.h:223
rrr::NewBdd::Man::ThenOfBvar
lit ThenOfBvar(bvar a) const
Definition rrrBddManager.h:211
rrr::NewBdd::Man::VarOfBvar
var VarOfBvar(bvar a) const
Definition rrrBddManager.h:210
rrr::NewBdd::Man::Var
var Var(lit x) const
Definition rrrBddManager.h:225
rrr::NewBdd::Man::Const1
lit Const1() const
Definition rrrBddManager.h:215
rrr::NewBdd::Man::OneCount
double OneCount(lit x) const
Definition rrrBddManager.h:230
rrr::NewBdd::Man::LitIrregular
lit LitIrregular(lit x) const
Definition rrrBddManager.h:220
rrr::NewBdd::Man::TurnOnReo
void TurnOnReo(int nReo_=0, std::vector< lit > const *vLits=NULL)
Definition rrrBddManager.h:776
rrr::NewBdd::Man::GetNumTotalCreatedNodes
unsigned long long GetNumTotalCreatedNodes()
Definition rrrBddManager.h:846
rrr::NewBdd::Man::Ref
ref Ref(lit x) const
Definition rrrBddManager.h:229
rrr::NewBdd::Man::And
lit And(lit x, lit y)
Definition rrrBddManager.h:750
rrr::NewBdd::Man::DecRef
void DecRef(lit x)
Definition rrrBddManager.h:240
p
Cube * p
Definition exorList.c:222
Var
int Var
Definition exorList.c:228
z0
#define z0
Definition extraBdd.h:77
z1
#define z1
Definition extraBdd.h:78
rrr::NewBdd::ref
unsigned short ref
Definition rrrBddManager.h:18
rrr::NewBdd::size
unsigned long long size
Definition rrrBddManager.h:19
rrr::NewBdd::var
unsigned short var
Definition rrrBddManager.h:15
rrr::NewBdd::edge
unsigned edge
Definition rrrBddManager.h:20
rrr::NewBdd::uniq
unsigned uniq
Definition rrrBddManager.h:21
rrr::NewBdd::cac
unsigned cac
Definition rrrBddManager.h:22
rrr::NewBdd::lit
unsigned lit
Definition rrrBddManager.h:17
rrr
Definition rrr.h:16
lit
int lit
Definition satVec.h:130
rrr::NewBdd::Param::pVar2Level
std::vector< var > * pVar2Level
Definition rrrBddManager.h:159