Version abc70818

2 files changed, 23 insertions, 12 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 1b5e2361..cd78f218 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -10974,11 +10974,11 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     int nFramesK;
     int fExdc;
-    int fImp;
+    int fUseImps;
     int fRewrite;
     int fLatchCorr;
     int fVerbose;
-    extern Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFrames, int fRewrite, int fLatchCorr, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFrames, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -10987,7 +10987,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     nFramesK   = 1;
     fExdc      = 1;
-    fImp       = 0;
+    fUseImps   = 0;
     fRewrite   = 0;
     fLatchCorr = 0;
     fVerbose   = 0;
@@ -11011,7 +11011,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
             fExdc ^= 1;
             break;
         case 'i':
-            fImp ^= 1;
+            fUseImps ^= 1;
             break;
         case 'r':
             fRewrite ^= 1;
@@ -11048,7 +11048,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the new network
-    pNtkRes = Abc_NtkSeqSweep( pNtk, nFramesK, fRewrite, fLatchCorr, fVerbose );
+    pNtkRes = Abc_NtkSeqSweep( pNtk, nFramesK, fRewrite, fUseImps, fLatchCorr, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Sequential sweeping has failed.\n" );
@@ -11059,11 +11059,11 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: ssweep [-F num] [-lrvh]\n" );
+    fprintf( pErr, "usage: ssweep [-F num] [-ilrvh]\n" );
     fprintf( pErr, "\t         performs sequential sweep using K-step induction\n" );
     fprintf( pErr, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", nFramesK );
 //    fprintf( pErr, "\t-e     : toggle writing EXDC network [default = %s]\n", fExdc? "yes": "no" );
-//    fprintf( pErr, "\t-i     : toggle computing implications [default = %s]\n", fImp? "yes": "no" );
+    fprintf( pErr, "\t-i     : toggle using implications [default = %s]\n", fUseImps? "yes": "no" );
     fprintf( pErr, "\t-l     : toggle latch correspondence only [default = %s]\n", fLatchCorr? "yes": "no" );
     fprintf( pErr, "\t-r     : toggle AIG rewriting [default = %s]\n", fRewrite? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 4013b98d..de527306 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -892,16 +892,26 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVer
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFramesK, int fRewrite, int fLatchCorr, int fVerbose )
+Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFramesK, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose )
 {
-    Abc_Ntk_t * pNtkAig;
+    Fraig_Params_t Params;
+    Abc_Ntk_t * pNtkAig, * pNtkFraig;
     Aig_Man_t * pMan, * pTemp;
-    pMan = Abc_NtkToDar( pNtk, 1 );
+
+    // preprocess the miter by fraiging it
+    // (note that for each functional class, fraiging leaves one representative;
+    // so fraiging does not reduce the number of functions represented by nodes
+    Fraig_ParamsSetDefault( &Params );
+    Params.nBTLimit = 100000;
+    pNtkFraig = Abc_NtkFraig( pNtk, &Params, 0, 0 );
+//    pNtkFraig = Abc_NtkDup( pNtk );
+
+    pMan = Abc_NtkToDar( pNtkFraig, 1 );
+    Abc_NtkDelete( pNtkFraig );
     if ( pMan == NULL )
         return NULL;
-//    pMan->nRegs = Abc_NtkLatchNum(pNtk);
 
-    pMan = Fra_FraigInduction( pTemp = pMan, nFramesK, fRewrite, fLatchCorr, fVerbose, NULL );
+    pMan = Fra_FraigInduction( pTemp = pMan, nFramesK, fRewrite, fUseImps, fLatchCorr, fVerbose, NULL );
     Aig_ManStop( pTemp );
 
     if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
@@ -960,6 +970,7 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fVerbo
     // (note that for each functional class, fraiging leaves one representative;
     // so fraiging does not reduce the number of functions represented by nodes
     Fraig_ParamsSetDefault( &Params );
+    Params.nBTLimit = 100000;
     pMiter = Abc_NtkFraig( pTemp = pMiter, &Params, 0, 0 );
     Abc_NtkDelete( pTemp );