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

1 files changed, 368 insertions, 124 deletions

diff --git a/src/base/abci/abcResub.c b/src/base/abci/abcResub.c
index 9323f9e7..b8934e23 100644
--- a/src/base/abci/abcResub.c
+++ b/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;