rewire clean up

This commit is contained in:
jiunhaochen 2025-04-19 00:43:48 +08:00
parent 5ea1240990
commit b1734ac297
2 changed files with 140 additions and 90 deletions

View File

@ -173,7 +173,7 @@ int Miaig::fromMiniAig(Mini_Aig_t *pMiniAig) {
Gia_Man_t *Miaig::toGia(void) {
int i, k, iLit, And2 = countAnd2();
Gia_Man_t *pGia = Gia_ManStart(1 + nIns() + And2 + nOuts()), *pTemp;
pGia->pName = Abc_UtilStrsav( _data->pName );
pGia->pName = Abc_UtilStrsav(_data->pName);
Gia_ManHashAlloc(pGia);
memset(_data->pCopy, 0, sizeof(int) * nObjs());
Miaig_ForEachInput(i)
@ -310,7 +310,7 @@ void Miaig::topoCollect_rec(int iObj) {
objTravId(iObj) = nTravIds();
Vi_PushOrder(_data->vOrder, iObj);
Miaig_ForEachObjFanin(iObj, iLit, i)
topoCollect_rec(Abc_Lit2Var(iLit));
topoCollect_rec(Rw_Lit2Var(iLit));
}
vi *Miaig::topoCollect(void) {
@ -320,7 +320,7 @@ vi *Miaig::topoCollect(void) {
Miaig_ForEachConstInput(i)
objTravId(i) = nTravIds();
Miaig_ForEachOutput(i)
topoCollect_rec(Abc_Lit2Var(objFanin0(i)));
topoCollect_rec(Rw_Lit2Var(objFanin0(i)));
return _data->vOrder;
}
@ -331,7 +331,7 @@ int Miaig::initializeLevels_rec(int iObj) {
return objLevel(iObj);
int level = -1;
Miaig_ForEachObjFanin(iObj, iLit, i) {
level = Abc_MaxInt(initializeLevels_rec(Abc_Lit2Var(iLit)), level);
level = Abc_MaxInt(initializeLevels_rec(Rw_Lit2Var(iLit)), level);
}
return objLevel(iObj) = level + 1;
}
@ -348,7 +348,7 @@ void Miaig::initializeLevels(void) {
objLevel(i) = 0;
}
Miaig_ForEachOutput(i) {
objLevel(i) = initializeLevels_rec(Abc_Lit2Var(objFanin0(i)));
objLevel(i) = initializeLevels_rec(Rw_Lit2Var(objFanin0(i)));
}
}
@ -366,7 +366,7 @@ void Miaig::markDistanceN_rec(int iObj, int n, int limit) {
if (n == limit)
return;
Miaig_ForEachObjFanin(iObj, iLit, i)
markDistanceN_rec(Abc_Lit2Var(iLit), n + 1, limit);
markDistanceN_rec(Rw_Lit2Var(iLit), n + 1, limit);
}
void Miaig::markDistanceN(int iObj, int n) {
@ -378,8 +378,8 @@ void Miaig::markDistanceN(int iObj, int n) {
if (objDist(j) >= 0) continue;
int minDist = nObjs();
Miaig_ForEachObjFanin(j, iLit, k) {
if (objDist(Abc_Lit2Var(iLit)) == -1) continue;
minDist = Abc_MinInt(minDist, objDist(Abc_Lit2Var(iLit)));
if (objDist(Rw_Lit2Var(iLit)) == -1) continue;
minDist = Rw_MinInt(minDist, objDist(Rw_Lit2Var(iLit)));
}
if (minDist != nObjs()) {
markDistanceN_rec(j, minDist + 1, n);
@ -388,26 +388,50 @@ void Miaig::markDistanceN(int iObj, int n) {
}
}
void Miaig::markCritical(void) {
int iObj;
int maxRequire = countLevel(0);
nTravIds()++;
Miaig_ForEachOutput(iObj) {
if (objLevel(iObj) != maxRequire) continue;
markCritical_rec(iObj);
}
}
void Miaig::markCritical_rec(int iObj) {
objTravId(iObj) = nTravIds();
if (objIsPi(iObj)) return;
int iLit, k;
int maxFaninLevel = objLevel(Rw_Lit2Var(objFanin0(iObj)));
Miaig_ForEachObjFaninStart(iObj, iLit, k, 1) {
maxFaninLevel = Rw_MaxInt(maxFaninLevel, objLevel(Rw_Lit2Var(iLit)));
}
Miaig_ForEachObjFanin(iObj, iLit, k) {
if (objLevel(Rw_Lit2Var(iLit)) != maxFaninLevel) continue;
markCritical_rec(Rw_Lit2Var(iLit));
}
}
// reference counting
void Miaig::refObj(int iObj) {
int k, iLit;
Miaig_ForEachObjFanin(iObj, iLit, k)
objRef(Abc_Lit2Var(iLit))++;
objRef(Rw_Lit2Var(iLit))++;
}
void Miaig::derefObj(int iObj) {
int k, iLit;
Miaig_ForEachObjFanin(iObj, iLit, k)
objRef(Abc_Lit2Var(iLit))--;
objRef(Rw_Lit2Var(iLit))--;
}
void Miaig::derefObj_rec(int iObj, int iLitSkip) {
int k, iLit;
Miaig_ForEachObjFanin(iObj, iLit, k) {
if (iLit != iLitSkip && --objRef(Abc_Lit2Var(iLit)) == 0 && objIsNode(Abc_Lit2Var(iLit))) {
derefObj_rec(Abc_Lit2Var(iLit), -1);
Vi_Fill(_data->pvFans + Abc_Lit2Var(iLit), 1, 0);
refObj(Abc_Lit2Var(iLit));
if (iLit != iLitSkip && --objRef(Rw_Lit2Var(iLit)) == 0 && objIsNode(Rw_Lit2Var(iLit))) {
derefObj_rec(Rw_Lit2Var(iLit), -1);
Vi_Fill(objFanins(Rw_Lit2Var(iLit)), 1, 0);
refObj(Rw_Lit2Var(iLit));
}
}
}
@ -423,7 +447,7 @@ void Miaig::verifyRefs(void) {
int i;
Miaig_ForEachNodeOutput(i)
derefObj(i);
for (i = 0; i < _data->nObjs; i++)
for (i = 0; i < nObjs(); i++)
if (objRef(i))
printf("Ref count of node %d is incorrect (%d).\n", i, objRef(i));
initializeRefs();
@ -436,7 +460,7 @@ void Miaig::markDfs_rec(int iObj) {
return;
objTravId(iObj) = nTravIds();
Miaig_ForEachObjFanin(iObj, iLit, i)
markDfs_rec(Abc_Lit2Var(iLit));
markDfs_rec(Rw_Lit2Var(iLit));
}
int Miaig::markDfs(void) {
@ -445,7 +469,7 @@ int Miaig::markDfs(void) {
Miaig_ForEachConstInput(i)
objTravId(i) = nTravIds();
Miaig_ForEachOutput(i)
markDfs_rec(Abc_Lit2Var(objFanin0(i)));
markDfs_rec(Rw_Lit2Var(objFanin0(i)));
Miaig_ForEachOutput(i)
objTravId(i) = nTravIds();
Miaig_ForEachNode(i)
@ -485,7 +509,7 @@ void Miaig::dupDfs_rec(Miaig &pNew, int iObj) {
return;
// 2. create fanins for a given node
Miaig_ForEachObjFanin(iObj, iLit, i)
dupDfs_rec(pNew, Abc_Lit2Var(iLit));
dupDfs_rec(pNew, Rw_Lit2Var(iLit));
assert(objCopy(iObj) < 0); // combinational loop catching
assert(objFaninNum(iObj) > 0);
// 3. create current node
@ -505,7 +529,7 @@ Miaig Miaig::dupDfs(void) {
objCopy(i) = i;
// 2. for each primary output we call recursive function for it's fanin
Miaig_ForEachOutput(i)
dupDfs_rec(pNew, Abc_Lit2Var(objFanin0(i)));
dupDfs_rec(pNew, Rw_Lit2Var(objFanin0(i)));
// 3. for each primary output append it's fanin
Miaig_ForEachOutput(i)
pNew.appendFanin(pNew.appendObj(), Rw_Lit2LitV(_data->pCopy, objFanin0(i)));
@ -544,10 +568,10 @@ void Miaig::reduceFanins(vi *v) {
int Miaig::hashTwo(int l0, int l1, int TableSize) {
unsigned Key = 0;
Key += Abc_Lit2Var(l0) * 7937;
Key += Abc_Lit2Var(l1) * 2971;
Key += Abc_LitIsCompl(l0) * 911;
Key += Abc_LitIsCompl(l1) * 353;
Key += Rw_Lit2Var(l0) * 7937;
Key += Rw_Lit2Var(l1) * 2971;
Key += Rw_LitIsCompl(l0) * 911;
Key += Rw_LitIsCompl(l1) * 353;
return Key % TableSize;
}
@ -573,14 +597,14 @@ int Miaig::buildNode(int l0, int l1, int fCprop, int fStrash) {
}
int *pPlace = NULL;
if (fStrash) {
pPlace = hashLookup(_data->pTable, Abc_MinInt(l0, l1), Abc_MaxInt(l0, l1), _data->TableSize);
pPlace = hashLookup(_data->pTable, Rw_MinInt(l0, l1), Rw_MaxInt(l0, l1), _data->TableSize);
if (*pPlace)
return *pPlace;
}
int iObj = appendObj();
appendFanin(iObj, Abc_MinInt(l0, l1));
appendFanin(iObj, Abc_MaxInt(l0, l1));
return pPlace ? (*pPlace = Abc_Var2Lit(iObj, 0)) : Abc_Var2Lit(iObj, 0);
appendFanin(iObj, Rw_MinInt(l0, l1));
appendFanin(iObj, Rw_MaxInt(l0, l1));
return pPlace ? (*pPlace = Rw_Var2Lit(iObj, 0)) : Rw_Var2Lit(iObj, 0);
}
int Miaig::buildNodeBalance_rec(Miaig &pNew, vi *vFanins, int begin, int end, int fCprop, int fStrash) {
@ -621,13 +645,13 @@ Miaig Miaig::dupStrash(int fCprop, int fStrash, int fCascade) {
pNew._data->pTable = (int *)calloc(sizeof(int), 3 * pNew._data->TableSize);
}
Miaig_ForEachInput(i)
objCopy(i) = Abc_Var2Lit(i, 0);
objCopy(i) = Rw_Var2Lit(i, 0);
Miaig_ForEachNode(i) {
assert(objFaninNum(i) > 0);
if (fCascade)
objCopy(i) = buildNodeCascade(pNew, _data->pvFans + i, fCprop, fStrash);
objCopy(i) = buildNodeCascade(pNew, objFanins(i), fCprop, fStrash);
else
objCopy(i) = buildNodeBalance(pNew, _data->pvFans + i, fCprop, fStrash);
objCopy(i) = buildNodeBalance(pNew, objFanins(i), fCprop, fStrash);
}
Miaig_ForEachOutput(i)
pNew.appendFanin(pNew.appendObj(), Rw_Lit2LitL(_data->pCopy, objFanin0(i)));
@ -643,21 +667,21 @@ int *Miaig::createStops(void) {
assert(objFaninNum(i) == 2);
int iLit0 = objFanin0(i);
int iLit1 = objFanin1(i);
pStop[Abc_Lit2Var(iLit0)] += 1 + Abc_LitIsCompl(iLit0);
pStop[Abc_Lit2Var(iLit1)] += 1 + Abc_LitIsCompl(iLit1);
pStop[Rw_Lit2Var(iLit0)] += 1 + Rw_LitIsCompl(iLit0);
pStop[Rw_Lit2Var(iLit1)] += 1 + Rw_LitIsCompl(iLit1);
}
Miaig_ForEachOutput(i)
pStop[Abc_Lit2Var(objFanin0(i))] += 2;
pStop[Rw_Lit2Var(objFanin0(i))] += 2;
return pStop;
}
void Miaig::collectSuper_rec(int iLit, int *pStop, vi *vSuper) {
if (pStop[Abc_Lit2Var(iLit)] > 1)
if (pStop[Rw_Lit2Var(iLit)] > 1)
Vi_Push(vSuper, Rw_Lit2LitL(_data->pCopy, iLit));
else {
assert(Abc_LitIsCompl(iLit) == 0);
collectSuper_rec(objFanin0(Abc_Lit2Var(iLit)), pStop, vSuper);
collectSuper_rec(objFanin1(Abc_Lit2Var(iLit)), pStop, vSuper);
assert(Rw_LitIsCompl(iLit) == 0);
collectSuper_rec(objFanin0(Rw_Lit2Var(iLit)), pStop, vSuper);
collectSuper_rec(objFanin1(Rw_Lit2Var(iLit)), pStop, vSuper);
}
}
@ -669,7 +693,7 @@ Miaig Miaig::dupMulti(int nFaninMax_, int nGrowth) {
assert(nFaninMax_ >= 2 && nGrowth >= 1);
memset(_data->pCopy, 0, sizeof(int) * nObjs()); // obj2lit
Miaig_ForEachConstInput(i)
objCopy(i) = Abc_Var2Lit(i, 0);
objCopy(i) = Rw_Var2Lit(i, 0);
Miaig_ForEachNode(i) {
if (pStop[i] == 1)
continue;
@ -693,7 +717,7 @@ Miaig Miaig::dupMulti(int nFaninMax_, int nGrowth) {
// create a cascade of nodes
while (Vi_Size(vArray) > nFaninMaxLocal) {
int iObj = pNew.appendObj();
vi *vFanins = pNew._data->pvFans + iObj;
vi *vFanins = pNew.objFanins(iObj);
assert(vFanins->ptr == NULL);
vFanins->cap = nFaninMaxLocal + nGrowthLocal;
vFanins->ptr = (int *)malloc(sizeof(int) * vFanins->cap);
@ -702,18 +726,18 @@ Miaig Miaig::dupMulti(int nFaninMax_, int nGrowth) {
assert(Vi_Space(vFanins) == nGrowthLocal);
for (k = 0; k < nFaninMaxLocal; k++)
Vi_Drop(vArray, 0);
Vi_Push(vArray, Abc_Var2Lit(iObj, 0));
Vi_Push(vArray, Rw_Var2Lit(iObj, 0));
}
// create the last node
int iObj = pNew.appendObj();
vi *vFanins = pNew._data->pvFans + iObj;
vi *vFanins = pNew.objFanins(iObj);
assert(vFanins->ptr == NULL);
vFanins->cap = Vi_Size(vArray) + nGrowthLocal;
vFanins->ptr = (int *)malloc(sizeof(int) * vFanins->cap);
Vi_ForEachEntry(vArray, iLit, k)
pNew.appendFanin(iObj, iLit);
assert(Vi_Space(vFanins) == nGrowthLocal);
objCopy(i) = Abc_Var2Lit(iObj, 0);
objCopy(i) = Rw_Var2Lit(iObj, 0);
}
}
Miaig_ForEachOutput(i)
@ -727,8 +751,8 @@ Miaig Miaig::dupMulti(int nFaninMax_, int nGrowth) {
void Miaig::truthSimNode(int i) {
int k, iLit;
Miaig_ForEachObjFanin(i, iLit, k) {
if (k == 0) Tt_DupC(objTruth(i, objType(i)), objTruth(Abc_Lit2Var(iLit), objType(Abc_Lit2Var(iLit))), Abc_LitIsCompl(iLit), nWords());
else Tt_Sharp(objTruth(i, objType(i)), objTruth(Abc_Lit2Var(iLit), objType(Abc_Lit2Var(iLit))), Abc_LitIsCompl(iLit), nWords());
if (k == 0) Tt_DupC(objTruth(i, objType(i)), objTruth(Rw_Lit2Var(iLit), objType(Rw_Lit2Var(iLit))), Rw_LitIsCompl(iLit), nWords());
else Tt_Sharp(objTruth(i, objType(i)), objTruth(Rw_Lit2Var(iLit), objType(Rw_Lit2Var(iLit))), Rw_LitIsCompl(iLit), nWords());
}
}
@ -739,9 +763,9 @@ word *Miaig::truthSimNodeSubset(int i, int m) {
Miaig_ForEachObjFanin(i, iLit, k) {
if ((m >> k) & 1) { // fanin is included in the subset
if (Counter++ == 0)
Tt_DupC(_data->pProd, objTruth(Abc_Lit2Var(iLit), 0), Abc_LitIsCompl(iLit), nWords());
Tt_DupC(_data->pProd, objTruth(Rw_Lit2Var(iLit), 0), Rw_LitIsCompl(iLit), nWords());
else
Tt_Sharp(_data->pProd, objTruth(Abc_Lit2Var(iLit), 0), Abc_LitIsCompl(iLit), nWords());
Tt_Sharp(_data->pProd, objTruth(Rw_Lit2Var(iLit), 0), Rw_LitIsCompl(iLit), nWords());
}
}
assert(Counter == Tt_BitCount16(m));
@ -751,8 +775,8 @@ word *Miaig::truthSimNodeSubset(int i, int m) {
word *Miaig::truthSimNodeSubset2(int i, vi *vFanins, int nFanins) {
int k, iLit;
Vi_ForEachEntryStop(vFanins, iLit, k, nFanins) {
if (k == 0) Tt_DupC(_data->pProd, objTruth(Abc_Lit2Var(iLit), 0), Abc_LitIsCompl(iLit), nWords());
else Tt_Sharp(_data->pProd, objTruth(Abc_Lit2Var(iLit), 0), Abc_LitIsCompl(iLit), nWords());
if (k == 0) Tt_DupC(_data->pProd, objTruth(Rw_Lit2Var(iLit), 0), Rw_LitIsCompl(iLit), nWords());
else Tt_Sharp(_data->pProd, objTruth(Rw_Lit2Var(iLit), 0), Rw_LitIsCompl(iLit), nWords());
}
return _data->pProd;
}
@ -808,7 +832,7 @@ int Miaig::computeTfo_rec(int iObj) {
if (objTravId(iObj) == nTravIds() - 1)
return 0;
Miaig_ForEachObjFanin(iObj, iLit, k) {
Value |= computeTfo_rec(Abc_Lit2Var(iLit));
Value |= computeTfo_rec(Rw_Lit2Var(iLit));
}
objTravId(iObj) = nTravIds() - 1 + Value;
if (Value) Vi_Push(_data->vTfo, iObj);
@ -867,7 +891,6 @@ void Miaig::addPair(vi *vPair, int iFan1, int iFan2) {
pArray = Vi_Array(vPair);
}
pArray[i + 2]++;
//printf( "Adding pair (%d, %d)\n", iFan1, iFan2 );
}
// find fanin pair that appears most often
@ -905,11 +928,11 @@ void Miaig::extractBest(vi *vPairs) {
int iBest = findPair(vPairs);
assert(iBest >= 0);
//printf( "Creating node %d with fanins (%d, %d).\n", iObj, pArray[iBest], pArray[iBest+1] );
assert(Vi_Size(_data->pvFans + iObj) == 0);
assert(Vi_Size(objFanins(iObj)) == 0);
appendFanin(iObj, pArray[iBest]);
appendFanin(iObj, pArray[iBest + 1]);
Miaig_ForEachNode(i)
Counter += updateFanins(_data->pvFans + i, pArray[iBest], pArray[iBest + 1], Abc_Var2Lit(iObj, 0));
Counter += updateFanins(objFanins(i), pArray[iBest], pArray[iBest + 1], Rw_Var2Lit(iObj, 0));
assert(Counter == pArray[iBest + 2]);
}
@ -918,7 +941,7 @@ vi *Miaig::findPairs(word *pSto, int nWords) {
vi *vPairs = Vi_Alloc(30);
int i, f1, f2, iFan1, iFan2;
Miaig_ForEachNode(i) {
vi *vFans = _data->pvFans + i;
vi *vFans = objFanins(i);
Vi_ForEachEntry(vFans, iFan1, f1) {
word *pRowFan1 = pSto + iFan1 * nWords;
Vi_ForEachEntryStart(vFans, iFan2, f2, f1 + 1) {
@ -964,7 +987,7 @@ int Miaig::checkConst(int iObj, word *pCare, word *pExc, int fCheck, int fVerbos
word *pFunc = objTruth(iObj, 0);
if (!Tt_IntersectC(pCare, pFunc, 0, nWords())) {
derefObj_rec(iObj, -1);
Vi_Fill(_data->pvFans + iObj, 1, 0); // const0
Vi_Fill(objFanins(iObj), 1, 0); // const0
refObj(iObj);
truthUpdate(_data->vTfo, pExc, fCheck);
if (fVerbose) printf("Detected Const0 at node %d.\n", iObj);
@ -972,7 +995,7 @@ int Miaig::checkConst(int iObj, word *pCare, word *pExc, int fCheck, int fVerbos
}
if (!Tt_IntersectC(pCare, pFunc, 1, nWords())) {
derefObj_rec(iObj, -1);
Vi_Fill(_data->pvFans + iObj, 1, 1); // const1
Vi_Fill(objFanins(iObj), 1, 1); // const1
refObj(iObj);
truthUpdate(_data->vTfo, pExc, fCheck);
if (fVerbose) printf("Detected Const1 at node %d.\n", iObj);
@ -985,10 +1008,10 @@ int Miaig::expandOne(int iObj, int nAddedMax, int nDist, int nExpandableLevel, w
int i, k, n, iLit, nAdded = 0;
word *pCare = computeCareSet(iObj, pExc);
assert(nAddedMax > 0);
assert(nAddedMax <= Vi_Space(_data->pvFans + iObj));
assert(nAddedMax <= Vi_Space(objFanins(iObj)));
// mark node's fanins
Miaig_ForEachObjFanin(iObj, iLit, k)
objTravId(Abc_Lit2Var(iLit)) = nTravIds();
objTravId(Rw_Lit2Var(iLit)) = nTravIds();
// compute the onset
word *pOnset = objTruth(iObj, 0);
Tt_Sharp(pOnset, pCare, 0, nWords());
@ -1005,13 +1028,13 @@ int Miaig::expandOne(int iObj, int nAddedMax, int nDist, int nExpandableLevel, w
int *pOrderF = Vi_Array(_data->vOrderF);
std::stable_sort(pOrderF, pOrderF + Vi_Size(_data->vOrderF), [&](int a, int b) {
return objLevel(Abc_Lit2Var(a)) > objLevel(Abc_Lit2Var(b));
return objLevel(Rw_Lit2Var(a)) > objLevel(Rw_Lit2Var(b));
});
std::stable_sort(pOrderF, pOrderF + Vi_Size(_data->vOrderF), [&](int a, int b) {
if (objLevel(Abc_Lit2Var(a)) == 0 || objLevel(Abc_Lit2Var(b)) == 0) {
if (objLevel(Rw_Lit2Var(a)) == 0 || objLevel(Rw_Lit2Var(b)) == 0) {
return false;
}
return objRef(Abc_Lit2Var(a)) < objRef(Abc_Lit2Var(b));
return objRef(Rw_Lit2Var(a)) < objRef(Rw_Lit2Var(b));
});
// iterate through candidate fanins (nodes that are not in the TFO of iObj)
@ -1020,8 +1043,8 @@ int Miaig::expandOne(int iObj, int nAddedMax, int nDist, int nExpandableLevel, w
// new fanin can be added if its offset does not intersect with the node's onset
for (n = 0; n < 2; n++)
if (!Tt_IntersectC(pOnset, objTruth(i, 0), !n, nWords())) {
if (fVerbose) printf("Adding node %d fanin %d\n", iObj, Abc_Var2Lit(i, n));
appendFanin(iObj, Abc_Var2Lit(i, n));
if (fVerbose) printf("Adding node %d fanin %d\n", iObj, Rw_Var2Lit(i, n));
appendFanin(iObj, Rw_Var2Lit(i, n));
objRef(i)++;
nAdded++;
break;
@ -1047,10 +1070,10 @@ int Miaig::reduceOne(int iObj, int fOnlyConst, int fOnlyBuffer, int fHeuristic,
// if one fanin can be used, take it
word *pFunc = objTruth(iObj, 0);
Miaig_ForEachObjFanin(iObj, iLit, k) {
Tt_DupC(_data->pProd, objTruth(Abc_Lit2Var(iLit), 0), Abc_LitIsCompl(iLit), nWords());
Tt_DupC(_data->pProd, objTruth(Rw_Lit2Var(iLit), 0), Rw_LitIsCompl(iLit), nWords());
if (Tt_EqualOnCare(pCare, pFunc, _data->pProd, nWords())) {
derefObj(iObj);
Vi_Fill(_data->pvFans + iObj, 1, iLit);
Vi_Fill(objFanins(iObj), 1, iLit);
refObj(iObj);
truthUpdate(_data->vTfo, pExc, fCheck);
if (fVerbose) printf("Reducing node %d fanin count from %d to %d.\n", iObj, nFans, objFaninNum(iObj));
@ -1067,13 +1090,13 @@ int Miaig::reduceOne(int iObj, int fOnlyConst, int fOnlyBuffer, int fHeuristic,
if (fHeuristic) {
int *pOrderF = Vi_Array(_data->vOrderF);
std::stable_sort(pOrderF, pOrderF + Vi_Size(_data->vOrderF), [&](int a, int b) {
return objLevel(Abc_Lit2Var(a)) < objLevel(Abc_Lit2Var(b));
return objLevel(Rw_Lit2Var(a)) < objLevel(Rw_Lit2Var(b));
});
std::stable_sort(pOrderF, pOrderF + Vi_Size(_data->vOrderF), [&](int a, int b) {
if (objLevel(Abc_Lit2Var(a)) == 0 || objLevel(Abc_Lit2Var(b)) == 0) {
if (objLevel(Rw_Lit2Var(a)) == 0 || objLevel(Rw_Lit2Var(b)) == 0) {
return false;
}
return objRef(Abc_Lit2Var(a)) > objRef(Abc_Lit2Var(b));
return objRef(Rw_Lit2Var(a)) > objRef(Rw_Lit2Var(b));
});
}
@ -1089,9 +1112,9 @@ int Miaig::reduceOne(int iObj, int fOnlyConst, int fOnlyBuffer, int fHeuristic,
// update the node if it is reduced
if (Vi_Size(_data->vOrderF) < nFans) {
derefObj(iObj);
Vi_Shrink(_data->pvFans + iObj, 0);
Vi_Shrink(objFanins(iObj), 0);
Vi_ForEachEntry(_data->vOrderF, iLit, k)
Vi_PushOrder(_data->pvFans + iObj, iLit);
Vi_PushOrder(objFanins(iObj), iLit);
refObj(iObj);
truthUpdate(_data->vTfo, pExc, fCheck);
if (fVerbose) printf("Reducing node %d fanin count from %d to %d.\n", iObj, nFans, objFaninNum(iObj));
@ -1101,7 +1124,7 @@ int Miaig::reduceOne(int iObj, int fOnlyConst, int fOnlyBuffer, int fHeuristic,
}
int Miaig::expandThenReduceOne(int iNode, int nFaninAddLimit, int nDist, int nExpandableLevel, word *pExc, int fCheck, int fVerbose) {
expandOne(iNode, Abc_MinInt(Vi_Space(_data->pvFans + iNode), nFaninAddLimit), nDist, nExpandableLevel, pExc, fCheck, fVerbose);
expandOne(iNode, std::min(Vi_Space(objFanins(iNode)), nFaninAddLimit), nDist, nExpandableLevel, pExc, fCheck, fVerbose);
reduceOne(iNode, 0, 0, 0, pExc, fCheck, fVerbose);
return 0;
}
@ -1125,12 +1148,12 @@ Miaig Miaig::expand(int nFaninAddLimitAll, int nDist, int nExpandableLevel, word
initializeLevels();
if (nDist) initializeDists();
Vi_ForEachEntry(vOrder, iNode, i) {
nAdded += expandOne(iNode, Abc_MinInt(Vi_Space(_data->pvFans + iNode), nFaninAddLimitAll - nAdded), nDist, nExpandableLevel, pExc, fCheck, fVerbose);
nAdded += expandOne(iNode, std::min(Vi_Space(objFanins(iNode)), nFaninAddLimitAll - nAdded), nDist, nExpandableLevel, pExc, fCheck, fVerbose);
if (nAdded >= nFaninAddLimitAll)
break;
}
assert(nAdded <= nFaninAddLimitAll);
verifyRefs();
if (fCheck) verifyRefs();
return dupDfs();
}
@ -1157,7 +1180,7 @@ Miaig Miaig::reduce(word *pExc, int fCheck, int fVerbose) {
// works best for final
Vi_ForEachEntry(vOrder, iNode, i)
reduceOne(iNode, 0, 0, 1, pExc, fCheck, fVerbose);
verifyRefs();
if (fCheck) verifyRefs();
return dupStrash(1, 1, 1);
}
@ -1173,7 +1196,7 @@ Miaig Miaig::expandThenReduce(int nFaninAddLimit, int nDist, int nExpandableLeve
Vi_ForEachEntry(vOrder, iNode, i) {
expandThenReduceOne(iNode, nFaninAddLimit, nDist, nExpandableLevel, pExc, fCheck, fVerbose);
}
verifyRefs();
if (fCheck) verifyRefs();
return dupDfs().dupStrash(1, 1, 1);
}

View File

@ -27,6 +27,15 @@
#include "base/abc/abc.h"
#include "aig/miniaig/miniaig.h"
#include "rewire_map.h"
#define RW_INT_MAX ABC_INT_MAX
#define Rw_MaxInt Abc_MaxInt
#define Rw_MinInt Abc_MinInt
#define Rw_Var2Lit Abc_Var2Lit
#define Rw_Lit2Var Abc_Lit2Var
#define Rw_LitIsCompl Abc_LitIsCompl
#define Rw_LitNot Abc_LitNot
#define Rw_LitNotCond Abc_LitNotCond
#define Rw_LitRegular Abc_LitRegular
#else
#ifdef _WIN32
typedef unsigned __int64 word; // 32-bit windows
@ -38,6 +47,15 @@ typedef __int64 iword; // 32-bit windows
#else
typedef long long iword; // other platforms
#endif
#define RW_INT_MAX (2147483647)
static inline int Rw_MaxInt( int a, int b ) { return a > b ? a : b; }
static inline int Rw_MinInt( int a, int b ) { return a < b ? a : b; }
static inline int Rw_Var2Lit( int Var, int c ) { assert(Var >= 0 && !(c >> 1)); return Var + Var + c; }
static inline int Rw_Lit2Var( int Lit ) { assert(Lit >= 0); return Lit >> 1; }
static inline int Rw_LitIsCompl( int Lit ) { assert(Lit >= 0); return Lit & 1; }
static inline int Rw_LitNot( int Lit ) { assert(Lit >= 0); return Lit ^ 1; }
static inline int Rw_LitNotCond( int Lit, int c ) { assert(Lit >= 0); return Lit ^ (int)(c > 0); }
static inline int Rw_LitRegular( int Lit ) { assert(Lit >= 0); return Lit & ~01; }
#endif // RW_ABC
#include "rewire_vec.h"
#include "rewire_tt.h"
@ -129,15 +147,16 @@ static inline int RW_XADD(int *addr, int delta) {
#define Miaig_ForEachNodeOutputStart(i, s) for (i = s; i < _data->nObjs; i++)
#define Miaig_ForEachObj(i) for (i = 0; i < _data->nObjs; i++)
#define Miaig_ForEachObjFanin(i, iLit, k) Vi_ForEachEntry(&_data->pvFans[i], iLit, k)
#define Miaig_ForEachObjFaninStart(i, iLit, k, s) Vi_ForEachEntryStart(&_data->pvFans[i], iLit, k, s)
static inline int Rw_Lit2LitV(int *pMapV2V, int Lit) {
assert(Lit >= 0);
return Abc_Var2Lit(pMapV2V[Abc_Lit2Var(Lit)], Abc_LitIsCompl(Lit));
return Rw_Var2Lit(pMapV2V[Rw_Lit2Var(Lit)], Rw_LitIsCompl(Lit));
}
static inline int Rw_Lit2LitL(int *pMapV2L, int Lit) {
assert(Lit >= 0);
return Abc_LitNotCond(pMapV2L[Abc_Lit2Var(Lit)], Abc_LitIsCompl(Lit));
return Rw_LitNotCond(pMapV2L[Rw_Lit2Var(Lit)], Rw_LitIsCompl(Lit));
}
struct Miaig_Data {
@ -222,6 +241,7 @@ public:
int &objDist(int i);
int &nTravIds(void);
word *objTruth(int i, int n);
vi *objFanins(int i);
int objType(int i);
int nWords(void);
void refObj(int iObj);
@ -242,6 +262,8 @@ private:
int markDfs(void);
void markDistanceN_rec(int iObj, int n, int limit);
void markDistanceN(int Obj, int n);
void markCritical(void);
void markCritical_rec(int iObj);
void topoCollect_rec(int iObj);
vi *topoCollect(void);
void reduceFanins(vi *v);
@ -269,7 +291,7 @@ public:
float countAnd2(int reset = 0, int fDummy = 0);
// 0: amap 1: &nf 2: &simap
float countTransistors(int reset = 0, int nMode = 0);
int countLevel(void);
int countLevel(int min = 0);
private:
void dupDfs_rec(Miaig &pNew, int iObj);
@ -416,15 +438,15 @@ inline int &Miaig::nObjsAlloc(void) {
}
inline int Miaig::objIsPi(int i) {
return i > 0 && i <= _data->nIns;
return i > 0 && i <= nIns();
}
inline int Miaig::objIsPo(int i) {
return i >= _data->nObjs - _data->nOuts;
return i >= nObjs() - nOuts();
}
inline int Miaig::objIsNode(int i) {
return i > _data->nIns && i < _data->nObjs - _data->nOuts;
return i > nIns() && i < nObjs() - nOuts();
}
inline int Miaig::objPiIdx(int i) {
@ -434,29 +456,29 @@ inline int Miaig::objPiIdx(int i) {
inline int Miaig::objPoIdx(int i) {
// assert(objIsPo(i));
return i - (_data->nObjs - _data->nOuts);
return i - (nObjs() - nOuts());
}
inline int Miaig::appendObj(void) {
assert(_data->nObjs < _data->nObjsAlloc);
return _data->nObjs++;
assert(nObjs() < nObjsAlloc());
return nObjs()++;
}
inline void Miaig::appendFanin(int i, int iLit) {
Vi_PushOrder(_data->pvFans + i, iLit);
Vi_PushOrder(objFanins(i), iLit);
}
inline int Miaig::objFaninNum(int i) {
return Vi_Size(_data->pvFans + i);
return Vi_Size(objFanins(i));
}
inline int Miaig::objFanin0(int i) {
return Vi_Read(_data->pvFans + i, 0);
return Vi_Read(objFanins(i), 0);
}
inline int Miaig::objFanin1(int i) {
assert(objFaninNum(i) == 2);
return Vi_Read(_data->pvFans + i, 1);
return Vi_Read(objFanins(i), 1);
}
inline int &Miaig::objLevel(int i) {
@ -495,11 +517,12 @@ inline float Miaig::countAnd2(int reset, int fDummy) {
return Counter;
}
inline int Miaig::countLevel(void) {
inline int Miaig::countLevel(int min) {
initializeLevels();
int i, Level = -1;
int i, Level = (min) ? RW_INT_MAX : -1;
int (*compareFunc)(int, int) = (min) ? Rw_MinInt : Rw_MaxInt;
Miaig_ForEachOutput(i) {
Level = Abc_MaxInt(Level, objLevel(i));
Level = compareFunc(Level, objLevel(i));
}
return Level;
}
@ -508,6 +531,10 @@ inline word *Miaig::objTruth(int i, int n) {
return _data->pTruths[n] + nWords() * i;
}
inline vi *Miaig::objFanins(int i) {
return _data->pvFans + i;
}
inline int Miaig::objType(int i) {
return objTravId(i) == nTravIds();
}