Adding AIG rehashing after LUT mapping in Gia.

4 files changed, 69 insertions, 6 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 6a1dc99e..a3fe1dc5 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -1305,6 +1305,7 @@ extern void                Gia_ManTransferTiming( Gia_Man_t * p, Gia_Man_t * pGi
 extern Gia_Man_t *         Gia_ManPerformMapping( Gia_Man_t * p, void * pIfPars );
 extern Gia_Man_t *         Gia_ManPerformSopBalance( Gia_Man_t * p, int nCutNum, int nRelaxRatio, int fVerbose );
 extern Gia_Man_t *         Gia_ManPerformDsdBalance( Gia_Man_t * p, int nLutSize, int nCutNum, int nRelaxRatio, int fVerbose );
+extern Gia_Man_t *         Gia_ManDupHashMapping( Gia_Man_t * p );
 /*=== giaJf.c ===========================================================*/
 extern void                Jf_ManSetDefaultPars( Jf_Par_t * pPars );
 extern Gia_Man_t *         Jf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars );
diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c
index f5071929..e6e326e3 100644
--- a/src/aig/gia/giaIf.c
+++ b/src/aig/gia/giaIf.c
@@ -2183,9 +2183,15 @@ Gia_Man_t * Gia_ManPerformMapping( Gia_Man_t * p, void * pp )
     }
     else 
     {
-        // mapping
+        int fHashMapping = 1;
         pNew = Gia_ManPerformMappingInt( p, (If_Par_t *)pp );
         Gia_ManTransferTiming( pNew, p );
+        if ( fHashMapping )
+        {
+            pNew = Gia_ManDupHashMapping( p = pNew );
+            Gia_ManTransferTiming( pNew, p );
+            Gia_ManStop( p );
+        }
     }
     pNew->MappedDelay = (int)((If_Par_t *)pp)->FinalDelay;
     pNew->MappedArea  = (int)((If_Par_t *)pp)->FinalArea;
@@ -2313,6 +2319,55 @@ void Gia_ManTestStruct( Gia_Man_t * p )
     printf( "\n" );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Performs hashing for a mapped AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     [] 
+
+***********************************************************************/
+Gia_Man_t * Gia_ManDupHashMapping( Gia_Man_t * p )
+{
+    Gia_Man_t * pNew; 
+    Vec_Int_t * vMapping; 
+    Gia_Obj_t * pObj, * pFanin;
+    int i, k;
+    assert( Gia_ManHasMapping(p) );
+    // copy the old manager with hashing
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManHashAlloc( pNew );
+    Gia_ManFillValue( p );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachCi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi( pNew );
+    Gia_ManForEachAnd( p, pObj, i )
+        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    Gia_ManForEachCo( p, pObj, i )
+        Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Gia_ManHashStop( pNew );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    // recreate mapping
+    vMapping = Vec_IntAlloc( Vec_IntSize(p->vMapping) );
+    Vec_IntFill( vMapping, Gia_ManObjNum(p), 0 );
+    Gia_ManForEachLut( p, i )
+    {
+        pObj = Gia_ManObj( p, i );
+        Vec_IntWriteEntry( vMapping, Abc_Lit2Var(pObj->Value), Vec_IntSize(vMapping) );
+        Vec_IntPush( vMapping, Gia_ObjLutSize(p, i) );
+        Gia_LutForEachFaninObj( p, i, pFanin, k )
+            Vec_IntPush( vMapping, Abc_Lit2Var(pFanin->Value)  );
+        Vec_IntPush( vMapping, Abc_Lit2Var(pObj->Value) );
+    }
+    pNew->vMapping = vMapping;
+    return pNew;
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/aig/gia/giaSatLut.c b/src/aig/gia/giaSatLut.c
index 55a9e303..d8921bca 100644
--- a/src/aig/gia/giaSatLut.c
+++ b/src/aig/gia/giaSatLut.c
@@ -46,6 +46,7 @@ struct Sbl_Man_t_
     int            nRuns;        // the number of runs
     int            nSmallWins;   // the number of small windows
     int            nLargeWins;   // the number of large windows
+    int            nIterOuts;    // the number of iters exceeded
     // parameters
     int            nBTLimit;     // conflicts
     int            DelayMax;     // external delay
@@ -1109,9 +1110,10 @@ int Sbl_ManTestSat( Sbl_Man_t * p, int iPivot )
                 printf( "LitCount = %d.\n", LitCount );
             printf( "\n" );
         }
-        if ( nIters == 20 )
+        if ( nIters == 10 )
         {
-            printf( "Obj %d : Quitting after %d iterations.\n", iPivot, nIters );
+            p->nIterOuts++;
+            //printf( "Obj %d : Quitting after %d iterations.\n", iPivot, nIters );
             break;
         }
     }
@@ -1183,8 +1185,8 @@ void Gia_ManLutSat( Gia_Man_t * pGia, int nNumber, int nImproves, int nBTLimit,
     }
     Gia_ManComputeOneWin( pGia, -1, NULL, NULL, NULL, NULL );
     if ( p->fVerbose )
-    printf( "Tried = %d. Improved = %d.  Small win = %d. Large win = %d.  Total SAT runs = %d.\n", 
-        p->nTried, p->nImproved, p->nSmallWins, p->nLargeWins, p->nRuns );
+    printf( "Tried = %d. Improved = %d. SmallWin = %d. LargeWin = %d. IterOut = %d.  SAT runs = %d.\n", 
+        p->nTried, p->nImproved, p->nSmallWins, p->nLargeWins, p->nIterOuts, p->nRuns );
     if ( p->fVerbose )
     Sbl_ManPrintRuntime( p );
     Sbl_ManStop( p );
diff --git a/src/aig/gia/giaTim.c b/src/aig/gia/giaTim.c
index 98f0ee44..c065ab5a 100644
--- a/src/aig/gia/giaTim.c
+++ b/src/aig/gia/giaTim.c
@@ -137,6 +137,7 @@ int Gia_ManIsNormalized( Gia_Man_t * p )
 ***********************************************************************/
 Gia_Man_t * Gia_ManDupNormalize( Gia_Man_t * p )
 {
+    int fHash = 1;
     Gia_Man_t * pNew;
     Gia_Obj_t * pObj;
     int i;
@@ -170,11 +171,15 @@ Gia_Man_t * Gia_ManDupNormalize( Gia_Man_t * p )
             Gia_ManCi(p, i)->Value = Gia_ManAppendCi(pNew);
         printf( "Warning: Shuffled CI order to be correct sequential AIG.\n" );
     }
+    if ( fHash ) Gia_ManHashAlloc( pNew );
     Gia_ManForEachAnd( p, pObj, i )
         if ( Gia_ObjIsBuf(pObj) )
             pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) );
-        else 
+        else if ( fHash )
+            pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+        else
             pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    if ( fHash ) Gia_ManHashStop( pNew );
     Gia_ManForEachCo( p, pObj, i )
         pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
     Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );