Skip to content

A
abc
Commit cf1fdc82 by Alan Mishchenko
Options

Bug fix in 'resub' to enable additional divisors, by Siang-Yun Lee.

parent ea1fbfc9
Showing with 368 additions and 124 deletions
src/base/abci/abcResub.c
......@@ -650,14 +650,12 @@ Dec_Graph_t * Abc_ManResubQuit1( Abc_Obj_t * pRoot, Abc_Obj_t * pObj0, Abc_Obj_t
{
Dec_Graph_t * pGraph;
Dec_Edge_t eRoot, eNode0, eNode1;
assert( pObj0 != pObj1 );
assert( !Abc_ObjIsComplement(pObj0) );
assert( !Abc_ObjIsComplement(pObj1) );
assert( Abc_ObjRegular(pObj0) != Abc_ObjRegular(pObj1) );
pGraph = Dec_GraphCreate( 2 );
Dec_GraphNode( pGraph, 0 )->pFunc = pObj0;
Dec_GraphNode( pGraph, 1 )->pFunc = pObj1;
eNode0 = Dec_EdgeCreate( 0, pObj0->fPhase );
eNode1 = Dec_EdgeCreate( 1, pObj1->fPhase );
Dec_GraphNode( pGraph, 0 )->pFunc = Abc_ObjRegular(pObj0);
Dec_GraphNode( pGraph, 1 )->pFunc = Abc_ObjRegular(pObj1);
eNode0 = Dec_EdgeCreate( 0, Abc_ObjRegular(pObj0)->fPhase ^ Abc_ObjIsComplement(pObj0) );
eNode1 = Dec_EdgeCreate( 1, Abc_ObjRegular(pObj1)->fPhase ^ Abc_ObjIsComplement(pObj1) );
if ( fOrGate )
eRoot = Dec_GraphAddNodeOr( pGraph, eNode0, eNode1 );
else
......@@ -683,17 +681,16 @@ Dec_Graph_t * Abc_ManResubQuit21( Abc_Obj_t * pRoot, Abc_Obj_t * pObj0, Abc_Obj_
{
Dec_Graph_t * pGraph;
Dec_Edge_t eRoot, eNode0, eNode1, eNode2;
assert( pObj0 != pObj1 );
assert( !Abc_ObjIsComplement(pObj0) );
assert( !Abc_ObjIsComplement(pObj1) );
assert( !Abc_ObjIsComplement(pObj2) );
assert( Abc_ObjRegular(pObj0) != Abc_ObjRegular(pObj1) );
assert( Abc_ObjRegular(pObj0) != Abc_ObjRegular(pObj2) );
assert( Abc_ObjRegular(pObj1) != Abc_ObjRegular(pObj2) );
pGraph = Dec_GraphCreate( 3 );
Dec_GraphNode( pGraph, 0 )->pFunc = pObj0;
Dec_GraphNode( pGraph, 1 )->pFunc = pObj1;
Dec_GraphNode( pGraph, 2 )->pFunc = pObj2;
eNode0 = Dec_EdgeCreate( 0, pObj0->fPhase );
eNode1 = Dec_EdgeCreate( 1, pObj1->fPhase );
eNode2 = Dec_EdgeCreate( 2, pObj2->fPhase );
Dec_GraphNode( pGraph, 0 )->pFunc = Abc_ObjRegular(pObj0);
Dec_GraphNode( pGraph, 1 )->pFunc = Abc_ObjRegular(pObj1);
Dec_GraphNode( pGraph, 2 )->pFunc = Abc_ObjRegular(pObj2);
eNode0 = Dec_EdgeCreate( 0, Abc_ObjRegular(pObj0)->fPhase ^ Abc_ObjIsComplement(pObj0) );
eNode1 = Dec_EdgeCreate( 1, Abc_ObjRegular(pObj1)->fPhase ^ Abc_ObjIsComplement(pObj1) );
eNode2 = Dec_EdgeCreate( 2, Abc_ObjRegular(pObj2)->fPhase ^ Abc_ObjIsComplement(pObj2) );
if ( fOrGate )
{
eRoot = Dec_GraphAddNodeOr( pGraph, eNode0, eNode1 );
......@@ -725,15 +722,14 @@ Dec_Graph_t * Abc_ManResubQuit2( Abc_Obj_t * pRoot, Abc_Obj_t * pObj0, Abc_Obj_t
{
Dec_Graph_t * pGraph;
Dec_Edge_t eRoot, ePrev, eNode0, eNode1, eNode2;
assert( pObj0 != pObj1 );
assert( pObj0 != pObj2 );
assert( pObj1 != pObj2 );
assert( !Abc_ObjIsComplement(pObj0) );
assert( Abc_ObjRegular(pObj0) != Abc_ObjRegular(pObj1) );
assert( Abc_ObjRegular(pObj0) != Abc_ObjRegular(pObj2) );
assert( Abc_ObjRegular(pObj1) != Abc_ObjRegular(pObj2) );
pGraph = Dec_GraphCreate( 3 );
Dec_GraphNode( pGraph, 0 )->pFunc = Abc_ObjRegular(pObj0);
Dec_GraphNode( pGraph, 1 )->pFunc = Abc_ObjRegular(pObj1);
Dec_GraphNode( pGraph, 2 )->pFunc = Abc_ObjRegular(pObj2);
eNode0 = Dec_EdgeCreate( 0, Abc_ObjRegular(pObj0)->fPhase );
eNode0 = Dec_EdgeCreate( 0, Abc_ObjRegular(pObj0)->fPhase ^ Abc_ObjIsComplement(pObj0) );
if ( Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) )
{
eNode1 = Dec_EdgeCreate( 1, Abc_ObjRegular(pObj1)->fPhase );
......@@ -771,8 +767,8 @@ Dec_Graph_t * Abc_ManResubQuit3( Abc_Obj_t * pRoot, Abc_Obj_t * pObj0, Abc_Obj_t
{
Dec_Graph_t * pGraph;
Dec_Edge_t eRoot, ePrev0, ePrev1, eNode0, eNode1, eNode2, eNode3;
assert( pObj0 != pObj1 );
assert( pObj2 != pObj3 );
assert( Abc_ObjRegular(pObj0) != Abc_ObjRegular(pObj1) );
assert( Abc_ObjRegular(pObj2) != Abc_ObjRegular(pObj3) );
pGraph = Dec_GraphCreate( 4 );
Dec_GraphNode( pGraph, 0 )->pFunc = Abc_ObjRegular(pObj0);
Dec_GraphNode( pGraph, 1 )->pFunc = Abc_ObjRegular(pObj1);
......@@ -840,6 +836,7 @@ Dec_Graph_t * Abc_ManResubQuit3( Abc_Obj_t * pRoot, Abc_Obj_t * pObj0, Abc_Obj_t
***********************************************************************/
void Abc_ManResubDivsS( Abc_ManRes_t * p, int Required )
{
int fMoreDivs = 1; // bug fix by Siang-Yun Lee
Abc_Obj_t * pObj;
unsigned * puData, * puDataR;
int i, w;
......@@ -863,6 +860,18 @@ void Abc_ManResubDivsS( Abc_ManRes_t * p, int Required )
Vec_PtrPush( p->vDivs1UP, pObj );
continue;
}
if ( fMoreDivs )
{
for ( w = 0; w < p->nWords; w++ )
// if ( ~puData[w] & ~puDataR[w] )
if ( ~puData[w] & ~puDataR[w] & p->pCareSet[w] ) // care set
break;
if ( w == p->nWords )
{
Vec_PtrPush( p->vDivs1UP, Abc_ObjNot(pObj) );
continue;
}
}
// check negative containment
for ( w = 0; w < p->nWords; w++ )
// if ( ~puData[w] & puDataR[w] )
......@@ -873,6 +882,18 @@ void Abc_ManResubDivsS( Abc_ManRes_t * p, int Required )
Vec_PtrPush( p->vDivs1UN, pObj );
continue;
}
if ( fMoreDivs )
{
for ( w = 0; w < p->nWords; w++ )
// if ( puData[w] & puDataR[w] )
if ( puData[w] & puDataR[w] & p->pCareSet[w] ) // care set
break;
if ( w == p->nWords )
{
Vec_PtrPush( p->vDivs1UN, Abc_ObjNot(pObj) );
continue;
}
}
// add the node to binates
Vec_PtrPush( p->vDivs1B, pObj );
}
......@@ -1081,14 +1102,38 @@ Dec_Graph_t * Abc_ManResubDivs1( Abc_ManRes_t * p, int Required )
// check positive unate divisors
Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs1UP, pObj0, i )
{
puData0 = (unsigned *)pObj0->pData;
puData0 = (unsigned *)Abc_ObjRegular(pObj0)->pData;
Vec_PtrForEachEntryStart( Abc_Obj_t *, p->vDivs1UP, pObj1, k, i + 1 )
{
puData1 = (unsigned *)pObj1->pData;
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] | puData1[w]) != puDataR[w] )
if ( ((puData0[w] | puData1[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
puData1 = (unsigned *)Abc_ObjRegular(pObj1)->pData;
if ( Abc_ObjIsComplement(pObj0) && Abc_ObjIsComplement(pObj1) )
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] | puData1[w]) != puDataR[w] )
if ( ((~puData0[w] | ~puData1[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
else if ( Abc_ObjIsComplement(pObj0) )
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] | puData1[w]) != puDataR[w] )
if ( ((~puData0[w] | puData1[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
else if ( Abc_ObjIsComplement(pObj1) )
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] | puData1[w]) != puDataR[w] )
if ( ((puData0[w] | ~puData1[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
else
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] | puData1[w]) != puDataR[w] )
if ( ((puData0[w] | puData1[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
if ( w == p->nWords )
{
p->nUsedNode1Or++;
......@@ -1099,14 +1144,38 @@ Dec_Graph_t * Abc_ManResubDivs1( Abc_ManRes_t * p, int Required )
// check negative unate divisors
Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs1UN, pObj0, i )
{
puData0 = (unsigned *)pObj0->pData;
puData0 = (unsigned *)Abc_ObjRegular(pObj0)->pData;
Vec_PtrForEachEntryStart( Abc_Obj_t *, p->vDivs1UN, pObj1, k, i + 1 )
{
puData1 = (unsigned *)pObj1->pData;
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] & puData1[w]) != puDataR[w] )
if ( ((puData0[w] & puData1[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
puData1 = (unsigned *)Abc_ObjRegular(pObj1)->pData;
if ( Abc_ObjIsComplement(pObj0) && Abc_ObjIsComplement(pObj1) )
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] & puData1[w]) != puDataR[w] )
if ( ((~puData0[w] & ~puData1[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
if ( Abc_ObjIsComplement(pObj0) )
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] & puData1[w]) != puDataR[w] )
if ( ((~puData0[w] & puData1[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
if ( Abc_ObjIsComplement(pObj1) )
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] & puData1[w]) != puDataR[w] )
if ( ((puData0[w] & ~puData1[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
else
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] & puData1[w]) != puDataR[w] )
if ( ((puData0[w] & puData1[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
if ( w == p->nWords )
{
p->nUsedNode1And++;
......@@ -1137,31 +1206,84 @@ Dec_Graph_t * Abc_ManResubDivs12( Abc_ManRes_t * p, int Required )
// check positive unate divisors
Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs1UP, pObj0, i )
{
puData0 = (unsigned *)pObj0->pData;
puData0 = (unsigned *)Abc_ObjRegular(pObj0)->pData;
Vec_PtrForEachEntryStart( Abc_Obj_t *, p->vDivs1UP, pObj1, k, i + 1 )
{
puData1 = (unsigned *)pObj1->pData;
puData1 = (unsigned *)Abc_ObjRegular(pObj1)->pData;
Vec_PtrForEachEntryStart( Abc_Obj_t *, p->vDivs1UP, pObj2, j, k + 1 )
{
puData2 = (unsigned *)pObj2->pData;
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] | puData1[w] | puData2[w]) != puDataR[w] )
if ( ((puData0[w] | puData1[w] | puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
puData2 = (unsigned *)Abc_ObjRegular(pObj2)->pData;
if ( Abc_ObjIsComplement(pObj0) && Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) )
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] | puData1[w] | puData2[w]) != puDataR[w] )
if ( ((~puData0[w] | ~puData1[w] | ~puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
else if ( Abc_ObjIsComplement(pObj0) && Abc_ObjIsComplement(pObj1) && !Abc_ObjIsComplement(pObj2) )
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] | puData1[w] | puData2[w]) != puDataR[w] )
if ( ((~puData0[w] | ~puData1[w] | puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
else if ( Abc_ObjIsComplement(pObj0) && !Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) )
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] | puData1[w] | puData2[w]) != puDataR[w] )
if ( ((~puData0[w] | puData1[w] | ~puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
else if ( Abc_ObjIsComplement(pObj0) && !Abc_ObjIsComplement(pObj1) && !Abc_ObjIsComplement(pObj2) )
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] | puData1[w] | puData2[w]) != puDataR[w] )
if ( ((~puData0[w] | puData1[w] | puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
else if ( !Abc_ObjIsComplement(pObj0) && Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) )
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] | puData1[w] | puData2[w]) != puDataR[w] )
if ( ((puData0[w] | ~puData1[w] | ~puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
else if ( !Abc_ObjIsComplement(pObj0) && Abc_ObjIsComplement(pObj1) && !Abc_ObjIsComplement(pObj2) )
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] | puData1[w] | puData2[w]) != puDataR[w] )
if ( ((puData0[w] | ~puData1[w] | puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
else if ( !Abc_ObjIsComplement(pObj0) && !Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) )
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] | puData1[w] | puData2[w]) != puDataR[w] )
if ( ((puData0[w] | puData1[w] | ~puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
else if ( !Abc_ObjIsComplement(pObj0) && !Abc_ObjIsComplement(pObj1) && !Abc_ObjIsComplement(pObj2) )
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] | puData1[w] | puData2[w]) != puDataR[w] )
if ( ((puData0[w] | puData1[w] | puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
else assert( 0 );
if ( w == p->nWords )
{
LevelMax = Abc_MaxInt( pObj0->Level, Abc_MaxInt(pObj1->Level, pObj2->Level) );
LevelMax = Abc_MaxInt( Abc_ObjRegular(pObj0)->Level, Abc_MaxInt(Abc_ObjRegular(pObj1)->Level, Abc_ObjRegular(pObj2)->Level) );
assert( LevelMax <= Required - 1 );
pObjMax = NULL;
if ( (int)pObj0->Level == LevelMax )
if ( (int)Abc_ObjRegular(pObj0)->Level == LevelMax )
pObjMax = pObj0, pObjMin0 = pObj1, pObjMin1 = pObj2;
if ( (int)pObj1->Level == LevelMax )
if ( (int)Abc_ObjRegular(pObj1)->Level == LevelMax )
{
if ( pObjMax ) continue;
pObjMax = pObj1, pObjMin0 = pObj0, pObjMin1 = pObj2;
}
if ( (int)pObj2->Level == LevelMax )
if ( (int)Abc_ObjRegular(pObj2)->Level == LevelMax )
{
if ( pObjMax ) continue;
pObjMax = pObj2, pObjMin0 = pObj0, pObjMin1 = pObj1;
......@@ -1178,31 +1300,84 @@ Dec_Graph_t * Abc_ManResubDivs12( Abc_ManRes_t * p, int Required )
// check negative unate divisors
Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs1UN, pObj0, i )
{
puData0 = (unsigned *)pObj0->pData;
puData0 = (unsigned *)Abc_ObjRegular(pObj0)->pData;
Vec_PtrForEachEntryStart( Abc_Obj_t *, p->vDivs1UN, pObj1, k, i + 1 )
{
puData1 = (unsigned *)pObj1->pData;
puData1 = (unsigned *)Abc_ObjRegular(pObj1)->pData;
Vec_PtrForEachEntryStart( Abc_Obj_t *, p->vDivs1UN, pObj2, j, k + 1 )
{
puData2 = (unsigned *)pObj2->pData;
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] & puData1[w] & puData2[w]) != puDataR[w] )
if ( ((puData0[w] & puData1[w] & puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
puData2 = (unsigned *)Abc_ObjRegular(pObj2)->pData;
if ( Abc_ObjIsComplement(pObj0) && Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) )
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] & puData1[w] & puData2[w]) != puDataR[w] )
if ( ((~puData0[w] & ~puData1[w] & ~puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
else if ( Abc_ObjIsComplement(pObj0) && Abc_ObjIsComplement(pObj1) && !Abc_ObjIsComplement(pObj2) )
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] & puData1[w] & puData2[w]) != puDataR[w] )
if ( ((~puData0[w] & ~puData1[w] & puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
else if ( Abc_ObjIsComplement(pObj0) && !Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) )
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] & puData1[w] & puData2[w]) != puDataR[w] )
if ( ((~puData0[w] & puData1[w] & ~puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
else if ( Abc_ObjIsComplement(pObj0) && !Abc_ObjIsComplement(pObj1) && !Abc_ObjIsComplement(pObj2) )
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] & puData1[w] & puData2[w]) != puDataR[w] )
if ( ((~puData0[w] & puData1[w] & puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
else if ( !Abc_ObjIsComplement(pObj0) && Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) )
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] & puData1[w] & puData2[w]) != puDataR[w] )
if ( ((puData0[w] & ~puData1[w] & ~puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
else if ( !Abc_ObjIsComplement(pObj0) && Abc_ObjIsComplement(pObj1) && !Abc_ObjIsComplement(pObj2) )
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] & puData1[w] & puData2[w]) != puDataR[w] )
if ( ((puData0[w] & ~puData1[w] & puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
else if ( !Abc_ObjIsComplement(pObj0) && !Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) )
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] & puData1[w] & puData2[w]) != puDataR[w] )
if ( ((puData0[w] & puData1[w] & ~puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
else if ( !Abc_ObjIsComplement(pObj0) && !Abc_ObjIsComplement(pObj1) && !Abc_ObjIsComplement(pObj2) )
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] & puData1[w] & puData2[w]) != puDataR[w] )
if ( ((puData0[w] & puData1[w] & puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
else assert( 0 );
if ( w == p->nWords )
{
LevelMax = Abc_MaxInt( pObj0->Level, Abc_MaxInt(pObj1->Level, pObj2->Level) );
LevelMax = Abc_MaxInt( Abc_ObjRegular(pObj0)->Level, Abc_MaxInt(Abc_ObjRegular(pObj1)->Level, Abc_ObjRegular(pObj2)->Level) );
assert( LevelMax <= Required - 1 );
pObjMax = NULL;
if ( (int)pObj0->Level == LevelMax )
if ( (int)Abc_ObjRegular(pObj0)->Level == LevelMax )
pObjMax = pObj0, pObjMin0 = pObj1, pObjMin1 = pObj2;
if ( (int)pObj1->Level == LevelMax )
if ( (int)Abc_ObjRegular(pObj1)->Level == LevelMax )
{
if ( pObjMax ) continue;
pObjMax = pObj1, pObjMin0 = pObj0, pObjMin1 = pObj2;
}
if ( (int)pObj2->Level == LevelMax )
if ( (int)Abc_ObjRegular(pObj2)->Level == LevelMax )
{
if ( pObjMax ) continue;
pObjMax = pObj2, pObjMin0 = pObj0, pObjMin1 = pObj1;
......@@ -1239,40 +1414,74 @@ Dec_Graph_t * Abc_ManResubDivs2( Abc_ManRes_t * p, int Required )
// check positive unate divisors
Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs1UP, pObj0, i )
{
puData0 = (unsigned *)pObj0->pData;
puData0 = (unsigned *)Abc_ObjRegular(pObj0)->pData;
Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs2UP0, pObj1, k )
{
pObj2 = (Abc_Obj_t *)Vec_PtrEntry( p->vDivs2UP1, k );
puData1 = (unsigned *)Abc_ObjRegular(pObj1)->pData;
puData2 = (unsigned *)Abc_ObjRegular(pObj2)->pData;
if ( Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) )
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] | (puData1[w] | puData2[w])) != puDataR[w] )
if ( ((puData0[w] | (puData1[w] | puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
else if ( Abc_ObjIsComplement(pObj1) )
if ( Abc_ObjIsComplement(pObj0) )
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] | (~puData1[w] & puData2[w])) != puDataR[w] )
if ( ((puData0[w] | (~puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
else if ( Abc_ObjIsComplement(pObj2) )
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] | (puData1[w] & ~puData2[w])) != puDataR[w] )
if ( ((puData0[w] | (puData1[w] & ~puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
if ( Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) )
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] | (puData1[w] | puData2[w])) != puDataR[w] )
if ( ((~puData0[w] | (puData1[w] | puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
else if ( Abc_ObjIsComplement(pObj1) )
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] | (~puData1[w] & puData2[w])) != puDataR[w] )
if ( ((~puData0[w] | (~puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
else if ( Abc_ObjIsComplement(pObj2) )
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] | (puData1[w] & ~puData2[w])) != puDataR[w] )
if ( ((~puData0[w] | (puData1[w] & ~puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
else
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] | (puData1[w] & puData2[w])) != puDataR[w] )
if ( ((~puData0[w] | (puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
}
else
else
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] | (puData1[w] & puData2[w])) != puDataR[w] )
if ( ((puData0[w] | (puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
if ( Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) )
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] | (puData1[w] | puData2[w])) != puDataR[w] )
if ( ((puData0[w] | (puData1[w] | puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
else if ( Abc_ObjIsComplement(pObj1) )
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] | (~puData1[w] & puData2[w])) != puDataR[w] )
if ( ((puData0[w] | (~puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
else if ( Abc_ObjIsComplement(pObj2) )
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] | (puData1[w] & ~puData2[w])) != puDataR[w] )
if ( ((puData0[w] | (puData1[w] & ~puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
else
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] | (puData1[w] & puData2[w])) != puDataR[w] )
if ( ((puData0[w] | (puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
}
if ( w == p->nWords )
{
......@@ -1284,40 +1493,74 @@ Dec_Graph_t * Abc_ManResubDivs2( Abc_ManRes_t * p, int Required )
// check negative unate divisors
Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs1UN, pObj0, i )
{
puData0 = (unsigned *)pObj0->pData;
puData0 = (unsigned *)Abc_ObjRegular(pObj0)->pData;
Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs2UN0, pObj1, k )
{
pObj2 = (Abc_Obj_t *)Vec_PtrEntry( p->vDivs2UN1, k );
puData1 = (unsigned *)Abc_ObjRegular(pObj1)->pData;
puData2 = (unsigned *)Abc_ObjRegular(pObj2)->pData;
if ( Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) )
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] & (puData1[w] | puData2[w])) != puDataR[w] )
if ( ((puData0[w] & (puData1[w] | puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
else if ( Abc_ObjIsComplement(pObj1) )
if ( Abc_ObjIsComplement(pObj0) )
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] & (~puData1[w] & puData2[w])) != puDataR[w] )
if ( ((puData0[w] & (~puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
else if ( Abc_ObjIsComplement(pObj2) )
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] & (puData1[w] & ~puData2[w])) != puDataR[w] )
if ( ((puData0[w] & (puData1[w] & ~puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
if ( Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) )
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] & (puData1[w] | puData2[w])) != puDataR[w] )
if ( ((~puData0[w] & (puData1[w] | puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
else if ( Abc_ObjIsComplement(pObj1) )
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] & (~puData1[w] & puData2[w])) != puDataR[w] )
if ( ((~puData0[w] & (~puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
else if ( Abc_ObjIsComplement(pObj2) )
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] & (puData1[w] & ~puData2[w])) != puDataR[w] )
if ( ((~puData0[w] & (puData1[w] & ~puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
else
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] & (puData1[w] & puData2[w])) != puDataR[w] )
if ( ((~puData0[w] & (puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
}
else
else
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] & (puData1[w] & puData2[w])) != puDataR[w] )
if ( ((puData0[w] & (puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
if ( Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) )
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] & (puData1[w] | puData2[w])) != puDataR[w] )
if ( ((puData0[w] & (puData1[w] | puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
else if ( Abc_ObjIsComplement(pObj1) )
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] & (~puData1[w] & puData2[w])) != puDataR[w] )
if ( ((puData0[w] & (~puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
else if ( Abc_ObjIsComplement(pObj2) )
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] & (puData1[w] & ~puData2[w])) != puDataR[w] )
if ( ((puData0[w] & (puData1[w] & ~puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
else
{
for ( w = 0; w < p->nWords; w++ )
// if ( (puData0[w] & (puData1[w] & puData2[w])) != puDataR[w] )
if ( ((puData0[w] & (puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set
break;
}
}
if ( w == p->nWords )
{
......@@ -1472,6 +1715,7 @@ Dec_Graph_t * Abc_ManResubDivs3( Abc_ManRes_t * p, int Required )
}
}
}
/*
// check negative unate divisors
Vec_PtrForEachEntry( Abc_Obj_t *, p->vDivs2UN0, pObj0, i )
......@@ -1493,85 +1737,85 @@ Dec_Graph_t * Abc_ManResubDivs3( Abc_ManRes_t * p, int Required )
{
case 0: // 0000
for ( w = 0; w < p->nWords; w++ )
if ( ((puData0[w] & puData1[w]) & (puData2[w] & puData3[w])) != puDataR[w] )
if ( (((puData0[w] & puData1[w]) & (puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] )
break;
break;
case 1: // 0001
for ( w = 0; w < p->nWords; w++ )
if ( ((puData0[w] & puData1[w]) & (puData2[w] & ~puData3[w])) != puDataR[w] )
if ( (((puData0[w] & puData1[w]) & (puData2[w] & ~puData3[w])) ^ puDataR[w]) & p->pCareSet[w] )
break;
break;
case 2: // 0010
for ( w = 0; w < p->nWords; w++ )
if ( ((puData0[w] & puData1[w]) & (~puData2[w] & puData3[w])) != puDataR[w] )
if ( (((puData0[w] & puData1[w]) & (~puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] )
break;
break;
case 3: // 0011
for ( w = 0; w < p->nWords; w++ )
if ( ((puData0[w] & puData1[w]) & (puData2[w] | puData3[w])) != puDataR[w] )
if ( (((puData0[w] & puData1[w]) & (puData2[w] | puData3[w])) ^ puDataR[w]) & p->pCareSet[w] )
break;
break;
case 4: // 0100
for ( w = 0; w < p->nWords; w++ )
if ( ((puData0[w] & ~puData1[w]) & (puData2[w] & puData3[w])) != puDataR[w] )
if ( (((puData0[w] & ~puData1[w]) & (puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] )
break;
break;
case 5: // 0101
for ( w = 0; w < p->nWords; w++ )
if ( ((puData0[w] & ~puData1[w]) & (puData2[w] & ~puData3[w])) != puDataR[w] )
if ( (((puData0[w] & ~puData1[w]) & (puData2[w] & ~puData3[w])) ^ puDataR[w]) & p->pCareSet[w] )
break;
break;
case 6: // 0110
for ( w = 0; w < p->nWords; w++ )
if ( ((puData0[w] & ~puData1[w]) & (~puData2[w] & puData3[w])) != puDataR[w] )
if ( (((puData0[w] & ~puData1[w]) & (~puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] )
break;
break;
case 7: // 0111
for ( w = 0; w < p->nWords; w++ )
if ( ((puData0[w] & ~puData1[w]) & (puData2[w] | puData3[w])) != puDataR[w] )
if ( (((puData0[w] & ~puData1[w]) & (puData2[w] | puData3[w])) ^ puDataR[w]) & p->pCareSet[w] )
break;
break;
case 8: // 1000
for ( w = 0; w < p->nWords; w++ )
if ( ((~puData0[w] & puData1[w]) & (puData2[w] & puData3[w])) != puDataR[w] )
if ( (((~puData0[w] & puData1[w]) & (puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] )
break;
break;
case 9: // 1001
for ( w = 0; w < p->nWords; w++ )
if ( ((~puData0[w] & puData1[w]) & (puData2[w] & ~puData3[w])) != puDataR[w] )
if ( (((~puData0[w] & puData1[w]) & (puData2[w] & ~puData3[w])) ^ puDataR[w]) & p->pCareSet[w] )
break;
break;
case 10: // 1010
for ( w = 0; w < p->nWords; w++ )
if ( ((~puData0[w] & puData1[w]) & (~puData2[w] & puData3[w])) != puDataR[w] )
if ( (((~puData0[w] & puData1[w]) & (~puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] )
break;
break;
case 11: // 1011
for ( w = 0; w < p->nWords; w++ )
if ( ((~puData0[w] & puData1[w]) & (puData2[w] | puData3[w])) != puDataR[w] )
if ( (((~puData0[w] & puData1[w]) & (puData2[w] | puData3[w])) ^ puDataR[w]) & p->pCareSet[w] )
break;
break;
case 12: // 1100
for ( w = 0; w < p->nWords; w++ )
if ( ((puData0[w] | puData1[w]) & (puData2[w] & puData3[w])) != puDataR[w] )
if ( (((puData0[w] | puData1[w]) & (puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] )
break;
break;
case 13: // 1101
for ( w = 0; w < p->nWords; w++ )
if ( ((puData0[w] | puData1[w]) & (puData2[w] & ~puData3[w])) != puDataR[w] )
if ( (((puData0[w] | puData1[w]) & (puData2[w] & ~puData3[w])) ^ puDataR[w]) & p->pCareSet[w] )
break;
break;
case 14: // 1110
for ( w = 0; w < p->nWords; w++ )
if ( ((puData0[w] | puData1[w]) & (~puData2[w] & puData3[w])) != puDataR[w] )
if ( (((puData0[w] | puData1[w]) & (~puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] )
break;
break;
case 15: // 1111
for ( w = 0; w < p->nWords; w++ )
if ( ((puData0[w] | puData1[w]) & (puData2[w] | puData3[w])) != puDataR[w] )
if ( (((puData0[w] | puData1[w]) & (puData2[w] | puData3[w])) ^ puDataR[w]) & p->pCareSet[w] )
break;
break;
......
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