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