Skip to content

A
abc
Unverified Commit 38cd47b4 by alanminko Committed by GitHub
Options

Merge pull request #219 from MyskYko/transduction 

Transduction method
parents eff805a6 3b946e76
Showing with 3141 additions and 1 deletions
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
......
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 );
......
src/aig/gia/giaNewBdd.h 0 → 100644
#ifndef ABC__aig__gia__giaNewBdd_h
#define ABC__aig__gia__giaNewBdd_h
#include <limits>
#include <vector>
#include <iostream>
#include <iomanip>
#include <cmath>
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<var>::max(); }
static inline bvar BvarMax() { return std::numeric_limits<bvar>::max(); }
static inline lit LitMax() { return std::numeric_limits<lit>::max(); }
static inline ref RefMax() { return std::numeric_limits<ref>::max(); }
static inline size SizeMax() { return std::numeric_limits<size>::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<lit> 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<var> *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<var> vVars;
std::vector<var> Var2Level;
std::vector<var> Level2Var;
std::vector<lit> vObjs;
std::vector<bvar> vNexts;
std::vector<bool> vMarks;
std::vector<ref> vRefs;
std::vector<edge> vEdges;
std::vector<double> vOneCounts;
std::vector<uniq> vUniqueMasks;
std::vector<bvar> vUniqueCounts;
std::vector<bvar> vUniqueTholds;
std::vector<std::vector<bvar> > 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<bvar>::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<bvar>::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<bvar>::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<bvar>::iterator p = vvUnique[v1].begin(); p != vvUnique[v1].end(); p++) {
std::vector<bvar>::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<bvar>::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<var> 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<lit> 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<lit> 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
src/aig/gia/giaNewTt.h 0 → 100644
#ifndef ABC__aig__gia__giaNewTt_h
#define ABC__aig__gia__giaNewTt_h
#include <limits>
#include <iomanip>
#include <iostream>
#include <vector>
#include <bitset>
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<bvar>::max(); }
static inline lit LitMax() { return std::numeric_limits<lit>::max(); }
static inline ref RefMax() { return std::numeric_limits<ref>::max(); }
static inline size SizeMax() { return std::numeric_limits<size>::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<word> vVals;
std::vector<bvar> vDeads;
std::vector<ref> 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<lit> 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
src/aig/gia/giaTransduction.cpp 0 → 100644
#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<NewBdd::Man, NewBdd::Param, NewBdd::lit, 0xffffffff> 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<NewTt::Man, NewTt::Param, NewTt::lit, 0xffffffff> 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
src/aig/gia/giaTransduction.h 0 → 100644
#ifndef ABC__aig__gia__giaTransduction_h
#define ABC__aig__gia__giaTransduction_h
#include <iostream>
#include <iomanip>
#include <sstream>
#include <vector>
#include <list>
#include <set>
#include <algorithm>
#include <cassert>
#include "gia.h"
ABC_NAMESPACE_CXX_HEADER_START
namespace Transduction {
enum PfState {none, cspf, mspf};
template <class Man, class lit, lit LitMax>
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<lit> &v) const {
for(unsigned i = 0; i < v.size(); i++)
DecRef(v[i]);
v.clear();
}
inline void DelVec(std::vector<std::vector<lit> > &v) const {
for(unsigned i = 0; i < v.size(); i++)
DelVec(v[i]);
v.clear();
}
inline void CopyVec(std::vector<lit> &v, std::vector<lit> const &u) const {
DelVec(v);
v = u;
for(unsigned i = 0; i < v.size(); i++)
IncRef(v[i]);
}
inline void CopyVec(std::vector<std::vector<lit> > &v, std::vector<std::vector<lit> > 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<lit> const &v, std::vector<lit> 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<std::vector<lit> > const &v, std::vector<std::vector<lit> > 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 Man, class lit, lit LitMax>
class TransductionBackup: ManUtil<Man, lit, LitMax> {
private:
int nObjsAlloc;
PfState state;
std::list<int> vObjs;
std::vector<std::vector<int> > vvFis;
std::vector<std::vector<int> > vvFos;
std::vector<int> vLevels;
std::vector<int> vSlacks;
std::vector<std::vector<int> > vvFiSlacks;
std::vector<lit> vFs;
std::vector<lit> vGs;
std::vector<std::vector<lit> > vvCs;
std::vector<bool> vUpdates;
std::vector<bool> vPfUpdates;
std::vector<bool> vFoConeShared;
template <class Man_, class Param, class lit_, lit_ LitMax_>
friend class Transduction;
public:
~TransductionBackup() {
if(this->man) {
this->DelVec(vFs);
this->DelVec(vGs);
this->DelVec(vvCs);
}
}
};
template <class Man, class Param, class lit, lit LitMax>
class Transduction: ManUtil<Man, lit, LitMax> {
private:
int nVerbose;
int nSortType;
bool fLevel;
int nObjsAlloc;
int nMaxLevels;
PfState state;
std::vector<int> vPis;
std::vector<int> vPos;
std::list<int> vObjs;
std::vector<std::vector<int> > vvFis;
std::vector<std::vector<int> > vvFos;
std::vector<int> vLevels;
std::vector<int> vSlacks;
std::vector<std::vector<int> > vvFiSlacks;
std::vector<lit> vFs;
std::vector<lit> vGs;
std::vector<std::vector<lit> > vvCs;
std::vector<bool> vUpdates;
std::vector<bool> vPfUpdates;
std::vector<bool> vFoConeShared;
std::vector<lit> vPoFs;
bool fNewLine;
abctime startclk;
private: // Helper functions
inline bool AllFalse(std::vector<bool> const &v) const {
for(std::list<int>::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<int>::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<int>::iterator const &it) {
for(unsigned j = 0; j < vvFis[*it].size(); j++) {
int i0 = vvFis[*it][j] >> 1;
if(!vvFis[i0].empty()) {
std::list<int>::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<int>::iterator it = find(vObjs.begin(), vObjs.end(), i);
std::list<int>::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<bool> &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<bool> &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<int> &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<int> 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<bool> &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<bool> const &a) {
for(unsigned i = 0; i < a.size() - 1; i++)
if(a[i])
return false;
return true;
}
inline bool noexcess(std::vector<bool> 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<int>::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<bool> 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<int>::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<lit> 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<lit> &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<int>::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<int>::iterator it = vObjs.begin(); it != vObjs.end(); it++)
vPfUpdates[*it] = vPfUpdates[*it] || vUpdates[*it];
for(std::list<int>::iterator it = vObjs.begin(); it != vObjs.end(); it++)
vUpdates[*it] = false;
assert(AllFalse(vUpdates));
}
void BuildFoConeCompl(int i, std::vector<lit> &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<lit> vFsCompl;
this->CopyVec(vFsCompl, vFs);
vFsCompl[i] = this->man->LitNot(vFs[i]);
std::vector<bool> vUpdatesCompl(nObjsAlloc);
for(unsigned j = 0; j < vvFos[i].size(); j++)
vUpdatesCompl[vvFos[i][j]] = true;
for(std::list<int>::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<int>::iterator it = vObjs.begin(); it != vObjs.end(); it++)
vPfUpdates[*it] = true;
state = cspf;
int count = 0;
for(std::list<int>::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<int>::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<int>::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<lit> 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<int>::iterator it = vObjs.begin(); it != vObjs.end(); it++)
vPfUpdates[*it] = true;
state = mspf;
int count = 0;
int restarts = 0;
for(std::list<int>::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<int>::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<int> vFisOld = vvFis[i];
std::vector<lit> 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<int>::iterator itfi = vFisOld.begin() + j;
typename std::vector<lit>::iterator itc = vCsOld.begin() + j;
for(unsigned jj = 0; jj < vvFis[i0].size(); jj++) {
int f = vvFis[i0][jj];
std::vector<int>::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<int>::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<int>::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<int>::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<int>::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<int>::iterator it = vObjs.begin(); it != vObjs.end(); it++) {
std::set<int> s1(vvFis[*it].begin(), vvFis[*it].end());
assert(s1.size() == vvFis[*it].size());
std::list<int>::iterator it2 = it;
for(it2++; it2 != vObjs.end(); it2++) {
std::set<int> s2(vvFis[*it2].begin(), vvFis[*it2].end());
std::set<int> 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<int>::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<int>::iterator it3 = s.begin(); it3 != s.end(); it3++)
ss << " " << (*it3 >> 1) << "(" << (*it3 & 1) << ")";
Print(ss.str(), true);
}
for(std::set<int>::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<Man, lit, LitMax> &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<Man, lit, LitMax> 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<Man, lit, LitMax> b;
Save(b);
int count_ = count;
std::list<int> targets = vObjs;
for(std::list<int>::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<bool> 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<bool> vMarks(nObjsAlloc);
MarkFoCone_rec(vMarks, *it);
std::list<int> targets2 = vObjs;
for(std::list<int>::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<int>::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<int> targets = vObjs;
for(std::list<int>::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<Man, lit, LitMax> 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<bool> vMarks(nObjsAlloc);
MarkFoCone_rec(vMarks, *it);
std::list<int> targets2 = vObjs;
for(std::list<int>::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<int>::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<int> targets = vObjs;
for(std::list<int>::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<bool> vMarks(nObjsAlloc);
MarkFoCone_rec(vMarks, *it);
for(std::list<int>::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<Man, lit, LitMax> 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<int> 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<lit> &vNodes) {
if(nVerbose > 6)
Print("\t\t\tBuild Exdc", true);
int i;
Gia_Obj_t *pObj;
std::vector<int> 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<lit> 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<int>::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<int>::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<lit> 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<int> values(nObjsAlloc);
values[0] = Gia_ManConst0Lit();
for(unsigned i = 0; i < vPis.size(); i++)
values[i + 1] = Gia_ManAppendCi(pGia);
for(std::list<int>::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<int>::iterator it = vObjs.begin(); it != vObjs.end(); it++)
vUpdates[*it] = true;
std::vector<lit> vFsOld;
CopyVec(vFsOld, vFs);
Build(false);
bool r = LitVecIsEq(vFsOld, vFs);
DelVec(vFsOld);
return r;
}
bool CspfDebug() {
std::vector<lit> vGsOld;
this->CopyVec(vGsOld, vGs);
std::vector<std::vector<lit> > 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<lit> vGsOld;
this->CopyVec(vGsOld, vGs);
std::vector<std::vector<lit> > 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<int>::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
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 \
......
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 );
......@@ -42582,6 +42584,173 @@ usage:
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] <file>\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<file> : 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 []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9LNetMap( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Abc_Ntk_t * Gia_ManPerformLNetMap( Gia_Man_t * p, int GroupSize, int fUseFixed, int fTryNew, int fVerbose );
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment