Merge pull request berkeley-abc#23 from jix/fold-s

fold: Option (-s) to make sequential cleanup optional
phsauter · Jun 28, 2023 · bb64142 · bb64142
2 parents 1de4eaf + 1bd088d
commit bb64142
Show file tree

Hide file tree

Showing 5 changed files with 16 additions and 9 deletions.
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
@@ -114,7 +114,7 @@ extern Aig_Man_t *       Saig_ManDupFoldConstrs( Aig_Man_t * pAig, Vec_Int_t * v
 extern int               Saig_ManDetectConstrTest( Aig_Man_t * p );
 extern void              Saig_ManDetectConstrFuncTest( Aig_Man_t * p, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose );
 /*=== saigConstr2.c ==========================================================*/
-extern Aig_Man_t *       Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbose );
+extern Aig_Man_t *       Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbose, int fSeqCleanup );
 extern Aig_Man_t *       Saig_ManDupUnfoldConstrsFunc( Aig_Man_t * pAig, int nFrames, int nConfs, int nProps, int fOldAlgo, int fVerbose );
 // -- jlong -- begin
 extern Aig_Man_t *       Saig_ManDupFoldConstrsFunc2( Aig_Man_t * pAig, int fCompl, int fVerbose, int typeII_cnt );

diff --git a/src/aig/saig/saigConstr2.c b/src/aig/saig/saigConstr2.c
@@ -939,7 +939,7 @@ Aig_Man_t * Saig_ManDupUnfoldConstrsFunc( Aig_Man_t * pAig, int nFrames, int nCo
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbose )
+Aig_Man_t * Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbose, int fSeqCleanup )
 {
     Aig_Man_t * pAigNew;
     Aig_Obj_t * pMiter, * pFlopOut, * pFlopIn, * pObj;
@@ -1000,7 +1000,8 @@ Aig_Man_t * Saig_ManDupFoldConstrsFunc( Aig_Man_t * pAig, int fCompl, int fVerbo
 
     // perform cleanup
     Aig_ManCleanup( pAigNew );
-    Aig_ManSeqCleanup( pAigNew );
+    if ( fSeqCleanup )
+        Aig_ManSeqCleanup( pAigNew );
     return pAigNew;
 }
 

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
@@ -28530,14 +28530,16 @@ int Abc_CommandFold( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Ntk_t * pNtk, * pNtkRes;
     int fCompl;
     int fVerbose;
+    int fSeqCleanup;
     int c;
-    extern Abc_Ntk_t * Abc_NtkDarFold( Abc_Ntk_t * pNtk, int fCompl, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkDarFold( Abc_Ntk_t * pNtk, int fCompl, int fVerbose, int fSeqCleanup );
     pNtk = Abc_FrameReadNtk(pAbc);
     // set defaults
     fCompl    =   0;
     fVerbose  =   0;
+    fSeqCleanup = 1;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "cvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "cvsh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -28547,6 +28549,9 @@ int Abc_CommandFold( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'v':
             fVerbose ^= 1;
             break;
+        case 's':
+            fSeqCleanup ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -28576,7 +28581,7 @@ int Abc_CommandFold( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( Abc_NtkIsComb(pNtk) )
         Abc_Print( 0, "The network is combinational.\n" );
     // modify the current network
-    pNtkRes = Abc_NtkDarFold( pNtk, fCompl, fVerbose );
+    pNtkRes = Abc_NtkDarFold( pNtk, fCompl, fVerbose, fSeqCleanup );
     if ( pNtkRes == NULL )
     {
         Abc_Print( 1,"Transformation has failed.\n" );
@@ -28591,6 +28596,7 @@ int Abc_CommandFold( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Print( -2, "\t         (constraints fail when any of them becomes 1 in any timeframe)\n" );
     Abc_Print( -2, "\t-c     : toggle complementing constraints while folding [default = %s]\n", fCompl? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-s     : toggle performing sequential cleanup [default = %s]\n", fSeqCleanup? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
 }

diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
@@ -4682,15 +4682,15 @@ Abc_Ntk_t * Abc_NtkDarUnfold( Abc_Ntk_t * pNtk, int nFrames, int nConfs, int nPr
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkDarFold( Abc_Ntk_t * pNtk, int fCompl, int fVerbose )
+Abc_Ntk_t * Abc_NtkDarFold( Abc_Ntk_t * pNtk, int fCompl, int fVerbose, int fSeqCleanup )
 {
     Abc_Ntk_t * pNtkAig;
     Aig_Man_t * pMan, * pTemp;
     assert( Abc_NtkIsStrash(pNtk) );
     pMan = Abc_NtkToDar( pNtk, 0, 1 );
     if ( pMan == NULL )
         return NULL;
-    pMan = Saig_ManDupFoldConstrsFunc( pTemp = pMan, fCompl, fVerbose );
+    pMan = Saig_ManDupFoldConstrsFunc( pTemp = pMan, fCompl, fVerbose, fSeqCleanup );
     Aig_ManStop( pTemp );
     pNtkAig = Abc_NtkFromAigPhase( pMan );
     pNtkAig->pName = Extra_UtilStrsav(pMan->pName);

diff --git a/src/base/wlc/wlcMem.c b/src/base/wlc/wlcMem.c
@@ -1024,7 +1024,7 @@ int Wlc_NtkMemAbstract( Wlc_Ntk_t * p, int nIterMax, int fDumpAbs, int fPdrVerbo
         pAig = Gia_ManToAigSimple( pAbs );
         Gia_ManStop( pAbs );
         pAig->nConstrs = 1;
-        pAig = Saig_ManDupFoldConstrsFunc( pTempAig = pAig, 0, 0 );
+        pAig = Saig_ManDupFoldConstrsFunc( pTempAig = pAig, 0, 0, 1 );
         Aig_ManStop( pTempAig );
         pAbs = Gia_ManFromAigSimple( pAig );
         Aig_ManStop( pAig );