ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
giaTransduction.h
Go to the documentation of this file.
1
20
21#ifndef ABC__aig__gia__giaTransduction_h
22#define ABC__aig__gia__giaTransduction_h
23
24#include <iostream>
25#include <iomanip>
26#include <sstream>
27#include <vector>
28#include <list>
29#include <set>
30#include <algorithm>
31#include <cassert>
32#include <iterator>
33
34#include "gia.h"
35
36ABC_NAMESPACE_CXX_HEADER_START
37
38namespace Transduction {
39
40enum PfState {none, cspf, mspf};
41
42template <class Man, class lit, lit LitMax>
43class ManUtil {
44protected:
45 Man *man;
46 inline void IncRef(lit x) const {
47 if(x != LitMax)
48 man->IncRef(x);
49 }
50 inline void DecRef(lit x) const {
51 if(x != LitMax)
52 man->DecRef(x);
53 }
54 inline void Update(lit &x, lit y) const {
55 DecRef(x);
56 x = y;
57 IncRef(x);
58 }
59 inline void DelVec(std::vector<lit> &v) const {
60 for(unsigned i = 0; i < v.size(); i++)
61 DecRef(v[i]);
62 v.clear();
63 }
64 inline void DelVec(std::vector<std::vector<lit> > &v) const {
65 for(unsigned i = 0; i < v.size(); i++)
66 DelVec(v[i]);
67 v.clear();
68 }
69 inline void CopyVec(std::vector<lit> &v, std::vector<lit> const &u) const {
70 DelVec(v);
71 v = u;
72 for(unsigned i = 0; i < v.size(); i++)
73 IncRef(v[i]);
74 }
75 inline void CopyVec(std::vector<std::vector<lit> > &v, std::vector<std::vector<lit> > const &u) const {
76 for(unsigned i = u.size(); i < v.size(); i++)
77 DelVec(v[i]);
78 v.resize(u.size());
79 for(unsigned i = 0; i < v.size(); i++)
80 CopyVec(v[i], u[i]);
81 }
82 inline bool LitVecIsEq(std::vector<lit> const &v, std::vector<lit> const &u) const {
83 if(v.size() != u.size())
84 return false;
85 for(unsigned i = 0; i < v.size(); i++)
86 if(!man->LitIsEq(v[i], u[i]))
87 return false;
88 return true;
89 }
90 inline bool LitVecIsEq(std::vector<std::vector<lit> > const &v, std::vector<std::vector<lit> > const &u) const {
91 if(v.size() != u.size())
92 return false;
93 for(unsigned i = 0; i < v.size(); i++)
94 if(!LitVecIsEq(v[i], u[i]))
95 return false;
96 return true;
97 }
98 inline lit Xor(lit x, lit y) const {
99 lit f = man->And(x, man->LitNot(y));
100 man->IncRef(f);
101 lit g = man->And(man->LitNot(x), y);
102 man->IncRef(g);
103 lit r = man->Or(f, g);
104 man->DecRef(f);
105 man->DecRef(g);
106 return r;
107 }
108};
109
110template <class Man, class lit, lit LitMax>
111class TransductionBackup: ManUtil<Man, lit, LitMax> {
112private:
113 int nObjsAlloc;
114 PfState state;
115 std::list<int> vObjs;
116 std::vector<std::vector<int> > vvFis;
117 std::vector<std::vector<int> > vvFos;
118 std::vector<int> vLevels;
119 std::vector<int> vSlacks;
120 std::vector<std::vector<int> > vvFiSlacks;
121 std::vector<lit> vFs;
122 std::vector<lit> vGs;
123 std::vector<std::vector<lit> > vvCs;
124 std::vector<bool> vUpdates;
125 std::vector<bool> vPfUpdates;
126 std::vector<bool> vFoConeShared;
127 template <class Man_, class Param, class lit_, lit_ LitMax_>
128 friend class Transduction;
129
130public:
131 ~TransductionBackup() {
132 if(this->man) {
133 this->DelVec(vFs);
134 this->DelVec(vGs);
135 this->DelVec(vvCs);
136 }
137 }
138};
139
140template <class Man, class Param, class lit, lit LitMax>
141class Transduction: ManUtil<Man, lit, LitMax> {
142private:
143 int nVerbose;
144 int nSortType;
145 bool fLevel;
146 int nObjsAlloc;
147 int nMaxLevels;
148 PfState state;
149 std::vector<int> vPis;
150 std::vector<int> vPos;
151 std::list<int> vObjs;
152 std::vector<std::vector<int> > vvFis;
153 std::vector<std::vector<int> > vvFos;
154 std::vector<int> vLevels;
155 std::vector<int> vSlacks;
156 std::vector<std::vector<int> > vvFiSlacks;
157 std::vector<lit> vFs;
158 std::vector<lit> vGs;
159 std::vector<std::vector<lit> > vvCs;
160 std::vector<bool> vUpdates;
161 std::vector<bool> vPfUpdates;
162 std::vector<bool> vFoConeShared;
163 std::vector<lit> vPoFs;
164
165 bool fNewLine;
166 abctime startclk;
167
168private: // Helper functions
169 inline bool AllFalse(std::vector<bool> const &v) const {
170 for(std::list<int>::const_iterator it = vObjs.begin(); it != vObjs.end(); it++)
171 if(v[*it])
172 return false;
173 return true;
174 }
175
176public: // Counting
177 inline int CountGates() const {
178 return vObjs.size();
179 }
180 inline int CountWires() const {
181 int count = 0;
182 for(std::list<int>::const_iterator it = vObjs.begin(); it != vObjs.end(); it++)
183 count += vvFis[*it].size();
184 return count;
185 }
186 inline int CountNodes() const {
187 return CountWires() - CountGates();
188 }
189 inline int CountLevels() const {
190 int count = 0;
191 for(unsigned i = 0; i < vPos.size(); i++)
192 count = std::max(count, vLevels[vvFis[vPos[i]][0] >> 1]);
193 return count;
194 }
195 inline void Print(std::string str, bool nl) const {
196 if(!fNewLine)
197 std::cout << "\33[2K\r";
198 std::cout << str;
199 if(fNewLine || nl)
200 std::cout << std::endl;
201 else
202 std::cout << std::flush;
203 }
204 inline void PrintStats(std::string prefix, bool nl, int prefix_size = 0) const {
205 if(!prefix_size)
206 prefix_size = prefix.size();
207 std::stringstream ss;
208 ss << std::left << std::setw(prefix_size) << prefix << ": " << std::right;
209 ss << "#nodes = " << std::setw(5) << CountNodes();
210 if(fLevel)
211 ss << ", #level = " << std::setw(5) << CountLevels();
212 ss << ", elapsed = " << std::setprecision(2) << std::fixed << std::setw(8) << 1.0 * (Abc_Clock() - startclk) / CLOCKS_PER_SEC << "s";
213 Print(ss.str(), nl);
214 }
215 inline void PrintPfHeader(std::string prefix, int block, int block_i0) {
216 std::stringstream ss;
217 ss << "\t\t" << prefix;
218 if(block_i0 != -1)
219 ss << " (blocking Wire " << block_i0 << " -> " << block << ")";
220 else if(block != -1)
221 ss << " (blocking Gate " << block << ")";
222 Print(ss.str(), true);
223 }
224
225private: // MIAIG
226 void SortObjs_rec(std::list<int>::iterator const &it) {
227 for(unsigned j = 0; j < vvFis[*it].size(); j++) {
228 int i0 = vvFis[*it][j] >> 1;
229 if(!vvFis[i0].empty()) {
230 std::list<int>::iterator it_i0 = std::find(it, vObjs.end(), i0);
231 if(it_i0 != vObjs.end()) {
232 // if(nVerbose > 6)
233 // std::cout << "\t\t\t\t\t\tMove " << i0 << " before " << *it << std::endl;
234 vObjs.erase(it_i0);
235 it_i0 = vObjs.insert(it, i0);
236 SortObjs_rec(it_i0);
237 }
238 }
239 }
240 }
241 inline void Connect(int i, int f, bool fSort = false, bool fUpdate = true, lit c = LitMax) {
242 int i0 = f >> 1;
243 if(nVerbose > 5) {
244 std::stringstream ss;
245 ss << "\t\t\t\t\tadd Wire " << std::setw(5) << i0 << "(" << (f & 1) << ")"
246 << " -> " << std::setw(5) << i;
247 Print(ss.str(), true);
248 }
249 assert(std::find(vvFis[i].begin(), vvFis[i].end(), f) == vvFis[i].end());
250 vvFis[i].push_back(f);
251 vvFos[i0].push_back(i);
252 if(fUpdate)
253 vUpdates[i] = true;
254 this->IncRef(c);
255 vvCs[i].push_back(c);
256 if(fSort && !vvFos[i].empty() && !vvFis[i0].empty()) {
257 std::list<int>::iterator it = find(vObjs.begin(), vObjs.end(), i);
258 std::list<int>::iterator it_i0 = find(it, vObjs.end(), i0);
259 if(it_i0 != vObjs.end()) {
260 // if(nVerbose > 6)
261 // std::cout << "\t\t\t\t\t\tMove " << i0 << " before " << *it << std::endl;
262 vObjs.erase(it_i0);
263 it_i0 = vObjs.insert(it, i0);
264 SortObjs_rec(it_i0);
265 }
266 }
267 }
268 inline void Disconnect(int i, int i0, unsigned j, bool fUpdate = true, bool fPfUpdate = true) {
269 if(nVerbose > 5) {
270 std::stringstream ss;
271 ss << "\t\t\t\t\tremove Wire " << std::setw(5) << i0 << "(" << (vvFis[i][j] & 1) << ")"
272 << " -> " << std::setw(5) << i;
273 Print(ss.str(), true);
274 }
275 vvFos[i0].erase(std::find(vvFos[i0].begin(), vvFos[i0].end(), i));
276 vvFis[i].erase(vvFis[i].begin() + j);
277 this->DecRef(vvCs[i][j]);
278 vvCs[i].erase(vvCs[i].begin() + j);
279 if(fUpdate)
280 vUpdates[i] = true;
281 if(fPfUpdate)
282 vPfUpdates[i0] = true;
283 }
284 inline int Remove(int i, bool fPfUpdate = true) {
285 if(nVerbose > 5) {
286 std::stringstream ss;
287 ss << "\t\t\t\t\tremove Gate " << std::setw(5) << i;
288 Print(ss.str(), true);
289 }
290 assert(vvFos[i].empty());
291 for(unsigned j = 0; j < vvFis[i].size(); j++) {
292 int i0 = vvFis[i][j] >> 1;
293 vvFos[i0].erase(std::find(vvFos[i0].begin(), vvFos[i0].end(), i));
294 if(fPfUpdate)
295 vPfUpdates[i0] = true;
296 }
297 int count = vvFis[i].size();
298 vvFis[i].clear();
299 this->DecRef(vFs[i]);
300 this->DecRef(vGs[i]);
301 vFs[i] = vGs[i] = LitMax;
302 this->DelVec(vvCs[i]);
303 vUpdates[i] = vPfUpdates[i] = false;
304 return count;
305 }
306 inline int FindFi(int i, int i0) const {
307 for(unsigned j = 0; j < vvFis[i].size(); j++)
308 if((vvFis[i][j] >> 1) == i0)
309 return j;
310 return -1;
311 }
312 inline int Replace(int i, int f, bool fUpdate = true) {
313 if(nVerbose > 4) {
314 std::stringstream ss;
315 ss << "\t\t\t\treplace Gate " << std::setw(5) << i
316 << " by Node " << std::setw(5) << (f >> 1) << "(" << (f & 1) << ")";
317 Print(ss.str(), true);
318 }
319 assert(i != (f >> 1));
320 int count = 0;
321 for(unsigned j = 0; j < vvFos[i].size(); j++) {
322 int k = vvFos[i][j];
323 int l = FindFi(k, i);
324 assert(l >= 0);
325 int fc = f ^ (vvFis[k][l] & 1);
326 if(find(vvFis[k].begin(), vvFis[k].end(), fc) != vvFis[k].end()) {
327 this->DecRef(vvCs[k][l]);
328 vvCs[k].erase(vvCs[k].begin() + l);
329 vvFis[k].erase(vvFis[k].begin() + l);
330 count++;
331 } else {
332 vvFis[k][l] = f ^ (vvFis[k][l] & 1);
333 vvFos[f >> 1].push_back(k);
334 }
335 if(fUpdate)
336 vUpdates[k] = true;
337 }
338 vvFos[i].clear();
339 vPfUpdates[f >> 1] = true;
340 return count + Remove(i);
341 }
342 int ReplaceByConst(int i, bool c) {
343 if(nVerbose > 4) {
344 std::stringstream ss;
345 ss << "\t\t\t\treplace Gate " << std::setw(5) << i << " by Const " << c;
346 Print(ss.str(), true);
347 }
348 int count = 0;
349 for(unsigned j = 0; j < vvFos[i].size(); j++) {
350 int k = vvFos[i][j];
351 int l = FindFi(k, i);
352 assert(l >= 0);
353 bool fc = c ^ (vvFis[k][l] & 1);
354 this->DecRef(vvCs[k][l]);
355 vvCs[k].erase(vvCs[k].begin() + l);
356 vvFis[k].erase(vvFis[k].begin() + l);
357 if(fc) {
358 if(vvFis[k].size() == 1)
359 count += Replace(k, vvFis[k][0]);
360 else
361 vUpdates[k] = true;
362 } else
363 count += ReplaceByConst(k, 0);
364 }
365 count += vvFos[i].size();
366 vvFos[i].clear();
367 return count + Remove(i);
368 }
369 inline void NewGate(int &pos) {
370 while(pos != nObjsAlloc && (!vvFis[pos].empty() || !vvFos[pos].empty()))
371 pos++;
372 if(nVerbose > 5) {
373 std::stringstream ss;
374 ss << "\t\t\t\t\tcreate Gate " << std::setw(5) << pos;
375 Print(ss.str(), true);
376 }
377 if(pos == nObjsAlloc) {
378 nObjsAlloc++;
379 vvFis.resize(nObjsAlloc);
380 vvFos.resize(nObjsAlloc);
381 if(fLevel) {
382 vLevels.resize(nObjsAlloc);
383 vSlacks.resize(nObjsAlloc);
384 vvFiSlacks.resize(nObjsAlloc);
385 }
386 vFs.resize(nObjsAlloc, LitMax);
387 vGs.resize(nObjsAlloc, LitMax);
388 vvCs.resize(nObjsAlloc);
389 vUpdates.resize(nObjsAlloc);
390 vPfUpdates.resize(nObjsAlloc);
391 }
392 }
393 void MarkFiCone_rec(std::vector<bool> &vMarks, int i) const {
394 if(vMarks[i])
395 return;
396 vMarks[i] = true;
397 for(unsigned j = 0; j < vvFis[i].size(); j++)
398 MarkFiCone_rec(vMarks, vvFis[i][j] >> 1);
399 }
400 void MarkFoCone_rec(std::vector<bool> &vMarks, int i) const {
401 if(vMarks[i])
402 return;
403 vMarks[i] = true;
404 for(unsigned j = 0; j < vvFos[i].size(); j++)
405 MarkFoCone_rec(vMarks, vvFos[i][j]);
406 }
407 bool IsFoConeShared_rec(std::vector<int> &vVisits, int i, int visitor) const {
408 if(vVisits[i] == visitor)
409 return false;
410 if(vVisits[i])
411 return true;
412 vVisits[i] = visitor;
413 for(unsigned j = 0; j < vvFos[i].size(); j++)
414 if(IsFoConeShared_rec(vVisits, vvFos[i][j], visitor))
415 return true;
416 return false;
417 }
418 inline bool IsFoConeShared(int i) const {
419 std::vector<int> vVisits(nObjsAlloc);
420 for(unsigned j = 0; j < vvFos[i].size(); j++)
421 if(IsFoConeShared_rec(vVisits, vvFos[i][j], j + 1))
422 return true;
423 return false;
424 }
425
426private: // Level calculation
427 inline void add(std::vector<bool> &a, unsigned i) {
428 if(a.size() <= i) {
429 a.resize(i + 1);
430 a[i] = true;
431 return;
432 }
433 for(; i < a.size() && a[i]; i++)
434 a[i] = false;
435 if(i == a.size())
436 a.resize(i + 1);
437 a[i] = true;
438 }
439 inline bool balanced(std::vector<bool> const &a) {
440 for(unsigned i = 0; i < a.size() - 1; i++)
441 if(a[i])
442 return false;
443 return true;
444 }
445 inline bool noexcess(std::vector<bool> const &a, unsigned i) {
446 if(a.size() <= i)
447 return false;
448 for(unsigned j = i; j < a.size(); j++)
449 if(!a[j])
450 return true;
451 for(unsigned j = 0; j < i; j++)
452 if(a[j])
453 return false;
454 return true;
455 }
456 inline void ComputeLevel() {
457 for(std::list<int>::iterator it = vObjs.begin(); it != vObjs.end(); it++) {
458 if(vvFis[*it].size() == 2)
459 vLevels[*it] = std::max(vLevels[vvFis[*it][0] >> 1], vLevels[vvFis[*it][1] >> 1]) + 1;
460 else {
461 std::vector<bool> lev;
462 for(unsigned j = 0; j < vvFis[*it].size(); j++)
463 add(lev, vLevels[vvFis[*it][j] >> 1]);
464 if(balanced(lev))
465 vLevels[*it] = (int)lev.size() - 1;
466 else
467 vLevels[*it] = (int)lev.size();
468 }
469 }
470 if(nMaxLevels == -1)
471 nMaxLevels = CountLevels();
472 for(unsigned i = 0; i < vPos.size(); i++) {
473 vvFiSlacks[vPos[i]].resize(1);
474 vvFiSlacks[vPos[i]][0] = nMaxLevels - vLevels[vvFis[vPos[i]][0] >> 1];
475 }
476 for(std::list<int>::reverse_iterator it = vObjs.rbegin(); it != vObjs.rend(); it++) {
477 vSlacks[*it] = nMaxLevels;
478 for(unsigned j = 0; j < vvFos[*it].size(); j++) {
479 int k = vvFos[*it][j];
480 int l = FindFi(k, *it);
481 assert(l >= 0);
482 vSlacks[*it] = std::min(vSlacks[*it], vvFiSlacks[k][l]);
483 }
484 vvFiSlacks[*it].resize(vvFis[*it].size());
485 for(unsigned j = 0; j < vvFis[*it].size(); j++)
486 vvFiSlacks[*it][j] = vSlacks[*it] + vLevels[*it] - 1 - vLevels[vvFis[*it][j] >> 1];
487 }
488 }
489
490private: // Cost function
491 inline void ShufflePis(int seed) {
492 srand(seed);
493 for(int i = (int)vPis.size() - 1; i > 0; i--)
494 std::swap(vPis[i], vPis[rand() % (i + 1)]);
495 }
496 inline bool CostCompare(int a, int b) const { // return (cost(a) > cost(b))
497 int a0 = a >> 1;
498 int b0 = b >> 1;
499 if(vvFis[a0].empty() && vvFis[b0].empty())
500 return std::find(find(vPis.begin(), vPis.end(), a0), vPis.end(), b0) != vPis.end();
501 if(vvFis[a0].empty() && !vvFis[b0].empty())
502 return false;
503 if(!vvFis[a0].empty() && vvFis[b0].empty())
504 return true;
505 if(vvFos[a0].size() > vvFos[b0].size())
506 return false;
507 if(vvFos[a0].size() < vvFos[b0].size())
508 return true;
509 bool ac = a & 1;
510 bool bc = b & 1;
511 switch(nSortType) {
512 case 0:
513 return std::find(find(vObjs.begin(), vObjs.end(), a0), vObjs.end(), b0) == vObjs.end();
514 case 1:
515 return this->man->OneCount(this->man->LitNotCond(vFs[a0], ac)) < this->man->OneCount(this->man->LitNotCond(vFs[b0], bc));
516 case 2:
517 return this->man->OneCount(vFs[a0]) < this->man->OneCount(vFs[b0]);
518 case 3:
519 return this->man->OneCount(this->man->LitNot(vFs[a0])) < this->man->OneCount(vFs[b0]); // pseudo random
520 default:
521 return false; // no sorting
522 }
523 }
524 inline bool SortFis(int i) {
525 if(nVerbose > 5) {
526 std::stringstream ss;
527 ss << "\t\t\t\tsort FIs Gate " << std::setw(5) << i;
528 Print(ss.str(), true);
529 }
530 bool fSort = false;
531 for(int p = 1; p < (int)vvFis[i].size(); p++) {
532 int f = vvFis[i][p];
533 lit c = vvCs[i][p];
534 int q = p - 1;
535 for(; q >= 0 && CostCompare(f, vvFis[i][q]); q--) {
536 vvFis[i][q + 1] = vvFis[i][q];
537 vvCs[i][q + 1] = vvCs[i][q];
538 }
539 if(q + 1 != p) {
540 fSort = true;
541 vvFis[i][q + 1] = f;
542 vvCs[i][q + 1] = c;
543 }
544 }
545 if(nVerbose > 5)
546 for(unsigned j = 0; j < vvFis[i].size(); j++) {
547 std::stringstream ss;
548 ss << "\t\t\t\t\tFI " << j << " = "
549 << std::setw(5) << (vvFis[i][j] >> 1) << "(" << (vvFis[i][j] & 1) << ")";
550 Print(ss.str(), true);
551 }
552 return fSort;
553 }
554
555private: // Symbolic simulation
556 inline lit LitFi(int i, int j) const {
557 int i0 = vvFis[i][j] >> 1;
558 bool c0 = vvFis[i][j] & 1;
559 return this->man->LitNotCond(vFs[i0], c0);
560 }
561 inline lit LitFi(int i, int j, std::vector<lit> const &vFs_) const {
562 int i0 = vvFis[i][j] >> 1;
563 bool c0 = vvFis[i][j] & 1;
564 return this->man->LitNotCond(vFs_[i0], c0);
565 }
566 inline void Build(int i, std::vector<lit> &vFs_) const {
567 if(nVerbose > 6) {
568 std::stringstream ss;
569 ss << "\t\t\t\tbuilding Gate" << std::setw(5) << i;
570 Print(ss.str(), nVerbose > 7);
571 }
572 this->Update(vFs_[i], this->man->Const1());
573 for(unsigned j = 0; j < vvFis[i].size(); j++)
574 this->Update(vFs_[i], this->man->And(vFs_[i], LitFi(i, j, vFs_)));
575 }
576 inline void Build(bool fPfUpdate = true) {
577 if(nVerbose > 6)
578 Print("\t\t\tBuild", true);
579 for(std::list<int>::iterator it = vObjs.begin(); it != vObjs.end(); it++)
580 if(vUpdates[*it]) {
581 lit x = vFs[*it];
582 this->IncRef(x);
583 Build(*it, vFs);
584 this->DecRef(x);
585 if(!this->man->LitIsEq(x, vFs[*it]))
586 for(unsigned j = 0; j < vvFos[*it].size(); j++)
587 vUpdates[vvFos[*it][j]] = true;
588 }
589 if(fPfUpdate)
590 for(std::list<int>::iterator it = vObjs.begin(); it != vObjs.end(); it++)
591 vPfUpdates[*it] = vPfUpdates[*it] || vUpdates[*it];
592 for(std::list<int>::iterator it = vObjs.begin(); it != vObjs.end(); it++)
593 vUpdates[*it] = false;
594 assert(AllFalse(vUpdates));
595 }
596 void BuildFoConeCompl(int i, std::vector<lit> &vPoFsCompl) const {
597 if(nVerbose > 6) {
598 std::stringstream ss;
599 ss << "\t\t\tBuild with complemented Gate " << std::setw(5) << i;
600 Print(ss.str(), true);
601 }
602 std::vector<lit> vFsCompl;
603 this->CopyVec(vFsCompl, vFs);
604 vFsCompl[i] = this->man->LitNot(vFs[i]);
605 std::vector<bool> vUpdatesCompl(nObjsAlloc);
606 for(unsigned j = 0; j < vvFos[i].size(); j++)
607 vUpdatesCompl[vvFos[i][j]] = true;
608 for(std::list<int>::const_iterator it = vObjs.begin(); it != vObjs.end(); it++)
609 if(vUpdatesCompl[*it]) {
610 Build(*it, vFsCompl);
611 if(!this->man->LitIsEq(vFsCompl[*it], vFs[*it]))
612 for(unsigned j = 0; j < vvFos[*it].size(); j++)
613 vUpdatesCompl[vvFos[*it][j]] = true;
614 }
615 for(unsigned j = 0; j < vPos.size(); j++)
616 this->Update(vPoFsCompl[j], LitFi(vPos[j], 0, vFsCompl));
617 this->DelVec(vFsCompl);
618 }
619
620private: // CSPF
621 inline int RemoveRedundantFis(int i, int block_i0 = -1, unsigned j = 0) {
622 int count = 0;
623 for(; j < vvFis[i].size(); j++) {
624 if(block_i0 == (vvFis[i][j] >> 1))
625 continue;
626 lit x = this->man->Const1();
627 this->IncRef(x);
628 for(unsigned jj = 0; jj < vvFis[i].size(); jj++)
629 if(j != jj)
630 this->Update(x, this->man->And(x, LitFi(i, jj)));
631 this->Update(x, this->man->Or(this->man->LitNot(x), vGs[i]));
632 this->Update(x, this->man->Or(x, LitFi(i, j)));
633 this->DecRef(x);
634 if(this->man->IsConst1(x)) {
635 int i0 = vvFis[i][j] >> 1;
636 if(nVerbose > 4) {
637 std::stringstream ss;
638 ss << "\t\t\t\t[Rrfi] remove Wire " << std::setw(5) << i0 << "(" << (vvFis[i][j] & 1) << ")"
639 << " -> " << std::setw(5) << i;
640 Print(ss.str(), true);
641 }
642 Disconnect(i, i0, j--);
643 count++;
644 }
645 }
646 return count;
647 }
648 inline void CalcG(int i) {
649 this->Update(vGs[i], this->man->Const1());
650 for(unsigned j = 0; j < vvFos[i].size(); j++) {
651 int k = vvFos[i][j];
652 int l = FindFi(k, i);
653 assert(l >= 0);
654 this->Update(vGs[i], this->man->And(vGs[i], vvCs[k][l]));
655 }
656 }
657 inline int CalcC(int i) {
658 int count = 0;
659 for(unsigned j = 0; j < vvFis[i].size(); j++) {
660 lit x = this->man->Const1();
661 this->IncRef(x);
662 for(unsigned jj = j + 1; jj < vvFis[i].size(); jj++)
663 this->Update(x, this->man->And(x, LitFi(i, jj)));
664 this->Update(x, this->man->Or(this->man->LitNot(x), vGs[i]));
665 int i0 = vvFis[i][j] >> 1;
666 if(this->man->IsConst1(this->man->Or(x, LitFi(i, j)))) {
667 if(nVerbose > 4) {
668 std::stringstream ss;
669 ss << "\t\t\t\t[Cspf] remove Wire " << std::setw(5) << i0 << "(" << (vvFis[i][j] & 1) << ")"
670 << " -> " << std::setw(5) << i;
671 Print(ss.str(), true);
672 }
673 Disconnect(i, i0, j--);
674 count++;
675 } else if(!this->man->LitIsEq(vvCs[i][j], x)) {
676 this->Update(vvCs[i][j], x);
677 vPfUpdates[i0] = true;
678 }
679 this->DecRef(x);
680 }
681 return count;
682 }
683 int Cspf(bool fSortRemove, int block = -1, int block_i0 = -1) {
684 if(nVerbose > 3)
685 PrintPfHeader("Cspf", block, block_i0);
686 if(state != cspf)
687 for(std::list<int>::iterator it = vObjs.begin(); it != vObjs.end(); it++)
688 vPfUpdates[*it] = true;
689 state = cspf;
690 int count = 0;
691 for(std::list<int>::reverse_iterator it = vObjs.rbegin(); it != vObjs.rend();) {
692 if(vvFos[*it].empty()) {
693 if(nVerbose > 3) {
694 std::stringstream ss;
695 ss << "\t\t\tremove unused Gate " << std::setw(5) << *it;
696 Print(ss.str(), nVerbose > 4);
697 }
698 count += Remove(*it);
699 it = std::list<int>::reverse_iterator(vObjs.erase(--(it.base())));
700 continue;
701 }
702 if(!vPfUpdates[*it]) {
703 it++;
704 continue;
705 }
706 if(nVerbose > 3) {
707 std::stringstream ss;
708 ss << "\t\t\tprocessing Gate " << std::setw(5) << *it
709 << " (" << std::setw(5) << std::distance(vObjs.rbegin(), it) + 1
710 << "/" << std::setw(5) << vObjs.size() << ")";
711 Print(ss.str(), nVerbose > 4);
712 }
713 CalcG(*it);
714 if(fSortRemove) {
715 if(*it != block)
716 SortFis(*it), count += RemoveRedundantFis(*it);
717 else if(block_i0 != -1)
718 count += RemoveRedundantFis(*it, block_i0);
719 }
720 count += CalcC(*it);
721 vPfUpdates[*it] = false;
722 assert(!vvFis[*it].empty());
723 if(vvFis[*it].size() == 1) {
724 count += Replace(*it, vvFis[*it][0]);
725 it = std::list<int>::reverse_iterator(vObjs.erase(--(it.base())));
726 continue;
727 }
728 it++;
729 }
730 Build(false);
731 assert(AllFalse(vPfUpdates));
732 if(fLevel)
733 ComputeLevel();
734 return count;
735 }
736
737private: // MSPF
738 inline bool MspfCalcG(int i) {
739 lit g = vGs[i];
740 this->IncRef(g);
741 std::vector<lit> vPoFsCompl(vPos.size(), LitMax);
742 BuildFoConeCompl(i, vPoFsCompl);
743 this->Update(vGs[i], this->man->Const1());
744 for(unsigned j = 0; j < vPos.size(); j++) {
745 lit x = this->man->LitNot(this->Xor(vPoFs[j], vPoFsCompl[j]));
746 this->IncRef(x);
747 this->Update(x, this->man->Or(x, vvCs[vPos[j]][0]));
748 this->Update(vGs[i], this->man->And(vGs[i], x));
749 this->DecRef(x);
750 }
751 this->DelVec(vPoFsCompl);
752 this->DecRef(g);
753 return !this->man->LitIsEq(vGs[i], g);
754 }
755 inline int MspfCalcC(int i, int block_i0 = -1) {
756 for(unsigned j = 0; j < vvFis[i].size(); j++) {
757 lit x = this->man->Const1();
758 this->IncRef(x);
759 for(unsigned jj = 0; jj < vvFis[i].size(); jj++)
760 if(j != jj)
761 this->Update(x, this->man->And(x, LitFi(i, jj)));
762 this->Update(x, this->man->Or(this->man->LitNot(x), vGs[i]));
763 int i0 = vvFis[i][j] >> 1;
764 if(i0 != block_i0 && this->man->IsConst1(this->man->Or(x, LitFi(i, j)))) {
765 if(nVerbose > 4) {
766 std::stringstream ss;
767 ss << "\t\t\t\t[Mspf] remove Wire " << std::setw(5) << i0 << "(" << (vvFis[i][j] & 1) << ")"
768 << " -> " << std::setw(5) << i;
769 Print(ss.str(), true);
770 }
771 Disconnect(i, i0, j);
772 this->DecRef(x);
773 return RemoveRedundantFis(i, block_i0, j) + 1;
774 } else if(!this->man->LitIsEq(vvCs[i][j], x)) {
775 this->Update(vvCs[i][j], x);
776 vPfUpdates[i0] = true;
777 }
778 this->DecRef(x);
779 }
780 return 0;
781 }
782 int Mspf(bool fSort, int block = -1, int block_i0 = -1) {
783 if(nVerbose > 3)
784 PrintPfHeader("Mspf", block, block_i0);
785 assert(AllFalse(vUpdates));
786 vFoConeShared.resize(nObjsAlloc);
787 if(state != mspf)
788 for(std::list<int>::iterator it = vObjs.begin(); it != vObjs.end(); it++)
789 vPfUpdates[*it] = true;
790 state = mspf;
791 int count = 0;
792 int restarts = 0;
793 for(std::list<int>::reverse_iterator it = vObjs.rbegin(); it != vObjs.rend();) {
794 if(vvFos[*it].empty()) {
795 if(nVerbose > 3) {
796 std::stringstream ss;
797 ss << "\t\t\tremove unused Gate " << std::setw(5) << *it;
798 Print(ss.str(), nVerbose > 4);
799 }
800 count += Remove(*it);
801 it = std::list<int>::reverse_iterator(vObjs.erase(--(it.base())));
802 continue;
803 }
804 if(!vFoConeShared[*it] && !vPfUpdates[*it] && (vvFos[*it].size() == 1 || !IsFoConeShared(*it))) {
805 it++;
806 continue;
807 }
808 if(nVerbose > 3) {
809 std::stringstream ss;
810 ss << "\t\t\tprocessing Gate " << std::setw(5) << *it
811 << " (" << std::setw(5) << std::distance(vObjs.rbegin(), it) + 1
812 << "/" << std::setw(5) << vObjs.size() << ")"
813 << ", #restarts = " << std::setw(3) << restarts;
814 Print(ss.str(), nVerbose > 4);
815 }
816 if(vvFos[*it].size() == 1 || !IsFoConeShared(*it)) {
817 if(vFoConeShared[*it]) {
818 vFoConeShared[*it] = false;
819 lit g = vGs[*it];
820 this->IncRef(g);
821 CalcG(*it);
822 this->DecRef(g);
823 if(g == vGs[*it] && !vPfUpdates[*it]) {
824 it++;
825 continue;
826 }
827 } else
828 CalcG(*it);
829 } else {
830 vFoConeShared[*it] = true;
831 if(!MspfCalcG(*it) && !vPfUpdates[*it]) {
832 it++;
833 continue;
834 }
835 bool IsConst1 = this->man->IsConst1(this->man->Or(vGs[*it], vFs[*it]));
836 bool IsConst0 = IsConst1? false: this->man->IsConst1(this->man->Or(vGs[*it], this->man->LitNot(vFs[*it])));
837 if(IsConst1 || IsConst0) {
838 count += ReplaceByConst(*it, (int)IsConst1);
839 vObjs.erase(--(it.base()));
840 Build();
841 it = vObjs.rbegin();
842 restarts++;
843 continue;
844 }
845 }
846 if(fSort && block != *it)
847 SortFis(*it);
848 if(int diff = (block == *it)? MspfCalcC(*it, block_i0): MspfCalcC(*it)) {
849 count += diff;
850 assert(!vvFis[*it].empty());
851 if(vvFis[*it].size() == 1) {
852 count += Replace(*it, vvFis[*it][0]);
853 vObjs.erase(--(it.base()));
854 }
855 Build();
856 it = vObjs.rbegin();
857 restarts++;
858 continue;
859 }
860 vPfUpdates[*it] = false;
861 it++;
862 }
863 assert(AllFalse(vUpdates));
864 assert(AllFalse(vPfUpdates));
865 if(fLevel)
866 ComputeLevel();
867 return count;
868 }
869
870private: // Merge/decompose one
871 inline int TrivialMergeOne(int i) {
872 int count = 0;
873 std::vector<int> vFisOld = vvFis[i];
874 std::vector<lit> vCsOld = vvCs[i];
875 vvFis[i].clear();
876 vvCs[i].clear();
877 for(unsigned j = 0; j < vFisOld.size(); j++) {
878 int i0 = vFisOld[j] >> 1;
879 int c0 = vFisOld[j] & 1;
880 if(vvFis[i0].empty() || vvFos[i0].size() > 1 || c0) {
881 if(nVerbose > 3) {
882 std::stringstream ss;
883 ss << "\t\t[TrivialMerge] adding Wire " << std::setw(5) << i0 << "(" << c0 << ")"
884 << " -> " << std::setw(5) << i;
885 Print(ss.str(), true);
886 }
887 vvFis[i].push_back(vFisOld[j]);
888 vvCs[i].push_back(vCsOld[j]);
889 continue;
890 }
891 vPfUpdates[i] = vPfUpdates[i] | vPfUpdates[i0];
892 vvFos[i0].erase(find(vvFos[i0].begin(), vvFos[i0].end(), i));
893 count++;
894 typename std::vector<int>::iterator itfi = vFisOld.begin() + j;
895 typename std::vector<lit>::iterator itc = vCsOld.begin() + j;
896 for(unsigned jj = 0; jj < vvFis[i0].size(); jj++) {
897 int f = vvFis[i0][jj];
898 std::vector<int>::iterator it = find(vvFis[i].begin(), vvFis[i].end(), f);
899 if(it == vvFis[i].end()) {
900 vvFos[f >> 1].push_back(i);
901 itfi = vFisOld.insert(itfi, f);
902 itc = vCsOld.insert(itc, vvCs[i0][jj]);
903 this->IncRef(*itc);
904 itfi++;
905 itc++;
906 count--;
907 } else {
908 assert(state == none);
909 }
910 }
911 count += Remove(i0, false);
912 vObjs.erase(find(vObjs.begin(), vObjs.end(), i0));
913 vFisOld.erase(itfi);
914 this->DecRef(*itc);
915 vCsOld.erase(itc);
916 j--;
917 }
918 return count;
919 }
920 inline int TrivialDecomposeOne(std::list<int>::iterator const &it, int &pos) {
921 if(nVerbose > 2) {
922 std::stringstream ss;
923 ss << "\tTrivialDecompose Gate " << std::setw(5) << *it;
924 Print(ss.str() , nVerbose > 3);
925 }
926 assert(vvFis[*it].size() > 2);
927 int count = 2 - vvFis[*it].size();
928 while(vvFis[*it].size() > 2) {
929 int f0 = vvFis[*it].back();
930 lit c0 = vvCs[*it].back();
931 Disconnect(*it, f0 >> 1, vvFis[*it].size() - 1, false, false);
932 int f1 = vvFis[*it].back();
933 lit c1 = vvCs[*it].back();
934 Disconnect(*it, f1 >> 1, vvFis[*it].size() - 1, false, false);
935 NewGate(pos);
936 Connect(pos, f1, false, false, c1);
937 Connect(pos, f0, false, false, c0);
938 if(!vPfUpdates[*it]) {
939 if(state == cspf)
940 this->Update(vGs[pos], vGs[*it]);
941 else if(state == mspf) {
942 lit x = this->man->Const1();
943 this->IncRef(x);
944 for(unsigned j = 0; j < vvFis[*it].size(); j++)
945 this->Update(x, this->man->And(x, LitFi(*it, j)));
946 this->Update(vGs[pos], this->man->Or(this->man->LitNot(x), vGs[*it]));
947 this->DecRef(x);
948 }
949 }
950 Connect(*it, pos << 1, false, false, vGs[pos]);
951 vObjs.insert(it, pos);
952 Build(pos, vFs);
953 }
954 return count;
955 }
956 inline int BalancedDecomposeOne(std::list<int>::iterator const &it, int &pos) {
957 if(nVerbose > 2) {
958 std::stringstream ss;
959 ss << "\tBalancedDecompose Gate " << std::setw(5) << *it;
960 Print(ss.str(), nVerbose > 3);
961 }
962 assert(fLevel);
963 assert(vvFis[*it].size() > 2);
964 for(int p = 1; p < (int)vvFis[*it].size(); p++) {
965 int f = vvFis[*it][p];
966 lit c = vvCs[*it][p];
967 int q = p - 1;
968 for(; q >= 0 && vLevels[f >> 1] > vLevels[vvFis[*it][q] >> 1]; q--) {
969 vvFis[*it][q + 1] = vvFis[*it][q];
970 vvCs[*it][q + 1] = vvCs[*it][q];
971 }
972 if(q + 1 != p) {
973 vvFis[*it][q + 1] = f;
974 vvCs[*it][q + 1] = c;
975 }
976 }
977 int count = 2 - vvFis[*it].size();
978 while(vvFis[*it].size() > 2) {
979 int f0 = vvFis[*it].back();
980 lit c0 = vvCs[*it].back();
981 Disconnect(*it, f0 >> 1, vvFis[*it].size() - 1, false, false);
982 int f1 = vvFis[*it].back();
983 lit c1 = vvCs[*it].back();
984 Disconnect(*it, f1 >> 1, vvFis[*it].size() - 1, false, false);
985 NewGate(pos);
986 Connect(pos, f1, false, false, c1);
987 Connect(pos, f0, false, false, c0);
988 Connect(*it, pos << 1, false, false);
989 Build(pos, vFs);
990 vLevels[pos] = std::max(vLevels[f0 >> 1], vLevels[f1 >> 1]) + 1;
991 vObjs.insert(it, pos);
992 int f = vvFis[*it].back();
993 lit c = vvCs[*it].back();
994 int q = (int)vvFis[*it].size() - 2;
995 for(; q >= 0 && vLevels[f >> 1] > vLevels[vvFis[*it][q] >> 1]; q--) {
996 vvFis[*it][q + 1] = vvFis[*it][q];
997 vvCs[*it][q + 1] = vvCs[*it][q];
998 }
999 if(q + 1 != (int)vvFis[*it].size() - 1) {
1000 vvFis[*it][q + 1] = f;
1001 vvCs[*it][q + 1] = c;
1002 }
1003 }
1004 vPfUpdates[*it] = true;
1005 return count;
1006 }
1007
1008public: // Merge/decompose
1009 int TrivialMerge() {
1010 int count = 0;
1011 for(std::list<int>::reverse_iterator it = vObjs.rbegin(); it != vObjs.rend();) {
1012 count += TrivialMergeOne(*it);
1013 it++;
1014 }
1015 return count;
1016 }
1017 int TrivialDecompose() {
1018 int count = 0;
1019 int pos = vPis.size() + 1;
1020 for(std::list<int>::iterator it = vObjs.begin(); it != vObjs.end(); it++)
1021 if(vvFis[*it].size() > 2)
1022 count += TrivialDecomposeOne(it, pos);
1023 return count;
1024 }
1025 int Decompose() {
1026 int count = 0;
1027 int pos = vPis.size() + 1;
1028 for(std::list<int>::iterator it = vObjs.begin(); it != vObjs.end(); it++) {
1029 std::set<int> s1(vvFis[*it].begin(), vvFis[*it].end());
1030 assert(s1.size() == vvFis[*it].size());
1031 std::list<int>::iterator it2 = it;
1032 for(it2++; it2 != vObjs.end(); it2++) {
1033 std::set<int> s2(vvFis[*it2].begin(), vvFis[*it2].end());
1034 std::set<int> s;
1035 std::set_intersection(s1.begin(), s1.end(), s2.begin(), s2.end(), std::inserter(s, s.begin()));
1036 if(s.size() > 1) {
1037 if(s == s1) {
1038 if(s == s2) {
1039 if(nVerbose > 2) {
1040 std::stringstream ss;
1041 ss << "\treplace Gate " << std::setw(5) << *it2
1042 << " by Gate " << std::setw(5) << *it;
1043 Print(ss.str() , nVerbose > 3);
1044 }
1045 count += Replace(*it2, *it << 1, false);
1046 it2 = vObjs.erase(it2);
1047 it2--;
1048 } else {
1049 if(nVerbose > 2) {
1050 std::stringstream ss;
1051 ss << "\tdecompose Gate " << std::setw(5) << *it2
1052 << " by Gate " << std::setw(5) << *it;
1053 Print(ss.str() , nVerbose > 3);
1054 }
1055 for(std::set<int>::iterator it3 = s.begin(); it3 != s.end(); it3++) {
1056 unsigned j = find(vvFis[*it2].begin(), vvFis[*it2].end(), *it3) - vvFis[*it2].begin();
1057 Disconnect(*it2, *it3 >> 1, j, false);
1058 }
1059 count += s.size();
1060 if(std::find(vvFis[*it2].begin(), vvFis[*it2].end(), *it << 1) == vvFis[*it2].end()) {
1061 Connect(*it2, *it << 1, false, false);
1062 count--;
1063 }
1064 vPfUpdates[*it2] = true;
1065 }
1066 continue;
1067 }
1068 if(s == s2) {
1069 it = vObjs.insert(it, *it2);
1070 vObjs.erase(it2);
1071 } else {
1072 NewGate(pos);
1073 if(nVerbose > 2) {
1074 std::stringstream ss;
1075 ss << "\tdecompose Gate " << std::setw(5) << *it
1076 << " and " << std::setw(5) << *it2
1077 << " by a new Gate " << std::setw(5) << pos;
1078 Print(ss.str() , nVerbose > 3);
1079 }
1080 if(nVerbose > 4) {
1081 std::stringstream ss;
1082 ss << "\t\tIntersection:";
1083 for(std::set<int>::iterator it3 = s.begin(); it3 != s.end(); it3++)
1084 ss << " " << (*it3 >> 1) << "(" << (*it3 & 1) << ")";
1085 Print(ss.str(), true);
1086 }
1087 for(std::set<int>::iterator it3 = s.begin(); it3 != s.end(); it3++)
1088 Connect(pos, *it3, false, false);
1089 count -= s.size();
1090 it = vObjs.insert(it, pos);
1091 Build(pos, vFs);
1092 vPfUpdates[*it] = true;
1093 }
1094 s1 = s;
1095 it2 = it;
1096 }
1097 }
1098 if(vvFis[*it].size() > 2)
1099 count += TrivialDecomposeOne(it, pos);
1100 }
1101 return count;
1102 }
1103
1104private: // Save/load
1105 inline void Save(TransductionBackup<Man, lit, LitMax> &b) const {
1106 b.man = this->man;
1107 b.nObjsAlloc = nObjsAlloc;
1108 b.state = state;
1109 b.vObjs = vObjs;
1110 b.vvFis = vvFis;
1111 b.vvFos = vvFos;
1112 b.vLevels = vLevels;
1113 b.vSlacks = vSlacks;
1114 b.vvFiSlacks = vvFiSlacks;
1115 this->CopyVec(b.vFs, vFs);
1116 this->CopyVec(b.vGs, vGs);
1117 this->CopyVec(b.vvCs, vvCs);
1118 b.vUpdates = vUpdates;
1119 b.vPfUpdates = vPfUpdates;
1120 b.vFoConeShared = vFoConeShared;
1121 }
1122 inline void Load(TransductionBackup<Man, lit, LitMax> const &b) {
1123 nObjsAlloc = b.nObjsAlloc;
1124 state = b.state;
1125 vObjs = b.vObjs;
1126 vvFis = b.vvFis;
1127 vvFos = b.vvFos;
1128 vLevels = b.vLevels;
1129 vSlacks = b.vSlacks;
1130 vvFiSlacks = b.vvFiSlacks;
1131 this->CopyVec(vFs, b.vFs);
1132 this->CopyVec(vGs, b.vGs);
1133 this->CopyVec(vvCs, b.vvCs);
1134 vUpdates = b.vUpdates;
1135 vPfUpdates = b.vPfUpdates;
1136 vFoConeShared = b.vFoConeShared;
1137 }
1138
1139private: // Connectable condition
1140 inline bool TryConnect(int i, int i0, bool c0) {
1141 int f = (i0 << 1) ^ (int)c0;
1142 if(find(vvFis[i].begin(), vvFis[i].end(), f) == vvFis[i].end()) {
1143 lit x = this->man->Or(this->man->LitNot(vFs[i]), vGs[i]);
1144 this->IncRef(x);
1145 if(this->man->IsConst1(this->man->Or(x, this->man->LitNotCond(vFs[i0], c0)))) {
1146 this->DecRef(x);
1147 if(nVerbose > 3) {
1148 std::stringstream ss;
1149 ss << "\t\t[TryConnect] adding Wire " << std::setw(5) << i0 << "(" << c0 << ")"
1150 << " -> " << std::setw(5) << i;
1151 Print(ss.str(), true);
1152 }
1153 Connect(i, f, true);
1154 return true;
1155 }
1156 this->DecRef(x);
1157 }
1158 return false;
1159 }
1160
1161public: // Resubs
1162 int Resub(bool fMspf) {
1163 int count = fMspf? Mspf(true): Cspf(true);
1164 int nodes = CountNodes();
1165 TransductionBackup<Man, lit, LitMax> b;
1166 Save(b);
1167 int count_ = count;
1168 std::list<int> targets = vObjs;
1169 for(std::list<int>::reverse_iterator it = targets.rbegin(); it != targets.rend(); it++) {
1170 if(nVerbose > 1) {
1171 std::stringstream ss;
1172 ss << "[Resub] processing Gate " << std::setw(5) << *it
1173 << " (" << std::setw(5) << std::distance(targets.rbegin(), it) + 1
1174 << "/" << std::setw(5) << targets.size() << ")";
1175 PrintStats(ss.str(), nVerbose > 2);
1176 }
1177 if(vvFos[*it].empty())
1178 continue;
1179 count += TrivialMergeOne(*it);
1180 std::vector<bool> lev;
1181 if(fLevel) {
1182 for(unsigned j = 0; j < vvFis[*it].size(); j++)
1183 add(lev, vLevels[vvFis[*it][j] >> 1]);
1184 if((int)lev.size() > vLevels[*it] + vSlacks[*it]) {
1185 Load(b);
1186 count = count_;
1187 continue;
1188 }
1189 lev.resize(vLevels[*it] + vSlacks[*it]);
1190 }
1191 bool fConnect = false;
1192 std::vector<bool> vMarks(nObjsAlloc);
1193 MarkFoCone_rec(vMarks, *it);
1194 std::list<int> targets2 = vObjs;
1195 for(std::list<int>::iterator it2 = targets2.begin(); it2 != targets2.end(); it2++) {
1196 if(fLevel && (int)lev.size() > vLevels[*it] + vSlacks[*it])
1197 break;
1198 if(!vMarks[*it2] && !vvFos[*it2].empty())
1199 if(!fLevel || noexcess(lev, vLevels[*it2]))
1200 if(TryConnect(*it, *it2, false) || TryConnect(*it, *it2, true)) {
1201 fConnect = true;
1202 count--;
1203 if(fLevel)
1204 add(lev, vLevels[*it2]);
1205 }
1206 }
1207 if(fConnect) {
1208 if(fMspf) {
1209 Build();
1210 count += Mspf(true, *it);
1211 } else {
1212 vPfUpdates[*it] = true;
1213 count += Cspf(true, *it);
1214 }
1215 if(!vvFos[*it].empty()) {
1216 vPfUpdates[*it] = true;
1217 count += fMspf? Mspf(true): Cspf(true);
1218 }
1219 }
1220 if(nodes < CountNodes()) {
1221 Load(b);
1222 count = count_;
1223 continue;
1224 }
1225 if(!vvFos[*it].empty() && vvFis[*it].size() > 2) {
1226 std::list<int>::iterator it2 = find(vObjs.begin(), vObjs.end(), *it);
1227 int pos = nObjsAlloc;
1228 if(fLevel)
1229 count += BalancedDecomposeOne(it2, pos) + (fMspf? Mspf(true): Cspf(true));
1230 else
1231 count += TrivialDecomposeOne(it2, pos);
1232 }
1233 nodes = CountNodes();
1234 Save(b);
1235 count_ = count;
1236 }
1237 if(nVerbose)
1238 PrintStats("Resub", true, 11);
1239 return count;
1240 }
1241 int ResubMono(bool fMspf) {
1242 int count = fMspf? Mspf(true): Cspf(true);
1243 std::list<int> targets = vObjs;
1244 for(std::list<int>::reverse_iterator it = targets.rbegin(); it != targets.rend(); it++) {
1245 if(nVerbose > 1) {
1246 std::stringstream ss;
1247 ss << "[ResubMono] processing Gate " << std::setw(5) << *it
1248 << " (" << std::setw(5) << std::distance(targets.rbegin(), it) + 1
1249 << "/" << std::setw(5) << targets.size() << ")";
1250 PrintStats(ss.str(), nVerbose > 2);
1251 }
1252 if(vvFos[*it].empty())
1253 continue;
1254 count += TrivialMergeOne(*it);
1255 TransductionBackup<Man, lit, LitMax> b;
1256 Save(b);
1257 int count_ = count;
1258 for(unsigned i = 0; i < vPis.size(); i++) {
1259 if(vvFos[*it].empty())
1260 break;
1261 if(nVerbose > 2) {
1262 std::stringstream ss;
1263 ss << "\ttrying a new fanin PI " << std::setw(2) << i;
1264 PrintStats(ss.str(), nVerbose > 3);
1265 }
1266 if(TryConnect(*it, vPis[i], false) || TryConnect(*it, vPis[i], true)) {
1267 count--;
1268 int diff;
1269 if(fMspf) {
1270 Build();
1271 diff = Mspf(true, *it, vPis[i]);
1272 } else {
1273 vPfUpdates[*it] = true;
1274 diff = Cspf(true, *it, vPis[i]);
1275 }
1276 if(diff) {
1277 count += diff;
1278 if(!vvFos[*it].empty()) {
1279 vPfUpdates[*it] = true;
1280 count += fMspf? Mspf(true): Cspf(true);
1281 }
1282 if(fLevel && CountLevels() > nMaxLevels) {
1283 Load(b);
1284 count = count_;
1285 } else {
1286 Save(b);
1287 count_ = count;
1288 }
1289 } else {
1290 Load(b);
1291 count = count_;
1292 }
1293 }
1294 }
1295 if(vvFos[*it].empty())
1296 continue;
1297 std::vector<bool> vMarks(nObjsAlloc);
1298 MarkFoCone_rec(vMarks, *it);
1299 std::list<int> targets2 = vObjs;
1300 for(std::list<int>::iterator it2 = targets2.begin(); it2 != targets2.end(); it2++) {
1301 if(vvFos[*it].empty())
1302 break;
1303 if(nVerbose > 2) {
1304 std::stringstream ss;
1305 ss << "\ttrying a new fanin Gate " << std::setw(5) << *it2
1306 << " (" << std::setw(5) << std::distance(targets2.begin(), it2) + 1
1307 << "/" << std::setw(5) << targets2.size() << ")";
1308 PrintStats(ss.str(), nVerbose > 3);
1309 }
1310 if(!vMarks[*it2] && !vvFos[*it2].empty())
1311 if(TryConnect(*it, *it2, false) || TryConnect(*it, *it2, true)) {
1312 count--;
1313 int diff;
1314 if(fMspf) {
1315 Build();
1316 diff = Mspf(true, *it, *it2);
1317 } else {
1318 vPfUpdates[*it] = true;
1319 diff = Cspf(true, *it, *it2);
1320 }
1321 if(diff) {
1322 count += diff;
1323 if(!vvFos[*it].empty()) {
1324 vPfUpdates[*it] = true;
1325 count += fMspf? Mspf(true): Cspf(true);
1326 }
1327 if(fLevel && CountLevels() > nMaxLevels) {
1328 Load(b);
1329 count = count_;
1330 } else {
1331 Save(b);
1332 count_ = count;
1333 }
1334 } else {
1335 Load(b);
1336 count = count_;
1337 }
1338 }
1339 }
1340 if(vvFos[*it].empty())
1341 continue;
1342 if(vvFis[*it].size() > 2) {
1343 std::list<int>::iterator it2 = find(vObjs.begin(), vObjs.end(), *it);
1344 int pos = nObjsAlloc;
1345 if(fLevel)
1346 count += BalancedDecomposeOne(it2, pos) + (fMspf? Mspf(true): Cspf(true));
1347 else
1348 count += TrivialDecomposeOne(it2, pos);
1349 }
1350 }
1351 if(nVerbose)
1352 PrintStats("ResubMono", true, 11);
1353 return count;
1354 }
1355 int ResubShared(bool fMspf) {
1356 int count = fMspf? Mspf(true): Cspf(true);
1357 std::list<int> targets = vObjs;
1358 for(std::list<int>::reverse_iterator it = targets.rbegin(); it != targets.rend(); it++) {
1359 if(nVerbose > 1) {
1360 std::stringstream ss;
1361 ss << "[ResubShared] processing Gate " << std::setw(5) << *it
1362 << " (" << std::setw(5) << std::distance(targets.rbegin(), it) + 1
1363 << "/" << std::setw(5) << targets.size() << ")";
1364 PrintStats(ss.str(), nVerbose > 2);
1365 }
1366 if(vvFos[*it].empty())
1367 continue;
1368 count += TrivialMergeOne(*it);
1369 bool fConnect = false;
1370 for(unsigned i = 0; i < vPis.size(); i++)
1371 if(TryConnect(*it, vPis[i], false) || TryConnect(*it, vPis[i], true)) {
1372 fConnect |= true;
1373 count--;
1374 }
1375 std::vector<bool> vMarks(nObjsAlloc);
1376 MarkFoCone_rec(vMarks, *it);
1377 for(std::list<int>::iterator it2 = targets.begin(); it2 != targets.end(); it2++)
1378 if(!vMarks[*it2] && !vvFos[*it2].empty())
1379 if(TryConnect(*it, *it2, false) || TryConnect(*it, *it2, true)) {
1380 fConnect |= true;
1381 count--;
1382 }
1383 if(fConnect) {
1384 if(fMspf) {
1385 Build();
1386 count += Mspf(true, *it);
1387 } else {
1388 vPfUpdates[*it] = true;
1389 count += Cspf(true, *it);
1390 }
1391 if(!vvFos[*it].empty()) {
1392 vPfUpdates[*it] = true;
1393 count += fMspf? Mspf(true): Cspf(true);
1394 }
1395 }
1396 }
1397 count += Decompose();
1398 if(nVerbose)
1399 PrintStats("ResubShared", true, 11);
1400 return count;
1401 }
1402
1403public: // Optimization scripts
1404 int RepeatResub(bool fMono, bool fMspf) {
1405 int count = 0;
1406 while(int diff = fMono? ResubMono(fMspf): Resub(fMspf))
1407 count += diff;
1408 return count;
1409 }
1410 int RepeatInner(bool fMspf, bool fInner) {
1411 int count = 0;
1412 while(int diff = RepeatResub(true, fMspf) + RepeatResub(false, fMspf)) {
1413 count += diff;
1414 if(!fInner)
1415 break;
1416 }
1417 return count;
1418 }
1419 int RepeatOuter(bool fMspf, bool fInner, bool fOuter) {
1420 int count = 0;
1421 while(int diff = fMspf? RepeatInner(false, fInner) + RepeatInner(true, fInner): RepeatInner(false, fInner)) {
1422 count += diff;
1423 if(!fOuter)
1424 break;
1425 }
1426 return count;
1427 }
1428 int RepeatAll(bool fFirstMerge, bool fMspfMerge, bool fMspfResub, bool fInner, bool fOuter) {
1429 TransductionBackup<Man, lit, LitMax> b;
1430 Save(b);
1431 int count = 0;
1432 int diff = 0;
1433 if(fFirstMerge)
1434 diff = ResubShared(fMspfMerge);
1435 diff += RepeatOuter(fMspfResub, fInner, fOuter);
1436 if(diff > 0) {
1437 count = diff;
1438 Save(b);
1439 diff = 0;
1440 }
1441 while(true) {
1442 diff += ResubShared(fMspfMerge) + RepeatOuter(fMspfResub, fInner, fOuter);
1443 if(diff > 0) {
1444 count += diff;
1445 Save(b);
1446 diff = 0;
1447 } else {
1448 Load(b);
1449 break;
1450 }
1451 }
1452 return count;
1453 }
1454
1455public: // Cspf/mspf
1456 int Cspf() {
1457 return Cspf(true);
1458 }
1459 int Mspf() {
1460 return Mspf(true);
1461 }
1462
1463private: // Setup
1464 void ImportAig(Gia_Man_t *pGia) {
1465 int i;
1466 Gia_Obj_t *pObj;
1467 nObjsAlloc = Gia_ManObjNum(pGia);
1468 vvFis.resize(nObjsAlloc);
1469 vvFos.resize(nObjsAlloc);
1470 if(fLevel) {
1471 vLevels.resize(nObjsAlloc);
1472 vSlacks.resize(nObjsAlloc);
1473 vvFiSlacks.resize(nObjsAlloc);
1474 }
1475 vFs.resize(nObjsAlloc, LitMax);
1476 vGs.resize(nObjsAlloc, LitMax);
1477 vvCs.resize(nObjsAlloc);
1478 vUpdates.resize(nObjsAlloc);
1479 vPfUpdates.resize(nObjsAlloc);
1480 std::vector<int> v(Gia_ManObjNum(pGia), -1);
1481 int nObjs = 0;
1482 v[Gia_ObjId(pGia, Gia_ManConst0(pGia))] = nObjs << 1;
1483 nObjs++;
1484 Gia_ManForEachCi(pGia, pObj, i) {
1485 v[Gia_ObjId(pGia, pObj)] = nObjs << 1;
1486 vPis.push_back(nObjs);
1487 nObjs++;
1488 }
1489 Gia_ManForEachAnd(pGia, pObj, i) {
1490 int id = Gia_ObjId(pGia, pObj);
1491 if(nVerbose > 5) {
1492 std::stringstream ss;
1493 ss << "\t\t\t\timport Gate " << std::setw(5) << id;
1494 Print(ss.str(), true);
1495 }
1496 int i0 = Gia_ObjId(pGia, Gia_ObjFanin0(pObj));
1497 int i1 = Gia_ObjId(pGia, Gia_ObjFanin1(pObj));
1498 int c0 = Gia_ObjFaninC0(pObj);
1499 int c1 = Gia_ObjFaninC1(pObj);
1500 if(i0 == i1) {
1501 if(c0 == c1)
1502 v[id] = v[i0] ^ c0;
1503 else
1504 v[id] = 0;
1505 } else {
1506 Connect(nObjs , v[i0] ^ c0);
1507 Connect(nObjs, v[i1] ^ c1);
1508 v[id] = nObjs << 1;
1509 vObjs.push_back(nObjs);
1510 nObjs++;
1511 }
1512 }
1513 Gia_ManForEachCo(pGia, pObj, i) {
1514 if(nVerbose > 5) {
1515 std::stringstream ss;
1516 ss << "\t\t\t\timport PO " << std::setw(2) << i;
1517 Print(ss.str(), true);
1518 }
1519 int i0 = Gia_ObjId(pGia, Gia_ObjFanin0(pObj));
1520 int c0 = Gia_ObjFaninC0(pObj);
1521 Connect(nObjs, v[i0] ^ c0);
1522 vPos.push_back(nObjs);
1523 nObjs++;
1524 }
1525 }
1526 void Aig2Bdd(Gia_Man_t *pGia, std::vector<lit> &vNodes) {
1527 if(nVerbose > 6)
1528 Print("\t\t\tBuild Exdc", true);
1529 int i;
1530 Gia_Obj_t *pObj;
1531 std::vector<int> vCounts(pGia->nObjs);
1532 Gia_ManStaticFanoutStart(pGia);
1533 Gia_ManForEachAnd(pGia, pObj, i)
1534 vCounts[Gia_ObjId(pGia, pObj)] = Gia_ObjFanoutNum(pGia, pObj);
1535 Gia_ManStaticFanoutStop(pGia);
1536 std::vector<lit> nodes(pGia->nObjs);
1537 nodes[Gia_ObjId(pGia, Gia_ManConst0(pGia))] = this->man->Const0();
1538 Gia_ManForEachCi(pGia, pObj, i)
1539 nodes[Gia_ObjId(pGia, pObj)] = this->man->IthVar(i);
1540 Gia_ManForEachAnd(pGia, pObj, i) {
1541 int id = Gia_ObjId(pGia, pObj);
1542 if(nVerbose > 6) {
1543 std::stringstream ss;
1544 ss << "\t\t\t\tbuilding Exdc (" << i << " / " << Gia_ManAndNum(pGia) << ")";
1545 Print(ss.str(), nVerbose > 7);
1546 }
1547 int i0 = Gia_ObjId(pGia, Gia_ObjFanin0(pObj));
1548 int i1 = Gia_ObjId(pGia, Gia_ObjFanin1(pObj));
1549 bool c0 = Gia_ObjFaninC0(pObj);
1550 bool c1 = Gia_ObjFaninC1(pObj);
1551 nodes[id] = this->man->And(this->man->LitNotCond(nodes[i0], c0), this->man->LitNotCond(nodes[i1], c1));
1552 this->IncRef(nodes[id]);
1553 vCounts[i0]--;
1554 if(!vCounts[i0])
1555 this->DecRef(nodes[i0]);
1556 vCounts[i1]--;
1557 if(!vCounts[i1])
1558 this->DecRef(nodes[i1]);
1559 }
1560 Gia_ManForEachCo(pGia, pObj, i) {
1561 int i0 = Gia_ObjId(pGia, Gia_ObjFanin0(pObj));
1562 bool c0 = Gia_ObjFaninC0(pObj);
1563 vNodes.push_back(this->man->LitNotCond(nodes[i0], c0));
1564 }
1565 }
1566 void RemoveConstOutputs() {
1567 bool fRemoved = false;
1568 for(unsigned i = 0; i < vPos.size(); i++) {
1569 int i0 = vvFis[vPos[i]][0] >> 1;
1570 lit c = vvCs[vPos[i]][0];
1571 if(i0) {
1572 if(this->man->IsConst1(this->man->Or(LitFi(vPos[i], 0), c))) {
1573 if(nVerbose > 3) {
1574 std::stringstream ss;
1575 ss << "\t\tPO " << std::setw(2) << i << " is Const 1";
1576 Print(ss.str(), true);
1577 }
1578 Disconnect(vPos[i], i0, 0, false, false);
1579 Connect(vPos[i], 1, false, false, c);
1580 fRemoved |= vvFos[i0].empty();
1581 } else if(this->man->IsConst1(this->man->Or(this->man->LitNot(LitFi(vPos[i], 0)), c))) {
1582 if(nVerbose > 3) {
1583 std::stringstream ss;
1584 ss << "\t\tPO " << std::setw(2) << i << " is Const 0";
1585 Print(ss.str(), true);
1586 }
1587 Disconnect(vPos[i], i0, 0, false, false);
1588 Connect(vPos[i], 0, false, false, c);
1589 fRemoved |= vvFos[i0].empty();
1590 }
1591 }
1592 }
1593 if(fRemoved) {
1594 for(std::list<int>::reverse_iterator it = vObjs.rbegin(); it != vObjs.rend();) {
1595 if(vvFos[*it].empty()) {
1596 if(nVerbose > 3) {
1597 std::stringstream ss;
1598 ss << "\t\tremove unused Gate " << std::setw(5) << *it;
1599 Print(ss.str(), true);
1600 }
1601 Remove(*it, false);
1602 it = std::list<int>::reverse_iterator(vObjs.erase(--(it.base())));
1603 continue;
1604 }
1605 it++;
1606 }
1607 }
1608 }
1609
1610public: // Constructor
1611 Transduction(Gia_Man_t *pGia, int nVerbose, bool fNewLine, int nSortType, int nPiShuffle, bool fLevel, Gia_Man_t *pExdc, Param &p): nVerbose(nVerbose), nSortType(nSortType), fLevel(fLevel), fNewLine(fNewLine) {
1612 startclk = Abc_Clock();
1613 p.nGbc = 1;
1614 p.nReo = 4000;
1615 if(nSortType && nSortType < 4)
1616 p.fCountOnes = true;
1617 this->man = new Man(Gia_ManCiNum(pGia), p);
1618 ImportAig(pGia);
1619 this->Update(vFs[0], this->man->Const0());
1620 for(unsigned i = 0; i < vPis.size(); i++)
1621 this->Update(vFs[i + 1], this->man->IthVar(i));
1622 nMaxLevels = -1;
1623 Build(false);
1624 this->man->Reorder();
1625 this->man->TurnOffReo();
1626 if(pExdc) {
1627 std::vector<lit> vExdc;
1628 Aig2Bdd(pExdc, vExdc);
1629 for(unsigned i = 0; i < vPos.size(); i++)
1630 vvCs[vPos[i]][0] = vExdc.size() == 1? vExdc[0]: vExdc[i];
1631 } else
1632 for(unsigned i = 0; i < vPos.size(); i++)
1633 this->Update(vvCs[vPos[i]][0], this->man->Const0());
1634 RemoveConstOutputs();
1635 vPoFs.resize(vPos.size(), LitMax);
1636 for(unsigned i = 0; i < vPos.size(); i++)
1637 this->Update(vPoFs[i], LitFi(vPos[i], 0));
1638 state = none;
1639 if(nPiShuffle)
1640 ShufflePis(nPiShuffle);
1641 if(fLevel)
1642 ComputeLevel();
1643 if(nVerbose)
1644 PrintStats("Init", true, 11);
1645 }
1646 ~Transduction() {
1647 if(nVerbose)
1648 PrintStats("End", true, 11);
1649 this->DelVec(vFs);
1650 this->DelVec(vGs);
1651 this->DelVec(vvCs);
1652 this->DelVec(vPoFs);
1653 //assert(this->man->CountNodes() == (int)vPis.size() + 1);
1654 //assert(!this->man->Ref(this->man->Const0()));
1655 delete this->man;
1656 }
1657
1658public: // Output
1659 Gia_Man_t *GenerateAig() const {
1660 Gia_Man_t * pGia, *pTemp;
1661 pGia = Gia_ManStart(1 + vPis.size() + CountNodes() + vPos.size());
1662 Gia_ManHashAlloc(pGia);
1663 std::vector<int> values(nObjsAlloc);
1664 values[0] = Gia_ManConst0Lit();
1665 for(unsigned i = 0; i < vPis.size(); i++)
1666 values[i + 1] = Gia_ManAppendCi(pGia);
1667 for(std::list<int>::const_iterator it = vObjs.begin(); it != vObjs.end(); it++) {
1668 assert(vvFis[*it].size() > 1);
1669 int i0 = vvFis[*it][0] >> 1;
1670 int i1 = vvFis[*it][1] >> 1;
1671 int c0 = vvFis[*it][0] & 1;
1672 int c1 = vvFis[*it][1] & 1;
1673 int r = Gia_ManHashAnd(pGia, Abc_LitNotCond(values[i0], c0), Abc_LitNotCond(values[i1], c1));
1674 for(unsigned i = 2; i < vvFis[*it].size(); i++) {
1675 int ii = vvFis[*it][i] >> 1;
1676 int ci = vvFis[*it][i] & 1;
1677 r = Gia_ManHashAnd(pGia, r, Abc_LitNotCond(values[ii], ci));
1678 }
1679 values[*it] = r;
1680 }
1681 for(unsigned i = 0; i < vPos.size(); i++) {
1682 int i0 = vvFis[vPos[i]][0] >> 1;
1683 int c0 = vvFis[vPos[i]][0] & 1;
1684 Gia_ManAppendCo(pGia, Abc_LitNotCond(values[i0], c0));
1685 }
1686 pGia = Gia_ManCleanup(pTemp = pGia);
1687 Gia_ManStop(pTemp);
1688 return pGia;
1689 }
1690
1691public: // Debug and print
1692 PfState State() const {
1693 return state;
1694 }
1695 bool BuildDebug() {
1696 for(std::list<int>::iterator it = vObjs.begin(); it != vObjs.end(); it++)
1697 vUpdates[*it] = true;
1698 std::vector<lit> vFsOld;
1699 CopyVec(vFsOld, vFs);
1700 Build(false);
1701 bool r = LitVecIsEq(vFsOld, vFs);
1702 DelVec(vFsOld);
1703 return r;
1704 }
1705 bool CspfDebug() {
1706 std::vector<lit> vGsOld;
1707 this->CopyVec(vGsOld, vGs);
1708 std::vector<std::vector<lit> > vvCsOld;
1709 this->CopyVec(vvCsOld, vvCs);
1710 state = none;
1711 Cspf(false);
1712 bool r = this->LitVecIsEq(vGsOld, vGs) && this->LitVecIsEq(vvCsOld, vvCs);
1713 this->DelVec(vGsOld);
1714 this->DelVec(vvCsOld);
1715 return r;
1716 }
1717 bool MspfDebug() {
1718 std::vector<lit> vGsOld;
1719 this->CopyVec(vGsOld, vGs);
1720 std::vector<std::vector<lit> > vvCsOld;
1721 this->CopyVec(vvCsOld, vvCs);
1722 state = none;
1723 Mspf(false);
1724 bool r = this->LitVecIsEq(vGsOld, vGs) && this->LitVecIsEq(vvCsOld, vvCs);
1725 this->DelVec(vGsOld);
1726 this->DelVec(vvCsOld);
1727 return r;
1728 }
1729 bool Verify() const {
1730 for(unsigned j = 0; j < vPos.size(); j++) {
1731 lit x = this->Xor(LitFi(vPos[j], 0), vPoFs[j]);
1732 this->IncRef(x);
1733 this->Update(x, this->man->And(x, this->man->LitNot(vvCs[vPos[j]][0])));
1734 this->DecRef(x);
1735 if(!this->man->IsConst0(x))
1736 return false;
1737 }
1738 return true;
1739 }
1740 void PrintObjs() const {
1741 for(std::list<int>::const_iterator it = vObjs.begin(); it != vObjs.end(); it++) {
1742 std::cout << "Gate " << *it << ":";
1743 if(fLevel)
1744 std::cout << " Level = " << vLevels[*it] << ", Slack = " << vSlacks[*it];
1745 std::cout << std::endl;
1746 std::string delim = "";
1747 std::cout << "\tFis: ";
1748 for(unsigned j = 0; j < vvFis[*it].size(); j++) {
1749 std::cout << delim << (vvFis[*it][j] >> 1) << "(" << (vvFis[*it][j] & 1) << ")";
1750 delim = ", ";
1751 }
1752 std::cout << std::endl;
1753 delim = "";
1754 std::cout << "\tFos: ";
1755 for(unsigned j = 0; j < vvFos[*it].size(); j++) {
1756 std::cout << delim << vvFos[*it][j];
1757 delim = ", ";
1758 }
1759 std::cout << std::endl;
1760 }
1761 }
1762};
1763
1764}
1765
1766ABC_NAMESPACE_CXX_HEADER_END
1767
1768#endif
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
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
b0
#define b0
Definition bbrImage.c:96
Transduction::ManUtil::DecRef
void DecRef(lit x) const
Definition giaTransduction.h:50
Transduction::ManUtil::DelVec
void DelVec(std::vector< lit > &v) const
Definition giaTransduction.h:59
Transduction::ManUtil::IncRef
void IncRef(lit x) const
Definition giaTransduction.h:46
Transduction::ManUtil::CopyVec
void CopyVec(std::vector< lit > &v, std::vector< lit > const &u) const
Definition giaTransduction.h:69
Transduction::ManUtil::LitVecIsEq
bool LitVecIsEq(std::vector< lit > const &v, std::vector< lit > const &u) const
Definition giaTransduction.h:82
Transduction::ManUtil::DelVec
void DelVec(std::vector< std::vector< lit > > &v) const
Definition giaTransduction.h:64
Transduction::ManUtil::LitVecIsEq
bool LitVecIsEq(std::vector< std::vector< lit > > const &v, std::vector< std::vector< lit > > const &u) const
Definition giaTransduction.h:90
Transduction::ManUtil::Update
void Update(lit &x, lit y) const
Definition giaTransduction.h:54
Transduction::ManUtil::CopyVec
void CopyVec(std::vector< std::vector< lit > > &v, std::vector< std::vector< lit > > const &u) const
Definition giaTransduction.h:75
Transduction::ManUtil::Xor
lit Xor(lit x, lit y) const
Definition giaTransduction.h:98
Transduction::Transduction::Transduction
Transduction(Gia_Man_t *pGia, int nVerbose, bool fNewLine, int nSortType, int nPiShuffle, bool fLevel, Gia_Man_t *pExdc, Param &p)
Definition giaTransduction.h:1611
Transduction::Transduction::RepeatAll
int RepeatAll(bool fFirstMerge, bool fMspfMerge, bool fMspfResub, bool fInner, bool fOuter)
Definition giaTransduction.h:1428
Transduction::Transduction::Print
void Print(std::string str, bool nl) const
Definition giaTransduction.h:195
Transduction::Transduction::RepeatResub
int RepeatResub(bool fMono, bool fMspf)
Definition giaTransduction.h:1404
Transduction::Transduction::RepeatOuter
int RepeatOuter(bool fMspf, bool fInner, bool fOuter)
Definition giaTransduction.h:1419
Transduction::Transduction::PrintStats
void PrintStats(std::string prefix, bool nl, int prefix_size=0) const
Definition giaTransduction.h:204
Transduction::Transduction::RepeatInner
int RepeatInner(bool fMspf, bool fInner)
Definition giaTransduction.h:1410
Transduction::Transduction::PrintPfHeader
void PrintPfHeader(std::string prefix, int block, int block_i0)
Definition giaTransduction.h:215
Transduction::Transduction::GenerateAig
Gia_Man_t * GenerateAig() const
Definition giaTransduction.h:1659
pos
bool pos
Definition globals.c:30
p
Cube * p
Definition exorList.c:222
a0
#define a0
Definition extraBdd.h:79
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition giaMan.c:82
Gia_ManStaticFanoutStart
void Gia_ManStaticFanoutStart(Gia_Man_t *p)
Definition giaFanout.c:238
Gia_ManStaticFanoutStop
void Gia_ManStaticFanoutStop(Gia_Man_t *p)
Definition giaFanout.c:393
Gia_ManForEachAnd
#define Gia_ManForEachAnd(p, pObj, i)
Definition gia.h:1214
Gia_ManHashAlloc
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition giaHash.c:105
Gia_ManStart
Gia_Man_t * Gia_ManStart(int nObjsMax)
FUNCTION DEFINITIONS ///.
Definition giaMan.c:57
Gia_Obj_t
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
Gia_Man_t
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
Gia_ManCleanup
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition giaScl.c:84
Gia_ManHashAnd
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition giaHash.c:576
Gia_ManForEachCo
#define Gia_ManForEachCo(p, pObj, i)
Definition gia.h:1236
Gia_ManForEachCi
#define Gia_ManForEachCi(p, pObj, i)
Definition gia.h:1228
NewBdd::size
unsigned long long size
Definition giaNewBdd.h:39
lit
int lit
Definition satVec.h:130
Gia_Man_t_::nObjs
int nObjs
Definition gia.h:103
assert
#define assert(ex)
Definition util_old.h:213