Intersection a bug in rewrite/refactor.

9 files changed, 84 insertions, 46 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index eea66f29..b4e22a38 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -559,7 +559,7 @@ extern ABC_DLL Abc_Obj_t *        Abc_AigOr( Abc_Aig_t * pMan, Abc_Obj_t * p0, A
 extern ABC_DLL Abc_Obj_t *        Abc_AigXor( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 );
 extern ABC_DLL Abc_Obj_t *        Abc_AigMux( Abc_Aig_t * pMan, Abc_Obj_t * pC, Abc_Obj_t * p1, Abc_Obj_t * p0 );
 extern ABC_DLL Abc_Obj_t *        Abc_AigMiter( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs, int fImplic );
-extern ABC_DLL void               Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, int  fUpdateLevel );
+extern ABC_DLL int                Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, int  fUpdateLevel );
 extern ABC_DLL void               Abc_AigDeleteNode( Abc_Aig_t * pMan, Abc_Obj_t * pOld );
 extern ABC_DLL void               Abc_AigRehash( Abc_Aig_t * pMan );
 extern ABC_DLL int                Abc_AigNodeHasComplFanoutEdge( Abc_Obj_t * pNode );
diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c
index d3347a13..8469789b 100644
--- a/src/base/abc/abcAig.c
+++ b/src/base/abc/abcAig.c
@@ -847,7 +847,7 @@ Abc_Obj_t * Abc_AigMiter2( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, int fUpdateLevel )
+int Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, int fUpdateLevel )
 {
     assert( Vec_PtrSize(pMan->vStackReplaceOld) == 0 );
     assert( Vec_PtrSize(pMan->vStackReplaceNew) == 0 );
@@ -859,6 +859,8 @@ void Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, int f
     {
         pOld = (Abc_Obj_t *)Vec_PtrPop( pMan->vStackReplaceOld );
         pNew = (Abc_Obj_t *)Vec_PtrPop( pMan->vStackReplaceNew );
+        if ( Abc_ObjFanoutNum(pOld) != 0 )
+            return 0;
         Abc_AigReplace_int( pMan, pOld, pNew, fUpdateLevel );
     }
     if ( fUpdateLevel )
@@ -867,6 +869,7 @@ void Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, int f
         if ( pMan->pNtkAig->vLevelsR ) 
             Abc_AigUpdateLevelR_int( pMan );
     }
+    return 1;
 }
 
 /**Function*************************************************************
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index c92917ac..06d7cb08 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -7312,8 +7312,8 @@ usage:
 ***********************************************************************/
 int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
-    int c;
+    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc), * pDup;
+    int c, RetValue;
     int fUpdateLevel;
     int fPrecompute;
     int fUseZeros;
@@ -7383,10 +7383,21 @@ int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // modify the current network
-    if ( !Abc_NtkRewrite( pNtk, fUpdateLevel, fUseZeros, fVerbose, fVeryVerbose, fPlaceEnable ) )
+    pDup = Abc_NtkDup( pNtk );
+    RetValue = Abc_NtkRewrite( pNtk, fUpdateLevel, fUseZeros, fVerbose, fVeryVerbose, fPlaceEnable );
+    if ( RetValue == -1 )
     {
-        Abc_Print( -1, "Rewriting has failed.\n" );
-        return 1;
+        Abc_FrameReplaceCurrentNetwork( pAbc, pDup );
+        printf( "An error occurred during computation. The original network is restored.\n" );
+    }
+    else
+    {
+        Abc_NtkDelete( pDup );
+        if ( RetValue == 0 )
+        {
+            Abc_Print( 0, "Rewriting has failed.\n" );
+            return 1;
+        }
     }
     return 0;
 
@@ -7415,8 +7426,8 @@ usage:
 ***********************************************************************/
 int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
-    int c;
+    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc), * pDup;
+    int c, RetValue;
     int nNodeSizeMax;
     int nConeSizeMax;
     int fUpdateLevel;
@@ -7506,10 +7517,21 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // modify the current network
-    if ( !Abc_NtkRefactor( pNtk, nNodeSizeMax, nConeSizeMax, fUpdateLevel, fUseZeros, fUseDcs, fVerbose ) )
+    pDup = Abc_NtkDup( pNtk );
+    RetValue = Abc_NtkRefactor( pNtk, nNodeSizeMax, nConeSizeMax, fUpdateLevel, fUseZeros, fUseDcs, fVerbose );
+    if ( RetValue == -1 )
     {
-        Abc_Print( -1, "Refactoring has failed.\n" );
-        return 1;
+        Abc_FrameReplaceCurrentNetwork( pAbc, pDup );
+        printf( "An error occurred during computation. The original network is restored.\n" );
+    }
+    else
+    {
+        Abc_NtkDelete( pDup );
+        if ( RetValue == 0 )
+        {
+            Abc_Print( 0, "Refactoring has failed.\n" );
+            return 1;
+        }
     }
     return 0;
 
diff --git a/src/base/abci/abcRefactor.c b/src/base/abci/abcRefactor.c
index 3cc6d793..8ec5944f 100644
--- a/src/base/abci/abcRefactor.c
+++ b/src/base/abci/abcRefactor.c
@@ -325,7 +325,7 @@ void Abc_NtkManRefPrintStats( Abc_ManRef_t * p )
 ***********************************************************************/
 int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, int fUpdateLevel, int fUseZeros, int fUseDcs, int fVerbose )
 {
-    extern void           Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain );
+    extern int           Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain );
     ProgressBar * pProgress;
     Abc_ManRef_t * pManRef;
     Abc_ManCut_t * pManCut;
@@ -333,7 +333,7 @@ int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, int f
     Vec_Ptr_t * vFanins;
     Abc_Obj_t * pNode;
     abctime clk, clkStart = Abc_Clock();
-    int i, nNodes;
+    int i, nNodes, RetValue = 1;
 
     assert( Abc_NtkIsStrash(pNtk) );
     // cleanup the AIG
@@ -377,7 +377,12 @@ pManRef->timeRes += Abc_Clock() - clk;
             continue;
         // acceptable replacement found, update the graph
 clk = Abc_Clock();
-        Dec_GraphUpdateNetwork( pNode, pFForm, fUpdateLevel, pManRef->nLastGain );
+        if ( !Dec_GraphUpdateNetwork( pNode, pFForm, fUpdateLevel, pManRef->nLastGain ) )
+        {
+            Dec_GraphFree( pFForm );
+            RetValue = -1;
+            break;
+        }
 pManRef->timeNtk += Abc_Clock() - clk;
         Dec_GraphFree( pFForm );
     }
@@ -394,18 +399,21 @@ pManRef->timeTotal = Abc_Clock() - clkStart;
     // put the nodes into the DFS order and reassign their IDs
     Abc_NtkReassignIds( pNtk );
 //    Abc_AigCheckFaninOrder( pNtk->pManFunc );
-    // fix the levels
-    if ( fUpdateLevel )
-        Abc_NtkStopReverseLevels( pNtk );
-    else
-        Abc_NtkLevel( pNtk );
-    // check
-    if ( !Abc_NtkCheck( pNtk ) )
+    if ( RetValue != -1 )
     {
-        printf( "Abc_NtkRefactor: The network check has failed.\n" );
-        return 0;
+        // fix the levels
+        if ( fUpdateLevel )
+            Abc_NtkStopReverseLevels( pNtk );
+        else
+            Abc_NtkLevel( pNtk );
+        // check
+        if ( !Abc_NtkCheck( pNtk ) )
+        {
+            printf( "Abc_NtkRefactor: The network check has failed.\n" );
+            return 0;
+        }
     }
-    return 1;
+    return RetValue;
 }
 
 
diff --git a/src/base/abci/abcRestruct.c b/src/base/abci/abcRestruct.c
index ef5dd451..87f15238 100644
--- a/src/base/abci/abcRestruct.c
+++ b/src/base/abci/abcRestruct.c
@@ -105,7 +105,7 @@ static void Abc_NtkManRstPrintStats( Abc_ManRst_t * p );
 ***********************************************************************/
 int Abc_NtkRestructure( Abc_Ntk_t * pNtk, int nCutMax, int fUpdateLevel, int fUseZeros, int fVerbose )
 {
-    extern void           Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain );
+    extern int           Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain );
     ProgressBar * pProgress;
     Abc_ManRst_t * pManRst;
     Cut_Man_t * pManCut;
diff --git a/src/base/abci/abcResub.c b/src/base/abci/abcResub.c
index b8934e23..dc1b6036 100644
--- a/src/base/abci/abcResub.c
+++ b/src/base/abci/abcResub.c
@@ -136,7 +136,7 @@ extern abctime s_ResubTime;
 ***********************************************************************/
 int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutMax, int nStepsMax, int nLevelsOdc, int fUpdateLevel, int fVerbose, int fVeryVerbose )
 {
-    extern void           Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain );
+    extern int           Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain );
     ProgressBar * pProgress;
     Abc_ManRes_t * pManRes;
     Abc_ManCut_t * pManCut;
diff --git a/src/base/abci/abcRewrite.c b/src/base/abci/abcRewrite.c
index 0b0881a6..1da7e4e8 100644
--- a/src/base/abci/abcRewrite.c
+++ b/src/base/abci/abcRewrite.c
@@ -60,14 +60,14 @@ extern void  Abc_PlaceUpdate( Vec_Ptr_t * vAddedCells, Vec_Ptr_t * vUpdatedNets
 ***********************************************************************/
 int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerbose, int fVeryVerbose, int fPlaceEnable )
 {
-    extern void           Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain );
+    extern int           Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain );
     ProgressBar * pProgress;
     Cut_Man_t * pManCut;
     Rwr_Man_t * pManRwr;
     Abc_Obj_t * pNode;
 //    Vec_Ptr_t * vAddedCells = NULL, * vUpdatedNets = NULL;
     Dec_Graph_t * pGraph;
-    int i, nNodes, nGain, fCompl;
+    int i, nNodes, nGain, fCompl, RetValue = 1;
     abctime clk, clkStart = Abc_Clock();
 
     assert( Abc_NtkIsStrash(pNtk) );
@@ -138,7 +138,11 @@ Rwr_ManAddTimeCuts( pManRwr, Abc_Clock() - clk );
         // complement the FF if needed
         if ( fCompl ) Dec_GraphComplement( pGraph );
 clk = Abc_Clock();
-        Dec_GraphUpdateNetwork( pNode, pGraph, fUpdateLevel, nGain );
+        if ( !Dec_GraphUpdateNetwork( pNode, pGraph, fUpdateLevel, nGain ) )
+        {
+            RetValue = -1;
+            break;
+        }
 Rwr_ManAddTimeUpdate( pManRwr, Abc_Clock() - clk );
         if ( fCompl ) Dec_GraphComplement( pGraph );
 
@@ -175,17 +179,20 @@ Rwr_ManAddTimeTotal( pManRwr, Abc_Clock() - clkStart );
     }
 //    Abc_AigCheckFaninOrder( pNtk->pManFunc );
     // fix the levels
-    if ( fUpdateLevel )
-        Abc_NtkStopReverseLevels( pNtk );
-    else
-        Abc_NtkLevel( pNtk );
-    // check
-    if ( !Abc_NtkCheck( pNtk ) )
+    if ( RetValue >= 0 )
     {
-        printf( "Abc_NtkRewrite: The network check has failed.\n" );
-        return 0;
+        if ( fUpdateLevel )
+            Abc_NtkStopReverseLevels( pNtk );
+        else
+            Abc_NtkLevel( pNtk );
+        // check
+        if ( !Abc_NtkCheck( pNtk ) )
+        {
+            printf( "Abc_NtkRewrite: The network check has failed.\n" );
+            return 0;
+        }
     }
-    return 1;
+    return RetValue;
 }
 
 
diff --git a/src/base/abci/abcRr.c b/src/base/abci/abcRr.c
index 52d1fd32..86c5f13e 100644
--- a/src/base/abci/abcRr.c
+++ b/src/base/abci/abcRr.c
@@ -397,10 +397,7 @@ int Abc_NtkRRUpdate( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, Abc_Obj_t * pFanin, Ab
     else assert( 0 );
     // replace
     if ( pFanout == NULL )
-    {
-        Abc_AigReplace( (Abc_Aig_t *)pNtk->pManFunc, pNode, pNodeNew, 1 );
-        return 1;
-    }
+        return Abc_AigReplace( (Abc_Aig_t *)pNtk->pManFunc, pNode, pNodeNew, 1 );
     // find the fanout after redundancy removal
     if ( pNode == Abc_ObjFanin0(pFanout) )
         pFanoutNew = Abc_AigAnd( (Abc_Aig_t *)pNtk->pManFunc, Abc_ObjNotCond(pNodeNew,Abc_ObjFaninC0(pFanout)), Abc_ObjChild1(pFanout) );
diff --git a/src/bool/dec/decAbc.c b/src/bool/dec/decAbc.c
index 6602702c..e440a652 100644
--- a/src/bool/dec/decAbc.c
+++ b/src/bool/dec/decAbc.c
@@ -237,20 +237,21 @@ int Dec_GraphToNetworkCount( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMa
   SeeAlso     []
 
 ***********************************************************************/
-void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain )
+int Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int fUpdateLevel, int nGain )
 {
     extern Abc_Obj_t *    Dec_GraphToNetwork( Abc_Ntk_t * pNtk, Dec_Graph_t * pGraph );
     Abc_Obj_t * pRootNew;
     Abc_Ntk_t * pNtk = pRoot->pNtk;
-    int nNodesNew, nNodesOld;
+    int nNodesNew, nNodesOld, RetValue;
     nNodesOld = Abc_NtkNodeNum(pNtk);
     // create the new structure of nodes
     pRootNew = Dec_GraphToNetwork( pNtk, pGraph );
     // remove the old nodes
-    Abc_AigReplace( (Abc_Aig_t *)pNtk->pManFunc, pRoot, pRootNew, fUpdateLevel );
+    RetValue = Abc_AigReplace( (Abc_Aig_t *)pNtk->pManFunc, pRoot, pRootNew, fUpdateLevel );
     // compare the gains
     nNodesNew = Abc_NtkNodeNum(pNtk);
     //assert( nGain <= nNodesOld - nNodesNew );
+    return RetValue;
 }