Improvements to handling boxes and flops.

3 files changed, 13 insertions, 33 deletions

diff --git a/src/aig/gia/giaSweep.c b/src/aig/gia/giaSweep.c
index 8c5405e4..76176d80 100644
--- a/src/aig/gia/giaSweep.c
+++ b/src/aig/gia/giaSweep.c
@@ -129,9 +129,7 @@ Gia_Man_t * Gia_ManDupWithBoxes( Gia_Man_t * p, int fSeq )
     Vec_Int_t * vBoxesLeft;
     int curCi, curCo, nBoxIns, nBoxOuts;
     int i, k, iShift, nMarked;
-    int CiLeft = 0, CoLeft = 0;
     assert( Gia_ManBoxNum(p) > 0 );
-    assert( Gia_ManRegBoxNum(p) > 0 );
     // mark useful boxes
     Gia_ManMarkSeqGiaWithBoxes( p, fSeq );
     // duplicate marked entries
@@ -181,29 +179,18 @@ Gia_Man_t * Gia_ManDupWithBoxes( Gia_Man_t * p, int fSeq )
         // check presence
         assert( nMarked == 0 || nMarked == nBoxIns + nBoxOuts );
         if ( nMarked )
-        {
             Vec_IntPush( vBoxesLeft, i );
-
-            CoLeft += nBoxIns;
-            CiLeft += nBoxOuts;
-        }
     }
     curCo += Tim_ManPoNum(pManTime);
     assert( curCi == Gia_ManCiNum(p) );
     assert( curCo == Gia_ManCoNum(p) );
     // update timing manager
-    pNew->pManTime = Gia_ManUpdateTimMan2( p, vBoxesLeft, Vec_IntSize(p->vRegClasses) - Vec_IntSize(pNew->vRegClasses) );
+    pNew->pManTime = Gia_ManUpdateTimMan2( p, vBoxesLeft, Gia_ManRegBoxNum(p) - Gia_ManRegBoxNum(pNew) );
     // update extra STG
     assert( p->pAigExtra != NULL );
     assert( pNew->pAigExtra == NULL );
     pNew->pAigExtra = Gia_ManUpdateExtraAig2( p->pManTime, p->pAigExtra, vBoxesLeft );
-    {
-        int a = Gia_ManCiNum(pNew);
-        int b = Tim_ManPiNum(pNew->pManTime);
-        int c = Gia_ManCoNum(pNew->pAigExtra);
-        int d = b + c;
     assert( Gia_ManCiNum(pNew) == Tim_ManPiNum(pNew->pManTime) + Gia_ManCoNum(pNew->pAigExtra) );
-    }
     Vec_IntFree( vBoxesLeft );
     return pNew;
 }
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 1e914309..2595c625 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -30849,10 +30849,9 @@ int Abc_CommandAbc9Sweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     Gia_Man_t * pTemp;
     Dch_Pars_t Pars, * pPars = &Pars;
     int c;
-    // set defaults
     Dch_ManSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptfvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "WCStvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -30889,18 +30888,9 @@ int Abc_CommandAbc9Sweep( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nSatVarMax < 0 )
                 goto usage;
             break;
-        case 's':
-            pPars->fSynthesis ^= 1;
-            break;
-        case 'p':
-            pPars->fPower ^= 1;
-            break;
         case 't':
             pPars->fSimulateTfo ^= 1;
             break;
-        case 'f':
-            pPars->fLightSynth ^= 1;
-            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -30928,15 +30918,12 @@ int Abc_CommandAbc9Sweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &sweep [-WCS num] [-sptfvh]\n" );
-    Abc_Print( -2, "\t         computes structural choices using a new approach\n" );
+    Abc_Print( -2, "usage: &sweep [-WCS num] [-tvh]\n" );
+    Abc_Print( -2, "\t         performs SAT sweeping for AIG with boxes\n" );
     Abc_Print( -2, "\t-W num : the max number of simulation words [default = %d]\n", pPars->nWords );
     Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
     Abc_Print( -2, "\t-S num : the max number of SAT variables [default = %d]\n", pPars->nSatVarMax );
-    Abc_Print( -2, "\t-s     : toggle synthesizing three snapshots [default = %s]\n", pPars->fSynthesis? "yes": "no" );
-    Abc_Print( -2, "\t-p     : toggle power-aware rewriting [default = %s]\n", pPars->fPower? "yes": "no" );
     Abc_Print( -2, "\t-t     : toggle simulation of the TFO classes [default = %s]\n", pPars->fSimulateTfo? "yes": "no" );
-    Abc_Print( -2, "\t-f     : toggle using lighter logic synthesis [default = %s]\n", pPars->fLightSynth? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
diff --git a/src/misc/tim/timMan.c b/src/misc/tim/timMan.c
index 27dd8bdb..43b2c6e7 100644
--- a/src/misc/tim/timMan.c
+++ b/src/misc/tim/timMan.c
@@ -284,16 +284,22 @@ Tim_Man_t * Tim_ManReduce( Tim_Man_t * p, Vec_Int_t * vBoxesLeft, int nTermsDiff
     // duplicate delay tables
     if ( Tim_ManDelayTableNum(p) > 0 )
     {
+        int fWarning = 0;
         pNew->vDelayTables = Vec_PtrStart( Vec_PtrSize(p->vDelayTables) );
         Tim_ManForEachTable( p, pDelayTable, i )
         {
             if ( pDelayTable == NULL )
                 continue;
-            assert( i == (int)pDelayTable[0] );
+            if ( i != (int)pDelayTable[0] && fWarning == 0 )
+            {
+                printf( "Warning: Mismatch in delay-table number between the manager and the box.\n" );
+                fWarning = 1;
+            }
+            //assert( i == (int)pDelayTable[0] );
             nInputs   = (int)pDelayTable[1];
             nOutputs  = (int)pDelayTable[2];
             pDelayTableNew = ABC_ALLOC( float, 3 + nInputs * nOutputs );
-            pDelayTableNew[0] = (int)pDelayTable[0];
+            pDelayTableNew[0] = i;//(int)pDelayTable[0];
             pDelayTableNew[1] = (int)pDelayTable[1];
             pDelayTableNew[2] = (int)pDelayTable[2];
             for ( k = 0; k < nInputs * nOutputs; k++ )
@@ -407,7 +413,7 @@ void Tim_ManCreate( Tim_Man_t * p, void * pLib, Vec_Flt_t * vInArrs, Vec_Flt_t *
     if ( p->vBoxes )
     Tim_ManForEachBox( p, pBox, i )
     {
-        if ( pBox->iDelayTable == -1 )
+        if ( pBox->iDelayTable == -1 || pLibBox == NULL )
         {
             // create table with constants
             pTable = ABC_ALLOC( float, 3 + pBox->nInputs * pBox->nOutputs );