Integrating sweeping information.

4 files changed, 198 insertions, 29 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 500096e1..62c97051 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -966,6 +966,8 @@ extern int                 Gia_ManSimSimulate( Gia_Man_t * pAig, Gia_ParSim_t *
 extern float               Gia_ManDelayTraceLut( Gia_Man_t * p );
 extern float               Gia_ManDelayTraceLutPrint( Gia_Man_t * p, int fVerbose );
 extern Gia_Man_t *         Gia_ManSpeedup( Gia_Man_t * p, int Percentage, int Degree, int fVerbose, int fVeryVerbose );
+/*=== giaSweep.c ============================================================*/
+extern Gia_Man_t *         Gia_ManFraigSweep( Gia_Man_t * p, void * pPars );
 /*=== giaSwitch.c ============================================================*/
 extern float               Gia_ManEvaluateSwitching( Gia_Man_t * p );
 extern float               Gia_ManComputeSwitching( Gia_Man_t * p, int nFrames, int nPref, int fProbOne );
diff --git a/src/aig/gia/giaSweep.c b/src/aig/gia/giaSweep.c
index 184bf91c..b8caa978 100644
--- a/src/aig/gia/giaSweep.c
+++ b/src/aig/gia/giaSweep.c
@@ -146,6 +146,61 @@ Gia_Man_t * Gia_ManFraigCreateGia( Gia_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Duplicates the AIG in the DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ObjFanin0CopyRepr( Gia_Man_t * p, Gia_Obj_t * pObj, int * pReprs )
+{
+    int faninId = Gia_ObjFaninId0p( p, pObj );
+    if ( pReprs[faninId] == -1 )
+        return Gia_ObjFanin0Copy( pObj );
+    assert( Abc_Lit2Var(pReprs[faninId]) < Gia_ObjId(p, pObj) );
+    return Abc_LitNotCond( Gia_ObjValue(Gia_ManObj(p, Abc_Lit2Var(pReprs[faninId]))), Abc_LitIsCompl(pReprs[faninId]) );
+}
+int Gia_ObjFanin1CopyRepr( Gia_Man_t * p, Gia_Obj_t * pObj, int * pReprs )
+{
+    int faninId = Gia_ObjFaninId1p( p, pObj );
+    if ( pReprs[faninId] == -1 )
+        return Gia_ObjFanin1Copy( pObj );
+    assert( Abc_Lit2Var(pReprs[faninId]) < Gia_ObjId(p, pObj) );
+    return Abc_LitNotCond( Gia_ObjValue(Gia_ManObj(p, Abc_Lit2Var(pReprs[faninId]))), Abc_LitIsCompl(pReprs[faninId]) );
+}
+Gia_Man_t * Gia_ManFraigReduceGia( Gia_Man_t * p, int * pReprs )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    int i;
+    assert( pReprs != NULL );
+    assert( Gia_ManRegNum(p) == 0 );
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManFillValue( p );
+    Gia_ManHashAlloc( pNew );
+    Gia_ManForEachObj( p, pObj, i )
+    {
+        if ( Gia_ObjIsAnd(pObj) )
+            pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0CopyRepr(p, pObj, pReprs), Gia_ObjFanin1CopyRepr(p, pObj, pReprs) );
+        else if ( Gia_ObjIsCi(pObj) )
+            pObj->Value = Gia_ManAppendCi( pNew );
+        else if ( Gia_ObjIsCo(pObj) )
+            pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0CopyRepr(p, pObj, pReprs) );
+        else if ( Gia_ObjIsConst0(pObj) )
+            pObj->Value = 0;
+        else assert( 0 );
+    }
+    Gia_ManHashStop( pNew );
+    return pNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -155,7 +210,7 @@ Gia_Man_t * Gia_ManFraigCreateGia( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Gia_ManFraigExtractGia( Gia_Man_t * p, int * pReprs )
+Gia_Man_t * Gia_ManFraigReduceGia2( Gia_Man_t * p, int * pReprs )
 {
     Gia_Man_t * pNew;
     Gia_Obj_t * pObj;
@@ -300,7 +355,7 @@ Gia_Man_t * Gia_ManFraigSweep( Gia_Man_t * p, void * pPars )
     pReprs = Gia_ManFraigSelectReprs( pNew, pGia, ((Dch_Pars_t *)pPars)->fVerbose );
     Gia_ManStop( pGia );
     // reduce AIG
-    pNew = Gia_ManFraigExtractGia( pTemp = pNew, pReprs );
+    pNew = Gia_ManFraigReduceGia( pTemp = pNew, pReprs );
     Gia_ManStop( pTemp );
     ABC_FREE( pReprs );
     // order reduced AIG
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 0a26bf4a..1e7468d8 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -352,6 +352,7 @@ static int Abc_CommandAbc9Reduce             ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9EquivMark          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Cec                ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Verify             ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Sweep              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Force              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Embed              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9If                 ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -813,6 +814,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&equiv_mark",   Abc_CommandAbc9EquivMark,    0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&cec",          Abc_CommandAbc9Cec,          0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&verify",       Abc_CommandAbc9Verify,       0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&sweep",        Abc_CommandAbc9Sweep,        0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&force",        Abc_CommandAbc9Force,        0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&embed",        Abc_CommandAbc9Embed,        0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&if",           Abc_CommandAbc9If,           0 );
@@ -27326,6 +27328,108 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+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 )
+    {
+        switch ( c )
+        {
+        case 'W':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nWords = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nWords < 0 )
+                goto usage;
+            break;
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nBTLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nBTLimit < 0 )
+                goto usage;
+            break;
+        case 'S':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nSatVarMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            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;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Sweep(): There is no AIG.\n" );
+        return 1;
+    }
+    pTemp = Gia_ManFraigSweep( pAbc->pGia, pPars );
+    Abc_CommandUpdate9( pAbc, pTemp );
+    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, "\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;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandAbc9Force( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     int nIters     = 20;
diff --git a/src/misc/tim/timMan.c b/src/misc/tim/timMan.c
index 4c61bf1c..bfebef05 100644
--- a/src/misc/tim/timMan.c
+++ b/src/misc/tim/timMan.c
@@ -90,16 +90,16 @@ Tim_Man_t * Tim_ManDup( Tim_Man_t * p, int fUnitDelay )
     Tim_Obj_t * pObj;
     float * pDelayTable, * pDelayTableNew;
     int i, k, nInputs, nOutputs;
+    // clear traversal IDs
+    Tim_ManForEachCi( p, pObj, i ) 
+        pObj->TravId = 0;          
+    Tim_ManForEachCo( p, pObj, i ) 
+        pObj->TravId = 0;          
     // create new manager
     pNew = Tim_ManStart( p->nCis, p->nCos );
     // copy box connectivity information
-    memcpy( pNew->pCis, p->pCis, sizeof(Tim_Obj_t) * p->nCis ); // why do we need this?
-    memcpy( pNew->pCos, p->pCos, sizeof(Tim_Obj_t) * p->nCos ); // why do we need this?
-    // clear traversal IDs
-    Tim_ManForEachCi( p, pObj, i ) // why do we need this?
-        pObj->TravId = 0;          // why do we need this?
-    Tim_ManForEachCo( p, pObj, i ) // why do we need this?
-        pObj->TravId = 0;          // why do we need this?
+    memcpy( pNew->pCis, p->pCis, sizeof(Tim_Obj_t) * p->nCis ); 
+    memcpy( pNew->pCos, p->pCos, sizeof(Tim_Obj_t) * p->nCos ); 
     if ( fUnitDelay )
     {
         // discretize PI arrival times
@@ -163,29 +163,31 @@ Tim_Man_t * Tim_ManTrim( Tim_Man_t * p, Vec_Int_t * vBoxPres )
     Tim_Box_t * pBox;
     Tim_Obj_t * pObj;
     float * pDelayTable, * pDelayTableNew;
-    int i, k, nInputs, nOutputs, nRemCis, nRemCos;
+    int i, k, nNewCis, nNewCos, nInputs, nOutputs;
     assert( Vec_IntSize(vBoxPres) == Tim_ManBoxNum(p) );
-    // count the number of CIs and COs due to removed boxes
+    // count the number of CIs and COs in the trimmed manager
+    nNewCis = Tim_ManPiNum(p);
+    nNewCos = Tim_ManPoNum(p);
     Tim_ManForEachBox( p, pBox, i )
-        if ( Vec_IntEntry(vBoxPres, i) == 0 )
+        if ( Vec_IntEntry(vBoxPres, i) )
         {
-            nRemCis += pBox->nOutputs;
-            nRemCos += pBox->nInputs;
+            nNewCis += pBox->nOutputs;
+            nNewCos += pBox->nInputs;
         }
-    if ( nRemCos == 0 && nRemCis == 0 )
+    if ( nNewCis == Tim_ManCiNum(p) && nNewCos == Tim_ManCoNum(p) )
         return Tim_ManDup( p, 0 );
-    assert( Tim_ManCiNum(p) - Tim_ManPiNum(p) >= nRemCis );
-    assert( Tim_ManCoNum(p) - Tim_ManPoNum(p) >= nRemCos );
+    assert( nNewCis < Tim_ManCiNum(p) );
+    assert( nNewCos < Tim_ManCoNum(p) );
+    // clear traversal IDs
+    Tim_ManForEachCi( p, pObj, i ) 
+        pObj->TravId = 0;          
+    Tim_ManForEachCo( p, pObj, i ) 
+        pObj->TravId = 0;          
     // create new manager
-    pNew = Tim_ManStart( p->nCis - nRemCis, p->nCos - nRemCos );
+    pNew = Tim_ManStart( p->nCis - nNewCis, p->nCos - nNewCos );
     // copy box connectivity information
-    memcpy( pNew->pCis, p->pCis, sizeof(Tim_Obj_t) * p->nCis ); // why do we need this?
-    memcpy( pNew->pCos, p->pCos, sizeof(Tim_Obj_t) * p->nCos ); // why do we need this?
-    // clear traversal IDs
-    Tim_ManForEachCi( p, pObj, i ) // why do we need this?
-        pObj->TravId = 0;          // why do we need this?
-    Tim_ManForEachCo( p, pObj, i ) // why do we need this?
-        pObj->TravId = 0;          // why do we need this?
+    memcpy( pNew->pCis, p->pCis, sizeof(Tim_Obj_t) * Tim_ManPiNum(p) );
+    memcpy( pNew->pCos, p->pCos, sizeof(Tim_Obj_t) * Tim_ManPoNum(p) );
     // duplicate delay tables
     if ( Tim_ManDelayTableNum(p) > 0 )
     {
@@ -206,20 +208,26 @@ Tim_Man_t * Tim_ManTrim( Tim_Man_t * p, Vec_Int_t * vBoxPres )
 //            assert( (int)pDelayTableNew[0] == Vec_PtrSize(pNew->vDelayTables) );
             assert( Vec_PtrEntry(pNew->vDelayTables, i) == NULL );
             Vec_PtrWriteEntry( pNew->vDelayTables, i, pDelayTableNew );
-//printf( "Finished duplicating delay table %d.\n", i );
         }
     }
     // duplicate boxes
     if ( Tim_ManBoxNum(p) > 0 )
     {
+        int curPi = Tim_ManPiNum(p);
+        int curPo = 0;
         pNew->vBoxes = Vec_PtrAlloc( Tim_ManBoxNum(p) );
         Tim_ManForEachBox( p, pBox, i )
             if ( Vec_IntEntry(vBoxPres, i) )
-                Tim_ManCreateBox( pNew, pBox->Inouts[0], pBox->nInputs, 
-                    pBox->Inouts[pBox->nInputs], pBox->nOutputs, pBox->iDelayTable );
+            {
+                Tim_ManCreateBox( pNew, curPo, pBox->nInputs, curPi, pBox->nOutputs, pBox->iDelayTable );
+                curPi += pBox->nOutputs;
+                curPo += pBox->nInputs;
+            }
+        curPo += Tim_ManPoNum(p);
+        assert( curPi == Tim_ManCiNum(pNew) );
+        assert( curPo == Tim_ManCoNum(pNew) );
     }
     return pNew;
-
 }