diff --git a/abclib.dsp b/abclib.dsp index d538db292..00e38bd09 100644 --- a/abclib.dsp +++ b/abclib.dsp @@ -5111,6 +5111,14 @@ SOURCE=.\src\aig\gia\giaMuxes.c # End Source File # Begin Source File +SOURCE=.\src\aig\gia\giaNewBdd.h +# End Source File +# Begin Source File + +SOURCE=.\src\aig\gia\giaNewTt.h +# End Source File +# Begin Source File + SOURCE=.\src\aig\gia\giaNf.c # End Source File # Begin Source File @@ -5307,6 +5315,14 @@ SOURCE=.\src\aig\gia\giaTtopt.cpp # End Source File # Begin Source File +SOURCE=.\src\aig\gia\giaTransduction.cpp +# End Source File +# Begin Source File + +SOURCE=.\src\aig\gia\giaTransduction.h +# End Source File +# Begin Source File + SOURCE=.\src\aig\gia\giaUnate.c # End Source File # Begin Source File diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index e44617689..fed64b1ad 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -1769,10 +1769,14 @@ extern int Gia_ManCountPosWithNonZeroDrivers( Gia_Man_t * p ); extern void Gia_ManUpdateCopy( Vec_Int_t * vCopy, Gia_Man_t * p ); extern Vec_Int_t * Gia_ManComputeDistance( Gia_Man_t * p, int iObj, Vec_Int_t * vObjs, int fVerbose ); -/*=== giaTtopt.c ===========================================================*/ +/*=== giaTtopt.cpp ===========================================================*/ extern Gia_Man_t * Gia_ManTtopt( Gia_Man_t * p, int nIns, int nOuts, int nRounds ); extern Gia_Man_t * Gia_ManTtoptCare( Gia_Man_t * p, int nIns, int nOuts, int nRounds, char * pFileName, int nRarity ); +/*=== giaTransduction.cpp ===========================================================*/ +extern Gia_Man_t * Gia_ManTransductionBdd( Gia_Man_t * pGia, int nType, int fMspf, int nRandom, int nSortType, int nPiShuffle, int nParameter, int fLevel, Gia_Man_t * pExdc, int fNewLine, int nVerbose ); +extern Gia_Man_t * Gia_ManTransductionTt( Gia_Man_t * pGia, int nType, int fMspf, int nRandom, int nSortType, int nPiShuffle, int nParameter, int fLevel, Gia_Man_t * pExdc, int fNewLine, int nVerbose ); + /*=== giaCTas.c ===========================================================*/ typedef struct Tas_Man_t_ Tas_Man_t; extern Tas_Man_t * Tas_ManAlloc( Gia_Man_t * pAig, int nBTLimit ); diff --git a/src/aig/gia/giaNewBdd.h b/src/aig/gia/giaNewBdd.h new file mode 100644 index 000000000..b9fd5960c --- /dev/null +++ b/src/aig/gia/giaNewBdd.h @@ -0,0 +1,819 @@ +#ifndef ABC__aig__gia__giaNewBdd_h +#define ABC__aig__gia__giaNewBdd_h + +#include +#include +#include +#include +#include + +ABC_NAMESPACE_CXX_HEADER_START + +namespace NewBdd { + + typedef unsigned short var; + typedef int bvar; + typedef unsigned lit; + typedef unsigned short ref; + typedef unsigned long long size; + typedef unsigned edge; + typedef unsigned uniq; + typedef unsigned cac; + static inline var VarMax() { return std::numeric_limits::max(); } + static inline bvar BvarMax() { return std::numeric_limits::max(); } + static inline lit LitMax() { return std::numeric_limits::max(); } + static inline ref RefMax() { return std::numeric_limits::max(); } + static inline size SizeMax() { return std::numeric_limits::max(); } + static inline uniq UniqHash(lit Arg0, lit Arg1) { return Arg0 + 4256249 * Arg1; } + static inline cac CacHash(lit Arg0, lit Arg1) { return Arg0 + 4256249 * Arg1; } + + class Cache { + private: + cac nSize; + cac nMax; + cac Mask; + size nLookups; + size nHits; + size nThold; + double HitRate; + int nVerbose; + std::vector vCache; + + public: + Cache(int nCacheSizeLog, int nCacheMaxLog, int nVerbose): nVerbose(nVerbose) { + if(nCacheMaxLog < nCacheSizeLog) + throw std::invalid_argument("nCacheMax must not be smaller than nCacheSize"); + nMax = (cac)1 << nCacheMaxLog; + if(!(nMax << 1)) + throw std::length_error("Memout (nCacheMax) in init"); + nSize = (cac)1 << nCacheSizeLog; + if(nVerbose) + std::cout << "Allocating " << nSize << " cache entries" << std::endl; + vCache.resize(nSize * 3); + Mask = nSize - 1; + nLookups = 0; + nHits = 0; + nThold = (nSize == nMax)? SizeMax(): nSize; + HitRate = 1; + } + ~Cache() { + if(nVerbose) + std::cout << "Free " << nSize << " cache entries" << std::endl; + } + inline lit Lookup(lit x, lit y) { + nLookups++; + if(nLookups > nThold) { + double NewHitRate = (double)nHits / nLookups; + if(nVerbose >= 2) + std::cout << "Cache Hits: " << std::setw(10) << nHits << ", " + << "Lookups: " << std::setw(10) << nLookups << ", " + << "Rate: " << std::setw(10) << NewHitRate + << std::endl; + if(NewHitRate > HitRate) + Resize(); + if(nSize == nMax) + nThold = SizeMax(); + else { + nThold <<= 1; + if(!nThold) + nThold = SizeMax(); + } + HitRate = NewHitRate; + } + cac i = (CacHash(x, y) & Mask) * 3; + if(vCache[i] == x && vCache[i + 1] == y) { + if(nVerbose >= 3) + std::cout << "Cache hit: " + << "x = " << std::setw(10) << x << ", " + << "y = " << std::setw(10) << y << ", " + << "z = " << std::setw(10) << vCache[i + 2] << ", " + << "hash = " << std::hex << (CacHash(x, y) & Mask) << std::dec + << std::endl; + nHits++; + return vCache[i + 2]; + } + return LitMax(); + } + inline void Insert(lit x, lit y, lit z) { + cac i = (CacHash(x, y) & Mask) * 3; + vCache[i] = x; + vCache[i + 1] = y; + vCache[i + 2] = z; + if(nVerbose >= 3) + std::cout << "Cache ent: " + << "x = " << std::setw(10) << x << ", " + << "y = " << std::setw(10) << y << ", " + << "z = " << std::setw(10) << z << ", " + << "hash = " << std::hex << (CacHash(x, y) & Mask) << std::dec + << std::endl; + } + inline void Clear() { + std::fill(vCache.begin(), vCache.end(), 0); + } + void Resize() { + cac nSizeOld = nSize; + nSize <<= 1; + if(nVerbose >= 2) + std::cout << "Reallocating " << nSize << " cache entries" << std::endl; + vCache.resize(nSize * 3); + Mask = nSize - 1; + for(cac j = 0; j < nSizeOld; j++) { + cac i = j * 3; + if(vCache[i] || vCache[i + 1]) { + cac hash = (CacHash(vCache[i], vCache[i + 1]) & Mask) * 3; + vCache[hash] = vCache[i]; + vCache[hash + 1] = vCache[i + 1]; + vCache[hash + 2] = vCache[i + 2]; + if(nVerbose >= 3) + std::cout << "Cache mov: " + << "x = " << std::setw(10) << vCache[i] << ", " + << "y = " << std::setw(10) << vCache[i + 1] << ", " + << "z = " << std::setw(10) << vCache[i + 2] << ", " + << "hash = " << std::hex << (CacHash(vCache[i], vCache[i + 1]) & Mask) << std::dec + << std::endl; + } + } + } + }; + + struct Param { + int nObjsAllocLog; + int nObjsMaxLog; + int nUniqueSizeLog; + double UniqueDensity; + int nCacheSizeLog; + int nCacheMaxLog; + int nCacheVerbose; + bool fCountOnes; + int nGbc; + bvar nReo; + double MaxGrowth; + bool fReoVerbose; + int nVerbose; + std::vector *pVar2Level; + Param() { + nObjsAllocLog = 20; + nObjsMaxLog = 25; + nUniqueSizeLog = 10; + UniqueDensity = 4; + nCacheSizeLog = 15; + nCacheMaxLog = 20; + nCacheVerbose = 0; + fCountOnes = false; + nGbc = 0; + nReo = BvarMax(); + MaxGrowth = 1.2; + fReoVerbose = false; + nVerbose = 0; + pVar2Level = NULL; + } + }; + + class Man { + private: + var nVars; + bvar nObjs; + bvar nObjsAlloc; + bvar nObjsMax; + bvar RemovedHead; + int nGbc; + bvar nReo; + double MaxGrowth; + bool fReoVerbose; + int nVerbose; + std::vector vVars; + std::vector Var2Level; + std::vector Level2Var; + std::vector vObjs; + std::vector vNexts; + std::vector vMarks; + std::vector vRefs; + std::vector vEdges; + std::vector vOneCounts; + std::vector vUniqueMasks; + std::vector vUniqueCounts; + std::vector vUniqueTholds; + std::vector > vvUnique; + Cache *cache; + + public: + inline lit Bvar2Lit(bvar a) const { return (lit)a << 1; } + inline lit Bvar2Lit(bvar a, bool c) const { return ((lit)a << 1) ^ (lit)c; } + inline bvar Lit2Bvar(lit x) const { return (bvar)(x >> 1); } + inline var VarOfBvar(bvar a) const { return vVars[a]; } + inline lit ThenOfBvar(bvar a) const { return vObjs[Bvar2Lit(a)]; } + inline lit ElseOfBvar(bvar a) const { return vObjs[Bvar2Lit(a, true)]; } + inline ref RefOfBvar(bvar a) const { return vRefs[a]; } + inline lit Const0() const { return (lit)0; } + inline lit Const1() const { return (lit)1; } + inline bool IsConst0(lit x) const { return x == Const0(); } + inline bool IsConst1(lit x) const { return x == Const1(); } + inline lit IthVar(var v) const { return Bvar2Lit((bvar)v + 1); } + inline lit LitRegular(lit x) const { return x & ~(lit)1; } + inline lit LitIrregular(lit x) const { return x | (lit)1; } + inline lit LitNot(lit x) const { return x ^ (lit)1; } + inline lit LitNotCond(lit x, bool c) const { return x ^ (lit)c; } + inline bool LitIsCompl(lit x) const { return x & (lit)1; } + inline bool LitIsEq(lit x, lit y) const { return x == y; } + inline var Var(lit x) const { return vVars[Lit2Bvar(x)]; } + inline var Level(lit x) const { return Var2Level[Var(x)]; } + inline lit Then(lit x) const { return LitNotCond(vObjs[LitRegular(x)], LitIsCompl(x)); } + inline lit Else(lit x) const { return LitNotCond(vObjs[LitIrregular(x)], LitIsCompl(x)); } + inline ref Ref(lit x) const { return vRefs[Lit2Bvar(x)]; } + inline double OneCount(lit x) const { + if(vOneCounts.empty()) + throw std::logic_error("fCountOnes was not set"); + if(LitIsCompl(x)) + return std::pow(2.0, nVars) - vOneCounts[Lit2Bvar(x)]; + return vOneCounts[Lit2Bvar(x)]; + } + + public: + inline void IncRef(lit x) { if(!vRefs.empty() && Ref(x) != RefMax()) vRefs[Lit2Bvar(x)]++; } + inline void DecRef(lit x) { if(!vRefs.empty() && Ref(x) != RefMax()) vRefs[Lit2Bvar(x)]--; } + + private: + inline bool Mark(lit x) const { return vMarks[Lit2Bvar(x)]; } + inline edge Edge(lit x) const { return vEdges[Lit2Bvar(x)]; } + inline void SetMark(lit x) { vMarks[Lit2Bvar(x)] = true; } + inline void ResetMark(lit x) { vMarks[Lit2Bvar(x)] = false; } + inline void IncEdge(lit x) { vEdges[Lit2Bvar(x)]++; } + inline void DecEdge(lit x) { vEdges[Lit2Bvar(x)]--; } + inline bool MarkOfBvar(bvar a) const { return vMarks[a]; } + inline edge EdgeOfBvar(bvar a) const { return vEdges[a]; } + inline void SetVarOfBvar(bvar a, var v) { vVars[a] = v; } + inline void SetThenOfBvar(bvar a, lit x) { vObjs[Bvar2Lit(a)] = x; } + inline void SetElseOfBvar(bvar a, lit x) { vObjs[Bvar2Lit(a, true)] = x; } + inline void SetMarkOfBvar(bvar a) { vMarks[a] = true; } + inline void ResetMarkOfBvar(bvar a) { vMarks[a] = false; } + inline void RemoveBvar(bvar a) { + var v = VarOfBvar(a); + SetVarOfBvar(a, VarMax()); + std::vector::iterator q = vvUnique[v].begin() + (UniqHash(ThenOfBvar(a), ElseOfBvar(a)) & vUniqueMasks[v]); + for(; *q; q = vNexts.begin() + *q) + if(*q == a) + break; + bvar next = vNexts[*q]; + vNexts[*q] = RemovedHead; + RemovedHead = *q; + *q = next; + vUniqueCounts[v]--; + } + + private: + void SetMark_rec(lit x) { + if(x < 2 || Mark(x)) + return; + SetMark(x); + SetMark_rec(Then(x)); + SetMark_rec(Else(x)); + } + void ResetMark_rec(lit x) { + if(x < 2 || !Mark(x)) + return; + ResetMark(x); + ResetMark_rec(Then(x)); + ResetMark_rec(Else(x)); + } + bvar CountNodes_rec(lit x) { + if(x < 2 || Mark(x)) + return 0; + SetMark(x); + return 1 + CountNodes_rec(Then(x)) + CountNodes_rec(Else(x)); + } + void CountEdges_rec(lit x) { + if(x < 2) + return; + IncEdge(x); + if(Mark(x)) + return; + SetMark(x); + CountEdges_rec(Then(x)); + CountEdges_rec(Else(x)); + } + void CountEdges() { + vEdges.resize(nObjsAlloc); + for(bvar a = (bvar)nVars + 1; a < nObjs; a++) + if(RefOfBvar(a)) + CountEdges_rec(Bvar2Lit(a)); + for(bvar a = 1; a <= (bvar)nVars; a++) + vEdges[a]++; + for(bvar a = (bvar)nVars + 1; a < nObjs; a++) + if(RefOfBvar(a)) + ResetMark_rec(Bvar2Lit(a)); + } + + public: + bool Resize() { + if(nObjsAlloc == nObjsMax) + return false; + lit nObjsAllocLit = (lit)nObjsAlloc << 1; + if(nObjsAllocLit > (lit)BvarMax()) + nObjsAlloc = BvarMax(); + else + nObjsAlloc = (bvar)nObjsAllocLit; + if(nVerbose >= 2) + std::cout << "Reallocating " << nObjsAlloc << " nodes" << std::endl; + vVars.resize(nObjsAlloc); + vObjs.resize((lit)nObjsAlloc * 2); + vNexts.resize(nObjsAlloc); + vMarks.resize(nObjsAlloc); + if(!vRefs.empty()) + vRefs.resize(nObjsAlloc); + if(!vEdges.empty()) + vEdges.resize(nObjsAlloc); + if(!vOneCounts.empty()) + vOneCounts.resize(nObjsAlloc); + return true; + } + void ResizeUnique(var v) { + uniq nUniqueSize, nUniqueSizeOld; + nUniqueSize = nUniqueSizeOld = vvUnique[v].size(); + nUniqueSize <<= 1; + if(!nUniqueSize) { + vUniqueTholds[v] = BvarMax(); + return; + } + if(nVerbose >= 2) + std::cout << "Reallocating " << nUniqueSize << " unique table entries for Var " << v << std::endl; + vvUnique[v].resize(nUniqueSize); + vUniqueMasks[v] = nUniqueSize - 1; + for(uniq i = 0; i < nUniqueSizeOld; i++) { + std::vector::iterator q, tail, tail1, tail2; + q = tail1 = vvUnique[v].begin() + i; + tail2 = q + nUniqueSizeOld; + while(*q) { + uniq hash = UniqHash(ThenOfBvar(*q), ElseOfBvar(*q)) & vUniqueMasks[v]; + if(hash == i) + tail = tail1; + else + tail = tail2; + if(tail != q) + *tail = *q, *q = 0; + q = vNexts.begin() + *tail; + if(tail == tail1) + tail1 = q; + else + tail2 = q; + } + } + vUniqueTholds[v] <<= 1; + if((lit)vUniqueTholds[v] > (lit)BvarMax()) + vUniqueTholds[v] = BvarMax(); + } + bool Gbc() { + if(nVerbose >= 2) + std::cout << "Garbage collect" << std::endl; + if(!vEdges.empty()) { + for(bvar a = (bvar)nVars + 1; a < nObjs; a++) + if(!EdgeOfBvar(a) && VarOfBvar(a) != VarMax()) + RemoveBvar(a); + } else { + for(bvar a = (bvar)nVars + 1; a < nObjs; a++) + if(RefOfBvar(a)) + SetMark_rec(Bvar2Lit(a)); + for(bvar a = (bvar)nVars + 1; a < nObjs; a++) + if(!MarkOfBvar(a) && VarOfBvar(a) != VarMax()) + RemoveBvar(a); + for(bvar a = (bvar)nVars + 1; a < nObjs; a++) + if(RefOfBvar(a)) + ResetMark_rec(Bvar2Lit(a)); + } + cache->Clear(); + return RemovedHead; + } + + private: + inline lit UniqueCreateInt(var v, lit x1, lit x0) { + std::vector::iterator p, q; + p = q = vvUnique[v].begin() + (UniqHash(x1, x0) & vUniqueMasks[v]); + for(; *q; q = vNexts.begin() + *q) + if(VarOfBvar(*q) == v && ThenOfBvar(*q) == x1 && ElseOfBvar(*q) == x0) + return Bvar2Lit(*q); + bvar next = *p; + if(nObjs < nObjsAlloc) + *p = nObjs++; + else if(RemovedHead) + *p = RemovedHead, RemovedHead = vNexts[*p]; + else + return LitMax(); + SetVarOfBvar(*p, v); + SetThenOfBvar(*p, x1); + SetElseOfBvar(*p, x0); + vNexts[*p] = next; + if(!vOneCounts.empty()) + vOneCounts[*p] = OneCount(x1) / 2 + OneCount(x0) / 2; + if(nVerbose >= 3) { + std::cout << "Create node " << std::setw(10) << *p << ": " + << "Var = " << std::setw(6) << v << ", " + << "Then = " << std::setw(10) << x1 << ", " + << "Else = " << std::setw(10) << x0; + if(!vOneCounts.empty()) + std::cout << ", Ones = " << std::setw(10) << vOneCounts[*q]; + std::cout << std::endl; + } + vUniqueCounts[v]++; + if(vUniqueCounts[v] > vUniqueTholds[v]) { + bvar a = *p; + ResizeUnique(v); + return Bvar2Lit(a); + } + return Bvar2Lit(*p); + } + inline lit UniqueCreate(var v, lit x1, lit x0) { + if(x1 == x0) + return x1; + lit x; + while(true) { + if(!LitIsCompl(x0)) + x = UniqueCreateInt(v, x1, x0); + else + x = UniqueCreateInt(v, LitNot(x1), LitNot(x0)); + if(x == LitMax()) { + bool fRemoved = false; + if(nGbc > 1) + fRemoved = Gbc(); + if(!Resize() && !fRemoved && (nGbc != 1 || !Gbc())) + throw std::length_error("Memout (node)"); + } else + break; + } + return LitIsCompl(x0)? LitNot(x): x; + } + lit And_rec(lit x, lit y) { + if(x == 0 || y == 1) + return x; + if(x == 1 || y == 0) + return y; + if(Lit2Bvar(x) == Lit2Bvar(y)) + return (x == y)? x: 0; + if(x > y) + std::swap(x, y); + lit z = cache->Lookup(x, y); + if(z != LitMax()) + return z; + var v; + lit x0, x1, y0, y1; + if(Level(x) < Level(y)) + v = Var(x), x1 = Then(x), x0 = Else(x), y0 = y1 = y; + else if(Level(x) > Level(y)) + v = Var(y), x0 = x1 = x, y1 = Then(y), y0 = Else(y); + else + v = Var(x), x1 = Then(x), x0 = Else(x), y1 = Then(y), y0 = Else(y); + lit z1 = And_rec(x1, y1); + IncRef(z1); + lit z0 = And_rec(x0, y0); + IncRef(z0); + z = UniqueCreate(v, z1, z0); + DecRef(z1); + DecRef(z0); + cache->Insert(x, y, z); + return z; + } + + private: + bvar Swap(var i) { + var v1 = Level2Var[i]; + var v2 = Level2Var[i + 1]; + bvar f = 0; + bvar diff = 0; + for(std::vector::iterator p = vvUnique[v1].begin(); p != vvUnique[v1].end(); p++) { + std::vector::iterator q = p; + while(*q) { + if(!EdgeOfBvar(*q)) { + SetVarOfBvar(*q, VarMax()); + bvar next = vNexts[*q]; + vNexts[*q] = RemovedHead; + RemovedHead = *q; + *q = next; + vUniqueCounts[v1]--; + continue; + } + lit f1 = ThenOfBvar(*q); + lit f0 = ElseOfBvar(*q); + if(Var(f1) == v2 || Var(f0) == v2) { + DecEdge(f1); + if(Var(f1) == v2 && !Edge(f1)) + DecEdge(Then(f1)), DecEdge(Else(f1)), diff--; + DecEdge(f0); + if(Var(f0) == v2 && !Edge(f0)) + DecEdge(Then(f0)), DecEdge(Else(f0)), diff--; + bvar next = vNexts[*q]; + vNexts[*q] = f; + f = *q; + *q = next; + vUniqueCounts[v1]--; + continue; + } + q = vNexts.begin() + *q; + } + } + while(f) { + lit f1 = ThenOfBvar(f); + lit f0 = ElseOfBvar(f); + lit f00, f01, f10, f11; + if(Var(f1) == v2) + f11 = Then(f1), f10 = Else(f1); + else + f10 = f11 = f1; + if(Var(f0) == v2) + f01 = Then(f0), f00 = Else(f0); + else + f00 = f01 = f0; + if(f11 == f01) + f1 = f11; + else { + f1 = UniqueCreate(v1, f11, f01); + if(!Edge(f1)) + IncEdge(f11), IncEdge(f01), diff++; + } + IncEdge(f1); + IncRef(f1); + if(f10 == f00) + f0 = f10; + else { + f0 = UniqueCreate(v1, f10, f00); + if(!Edge(f0)) + IncEdge(f10), IncEdge(f00), diff++; + } + IncEdge(f0); + DecRef(f1); + SetVarOfBvar(f, v2); + SetThenOfBvar(f, f1); + SetElseOfBvar(f, f0); + std::vector::iterator q = vvUnique[v2].begin() + (UniqHash(f1, f0) & vUniqueMasks[v2]); + lit next = vNexts[f]; + vNexts[f] = *q; + *q = f; + vUniqueCounts[v2]++; + f = next; + } + Var2Level[v1] = i + 1; + Var2Level[v2] = i; + Level2Var[i] = v2; + Level2Var[i + 1] = v1; + return diff; + } + void Sift() { + bvar count = CountNodes(); + std::vector sift_order(nVars); + for(var v = 0; v < nVars; v++) + sift_order[v] = v; + for(var i = 0; i < nVars; i++) { + var max_j = i; + for(var j = i + 1; j < nVars; j++) + if(vUniqueCounts[sift_order[j]] > vUniqueCounts[sift_order[max_j]]) + max_j = j; + if(max_j != i) + std::swap(sift_order[max_j], sift_order[i]); + } + for(var v = 0; v < nVars; v++) { + bvar lev = Var2Level[sift_order[v]]; + bool UpFirst = lev < (bvar)(nVars / 2); + bvar min_lev = lev; + bvar min_diff = 0; + bvar diff = 0; + bvar thold = count * (MaxGrowth - 1); + if(fReoVerbose) + std::cout << "Sift " << sift_order[v] << " : Level = " << lev << " Count = " << count << " Thold = " << thold << std::endl; + if(UpFirst) { + lev--; + for(; lev >= 0; lev--) { + diff += Swap(lev); + if(fReoVerbose) + std::cout << "\tSwap " << lev << " : Diff = " << diff << " Thold = " << thold << std::endl; + if(diff < min_diff) + min_lev = lev, min_diff = diff, thold = (count + diff) * (MaxGrowth - 1); + else if(diff > thold) { + lev--; + break; + } + } + lev++; + } + for(; lev < (bvar)nVars - 1; lev++) { + diff += Swap(lev); + if(fReoVerbose) + std::cout << "\tSwap " << lev << " : Diff = " << diff << " Thold = " << thold << std::endl; + if(diff <= min_diff) + min_lev = lev + 1, min_diff = diff, thold = (count + diff) * (MaxGrowth - 1); + else if(diff > thold) { + lev++; + break; + } + } + lev--; + if(UpFirst) { + for(; lev >= min_lev; lev--) { + diff += Swap(lev); + if(fReoVerbose) + std::cout << "\tSwap " << lev << " : Diff = " << diff << " Thold = " << thold << std::endl; + } + } else { + for(; lev >= 0; lev--) { + diff += Swap(lev); + if(fReoVerbose) + std::cout << "\tSwap " << lev << " : Diff = " << diff << " Thold = " << thold << std::endl; + if(diff <= min_diff) + min_lev = lev, min_diff = diff, thold = (count + diff) * (MaxGrowth - 1); + else if(diff > thold) { + lev--; + break; + } + } + lev++; + for(; lev < min_lev; lev++) { + diff += Swap(lev); + if(fReoVerbose) + std::cout << "\tSwap " << lev << " : Diff = " << diff << " Thold = " << thold << std::endl; + } + } + count += min_diff; + if(fReoVerbose) + std::cout << "Sifted " << sift_order[v] << " : Level = " << min_lev << " Count = " << count << " Thold = " << thold << std::endl; + } + } + + public: + Man(int nVars_, Param p) { + nVerbose = p.nVerbose; + // parameter sanity check + if(p.nObjsMaxLog < p.nObjsAllocLog) + throw std::invalid_argument("nObjsMax must not be smaller than nObjsAlloc"); + if(nVars_ >= (int)VarMax()) + throw std::length_error("Memout (nVars) in init"); + nVars = nVars_; + lit nObjsMaxLit = (lit)1 << p.nObjsMaxLog; + if(!nObjsMaxLit) + throw std::length_error("Memout (nObjsMax) in init"); + if(nObjsMaxLit > (lit)BvarMax()) + nObjsMax = BvarMax(); + else + nObjsMax = (bvar)nObjsMaxLit; + lit nObjsAllocLit = (lit)1 << p.nObjsAllocLog; + if(!nObjsAllocLit) + throw std::length_error("Memout (nObjsAlloc) in init"); + if(nObjsAllocLit > (lit)BvarMax()) + nObjsAlloc = BvarMax(); + else + nObjsAlloc = (bvar)nObjsAllocLit; + if(nObjsAlloc <= (bvar)nVars) + throw std::invalid_argument("nObjsAlloc must be larger than nVars"); + uniq nUniqueSize = (uniq)1 << p.nUniqueSizeLog; + if(!nUniqueSize) + throw std::length_error("Memout (nUniqueSize) in init"); + // allocation + if(nVerbose) + std::cout << "Allocating " << nObjsAlloc << " nodes and " << nVars << " x " << nUniqueSize << " unique table entries" << std::endl; + vVars.resize(nObjsAlloc); + vObjs.resize((lit)nObjsAlloc * 2); + vNexts.resize(nObjsAlloc); + vMarks.resize(nObjsAlloc); + vvUnique.resize(nVars); + vUniqueMasks.resize(nVars); + vUniqueCounts.resize(nVars); + vUniqueTholds.resize(nVars); + for(var v = 0; v < nVars; v++) { + vvUnique[v].resize(nUniqueSize); + vUniqueMasks[v] = nUniqueSize - 1; + if((lit)(nUniqueSize * p.UniqueDensity) > (lit)BvarMax()) + vUniqueTholds[v] = BvarMax(); + else + vUniqueTholds[v] = (bvar)(nUniqueSize * p.UniqueDensity); + } + if(p.fCountOnes) { + if(nVars > 1023) + throw std::length_error("nVars must be less than 1024 to count ones"); + vOneCounts.resize(nObjsAlloc); + } + // set up cache + cache = new Cache(p.nCacheSizeLog, p.nCacheMaxLog, p.nCacheVerbose); + // create nodes for variables + nObjs = 1; + vVars[0] = VarMax(); + for(var v = 0; v < nVars; v++) + UniqueCreateInt(v, 1, 0); + // set up variable order + Var2Level.resize(nVars); + Level2Var.resize(nVars); + for(var v = 0; v < nVars; v++) { + if(p.pVar2Level) + Var2Level[v] = (*p.pVar2Level)[v]; + else + Var2Level[v] = v; + Level2Var[Var2Level[v]] = v; + } + // set other parameters + RemovedHead = 0; + nGbc = p.nGbc; + nReo = p.nReo; + MaxGrowth = p.MaxGrowth; + fReoVerbose = p.fReoVerbose; + if(nGbc || nReo != BvarMax()) + vRefs.resize(nObjsAlloc); + } + ~Man() { + if(nVerbose) { + std::cout << "Free " << nObjsAlloc << " nodes (" << nObjs << " live nodes)" << std::endl; + std::cout << "Free {"; + std::string delim; + for(var v = 0; v < nVars; v++) { + std::cout << delim << vvUnique[v].size(); + delim = ", "; + } + std::cout << "} unique table entries" << std::endl; + if(!vRefs.empty()) + std::cout << "Free " << vRefs.size() << " refs" << std::endl; + } + delete cache; + } + void Reorder() { + if(nVerbose >= 2) + std::cout << "Reorder" << std::endl; + int nGbc_ = nGbc; + nGbc = 0; + CountEdges(); + Sift(); + vEdges.clear(); + cache->Clear(); + nGbc = nGbc_; + } + inline lit And(lit x, lit y) { + if(nObjs > nReo) { + Reorder(); + while(nReo < nObjs) { + nReo <<= 1; + if((lit)nReo > (lit)BvarMax()) + nReo = BvarMax(); + } + } + return And_rec(x, y); + } + inline lit Or(lit x, lit y) { + return LitNot(And(LitNot(x), LitNot(y))); + } + + public: + void SetRef(std::vector const &vLits) { + vRefs.clear(); + vRefs.resize(nObjsAlloc); + for(size_t i = 0; i < vLits.size(); i++) + IncRef(vLits[i]); + } + void TurnOffReo() { + nReo = BvarMax(); + if(!nGbc) + vRefs.clear(); + } + bvar CountNodes() { + bvar count = 1; + if(!vEdges.empty()) { + for(bvar a = 1; a < nObjs; a++) + if(EdgeOfBvar(a)) + count++; + return count; + } + for(bvar a = 1; a <= (bvar)nVars; a++) { + count++; + SetMarkOfBvar(a); + } + for(bvar a = (bvar)nVars + 1; a < nObjs; a++) + if(RefOfBvar(a)) + count += CountNodes_rec(Bvar2Lit(a)); + for(bvar a = 1; a <= (bvar)nVars; a++) + ResetMarkOfBvar(a); + for(bvar a = (bvar)nVars + 1; a < nObjs; a++) + if(RefOfBvar(a)) + ResetMark_rec(Bvar2Lit(a)); + return count; + } + bvar CountNodes(std::vector const &vLits) { + bvar count = 1; + for(size_t i = 0; i < vLits.size(); i++) + count += CountNodes_rec(vLits[i]); + for(size_t i = 0; i < vLits.size(); i++) + ResetMark_rec(vLits[i]); + return count; + } + void PrintStats() { + bvar nRemoved = 0; + bvar a = RemovedHead; + while(a) + a = vNexts[a], nRemoved++; + bvar nLive = 1; + for(var v = 0; v < nVars; v++) + nLive += vUniqueCounts[v]; + std::cout << "ref: " << std::setw(10) << (vRefs.empty()? 0: CountNodes()) << ", " + << "used: " << std::setw(10) << nObjs << ", " + << "live: " << std::setw(10) << nLive << ", " + << "dead: " << std::setw(10) << nRemoved << ", " + << "alloc: " << std::setw(10) << nObjsAlloc + << std::endl; + } + }; + +} + +ABC_NAMESPACE_CXX_HEADER_END + +#endif diff --git a/src/aig/gia/giaNewTt.h b/src/aig/gia/giaNewTt.h new file mode 100644 index 000000000..15dfc53a9 --- /dev/null +++ b/src/aig/gia/giaNewTt.h @@ -0,0 +1,261 @@ +#ifndef ABC__aig__gia__giaNewTt_h +#define ABC__aig__gia__giaNewTt_h + +#include +#include +#include +#include +#include + +ABC_NAMESPACE_CXX_HEADER_START + +namespace NewTt { + + typedef int bvar; + typedef unsigned lit; + typedef unsigned short ref; + typedef unsigned long long size; + + static inline bvar BvarMax() { return std::numeric_limits::max(); } + static inline lit LitMax() { return std::numeric_limits::max(); } + static inline ref RefMax() { return std::numeric_limits::max(); } + static inline size SizeMax() { return std::numeric_limits::max(); } + + struct Param { + int nObjsAllocLog; + int nObjsMaxLog; + int nVerbose; + bool fCountOnes; + int nGbc; + int nReo; // dummy + Param() { + nObjsAllocLog = 15; + nObjsMaxLog = 20; + nVerbose = 0; + fCountOnes = false; + nGbc = 0; + nReo = BvarMax(); + } + }; + + class Man { + private: + typedef unsigned long long word; + typedef std::bitset<64> bsw; + static inline int ww() { return 64; } // word width + static inline int lww() { return 6; } // log word width + static inline word one() {return 0xffffffffffffffffull; } + static inline word vars(int i) { + static const word vars[] = {0xaaaaaaaaaaaaaaaaull, + 0xccccccccccccccccull, + 0xf0f0f0f0f0f0f0f0ull, + 0xff00ff00ff00ff00ull, + 0xffff0000ffff0000ull, + 0xffffffff00000000ull}; + return vars[i]; + } + static inline word ones(int i) { + static const word ones[] = {0x0000000000000001ull, + 0x0000000000000003ull, + 0x000000000000000full, + 0x00000000000000ffull, + 0x000000000000ffffull, + 0x00000000ffffffffull, + 0xffffffffffffffffull}; + return ones[i]; + } + + private: + int nVars; + bvar nObjs; + bvar nObjsAlloc; + bvar nObjsMax; + size nSize; + size nTotalSize; + std::vector vVals; + std::vector vDeads; + std::vector vRefs; + int nGbc; + int nVerbose; + + public: + inline lit Bvar2Lit(bvar a) const { return (lit)a << 1; } + inline bvar Lit2Bvar(lit x) const { return (bvar)(x >> 1); } + inline lit IthVar(int v) const { return ((lit)v + 1) << 1; } + inline lit LitNot(lit x) const { return x ^ (lit)1; } + inline lit LitNotCond(lit x, bool c) const { return x ^ (lit)c; } + inline bool LitIsCompl(lit x) const { return x & (lit)1; } + inline ref Ref(lit x) const { return vRefs[Lit2Bvar(x)]; } + inline lit Const0() const { return (lit)0; } + inline lit Const1() const { return (lit)1; } + inline bool IsConst0(lit x) const { + bvar a = Lit2Bvar(x); + word c = LitIsCompl(x)? one(): 0; + for(size j = 0; j < nSize; j++) + if(vVals[nSize * a + j] ^ c) + return false; + return true; + } + inline bool IsConst1(lit x) const { + bvar a = Lit2Bvar(x); + word c = LitIsCompl(x)? one(): 0; + for(size j = 0; j < nSize; j++) + if(~(vVals[nSize * a + j] ^ c)) + return false; + return true; + } + inline bool LitIsEq(lit x, lit y) const { + if(x == y) + return true; + if(x == LitMax() || y == LitMax()) + return false; + bvar xvar = Lit2Bvar(x); + bvar yvar = Lit2Bvar(y); + word c = LitIsCompl(x) ^ LitIsCompl(y)? one(): 0; + for(size j = 0; j < nSize; j++) + if(vVals[nSize * xvar + j] ^ vVals[nSize * yvar + j] ^ c) + return false; + return true; + } + inline size OneCount(lit x) const { + bvar a = Lit2Bvar(x); + size count = 0; + if(nVars > 6) { + for(size j = 0; j < nSize; j++) + count += bsw(vVals[nSize * a + j]).count(); + } else + count = bsw(vVals[nSize * a] & ones(nVars)).count(); + return LitIsCompl(x)? ((size)1 << nVars) - count: count; + } + + public: + inline void IncRef(lit x) { if(!vRefs.empty() && Ref(x) != RefMax()) vRefs[Lit2Bvar(x)]++; } + inline void DecRef(lit x) { if(!vRefs.empty() && Ref(x) != RefMax()) vRefs[Lit2Bvar(x)]--; } + + public: + bool Resize() { + if(nObjsAlloc == nObjsMax) + return false; + lit nObjsAllocLit = (lit)nObjsAlloc << 1; + if(nObjsAllocLit > (lit)BvarMax()) + nObjsAlloc = BvarMax(); + else + nObjsAlloc = (bvar)nObjsAllocLit; + nTotalSize = nTotalSize << 1; + if(nVerbose >= 2) + std::cout << "Reallocating " << nObjsAlloc << " nodes" << std::endl; + vVals.resize(nTotalSize); + if(!vRefs.empty()) + vRefs.resize(nObjsAlloc); + return true; + } + bool Gbc() { + if(nVerbose >= 2) + std::cout << "Garbage collect" << std::endl; + for(bvar a = nVars + 1; a < nObjs; a++) + if(!vRefs[a]) + vDeads.push_back(a); + return vDeads.size(); + } + + public: + Man(int nVars, Param p): nVars(nVars) { + if(p.nObjsMaxLog < p.nObjsAllocLog) + throw std::invalid_argument("nObjsMax must not be smaller than nObjsAlloc"); + if(nVars >= lww()) + nSize = 1ull << (nVars - lww()); + else + nSize = 1; + if(!nSize) + throw std::length_error("Memout (nVars) in init"); + if(!(nSize << p.nObjsMaxLog)) + throw std::length_error("Memout (nObjsMax) in init"); + lit nObjsMaxLit = (lit)1 << p.nObjsMaxLog; + if(!nObjsMaxLit) + throw std::length_error("Memout (nObjsMax) in init"); + if(nObjsMaxLit > (lit)BvarMax()) + nObjsMax = BvarMax(); + else + nObjsMax = (bvar)nObjsMaxLit; + lit nObjsAllocLit = (lit)1 << p.nObjsAllocLog; + if(!nObjsAllocLit) + throw std::length_error("Memout (nObjsAlloc) in init"); + if(nObjsAllocLit > (lit)BvarMax()) + nObjsAlloc = BvarMax(); + else + nObjsAlloc = (bvar)nObjsAllocLit; + if(nObjsAlloc <= (bvar)nVars) + throw std::invalid_argument("nObjsAlloc must be larger than nVars"); + nTotalSize = nSize << p.nObjsAllocLog; + vVals.resize(nTotalSize); + if(p.fCountOnes && nVars > 63) + throw std::length_error("nVars must be less than 64 to count ones"); + nObjs = 1; + for(int i = 0; i < 6 && i < nVars; i++) { + for(size j = 0; j < nSize; j++) + vVals[nSize * nObjs + j] = vars(i); + nObjs++; + } + for(int i = 0; i < nVars - 6; i++) { + for(size j = 0; j < nSize; j += (2ull << i)) + for(size k = 0; k < (1ull << i); k++) + vVals[nSize * nObjs + j + k] = one(); + nObjs++; + } + nVerbose = p.nVerbose; + nGbc = p.nGbc; + if(nGbc || p.nReo != BvarMax()) + vRefs.resize(nObjsAlloc); + } + inline lit And(lit x, lit y) { + bvar xvar = Lit2Bvar(x); + bvar yvar = Lit2Bvar(y); + word xcompl = LitIsCompl(x)? one(): 0; + word ycompl = LitIsCompl(y)? one(): 0; + unsigned j; + if(nObjs >= nObjsAlloc && vDeads.empty()) { + bool fRemoved = false; + if(nGbc > 1) + fRemoved = Gbc(); + if(!Resize() && !fRemoved && (nGbc != 1 || !Gbc())) + throw std::length_error("Memout (node)"); + } + bvar zvar; + if(nObjs < nObjsAlloc) + zvar = nObjs++; + else + zvar = vDeads.back(), vDeads.resize(vDeads.size() - 1); + for(j = 0; j < nSize; j++) + vVals[nSize * zvar + j] = (vVals[nSize * xvar + j] ^ xcompl) & (vVals[nSize * yvar + j] ^ ycompl); + return zvar << 1; + } + inline lit Or(lit x, lit y) { + return LitNot(And(LitNot(x), LitNot(y))); + } + void Reorder() {} // dummy + + public: + void SetRef(std::vector const &vLits) { + vRefs.clear(); + vRefs.resize(nObjsAlloc); + for(size_t i = 0; i < vLits.size(); i++) + IncRef(vLits[i]); + } + void TurnOffReo() { + if(!nGbc) + vRefs.clear(); + } + void PrintNode(lit x) const { + bvar a = Lit2Bvar(x); + word c = LitIsCompl(x)? one(): 0; + for(size j = 0; j < nSize; j++) + std::cout << bsw(vVals[nSize * a + j] ^ c); + std::cout << std::endl; + } + }; + +} + +ABC_NAMESPACE_CXX_HEADER_END + +#endif diff --git a/src/aig/gia/giaTransduction.cpp b/src/aig/gia/giaTransduction.cpp new file mode 100644 index 000000000..8bb680cb4 --- /dev/null +++ b/src/aig/gia/giaTransduction.cpp @@ -0,0 +1,125 @@ +#ifdef _WIN32 +#ifndef __MINGW32__ +#pragma warning(disable : 4786) // warning C4786: identifier was truncated to '255' characters in the browser information +#endif +#endif + +#include "giaTransduction.h" +#include "giaNewBdd.h" +#include "giaNewTt.h" + +ABC_NAMESPACE_IMPL_START + +Gia_Man_t *Gia_ManTransductionBdd(Gia_Man_t *pGia, int nType, int fMspf, int nRandom, int nSortType, int nPiShuffle, int nParameter, int fLevel, Gia_Man_t *pExdc, int fNewLine, int nVerbose) { + if(nRandom) { + srand(nRandom); + nSortType = rand() % 4; + nPiShuffle = rand(); + nParameter = rand() % 16; + } + NewBdd::Param p; + Transduction::Transduction t(pGia, nVerbose, fNewLine, nSortType, nPiShuffle, fLevel, pExdc, p); + int count = t.CountWires(); + switch(nType) { + case 0: + count -= fMspf? t.Mspf(): t.Cspf(); + break; + case 1: + count -= t.Resub(fMspf); + break; + case 2: + count -= t.ResubMono(fMspf); + break; + case 3: + count -= t.ResubShared(fMspf); + break; + case 4: + count -= t.RepeatResub(false, fMspf); + break; + case 5: + count -= t.RepeatResub(true, fMspf); + break; + case 6: { + bool fInner = (nParameter / 4) % 2; + count -= t.RepeatInner(fMspf, fInner); + break; + } + case 7: { + bool fInner = (nParameter / 4) % 2; + bool fOuter = (nParameter / 8) % 2; + count -= t.RepeatOuter(fMspf, fInner, fOuter); + break; + } + case 8: { + bool fFirstMerge = nParameter % 2; + bool fMspfMerge = fMspf? (nParameter / 2) % 2: false; + bool fInner = (nParameter / 4) % 2; + bool fOuter = (nParameter / 8) % 2; + count -= t.RepeatAll(fFirstMerge, fMspfMerge, fMspf, fInner, fOuter); + break; + } + default: + std::cout << "Unknown transduction type " << nType << std::endl; + } + assert(t.Verify()); + assert(count == t.CountWires()); + return t.GenerateAig(); +} + +Gia_Man_t *Gia_ManTransductionTt(Gia_Man_t *pGia, int nType, int fMspf, int nRandom, int nSortType, int nPiShuffle, int nParameter, int fLevel, Gia_Man_t *pExdc, int fNewLine, int nVerbose) { + if(nRandom) { + srand(nRandom); + nSortType = rand() % 4; + nPiShuffle = rand(); + nParameter = rand() % 16; + } + NewTt::Param p; + Transduction::Transduction t(pGia, nVerbose, fNewLine, nSortType, nPiShuffle, fLevel, pExdc, p); + int count = t.CountWires(); + switch(nType) { + case 0: + count -= fMspf? t.Mspf(): t.Cspf(); + break; + case 1: + count -= t.Resub(fMspf); + break; + case 2: + count -= t.ResubMono(fMspf); + break; + case 3: + count -= t.ResubShared(fMspf); + break; + case 4: + count -= t.RepeatResub(false, fMspf); + break; + case 5: + count -= t.RepeatResub(true, fMspf); + break; + case 6: { + bool fInner = (nParameter / 4) % 2; + count -= t.RepeatInner(fMspf, fInner); + break; + } + case 7: { + bool fInner = (nParameter / 4) % 2; + bool fOuter = (nParameter / 8) % 2; + count -= t.RepeatOuter(fMspf, fInner, fOuter); + break; + } + case 8: { + bool fFirstMerge = nParameter % 2; + bool fMspfMerge = fMspf? (nParameter / 2) % 2: false; + bool fInner = (nParameter / 4) % 2; + bool fOuter = (nParameter / 8) % 2; + count -= t.RepeatAll(fFirstMerge, fMspfMerge, fMspf, fInner, fOuter); + break; + } + default: + std::cout << "Unknown transduction type " << nType << std::endl; + } + assert(t.Verify()); + assert(count == t.CountWires()); + return t.GenerateAig(); +} + +ABC_NAMESPACE_IMPL_END diff --git a/src/aig/gia/giaTransduction.h b/src/aig/gia/giaTransduction.h new file mode 100644 index 000000000..963147839 --- /dev/null +++ b/src/aig/gia/giaTransduction.h @@ -0,0 +1,1745 @@ +#ifndef ABC__aig__gia__giaTransduction_h +#define ABC__aig__gia__giaTransduction_h + +#include +#include +#include +#include +#include +#include +#include +#include + +#include "gia.h" + +ABC_NAMESPACE_CXX_HEADER_START + +namespace Transduction { + +enum PfState {none, cspf, mspf}; + +template +class ManUtil { +protected: + Man *man; + inline void IncRef(lit x) const { + if(x != LitMax) + man->IncRef(x); + } + inline void DecRef(lit x) const { + if(x != LitMax) + man->DecRef(x); + } + inline void Update(lit &x, lit y) const { + DecRef(x); + x = y; + IncRef(x); + } + inline void DelVec(std::vector &v) const { + for(unsigned i = 0; i < v.size(); i++) + DecRef(v[i]); + v.clear(); + } + inline void DelVec(std::vector > &v) const { + for(unsigned i = 0; i < v.size(); i++) + DelVec(v[i]); + v.clear(); + } + inline void CopyVec(std::vector &v, std::vector const &u) const { + DelVec(v); + v = u; + for(unsigned i = 0; i < v.size(); i++) + IncRef(v[i]); + } + inline void CopyVec(std::vector > &v, std::vector > const &u) const { + for(unsigned i = u.size(); i < v.size(); i++) + DelVec(v[i]); + v.resize(u.size()); + for(unsigned i = 0; i < v.size(); i++) + CopyVec(v[i], u[i]); + } + inline bool LitVecIsEq(std::vector const &v, std::vector const &u) const { + if(v.size() != u.size()) + return false; + for(unsigned i = 0; i < v.size(); i++) + if(!man->LitIsEq(v[i], u[i])) + return false; + return true; + } + inline bool LitVecIsEq(std::vector > const &v, std::vector > const &u) const { + if(v.size() != u.size()) + return false; + for(unsigned i = 0; i < v.size(); i++) + if(!LitVecIsEq(v[i], u[i])) + return false; + return true; + } + inline lit Xor(lit x, lit y) const { + lit f = man->And(x, man->LitNot(y)); + man->IncRef(f); + lit g = man->And(man->LitNot(x), y); + man->IncRef(g); + lit r = man->Or(f, g); + man->DecRef(f); + man->DecRef(g); + return r; + } +}; + +template +class TransductionBackup: ManUtil { +private: + int nObjsAlloc; + PfState state; + std::list vObjs; + std::vector > vvFis; + std::vector > vvFos; + std::vector vLevels; + std::vector vSlacks; + std::vector > vvFiSlacks; + std::vector vFs; + std::vector vGs; + std::vector > vvCs; + std::vector vUpdates; + std::vector vPfUpdates; + std::vector vFoConeShared; + template + friend class Transduction; + +public: + ~TransductionBackup() { + if(this->man) { + this->DelVec(vFs); + this->DelVec(vGs); + this->DelVec(vvCs); + } + } +}; + +template +class Transduction: ManUtil { +private: + int nVerbose; + int nSortType; + bool fLevel; + int nObjsAlloc; + int nMaxLevels; + PfState state; + std::vector vPis; + std::vector vPos; + std::list vObjs; + std::vector > vvFis; + std::vector > vvFos; + std::vector vLevels; + std::vector vSlacks; + std::vector > vvFiSlacks; + std::vector vFs; + std::vector vGs; + std::vector > vvCs; + std::vector vUpdates; + std::vector vPfUpdates; + std::vector vFoConeShared; + std::vector vPoFs; + + bool fNewLine; + abctime startclk; + +private: // Helper functions + inline bool AllFalse(std::vector const &v) const { + for(std::list::const_iterator it = vObjs.begin(); it != vObjs.end(); it++) + if(v[*it]) + return false; + return true; + } + +public: // Counting + inline int CountGates() const { + return vObjs.size(); + } + inline int CountWires() const { + int count = 0; + for(std::list::const_iterator it = vObjs.begin(); it != vObjs.end(); it++) + count += vvFis[*it].size(); + return count; + } + inline int CountNodes() const { + return CountWires() - CountGates(); + } + inline int CountLevels() const { + int count = 0; + for(unsigned i = 0; i < vPos.size(); i++) + count = std::max(count, vLevels[vvFis[vPos[i]][0] >> 1]); + return count; + } + inline void Print(std::string str, bool nl) const { + if(!fNewLine) + std::cout << "\33[2K\r"; + std::cout << str; + if(fNewLine || nl) + std::cout << std::endl; + else + std::cout << std::flush; + } + inline void PrintStats(std::string prefix, bool nl, int prefix_size = 0) const { + if(!prefix_size) + prefix_size = prefix.size(); + std::stringstream ss; + ss << std::left << std::setw(prefix_size) << prefix << ": " << std::right; + ss << "#nodes = " << std::setw(5) << CountNodes(); + if(fLevel) + ss << ", #level = " << std::setw(5) << CountLevels(); + ss << ", elapsed = " << std::setprecision(2) << std::fixed << std::setw(8) << 1.0 * (Abc_Clock() - startclk) / CLOCKS_PER_SEC << "s"; + Print(ss.str(), nl); + } + inline void PrintPfHeader(std::string prefix, int block, int block_i0) { + std::stringstream ss; + ss << "\t\t" << prefix; + if(block_i0 != -1) + ss << " (blocking Wire " << block_i0 << " -> " << block << ")"; + else if(block != -1) + ss << " (blocking Gate " << block << ")"; + Print(ss.str(), true); + } + +private: // MIAIG + void SortObjs_rec(std::list::iterator const &it) { + for(unsigned j = 0; j < vvFis[*it].size(); j++) { + int i0 = vvFis[*it][j] >> 1; + if(!vvFis[i0].empty()) { + std::list::iterator it_i0 = std::find(it, vObjs.end(), i0); + if(it_i0 != vObjs.end()) { + // if(nVerbose > 6) + // std::cout << "\t\t\t\t\t\tMove " << i0 << " before " << *it << std::endl; + vObjs.erase(it_i0); + it_i0 = vObjs.insert(it, i0); + SortObjs_rec(it_i0); + } + } + } + } + inline void Connect(int i, int f, bool fSort = false, bool fUpdate = true, lit c = LitMax) { + int i0 = f >> 1; + if(nVerbose > 5) { + std::stringstream ss; + ss << "\t\t\t\t\tadd Wire " << std::setw(5) << i0 << "(" << (f & 1) << ")" + << " -> " << std::setw(5) << i; + Print(ss.str(), true); + } + assert(std::find(vvFis[i].begin(), vvFis[i].end(), f) == vvFis[i].end()); + vvFis[i].push_back(f); + vvFos[i0].push_back(i); + if(fUpdate) + vUpdates[i] = true; + this->IncRef(c); + vvCs[i].push_back(c); + if(fSort && !vvFos[i].empty() && !vvFis[i0].empty()) { + std::list::iterator it = find(vObjs.begin(), vObjs.end(), i); + std::list::iterator it_i0 = find(it, vObjs.end(), i0); + if(it_i0 != vObjs.end()) { + // if(nVerbose > 6) + // std::cout << "\t\t\t\t\t\tMove " << i0 << " before " << *it << std::endl; + vObjs.erase(it_i0); + it_i0 = vObjs.insert(it, i0); + SortObjs_rec(it_i0); + } + } + } + inline void Disconnect(int i, int i0, unsigned j, bool fUpdate = true, bool fPfUpdate = true) { + if(nVerbose > 5) { + std::stringstream ss; + ss << "\t\t\t\t\tremove Wire " << std::setw(5) << i0 << "(" << (vvFis[i][j] & 1) << ")" + << " -> " << std::setw(5) << i; + Print(ss.str(), true); + } + vvFos[i0].erase(std::find(vvFos[i0].begin(), vvFos[i0].end(), i)); + vvFis[i].erase(vvFis[i].begin() + j); + this->DecRef(vvCs[i][j]); + vvCs[i].erase(vvCs[i].begin() + j); + if(fUpdate) + vUpdates[i] = true; + if(fPfUpdate) + vPfUpdates[i0] = true; + } + inline int Remove(int i, bool fPfUpdate = true) { + if(nVerbose > 5) { + std::stringstream ss; + ss << "\t\t\t\t\tremove Gate " << std::setw(5) << i; + Print(ss.str(), true); + } + assert(vvFos[i].empty()); + for(unsigned j = 0; j < vvFis[i].size(); j++) { + int i0 = vvFis[i][j] >> 1; + vvFos[i0].erase(std::find(vvFos[i0].begin(), vvFos[i0].end(), i)); + if(fPfUpdate) + vPfUpdates[i0] = true; + } + int count = vvFis[i].size(); + vvFis[i].clear(); + this->DecRef(vFs[i]); + this->DecRef(vGs[i]); + vFs[i] = vGs[i] = LitMax; + this->DelVec(vvCs[i]); + vUpdates[i] = vPfUpdates[i] = false; + return count; + } + inline int FindFi(int i, int i0) const { + for(unsigned j = 0; j < vvFis[i].size(); j++) + if((vvFis[i][j] >> 1) == i0) + return j; + return -1; + } + inline int Replace(int i, int f, bool fUpdate = true) { + if(nVerbose > 4) { + std::stringstream ss; + ss << "\t\t\t\treplace Gate " << std::setw(5) << i + << " by Node " << std::setw(5) << (f >> 1) << "(" << (f & 1) << ")"; + Print(ss.str(), true); + } + assert(i != (f >> 1)); + int count = 0; + for(unsigned j = 0; j < vvFos[i].size(); j++) { + int k = vvFos[i][j]; + int l = FindFi(k, i); + assert(l >= 0); + int fc = f ^ (vvFis[k][l] & 1); + if(find(vvFis[k].begin(), vvFis[k].end(), fc) != vvFis[k].end()) { + this->DecRef(vvCs[k][l]); + vvCs[k].erase(vvCs[k].begin() + l); + vvFis[k].erase(vvFis[k].begin() + l); + count++; + } else { + vvFis[k][l] = f ^ (vvFis[k][l] & 1); + vvFos[f >> 1].push_back(k); + } + if(fUpdate) + vUpdates[k] = true; + } + vvFos[i].clear(); + vPfUpdates[f >> 1] = true; + return count + Remove(i); + } + int ReplaceByConst(int i, bool c) { + if(nVerbose > 4) { + std::stringstream ss; + ss << "\t\t\t\treplace Gate " << std::setw(5) << i << " by Const " << c; + Print(ss.str(), true); + } + int count = 0; + for(unsigned j = 0; j < vvFos[i].size(); j++) { + int k = vvFos[i][j]; + int l = FindFi(k, i); + assert(l >= 0); + bool fc = c ^ (vvFis[k][l] & 1); + this->DecRef(vvCs[k][l]); + vvCs[k].erase(vvCs[k].begin() + l); + vvFis[k].erase(vvFis[k].begin() + l); + if(fc) { + if(vvFis[k].size() == 1) + count += Replace(k, vvFis[k][0]); + else + vUpdates[k] = true; + } else + count += ReplaceByConst(k, 0); + } + count += vvFos[i].size(); + vvFos[i].clear(); + return count + Remove(i); + } + inline void NewGate(int &pos) { + while(pos != nObjsAlloc && (!vvFis[pos].empty() || !vvFos[pos].empty())) + pos++; + if(nVerbose > 5) { + std::stringstream ss; + ss << "\t\t\t\t\tcreate Gate " << std::setw(5) << pos; + Print(ss.str(), true); + } + if(pos == nObjsAlloc) { + nObjsAlloc++; + vvFis.resize(nObjsAlloc); + vvFos.resize(nObjsAlloc); + if(fLevel) { + vLevels.resize(nObjsAlloc); + vSlacks.resize(nObjsAlloc); + vvFiSlacks.resize(nObjsAlloc); + } + vFs.resize(nObjsAlloc, LitMax); + vGs.resize(nObjsAlloc, LitMax); + vvCs.resize(nObjsAlloc); + vUpdates.resize(nObjsAlloc); + vPfUpdates.resize(nObjsAlloc); + } + } + void MarkFiCone_rec(std::vector &vMarks, int i) const { + if(vMarks[i]) + return; + vMarks[i] = true; + for(unsigned j = 0; j < vvFis[i].size(); j++) + MarkFiCone_rec(vMarks, vvFis[i][j] >> 1); + } + void MarkFoCone_rec(std::vector &vMarks, int i) const { + if(vMarks[i]) + return; + vMarks[i] = true; + for(unsigned j = 0; j < vvFos[i].size(); j++) + MarkFoCone_rec(vMarks, vvFos[i][j]); + } + bool IsFoConeShared_rec(std::vector &vVisits, int i, int visitor) const { + if(vVisits[i] == visitor) + return false; + if(vVisits[i]) + return true; + vVisits[i] = visitor; + for(unsigned j = 0; j < vvFos[i].size(); j++) + if(IsFoConeShared_rec(vVisits, vvFos[i][j], visitor)) + return true; + return false; + } + inline bool IsFoConeShared(int i) const { + std::vector vVisits(nObjsAlloc); + for(unsigned j = 0; j < vvFos[i].size(); j++) + if(IsFoConeShared_rec(vVisits, vvFos[i][j], j + 1)) + return true; + return false; + } + +private: // Level calculation + inline void add(std::vector &a, unsigned i) { + if(a.size() <= i) { + a.resize(i + 1); + a[i] = true; + return; + } + for(; i < a.size() && a[i]; i++) + a[i] = false; + if(i == a.size()) + a.resize(i + 1); + a[i] = true; + } + inline bool balanced(std::vector const &a) { + for(unsigned i = 0; i < a.size() - 1; i++) + if(a[i]) + return false; + return true; + } + inline bool noexcess(std::vector const &a, unsigned i) { + if(a.size() <= i) + return false; + for(unsigned j = i; j < a.size(); j++) + if(!a[j]) + return true; + for(unsigned j = 0; j < i; j++) + if(a[j]) + return false; + return true; + } + inline void ComputeLevel() { + for(std::list::iterator it = vObjs.begin(); it != vObjs.end(); it++) { + if(vvFis[*it].size() == 2) + vLevels[*it] = std::max(vLevels[vvFis[*it][0] >> 1], vLevels[vvFis[*it][1] >> 1]) + 1; + else { + std::vector lev; + for(unsigned j = 0; j < vvFis[*it].size(); j++) + add(lev, vLevels[vvFis[*it][j] >> 1]); + if(balanced(lev)) + vLevels[*it] = (int)lev.size() - 1; + else + vLevels[*it] = (int)lev.size(); + } + } + if(nMaxLevels == -1) + nMaxLevels = CountLevels(); + for(unsigned i = 0; i < vPos.size(); i++) { + vvFiSlacks[vPos[i]].resize(1); + vvFiSlacks[vPos[i]][0] = nMaxLevels - vLevels[vvFis[vPos[i]][0] >> 1]; + } + for(std::list::reverse_iterator it = vObjs.rbegin(); it != vObjs.rend(); it++) { + vSlacks[*it] = nMaxLevels; + for(unsigned j = 0; j < vvFos[*it].size(); j++) { + int k = vvFos[*it][j]; + int l = FindFi(k, *it); + assert(l >= 0); + vSlacks[*it] = std::min(vSlacks[*it], vvFiSlacks[k][l]); + } + vvFiSlacks[*it].resize(vvFis[*it].size()); + for(unsigned j = 0; j < vvFis[*it].size(); j++) + vvFiSlacks[*it][j] = vSlacks[*it] + vLevels[*it] - 1 - vLevels[vvFis[*it][j] >> 1]; + } + } + +private: // Cost function + inline void ShufflePis(int seed) { + srand(seed); + for(int i = (int)vPis.size() - 1; i > 0; i--) + std::swap(vPis[i], vPis[rand() % (i + 1)]); + } + inline bool CostCompare(int a, int b) const { // return (cost(a) > cost(b)) + int a0 = a >> 1; + int b0 = b >> 1; + if(vvFis[a0].empty() && vvFis[b0].empty()) + return std::find(find(vPis.begin(), vPis.end(), a0), vPis.end(), b0) != vPis.end(); + if(vvFis[a0].empty() && !vvFis[b0].empty()) + return false; + if(!vvFis[a0].empty() && vvFis[b0].empty()) + return true; + if(vvFos[a0].size() > vvFos[b0].size()) + return false; + if(vvFos[a0].size() < vvFos[b0].size()) + return true; + bool ac = a & 1; + bool bc = b & 1; + switch(nSortType) { + case 0: + return std::find(find(vObjs.begin(), vObjs.end(), a0), vObjs.end(), b0) == vObjs.end(); + case 1: + return this->man->OneCount(this->man->LitNotCond(vFs[a0], ac)) < this->man->OneCount(this->man->LitNotCond(vFs[b0], bc)); + case 2: + return this->man->OneCount(vFs[a0]) < this->man->OneCount(vFs[b0]); + case 3: + return this->man->OneCount(this->man->LitNot(vFs[a0])) < this->man->OneCount(vFs[b0]); // pseudo random + default: + return false; // no sorting + } + } + inline bool SortFis(int i) { + if(nVerbose > 5) { + std::stringstream ss; + ss << "\t\t\t\tsort FIs Gate " << std::setw(5) << i; + Print(ss.str(), true); + } + bool fSort = false; + for(int p = 1; p < (int)vvFis[i].size(); p++) { + int f = vvFis[i][p]; + lit c = vvCs[i][p]; + int q = p - 1; + for(; q >= 0 && CostCompare(f, vvFis[i][q]); q--) { + vvFis[i][q + 1] = vvFis[i][q]; + vvCs[i][q + 1] = vvCs[i][q]; + } + if(q + 1 != p) { + fSort = true; + vvFis[i][q + 1] = f; + vvCs[i][q + 1] = c; + } + } + if(nVerbose > 5) + for(unsigned j = 0; j < vvFis[i].size(); j++) { + std::stringstream ss; + ss << "\t\t\t\t\tFI " << j << " = " + << std::setw(5) << (vvFis[i][j] >> 1) << "(" << (vvFis[i][j] & 1) << ")"; + Print(ss.str(), true); + } + return fSort; + } + +private: // Symbolic simulation + inline lit LitFi(int i, int j) const { + int i0 = vvFis[i][j] >> 1; + bool c0 = vvFis[i][j] & 1; + return this->man->LitNotCond(vFs[i0], c0); + } + inline lit LitFi(int i, int j, std::vector const &vFs_) const { + int i0 = vvFis[i][j] >> 1; + bool c0 = vvFis[i][j] & 1; + return this->man->LitNotCond(vFs_[i0], c0); + } + inline void Build(int i, std::vector &vFs_) const { + if(nVerbose > 6) { + std::stringstream ss; + ss << "\t\t\t\tbuilding Gate" << std::setw(5) << i; + Print(ss.str(), nVerbose > 7); + } + this->Update(vFs_[i], this->man->Const1()); + for(unsigned j = 0; j < vvFis[i].size(); j++) + this->Update(vFs_[i], this->man->And(vFs_[i], LitFi(i, j, vFs_))); + } + inline void Build(bool fPfUpdate = true) { + if(nVerbose > 6) + Print("\t\t\tBuild", true); + for(std::list::iterator it = vObjs.begin(); it != vObjs.end(); it++) + if(vUpdates[*it]) { + lit x = vFs[*it]; + this->IncRef(x); + Build(*it, vFs); + this->DecRef(x); + if(!this->man->LitIsEq(x, vFs[*it])) + for(unsigned j = 0; j < vvFos[*it].size(); j++) + vUpdates[vvFos[*it][j]] = true; + } + if(fPfUpdate) + for(std::list::iterator it = vObjs.begin(); it != vObjs.end(); it++) + vPfUpdates[*it] = vPfUpdates[*it] || vUpdates[*it]; + for(std::list::iterator it = vObjs.begin(); it != vObjs.end(); it++) + vUpdates[*it] = false; + assert(AllFalse(vUpdates)); + } + void BuildFoConeCompl(int i, std::vector &vPoFsCompl) const { + if(nVerbose > 6) { + std::stringstream ss; + ss << "\t\t\tBuild with complemented Gate " << std::setw(5) << i; + Print(ss.str(), true); + } + std::vector vFsCompl; + this->CopyVec(vFsCompl, vFs); + vFsCompl[i] = this->man->LitNot(vFs[i]); + std::vector vUpdatesCompl(nObjsAlloc); + for(unsigned j = 0; j < vvFos[i].size(); j++) + vUpdatesCompl[vvFos[i][j]] = true; + for(std::list::const_iterator it = vObjs.begin(); it != vObjs.end(); it++) + if(vUpdatesCompl[*it]) { + Build(*it, vFsCompl); + if(!this->man->LitIsEq(vFsCompl[*it], vFs[*it])) + for(unsigned j = 0; j < vvFos[*it].size(); j++) + vUpdatesCompl[vvFos[*it][j]] = true; + } + for(unsigned j = 0; j < vPos.size(); j++) + this->Update(vPoFsCompl[j], LitFi(vPos[j], 0, vFsCompl)); + this->DelVec(vFsCompl); + } + +private: // CSPF + inline int RemoveRedundantFis(int i, int block_i0 = -1, unsigned j = 0) { + int count = 0; + for(; j < vvFis[i].size(); j++) { + if(block_i0 == (vvFis[i][j] >> 1)) + continue; + lit x = this->man->Const1(); + this->IncRef(x); + for(unsigned jj = 0; jj < vvFis[i].size(); jj++) + if(j != jj) + this->Update(x, this->man->And(x, LitFi(i, jj))); + this->Update(x, this->man->Or(this->man->LitNot(x), vGs[i])); + this->Update(x, this->man->Or(x, LitFi(i, j))); + this->DecRef(x); + if(this->man->IsConst1(x)) { + int i0 = vvFis[i][j] >> 1; + if(nVerbose > 4) { + std::stringstream ss; + ss << "\t\t\t\t[Rrfi] remove Wire " << std::setw(5) << i0 << "(" << (vvFis[i][j] & 1) << ")" + << " -> " << std::setw(5) << i; + Print(ss.str(), true); + } + Disconnect(i, i0, j--); + count++; + } + } + return count; + } + inline void CalcG(int i) { + this->Update(vGs[i], this->man->Const1()); + for(unsigned j = 0; j < vvFos[i].size(); j++) { + int k = vvFos[i][j]; + int l = FindFi(k, i); + assert(l >= 0); + this->Update(vGs[i], this->man->And(vGs[i], vvCs[k][l])); + } + } + inline int CalcC(int i) { + int count = 0; + for(unsigned j = 0; j < vvFis[i].size(); j++) { + lit x = this->man->Const1(); + this->IncRef(x); + for(unsigned jj = j + 1; jj < vvFis[i].size(); jj++) + this->Update(x, this->man->And(x, LitFi(i, jj))); + this->Update(x, this->man->Or(this->man->LitNot(x), vGs[i])); + int i0 = vvFis[i][j] >> 1; + if(this->man->IsConst1(this->man->Or(x, LitFi(i, j)))) { + if(nVerbose > 4) { + std::stringstream ss; + ss << "\t\t\t\t[Cspf] remove Wire " << std::setw(5) << i0 << "(" << (vvFis[i][j] & 1) << ")" + << " -> " << std::setw(5) << i; + Print(ss.str(), true); + } + Disconnect(i, i0, j--); + count++; + } else if(!this->man->LitIsEq(vvCs[i][j], x)) { + this->Update(vvCs[i][j], x); + vPfUpdates[i0] = true; + } + this->DecRef(x); + } + return count; + } + int Cspf(bool fSortRemove, int block = -1, int block_i0 = -1) { + if(nVerbose > 3) + PrintPfHeader("Cspf", block, block_i0); + if(state != cspf) + for(std::list::iterator it = vObjs.begin(); it != vObjs.end(); it++) + vPfUpdates[*it] = true; + state = cspf; + int count = 0; + for(std::list::reverse_iterator it = vObjs.rbegin(); it != vObjs.rend();) { + if(vvFos[*it].empty()) { + if(nVerbose > 3) { + std::stringstream ss; + ss << "\t\t\tremove unused Gate " << std::setw(5) << *it; + Print(ss.str(), nVerbose > 4); + } + count += Remove(*it); + it = std::list::reverse_iterator(vObjs.erase(--(it.base()))); + continue; + } + if(!vPfUpdates[*it]) { + it++; + continue; + } + if(nVerbose > 3) { + std::stringstream ss; + ss << "\t\t\tprocessing Gate " << std::setw(5) << *it + << " (" << std::setw(5) << std::distance(vObjs.rbegin(), it) + 1 + << "/" << std::setw(5) << vObjs.size() << ")"; + Print(ss.str(), nVerbose > 4); + } + CalcG(*it); + if(fSortRemove) { + if(*it != block) + SortFis(*it), count += RemoveRedundantFis(*it); + else if(block_i0 != -1) + count += RemoveRedundantFis(*it, block_i0); + } + count += CalcC(*it); + vPfUpdates[*it] = false; + assert(!vvFis[*it].empty()); + if(vvFis[*it].size() == 1) { + count += Replace(*it, vvFis[*it][0]); + it = std::list::reverse_iterator(vObjs.erase(--(it.base()))); + continue; + } + it++; + } + Build(false); + assert(AllFalse(vPfUpdates)); + if(fLevel) + ComputeLevel(); + return count; + } + +private: // MSPF + inline bool MspfCalcG(int i) { + lit g = vGs[i]; + this->IncRef(g); + std::vector vPoFsCompl(vPos.size(), LitMax); + BuildFoConeCompl(i, vPoFsCompl); + this->Update(vGs[i], this->man->Const1()); + for(unsigned j = 0; j < vPos.size(); j++) { + lit x = this->man->LitNot(this->Xor(vPoFs[j], vPoFsCompl[j])); + this->IncRef(x); + this->Update(x, this->man->Or(x, vvCs[vPos[j]][0])); + this->Update(vGs[i], this->man->And(vGs[i], x)); + this->DecRef(x); + } + this->DelVec(vPoFsCompl); + this->DecRef(g); + return !this->man->LitIsEq(vGs[i], g); + } + inline int MspfCalcC(int i, int block_i0 = -1) { + for(unsigned j = 0; j < vvFis[i].size(); j++) { + lit x = this->man->Const1(); + this->IncRef(x); + for(unsigned jj = 0; jj < vvFis[i].size(); jj++) + if(j != jj) + this->Update(x, this->man->And(x, LitFi(i, jj))); + this->Update(x, this->man->Or(this->man->LitNot(x), vGs[i])); + int i0 = vvFis[i][j] >> 1; + if(i0 != block_i0 && this->man->IsConst1(this->man->Or(x, LitFi(i, j)))) { + if(nVerbose > 4) { + std::stringstream ss; + ss << "\t\t\t\t[Mspf] remove Wire " << std::setw(5) << i0 << "(" << (vvFis[i][j] & 1) << ")" + << " -> " << std::setw(5) << i; + Print(ss.str(), true); + } + Disconnect(i, i0, j); + this->DecRef(x); + return RemoveRedundantFis(i, block_i0, j) + 1; + } else if(!this->man->LitIsEq(vvCs[i][j], x)) { + this->Update(vvCs[i][j], x); + vPfUpdates[i0] = true; + } + this->DecRef(x); + } + return 0; + } + int Mspf(bool fSort, int block = -1, int block_i0 = -1) { + if(nVerbose > 3) + PrintPfHeader("Mspf", block, block_i0); + assert(AllFalse(vUpdates)); + vFoConeShared.resize(nObjsAlloc); + if(state != mspf) + for(std::list::iterator it = vObjs.begin(); it != vObjs.end(); it++) + vPfUpdates[*it] = true; + state = mspf; + int count = 0; + int restarts = 0; + for(std::list::reverse_iterator it = vObjs.rbegin(); it != vObjs.rend();) { + if(vvFos[*it].empty()) { + if(nVerbose > 3) { + std::stringstream ss; + ss << "\t\t\tremove unused Gate " << std::setw(5) << *it; + Print(ss.str(), nVerbose > 4); + } + count += Remove(*it); + it = std::list::reverse_iterator(vObjs.erase(--(it.base()))); + continue; + } + if(!vFoConeShared[*it] && !vPfUpdates[*it] && (vvFos[*it].size() == 1 || !IsFoConeShared(*it))) { + it++; + continue; + } + if(nVerbose > 3) { + std::stringstream ss; + ss << "\t\t\tprocessing Gate " << std::setw(5) << *it + << " (" << std::setw(5) << std::distance(vObjs.rbegin(), it) + 1 + << "/" << std::setw(5) << vObjs.size() << ")" + << ", #restarts = " << std::setw(3) << restarts; + Print(ss.str(), nVerbose > 4); + } + if(vvFos[*it].size() == 1 || !IsFoConeShared(*it)) { + if(vFoConeShared[*it]) { + vFoConeShared[*it] = false; + lit g = vGs[*it]; + this->IncRef(g); + CalcG(*it); + this->DecRef(g); + if(g == vGs[*it] && !vPfUpdates[*it]) { + it++; + continue; + } + } else + CalcG(*it); + } else { + vFoConeShared[*it] = true; + if(!MspfCalcG(*it) && !vPfUpdates[*it]) { + it++; + continue; + } + bool IsConst1 = this->man->IsConst1(this->man->Or(vGs[*it], vFs[*it])); + bool IsConst0 = IsConst1? false: this->man->IsConst1(this->man->Or(vGs[*it], this->man->LitNot(vFs[*it]))); + if(IsConst1 || IsConst0) { + count += ReplaceByConst(*it, (int)IsConst1); + vObjs.erase(--(it.base())); + Build(); + it = vObjs.rbegin(); + restarts++; + continue; + } + } + if(fSort && block != *it) + SortFis(*it); + if(int diff = (block == *it)? MspfCalcC(*it, block_i0): MspfCalcC(*it)) { + count += diff; + assert(!vvFis[*it].empty()); + if(vvFis[*it].size() == 1) { + count += Replace(*it, vvFis[*it][0]); + vObjs.erase(--(it.base())); + } + Build(); + it = vObjs.rbegin(); + restarts++; + continue; + } + vPfUpdates[*it] = false; + it++; + } + assert(AllFalse(vUpdates)); + assert(AllFalse(vPfUpdates)); + if(fLevel) + ComputeLevel(); + return count; + } + +private: // Merge/decompose one + inline int TrivialMergeOne(int i) { + int count = 0; + std::vector vFisOld = vvFis[i]; + std::vector vCsOld = vvCs[i]; + vvFis[i].clear(); + vvCs[i].clear(); + for(unsigned j = 0; j < vFisOld.size(); j++) { + int i0 = vFisOld[j] >> 1; + int c0 = vFisOld[j] & 1; + if(vvFis[i0].empty() || vvFos[i0].size() > 1 || c0) { + if(nVerbose > 3) { + std::stringstream ss; + ss << "\t\t[TrivialMerge] adding Wire " << std::setw(5) << i0 << "(" << c0 << ")" + << " -> " << std::setw(5) << i; + Print(ss.str(), true); + } + vvFis[i].push_back(vFisOld[j]); + vvCs[i].push_back(vCsOld[j]); + continue; + } + vPfUpdates[i] = vPfUpdates[i] | vPfUpdates[i0]; + vvFos[i0].erase(find(vvFos[i0].begin(), vvFos[i0].end(), i)); + count++; + typename std::vector::iterator itfi = vFisOld.begin() + j; + typename std::vector::iterator itc = vCsOld.begin() + j; + for(unsigned jj = 0; jj < vvFis[i0].size(); jj++) { + int f = vvFis[i0][jj]; + std::vector::iterator it = find(vvFis[i].begin(), vvFis[i].end(), f); + if(it == vvFis[i].end()) { + vvFos[f >> 1].push_back(i); + itfi = vFisOld.insert(itfi, f); + itc = vCsOld.insert(itc, vvCs[i0][jj]); + this->IncRef(*itc); + itfi++; + itc++; + count--; + } else { + assert(state == none); + } + } + count += Remove(i0, false); + vObjs.erase(find(vObjs.begin(), vObjs.end(), i0)); + vFisOld.erase(itfi); + this->DecRef(*itc); + vCsOld.erase(itc); + j--; + } + return count; + } + inline int TrivialDecomposeOne(std::list::iterator const &it, int &pos) { + if(nVerbose > 2) { + std::stringstream ss; + ss << "\tTrivialDecompose Gate " << std::setw(5) << *it; + Print(ss.str() , nVerbose > 3); + } + assert(vvFis[*it].size() > 2); + int count = 2 - vvFis[*it].size(); + while(vvFis[*it].size() > 2) { + int f0 = vvFis[*it].back(); + lit c0 = vvCs[*it].back(); + Disconnect(*it, f0 >> 1, vvFis[*it].size() - 1, false, false); + int f1 = vvFis[*it].back(); + lit c1 = vvCs[*it].back(); + Disconnect(*it, f1 >> 1, vvFis[*it].size() - 1, false, false); + NewGate(pos); + Connect(pos, f1, false, false, c1); + Connect(pos, f0, false, false, c0); + if(!vPfUpdates[*it]) { + if(state == cspf) + this->Update(vGs[pos], vGs[*it]); + else if(state == mspf) { + lit x = this->man->Const1(); + this->IncRef(x); + for(unsigned j = 0; j < vvFis[*it].size(); j++) + this->Update(x, this->man->And(x, LitFi(*it, j))); + this->Update(vGs[pos], this->man->Or(this->man->LitNot(x), vGs[*it])); + this->DecRef(x); + } + } + Connect(*it, pos << 1, false, false, vGs[pos]); + vObjs.insert(it, pos); + Build(pos, vFs); + } + return count; + } + inline int BalancedDecomposeOne(std::list::iterator const &it, int &pos) { + if(nVerbose > 2) { + std::stringstream ss; + ss << "\tBalancedDecompose Gate " << std::setw(5) << *it; + Print(ss.str(), nVerbose > 3); + } + assert(fLevel); + assert(vvFis[*it].size() > 2); + for(int p = 1; p < (int)vvFis[*it].size(); p++) { + int f = vvFis[*it][p]; + lit c = vvCs[*it][p]; + int q = p - 1; + for(; q >= 0 && vLevels[f >> 1] > vLevels[vvFis[*it][q] >> 1]; q--) { + vvFis[*it][q + 1] = vvFis[*it][q]; + vvCs[*it][q + 1] = vvCs[*it][q]; + } + if(q + 1 != p) { + vvFis[*it][q + 1] = f; + vvCs[*it][q + 1] = c; + } + } + int count = 2 - vvFis[*it].size(); + while(vvFis[*it].size() > 2) { + int f0 = vvFis[*it].back(); + lit c0 = vvCs[*it].back(); + Disconnect(*it, f0 >> 1, vvFis[*it].size() - 1, false, false); + int f1 = vvFis[*it].back(); + lit c1 = vvCs[*it].back(); + Disconnect(*it, f1 >> 1, vvFis[*it].size() - 1, false, false); + NewGate(pos); + Connect(pos, f1, false, false, c1); + Connect(pos, f0, false, false, c0); + Connect(*it, pos << 1, false, false); + Build(pos, vFs); + vLevels[pos] = std::max(vLevels[f0 >> 1], vLevels[f1 >> 1]) + 1; + vObjs.insert(it, pos); + int f = vvFis[*it].back(); + lit c = vvCs[*it].back(); + int q = (int)vvFis[*it].size() - 2; + for(; q >= 0 && vLevels[f >> 1] > vLevels[vvFis[*it][q] >> 1]; q--) { + vvFis[*it][q + 1] = vvFis[*it][q]; + vvCs[*it][q + 1] = vvCs[*it][q]; + } + if(q + 1 != (int)vvFis[*it].size() - 1) { + vvFis[*it][q + 1] = f; + vvCs[*it][q + 1] = c; + } + } + vPfUpdates[*it] = true; + return count; + } + +public: // Merge/decompose + int TrivialMerge() { + int count = 0; + for(std::list::reverse_iterator it = vObjs.rbegin(); it != vObjs.rend();) { + count += TrivialMergeOne(*it); + it++; + } + return count; + } + int TrivialDecompose() { + int count = 0; + int pos = vPis.size() + 1; + for(std::list::iterator it = vObjs.begin(); it != vObjs.end(); it++) + if(vvFis[*it].size() > 2) + count += TrivialDecomposeOne(it, pos); + return count; + } + int Decompose() { + int count = 0; + int pos = vPis.size() + 1; + for(std::list::iterator it = vObjs.begin(); it != vObjs.end(); it++) { + std::set s1(vvFis[*it].begin(), vvFis[*it].end()); + assert(s1.size() == vvFis[*it].size()); + std::list::iterator it2 = it; + for(it2++; it2 != vObjs.end(); it2++) { + std::set s2(vvFis[*it2].begin(), vvFis[*it2].end()); + std::set s; + std::set_intersection(s1.begin(), s1.end(), s2.begin(), s2.end(), inserter(s, s.begin())); + if(s.size() > 1) { + if(s == s1) { + if(s == s2) { + if(nVerbose > 2) { + std::stringstream ss; + ss << "\treplace Gate " << std::setw(5) << *it2 + << " by Gate " << std::setw(5) << *it; + Print(ss.str() , nVerbose > 3); + } + count += Replace(*it2, *it << 1, false); + it2 = vObjs.erase(it2); + it2--; + } else { + if(nVerbose > 2) { + std::stringstream ss; + ss << "\tdecompose Gate " << std::setw(5) << *it2 + << " by Gate " << std::setw(5) << *it; + Print(ss.str() , nVerbose > 3); + } + for(std::set::iterator it3 = s.begin(); it3 != s.end(); it3++) { + unsigned j = find(vvFis[*it2].begin(), vvFis[*it2].end(), *it3) - vvFis[*it2].begin(); + Disconnect(*it2, *it3 >> 1, j, false); + } + count += s.size(); + if(std::find(vvFis[*it2].begin(), vvFis[*it2].end(), *it << 1) == vvFis[*it2].end()) { + Connect(*it2, *it << 1, false, false); + count--; + } + vPfUpdates[*it2] = true; + } + continue; + } + if(s == s2) { + it = vObjs.insert(it, *it2); + vObjs.erase(it2); + } else { + NewGate(pos); + if(nVerbose > 2) { + std::stringstream ss; + ss << "\tdecompose Gate " << std::setw(5) << *it + << " and " << std::setw(5) << *it2 + << " by a new Gate " << std::setw(5) << pos; + Print(ss.str() , nVerbose > 3); + } + if(nVerbose > 4) { + std::stringstream ss; + ss << "\t\tIntersection:"; + for(std::set::iterator it3 = s.begin(); it3 != s.end(); it3++) + ss << " " << (*it3 >> 1) << "(" << (*it3 & 1) << ")"; + Print(ss.str(), true); + } + for(std::set::iterator it3 = s.begin(); it3 != s.end(); it3++) + Connect(pos, *it3, false, false); + count -= s.size(); + it = vObjs.insert(it, pos); + Build(pos, vFs); + vPfUpdates[*it] = true; + } + s1 = s; + it2 = it; + } + } + if(vvFis[*it].size() > 2) + count += TrivialDecomposeOne(it, pos); + } + return count; + } + +private: // Save/load + inline void Save(TransductionBackup &b) const { + b.man = this->man; + b.nObjsAlloc = nObjsAlloc; + b.state = state; + b.vObjs = vObjs; + b.vvFis = vvFis; + b.vvFos = vvFos; + b.vLevels = vLevels; + b.vSlacks = vSlacks; + b.vvFiSlacks = vvFiSlacks; + this->CopyVec(b.vFs, vFs); + this->CopyVec(b.vGs, vGs); + this->CopyVec(b.vvCs, vvCs); + b.vUpdates = vUpdates; + b.vPfUpdates = vPfUpdates; + b.vFoConeShared = vFoConeShared; + } + inline void Load(TransductionBackup const &b) { + nObjsAlloc = b.nObjsAlloc; + state = b.state; + vObjs = b.vObjs; + vvFis = b.vvFis; + vvFos = b.vvFos; + vLevels = b.vLevels; + vSlacks = b.vSlacks; + vvFiSlacks = b.vvFiSlacks; + this->CopyVec(vFs, b.vFs); + this->CopyVec(vGs, b.vGs); + this->CopyVec(vvCs, b.vvCs); + vUpdates = b.vUpdates; + vPfUpdates = b.vPfUpdates; + vFoConeShared = b.vFoConeShared; + } + +private: // Connectable condition + inline bool TryConnect(int i, int i0, bool c0) { + int f = (i0 << 1) ^ (int)c0; + if(find(vvFis[i].begin(), vvFis[i].end(), f) == vvFis[i].end()) { + lit x = this->man->Or(this->man->LitNot(vFs[i]), vGs[i]); + this->IncRef(x); + if(this->man->IsConst1(this->man->Or(x, this->man->LitNotCond(vFs[i0], c0)))) { + this->DecRef(x); + if(nVerbose > 3) { + std::stringstream ss; + ss << "\t\t[TryConnect] adding Wire " << std::setw(5) << i0 << "(" << c0 << ")" + << " -> " << std::setw(5) << i; + Print(ss.str(), true); + } + Connect(i, f, true); + return true; + } + this->DecRef(x); + } + return false; + } + +public: // Resubs + int Resub(bool fMspf) { + int count = fMspf? Mspf(true): Cspf(true); + int nodes = CountNodes(); + TransductionBackup b; + Save(b); + int count_ = count; + std::list targets = vObjs; + for(std::list::reverse_iterator it = targets.rbegin(); it != targets.rend(); it++) { + if(nVerbose > 1) { + std::stringstream ss; + ss << "[Resub] processing Gate " << std::setw(5) << *it + << " (" << std::setw(5) << std::distance(targets.rbegin(), it) + 1 + << "/" << std::setw(5) << targets.size() << ")"; + PrintStats(ss.str(), nVerbose > 2); + } + if(vvFos[*it].empty()) + continue; + count += TrivialMergeOne(*it); + std::vector lev; + if(fLevel) { + for(unsigned j = 0; j < vvFis[*it].size(); j++) + add(lev, vLevels[vvFis[*it][j] >> 1]); + if((int)lev.size() > vLevels[*it] + vSlacks[*it]) { + Load(b); + count = count_; + continue; + } + lev.resize(vLevels[*it] + vSlacks[*it]); + } + bool fConnect = false; + std::vector vMarks(nObjsAlloc); + MarkFoCone_rec(vMarks, *it); + std::list targets2 = vObjs; + for(std::list::iterator it2 = targets2.begin(); it2 != targets2.end(); it2++) { + if(fLevel && (int)lev.size() > vLevels[*it] + vSlacks[*it]) + break; + if(!vMarks[*it2] && !vvFos[*it2].empty()) + if(!fLevel || noexcess(lev, vLevels[*it2])) + if(TryConnect(*it, *it2, false) || TryConnect(*it, *it2, true)) { + fConnect = true; + count--; + if(fLevel) + add(lev, vLevels[*it2]); + } + } + if(fConnect) { + if(fMspf) { + Build(); + count += Mspf(true, *it); + } else { + vPfUpdates[*it] = true; + count += Cspf(true, *it); + } + if(!vvFos[*it].empty()) { + vPfUpdates[*it] = true; + count += fMspf? Mspf(true): Cspf(true); + } + } + if(nodes < CountNodes()) { + Load(b); + count = count_; + continue; + } + if(!vvFos[*it].empty() && vvFis[*it].size() > 2) { + std::list::iterator it2 = find(vObjs.begin(), vObjs.end(), *it); + int pos = nObjsAlloc; + if(fLevel) + count += BalancedDecomposeOne(it2, pos) + (fMspf? Mspf(true): Cspf(true)); + else + count += TrivialDecomposeOne(it2, pos); + } + nodes = CountNodes(); + Save(b); + count_ = count; + } + if(nVerbose) + PrintStats("Resub", true, 11); + return count; + } + int ResubMono(bool fMspf) { + int count = fMspf? Mspf(true): Cspf(true); + std::list targets = vObjs; + for(std::list::reverse_iterator it = targets.rbegin(); it != targets.rend(); it++) { + if(nVerbose > 1) { + std::stringstream ss; + ss << "[ResubMono] processing Gate " << std::setw(5) << *it + << " (" << std::setw(5) << std::distance(targets.rbegin(), it) + 1 + << "/" << std::setw(5) << targets.size() << ")"; + PrintStats(ss.str(), nVerbose > 2); + } + if(vvFos[*it].empty()) + continue; + count += TrivialMergeOne(*it); + TransductionBackup b; + Save(b); + int count_ = count; + for(unsigned i = 0; i < vPis.size(); i++) { + if(vvFos[*it].empty()) + break; + if(nVerbose > 2) { + std::stringstream ss; + ss << "\ttrying a new fanin PI " << std::setw(2) << i; + PrintStats(ss.str(), nVerbose > 3); + } + if(TryConnect(*it, vPis[i], false) || TryConnect(*it, vPis[i], true)) { + count--; + int diff; + if(fMspf) { + Build(); + diff = Mspf(true, *it, vPis[i]); + } else { + vPfUpdates[*it] = true; + diff = Cspf(true, *it, vPis[i]); + } + if(diff) { + count += diff; + if(!vvFos[*it].empty()) { + vPfUpdates[*it] = true; + count += fMspf? Mspf(true): Cspf(true); + } + if(fLevel && CountLevels() > nMaxLevels) { + Load(b); + count = count_; + } else { + Save(b); + count_ = count; + } + } else { + Load(b); + count = count_; + } + } + } + if(vvFos[*it].empty()) + continue; + std::vector vMarks(nObjsAlloc); + MarkFoCone_rec(vMarks, *it); + std::list targets2 = vObjs; + for(std::list::iterator it2 = targets2.begin(); it2 != targets2.end(); it2++) { + if(vvFos[*it].empty()) + break; + if(nVerbose > 2) { + std::stringstream ss; + ss << "\ttrying a new fanin Gate " << std::setw(5) << *it2 + << " (" << std::setw(5) << std::distance(targets2.begin(), it2) + 1 + << "/" << std::setw(5) << targets2.size() << ")"; + PrintStats(ss.str(), nVerbose > 3); + } + if(!vMarks[*it2] && !vvFos[*it2].empty()) + if(TryConnect(*it, *it2, false) || TryConnect(*it, *it2, true)) { + count--; + int diff; + if(fMspf) { + Build(); + diff = Mspf(true, *it, *it2); + } else { + vPfUpdates[*it] = true; + diff = Cspf(true, *it, *it2); + } + if(diff) { + count += diff; + if(!vvFos[*it].empty()) { + vPfUpdates[*it] = true; + count += fMspf? Mspf(true): Cspf(true); + } + if(fLevel && CountLevels() > nMaxLevels) { + Load(b); + count = count_; + } else { + Save(b); + count_ = count; + } + } else { + Load(b); + count = count_; + } + } + } + if(vvFos[*it].empty()) + continue; + if(vvFis[*it].size() > 2) { + std::list::iterator it2 = find(vObjs.begin(), vObjs.end(), *it); + int pos = nObjsAlloc; + if(fLevel) + count += BalancedDecomposeOne(it2, pos) + (fMspf? Mspf(true): Cspf(true)); + else + count += TrivialDecomposeOne(it2, pos); + } + } + if(nVerbose) + PrintStats("ResubMono", true, 11); + return count; + } + int ResubShared(bool fMspf) { + int count = fMspf? Mspf(true): Cspf(true); + std::list targets = vObjs; + for(std::list::reverse_iterator it = targets.rbegin(); it != targets.rend(); it++) { + if(nVerbose > 1) { + std::stringstream ss; + ss << "[ResubShared] processing Gate " << std::setw(5) << *it + << " (" << std::setw(5) << std::distance(targets.rbegin(), it) + 1 + << "/" << std::setw(5) << targets.size() << ")"; + PrintStats(ss.str(), nVerbose > 2); + } + if(vvFos[*it].empty()) + continue; + count += TrivialMergeOne(*it); + bool fConnect = false; + for(unsigned i = 0; i < vPis.size(); i++) + if(TryConnect(*it, vPis[i], false) || TryConnect(*it, vPis[i], true)) { + fConnect |= true; + count--; + } + std::vector vMarks(nObjsAlloc); + MarkFoCone_rec(vMarks, *it); + for(std::list::iterator it2 = targets.begin(); it2 != targets.end(); it2++) + if(!vMarks[*it2] && !vvFos[*it2].empty()) + if(TryConnect(*it, *it2, false) || TryConnect(*it, *it2, true)) { + fConnect |= true; + count--; + } + if(fConnect) { + if(fMspf) { + Build(); + count += Mspf(true, *it); + } else { + vPfUpdates[*it] = true; + count += Cspf(true, *it); + } + if(!vvFos[*it].empty()) { + vPfUpdates[*it] = true; + count += fMspf? Mspf(true): Cspf(true); + } + } + } + count += Decompose(); + if(nVerbose) + PrintStats("ResubShared", true, 11); + return count; + } + +public: // Optimization scripts + int RepeatResub(bool fMono, bool fMspf) { + int count = 0; + while(int diff = fMono? ResubMono(fMspf): Resub(fMspf)) + count += diff; + return count; + } + int RepeatInner(bool fMspf, bool fInner) { + int count = 0; + while(int diff = RepeatResub(true, fMspf) + RepeatResub(false, fMspf)) { + count += diff; + if(!fInner) + break; + } + return count; + } + int RepeatOuter(bool fMspf, bool fInner, bool fOuter) { + int count = 0; + while(int diff = fMspf? RepeatInner(false, fInner) + RepeatInner(true, fInner): RepeatInner(false, fInner)) { + count += diff; + if(!fOuter) + break; + } + return count; + } + int RepeatAll(bool fFirstMerge, bool fMspfMerge, bool fMspfResub, bool fInner, bool fOuter) { + TransductionBackup b; + Save(b); + int count = 0; + int diff = 0; + if(fFirstMerge) + diff = ResubShared(fMspfMerge); + diff += RepeatOuter(fMspfResub, fInner, fOuter); + if(diff > 0) { + count = diff; + Save(b); + diff = 0; + } + while(true) { + diff += ResubShared(fMspfMerge) + RepeatOuter(fMspfResub, fInner, fOuter); + if(diff > 0) { + count += diff; + Save(b); + diff = 0; + } else { + Load(b); + break; + } + } + return count; + } + +public: // Cspf/mspf + int Cspf() { + return Cspf(true); + } + int Mspf() { + return Mspf(true); + } + +private: // Setup + void ImportAig(Gia_Man_t *pGia) { + int i; + Gia_Obj_t *pObj; + nObjsAlloc = Gia_ManObjNum(pGia); + vvFis.resize(nObjsAlloc); + vvFos.resize(nObjsAlloc); + if(fLevel) { + vLevels.resize(nObjsAlloc); + vSlacks.resize(nObjsAlloc); + vvFiSlacks.resize(nObjsAlloc); + } + vFs.resize(nObjsAlloc, LitMax); + vGs.resize(nObjsAlloc, LitMax); + vvCs.resize(nObjsAlloc); + vUpdates.resize(nObjsAlloc); + vPfUpdates.resize(nObjsAlloc); + std::vector v(Gia_ManObjNum(pGia), -1); + int nObjs = 0; + v[Gia_ObjId(pGia, Gia_ManConst0(pGia))] = nObjs << 1; + nObjs++; + Gia_ManForEachCi(pGia, pObj, i) { + v[Gia_ObjId(pGia, pObj)] = nObjs << 1; + vPis.push_back(nObjs); + nObjs++; + } + Gia_ManForEachAnd(pGia, pObj, i) { + int id = Gia_ObjId(pGia, pObj); + if(nVerbose > 5) { + std::stringstream ss; + ss << "\t\t\t\timport Gate " << std::setw(5) << id; + Print(ss.str(), true); + } + int i0 = Gia_ObjId(pGia, Gia_ObjFanin0(pObj)); + int i1 = Gia_ObjId(pGia, Gia_ObjFanin1(pObj)); + int c0 = Gia_ObjFaninC0(pObj); + int c1 = Gia_ObjFaninC1(pObj); + if(i0 == i1) { + if(c0 == c1) + v[id] = v[i0] ^ c0; + else + v[id] = 0; + } else { + Connect(nObjs , v[i0] ^ c0); + Connect(nObjs, v[i1] ^ c1); + v[id] = nObjs << 1; + vObjs.push_back(nObjs); + nObjs++; + } + } + Gia_ManForEachCo(pGia, pObj, i) { + if(nVerbose > 5) { + std::stringstream ss; + ss << "\t\t\t\timport PO " << std::setw(2) << i; + Print(ss.str(), true); + } + int i0 = Gia_ObjId(pGia, Gia_ObjFanin0(pObj)); + int c0 = Gia_ObjFaninC0(pObj); + Connect(nObjs, v[i0] ^ c0); + vPos.push_back(nObjs); + nObjs++; + } + } + void Aig2Bdd(Gia_Man_t *pGia, std::vector &vNodes) { + if(nVerbose > 6) + Print("\t\t\tBuild Exdc", true); + int i; + Gia_Obj_t *pObj; + std::vector vCounts(pGia->nObjs); + Gia_ManStaticFanoutStart(pGia); + Gia_ManForEachAnd(pGia, pObj, i) + vCounts[Gia_ObjId(pGia, pObj)] = Gia_ObjFanoutNum(pGia, pObj); + Gia_ManStaticFanoutStop(pGia); + std::vector nodes(pGia->nObjs); + nodes[Gia_ObjId(pGia, Gia_ManConst0(pGia))] = this->man->Const0(); + Gia_ManForEachCi(pGia, pObj, i) + nodes[Gia_ObjId(pGia, pObj)] = this->man->IthVar(i); + Gia_ManForEachAnd(pGia, pObj, i) { + int id = Gia_ObjId(pGia, pObj); + if(nVerbose > 6) { + std::stringstream ss; + ss << "\t\t\t\tbuilding Exdc (" << i << " / " << Gia_ManAndNum(pGia) << ")"; + Print(ss.str(), nVerbose > 7); + } + int i0 = Gia_ObjId(pGia, Gia_ObjFanin0(pObj)); + int i1 = Gia_ObjId(pGia, Gia_ObjFanin1(pObj)); + bool c0 = Gia_ObjFaninC0(pObj); + bool c1 = Gia_ObjFaninC1(pObj); + nodes[id] = this->man->And(this->man->LitNotCond(nodes[i0], c0), this->man->LitNotCond(nodes[i1], c1)); + this->IncRef(nodes[id]); + vCounts[i0]--; + if(!vCounts[i0]) + this->DecRef(nodes[i0]); + vCounts[i1]--; + if(!vCounts[i1]) + this->DecRef(nodes[i1]); + } + Gia_ManForEachCo(pGia, pObj, i) { + int i0 = Gia_ObjId(pGia, Gia_ObjFanin0(pObj)); + bool c0 = Gia_ObjFaninC0(pObj); + vNodes.push_back(this->man->LitNotCond(nodes[i0], c0)); + } + } + void RemoveConstOutputs() { + bool fRemoved = false; + for(unsigned i = 0; i < vPos.size(); i++) { + int i0 = vvFis[vPos[i]][0] >> 1; + lit c = vvCs[vPos[i]][0]; + if(i0) { + if(this->man->IsConst1(this->man->Or(LitFi(vPos[i], 0), c))) { + if(nVerbose > 3) { + std::stringstream ss; + ss << "\t\tPO " << std::setw(2) << i << " is Const 1"; + Print(ss.str(), true); + } + Disconnect(vPos[i], i0, 0, false, false); + Connect(vPos[i], 1, false, false, c); + fRemoved |= vvFos[i0].empty(); + } else if(this->man->IsConst1(this->man->Or(this->man->LitNot(LitFi(vPos[i], 0)), c))) { + if(nVerbose > 3) { + std::stringstream ss; + ss << "\t\tPO " << std::setw(2) << i << " is Const 0"; + Print(ss.str(), true); + } + Disconnect(vPos[i], i0, 0, false, false); + Connect(vPos[i], 0, false, false, c); + fRemoved |= vvFos[i0].empty(); + } + } + } + if(fRemoved) { + for(std::list::reverse_iterator it = vObjs.rbegin(); it != vObjs.rend();) { + if(vvFos[*it].empty()) { + if(nVerbose > 3) { + std::stringstream ss; + ss << "\t\tremove unused Gate " << std::setw(5) << *it; + Print(ss.str(), true); + } + Remove(*it, false); + it = std::list::reverse_iterator(vObjs.erase(--(it.base()))); + continue; + } + it++; + } + } + } + +public: // Constructor + 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) { + startclk = Abc_Clock(); + p.nGbc = 1; + p.nReo = 4000; + if(nSortType && nSortType < 4) + p.fCountOnes = true; + this->man = new Man(Gia_ManCiNum(pGia), p); + ImportAig(pGia); + this->Update(vFs[0], this->man->Const0()); + for(unsigned i = 0; i < vPis.size(); i++) + this->Update(vFs[i + 1], this->man->IthVar(i)); + nMaxLevels = -1; + Build(false); + this->man->Reorder(); + this->man->TurnOffReo(); + if(pExdc) { + std::vector vExdc; + Aig2Bdd(pExdc, vExdc); + for(unsigned i = 0; i < vPos.size(); i++) + vvCs[vPos[i]][0] = vExdc.size() == 1? vExdc[0]: vExdc[i]; + } else + for(unsigned i = 0; i < vPos.size(); i++) + this->Update(vvCs[vPos[i]][0], this->man->Const0()); + RemoveConstOutputs(); + vPoFs.resize(vPos.size(), LitMax); + for(unsigned i = 0; i < vPos.size(); i++) + this->Update(vPoFs[i], LitFi(vPos[i], 0)); + state = none; + if(nPiShuffle) + ShufflePis(nPiShuffle); + if(fLevel) + ComputeLevel(); + if(nVerbose) + PrintStats("Init", true, 11); + } + ~Transduction() { + this->DelVec(vFs); + this->DelVec(vGs); + this->DelVec(vvCs); + this->DelVec(vPoFs); + //assert(this->man->CountNodes() == (int)vPis.size() + 1); + //assert(!this->man->Ref(this->man->Const0())); + delete this->man; + } + +public: // Output + Gia_Man_t *GenerateAig() const { + Gia_Man_t * pGia, *pTemp; + pGia = Gia_ManStart(1 + vPis.size() + CountNodes() + vPos.size()); + Gia_ManHashAlloc(pGia); + std::vector values(nObjsAlloc); + values[0] = Gia_ManConst0Lit(); + for(unsigned i = 0; i < vPis.size(); i++) + values[i + 1] = Gia_ManAppendCi(pGia); + for(std::list::const_iterator it = vObjs.begin(); it != vObjs.end(); it++) { + assert(vvFis[*it].size() > 1); + int i0 = vvFis[*it][0] >> 1; + int i1 = vvFis[*it][1] >> 1; + int c0 = vvFis[*it][0] & 1; + int c1 = vvFis[*it][1] & 1; + int r = Gia_ManHashAnd(pGia, Abc_LitNotCond(values[i0], c0), Abc_LitNotCond(values[i1], c1)); + for(unsigned i = 2; i < vvFis[*it].size(); i++) { + int ii = vvFis[*it][i] >> 1; + int ci = vvFis[*it][i] & 1; + r = Gia_ManHashAnd(pGia, r, Abc_LitNotCond(values[ii], ci)); + } + values[*it] = r; + } + for(unsigned i = 0; i < vPos.size(); i++) { + int i0 = vvFis[vPos[i]][0] >> 1; + int c0 = vvFis[vPos[i]][0] & 1; + Gia_ManAppendCo(pGia, Abc_LitNotCond(values[i0], c0)); + } + pGia = Gia_ManCleanup(pTemp = pGia); + Gia_ManStop(pTemp); + return pGia; + } + +public: // Debug and print + PfState State() const { + return state; + } + bool BuildDebug() { + for(std::list::iterator it = vObjs.begin(); it != vObjs.end(); it++) + vUpdates[*it] = true; + std::vector vFsOld; + CopyVec(vFsOld, vFs); + Build(false); + bool r = LitVecIsEq(vFsOld, vFs); + DelVec(vFsOld); + return r; + } + bool CspfDebug() { + std::vector vGsOld; + this->CopyVec(vGsOld, vGs); + std::vector > vvCsOld; + this->CopyVec(vvCsOld, vvCs); + state = none; + Cspf(false); + bool r = this->LitVecIsEq(vGsOld, vGs) && this->LitVecIsEq(vvCsOld, vvCs); + this->DelVec(vGsOld); + this->DelVec(vvCsOld); + return r; + } + bool MspfDebug() { + std::vector vGsOld; + this->CopyVec(vGsOld, vGs); + std::vector > vvCsOld; + this->CopyVec(vvCsOld, vvCs); + state = none; + Mspf(false); + bool r = this->LitVecIsEq(vGsOld, vGs) && this->LitVecIsEq(vvCsOld, vvCs); + this->DelVec(vGsOld); + this->DelVec(vvCsOld); + return r; + } + bool Verify() const { + for(unsigned j = 0; j < vPos.size(); j++) { + lit x = this->Xor(LitFi(vPos[j], 0), vPoFs[j]); + this->IncRef(x); + this->Update(x, this->man->And(x, this->man->LitNot(vvCs[vPos[j]][0]))); + this->DecRef(x); + if(!this->man->IsConst0(x)) + return false; + } + return true; + } + void PrintObjs() const { + for(std::list::const_iterator it = vObjs.begin(); it != vObjs.end(); it++) { + std::cout << "Gate " << *it << ":"; + if(fLevel) + std::cout << " Level = " << vLevels[*it] << ", Slack = " << vSlacks[*it]; + std::cout << std::endl; + std::string delim = ""; + std::cout << "\tFis: "; + for(unsigned j = 0; j < vvFis[*it].size(); j++) { + std::cout << delim << (vvFis[*it][j] >> 1) << "(" << (vvFis[*it][j] & 1) << ")"; + delim = ", "; + } + std::cout << std::endl; + delim = ""; + std::cout << "\tFos: "; + for(unsigned j = 0; j < vvFos[*it].size(); j++) { + std::cout << delim << vvFos[*it][j]; + delim = ", "; + } + std::cout << std::endl; + } + } +}; + +} + +ABC_NAMESPACE_CXX_HEADER_END + +#endif diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make index 870da208e..8584f3764 100644 --- a/src/aig/gia/module.make +++ b/src/aig/gia/module.make @@ -103,6 +103,7 @@ SRC += src/aig/gia/giaAig.c \ src/aig/gia/giaSwitch.c \ src/aig/gia/giaTim.c \ src/aig/gia/giaTis.c \ + src/aig/gia/giaTransduction.cpp \ src/aig/gia/giaTruth.c \ src/aig/gia/giaTsim.c \ src/aig/gia/giaTtopt.cpp \ diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 93b92f096..f032c7605 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -503,6 +503,7 @@ static int Abc_CommandAbc9LNetEval ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9LNetOpt ( Abc_Frame_t * pAbc, int argc, char ** argv ); //#ifndef _WIN32 static int Abc_CommandAbc9Ttopt ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Transduction ( Abc_Frame_t * pAbc, int argc, char ** argv ); //#endif static int Abc_CommandAbc9LNetMap ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Unmap ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -1260,6 +1261,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&lnetopt", Abc_CommandAbc9LNetOpt, 0 ); //#ifndef _WIN32 Cmd_CommandAdd( pAbc, "ABC9", "&ttopt", Abc_CommandAbc9Ttopt, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&transduction", Abc_CommandAbc9Transduction, 0 ); //#endif Cmd_CommandAdd( pAbc, "ABC9", "&lnetmap", Abc_CommandAbc9LNetMap, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&unmap", Abc_CommandAbc9Unmap, 0 ); @@ -42571,6 +42573,173 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9Transduction( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Gia_Man_t * pTemp, * pExdc = NULL; + int c, nType = 1, fMspf = 0, nRandom = 0, nSortType = 0, nPiShuffle = 0, nParameter = 0, fLevel = 0, fTruth = 0, fNewLine = 0, nVerbose = 2; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "TSIPRVtmnl" ) ) != EOF ) + { + switch ( c ) + { + case 'T': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-T\" should be followed by a positive integer.\n" ); + goto usage; + } + nType = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; + case 'R': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-R\" should be followed by a positive integer.\n" ); + goto usage; + } + nRandom = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; + case 'S': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-S\" should be followed by a positive integer.\n" ); + goto usage; + } + nSortType = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; + case 'I': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-I\" should be followed by a positive integer.\n" ); + goto usage; + } + nPiShuffle = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; + case 'P': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-P\" should be followed by a positive integer.\n" ); + goto usage; + } + nParameter = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; + case 'V': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-V\" should be followed by a positive integer.\n" ); + goto usage; + } + nVerbose = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; + case 't': + fTruth ^= 1; + break; + case 'm': + fMspf ^= 1; + break; + case 'n': + fNewLine ^= 1; + break; + case 'l': + fLevel ^= 1; + break; + case 'h': + default: + goto usage; + } + } + if ( argc > globalUtilOptind + 1 ) + { + Abc_Print( -1, "Wrong number of auguments.\n" ); + goto usage; + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Empty GIA network.\n" ); + return 1; + } + if ( argc == globalUtilOptind + 1 ) + { + FILE * pFile = fopen( argv[globalUtilOptind], "rb" ); + if ( pFile == NULL ) + { + Abc_Print( -1, "Cannot open input file \"%s\". ", argv[globalUtilOptind] ); + return 1; + } + fclose( pFile ); + pExdc = Gia_AigerRead( argv[globalUtilOptind], 0, 0, 0 ); + if ( pExdc == NULL ) + { + Abc_Print( -1, "Reading AIGER has failed.\n" ); + return 1; + } + } + + if ( fLevel && (nType == 3 || nType == 8) ) + { + Abc_Print( -1, "Level preserving optimization does not work with transduction type 3 and 8.\n" ); + return 1; + } + + if ( fTruth ) + pTemp = Gia_ManTransductionTt( pAbc->pGia, nType, fMspf, nRandom, nSortType, nPiShuffle, nParameter, fLevel, pExdc, fNewLine, nVerbose ); + else + pTemp = Gia_ManTransductionBdd( pAbc->pGia, nType, fMspf, nRandom, nSortType, nPiShuffle, nParameter, fLevel, pExdc, fNewLine, nVerbose ); + if ( pExdc != NULL ) + Gia_ManStop( pExdc ); + Abc_FrameUpdateGia( pAbc, pTemp ); + return 0; + +usage: + Abc_Print( -2, "usage: &transduction [-TSIPRV num] [-bmlh] \n" ); + Abc_Print( -2, "\t performs transduction-based AIG optimization\n" ); + Abc_Print( -2, "\t-T num : transduction type [default = %d]\n", nType ); + Abc_Print( -2, "\t 0: remove simply redundant nodes\n" ); + Abc_Print( -2, "\t 1: Resub\n" ); + Abc_Print( -2, "\t 2: ResubMono\n" ); + Abc_Print( -2, "\t 3: ResubShared\n" ); + Abc_Print( -2, "\t 4: repeat Resub\n" ); + Abc_Print( -2, "\t 5: repeat ResubMono\n" ); + Abc_Print( -2, "\t 6: script RepeatInner\n" ); + Abc_Print( -2, "\t 7: script RepeatOuter\n" ); + Abc_Print( -2, "\t 8: script RepeatAll\n" ); + Abc_Print( -2, "\t-S num : fanin sort type [default = %d]\n", nSortType ); + Abc_Print( -2, "\t 0: topological order\n" ); + Abc_Print( -2, "\t 1: number of ones\n" ); + Abc_Print( -2, "\t 2: number of ones before complemented edges\n" ); + Abc_Print( -2, "\t 3: pseudo random\n" ); + Abc_Print( -2, "\t 4: no sorting\n" ); + Abc_Print( -2, "\t-I num : random seed to shuffle PIs (0 = no shuffle) [default = %d]\n", nPiShuffle ); + Abc_Print( -2, "\t-P num : parameters for scripts [default = %d]\n", nParameter ); + Abc_Print( -2, "\t-R num : random seed to set all parameters (0 = no random) ([default = %d]\n", nRandom ); + Abc_Print( -2, "\t-V num : verbosity level [default = %d]\n", nVerbose); + Abc_Print( -2, "\t-t : toggles using truth table instead of BDD [default = %s]\n", fTruth? "yes": "no" ); + Abc_Print( -2, "\t-m : toggles using MSPF [default = %s]\n", fMspf? "yes": "no" ); + Abc_Print( -2, "\t-n : toggles printing with a new line [default = %s]\n", fNewLine? "yes": "no" ); + Abc_Print( -2, "\t-l : toggles level preserving optimization [default = %s]\n", fLevel? "yes": "no" ); + Abc_Print( -2, "\t-h : prints the command usage\n"); + Abc_Print( -2, "\t : AIGER specifying external don't-cares\n"); + Abc_Print( -2, "\t\n" ); + Abc_Print( -2, "\t This command was contributed by Yukio Miyasaka.\n" ); + return 1; +} + /**Function************************************************************* Synopsis []