Changes to make GIA structural hashing use a dedicated array instead of pObj->Value.

src/aig/gia/gia.h

@@ -108,8 +108,8 @@ struct Gia_Man_t_
     int            nBufs;         // the number of buffers
     Vec_Int_t *    vCis;          // the vector of CIs (PIs + LOs)
     Vec_Int_t *    vCos;          // the vector of COs (POs + LIs)
-    int *          pHTable;       // hash table
-    int            nHTable;       // hash table size 
+    Vec_Int_t      vHash;         // hash links
+    Vec_Int_t      vHTable;       // hash table
     int            fAddStrash;    // performs additional structural hashing
     int            fSweeper;      // sweeper is running
     int            fGiaSimple;    // simple mode (no const-propagation and strashing)
@@ -640,6 +640,7 @@ static inline Gia_Obj_t * Gia_ManAppendObj( Gia_Man_t * p )
         }
         p->nObjsAlloc = nObjNew;
     }
+    if ( Vec_IntSize(&p->vHTable) ) Vec_IntPush( &p->vHash, 0 );
     return Gia_ManObj( p, p->nObjs++ );
 }
 static inline int Gia_ManAppendCi( Gia_Man_t * p )  
@@ -731,7 +732,7 @@ static inline int Gia_ManAppendMuxReal( Gia_Man_t * p, int iLitC, int iLit1, int
     assert( Abc_Lit2Var(iLit0) != Abc_Lit2Var(iLit1) );
     assert( Abc_Lit2Var(iLitC) != Abc_Lit2Var(iLit0) );
     assert( Abc_Lit2Var(iLitC) != Abc_Lit2Var(iLit1) );
-    assert( !p->pHTable || !Abc_LitIsCompl(iLit1) );
+    assert( !Vec_IntSize(&p->vHTable) || !Abc_LitIsCompl(iLit1) );
     if ( Abc_Lit2Var(iLit0) < Abc_Lit2Var(iLit1) )
     {
         pObj->iDiff0  = Gia_ObjId(p, pObj) - Abc_Lit2Var(iLit0);

src/aig/gia/giaDup.c

@@ -942,7 +942,7 @@ void Gia_ManDupAppend( Gia_Man_t * pNew, Gia_Man_t * pTwo )
     int i;
     if ( pNew->nRegs > 0 )
         pNew->nRegs = 0;
-    if ( pNew->pHTable == NULL )
+    if ( Vec_IntSize(&pNew->vHTable) == 0 )
         Gia_ManHashStart( pNew );
     Gia_ManConst0(pTwo)->Value = 0;
     Gia_ManForEachObj1( pTwo, pObj, i )
@@ -960,7 +960,7 @@ void Gia_ManDupAppendShare( Gia_Man_t * pNew, Gia_Man_t * pTwo )
     Gia_Obj_t * pObj;
     int i;
     assert( Gia_ManCiNum(pNew) == Gia_ManCiNum(pTwo) );
-    if ( pNew->pHTable == NULL )
+    if ( Vec_IntSize(&pNew->vHTable) == 0 )
         Gia_ManHashStart( pNew );
     Gia_ManConst0(pTwo)->Value = 0;
     Gia_ManForEachObj1( pTwo, pObj, i )
@@ -1425,7 +1425,7 @@ int Gia_ManDupDfs2_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
     if ( Gia_ObjIsCo(pObj) )
         return pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
     Gia_ManDupDfs2_rec( pNew, p, Gia_ObjFanin1(pObj) );
-    if ( pNew->pHTable )
+    if ( Vec_IntSize(&pNew->vHTable) )
         return pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
     return pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
 } 

src/aig/gia/giaMan.c

@@ -140,6 +140,8 @@ void Gia_ManStop( Gia_Man_t * p )
     Gia_ManStopP( &p->pAigExtra );
     Vec_IntFree( p->vCis );
     Vec_IntFree( p->vCos );
+    Vec_IntErase( &p->vHash );
+    Vec_IntErase( &p->vHTable );
     ABC_FREE( p->pData2 );
     ABC_FREE( p->pTravIds );
     ABC_FREE( p->pPlacement );
@@ -155,7 +157,7 @@ void Gia_ManStop( Gia_Man_t * p )
     ABC_FREE( p->pSibls );
     ABC_FREE( p->pRefs );
     ABC_FREE( p->pLutRefs );
-    ABC_FREE( p->pHTable );
+//    ABC_FREE( p->pHTable );
     ABC_FREE( p->pMuxes );
     ABC_FREE( p->pObjs );
     ABC_FREE( p->pSpec );
@@ -180,7 +182,7 @@ double Gia_ManMemory( Gia_Man_t * p )
     Memory += sizeof(Gia_Obj_t) * Gia_ManObjNum(p);
     Memory += sizeof(int) * Gia_ManCiNum(p);
     Memory += sizeof(int) * Gia_ManCoNum(p);
-    Memory += sizeof(int) * p->nHTable * (p->pHTable != NULL);
+    Memory += sizeof(int) * Vec_IntSize(&p->vHTable);
     Memory += sizeof(int) * Gia_ManObjNum(p) * (p->pRefs != NULL);
     Memory += Vec_IntMemory( p->vLevels );
     Memory += Vec_IntMemory( p->vCellMapping );

src/aig/gia/giaSweeper.c

@@ -108,7 +108,7 @@ static inline Swp_Man_t * Swp_ManStart( Gia_Man_t * pGia )
 {
     Swp_Man_t * p;
     int Lit;
-    assert( pGia->pHTable != NULL );
+    assert( Vec_IntSize(&pGia->vHTable) );
     pGia->pData = p = ABC_CALLOC( Swp_Man_t, 1 );
     p->pGia         = pGia;
     p->nConfMax     = 1000;
@@ -146,7 +146,7 @@ Gia_Man_t * Gia_SweeperStart( Gia_Man_t * pGia )
 {
     if ( pGia == NULL )
         pGia = Gia_ManStart( 10000 );
-    if ( pGia->pHTable == NULL )
+    if ( Vec_IntSize(&pGia->vHTable) == 0 )
         Gia_ManHashStart( pGia );
     // recompute fPhase and fMark1 to mark multiple fanout nodes if AIG is already defined!!!
 

src/base/abci/abcRec3.c

@@ -585,7 +585,7 @@ void Abc_NtkRecLibMerge3( Gia_Man_t * pLib )
     assert( Gia_ManCiNum(pLib) == Gia_ManCiNum(pGia) );
 
     // create hash table if not available
-    if ( pGia->pHTable == NULL )
+    if ( Vec_IntSize(&pGia->vHTable) == 0 )
         Gia_ManHashStart( pGia );
 
     // add AIG subgraphs
@@ -841,7 +841,7 @@ void Abc_NtkRecAdd3( Abc_Ntk_t * pNtk, int fUseSOPB )
     // remember that the manager was used for library construction
     s_pMan3->fLibConstr = 1;
     // create hash table if not available
-    if ( s_pMan3->pGia && s_pMan3->pGia->pHTable == NULL )
+    if ( s_pMan3->pGia && Vec_IntSize(&s_pMan3->pGia->vHTable) == 0 )
         Gia_ManHashStart( s_pMan3->pGia );
 
     // set defaults

src/opt/dau/dauGia.c

@@ -238,7 +238,7 @@ int Dau_DsdBalance( Gia_Man_t * pGia, int * pFans, int nFans, int fAnd )
     assert( nFans > 1 );
     iFan0 = pFans[--nFans];
     iFan1 = pFans[--nFans];
-    if ( pGia->pHTable == NULL )
+    if ( Vec_IntSize(&pGia->vHTable) == 0 )
     {
         if ( fAnd )
             iFan = Gia_ManAppendAnd2( pGia, iFan0, iFan1 );
@@ -356,7 +356,7 @@ int Dau_DsdToGia_rec( Gia_Man_t * pGia, char * pStr, char ** p, int * pMatches,
             assert( **p == '{' && *q == '}' );
             *p = q;
         }
-        if ( pGia->pHTable == NULL )
+        if ( Vec_IntSize(&pGia->vHTable) == 0 )
         {
             if ( pGia->pMuxes )
                 Res = Gia_ManAppendMux( pGia, Temp[0], Temp[1], Temp[2] );
@@ -373,7 +373,7 @@ int Dau_DsdToGia_rec( Gia_Man_t * pGia, char * pStr, char ** p, int * pMatches,
         pObj = Gia_ManObj(pGia, Abc_Lit2Var(Res));
         if ( Gia_ObjIsAnd(pObj) )
         {
-            if ( pGia->pMuxes && pGia->pHTable != NULL )
+            if ( pGia->pMuxes && Vec_IntSize(&pGia->vHTable) )
                 Gia_ObjSetMuxLevel( pGia, pObj );
             else 
             {
@@ -403,7 +403,7 @@ int Dau_DsdToGia_rec( Gia_Man_t * pGia, char * pStr, char ** p, int * pMatches,
         vLeaves.nSize = nVars;
         vLeaves.pArray = Fanins;      
         nObjOld = Gia_ManObjNum(pGia);
-        Res = Kit_TruthToGia( pGia, (unsigned *)pFunc, nVars, vCover, &vLeaves, pGia->pHTable != NULL );
+        Res = Kit_TruthToGia( pGia, (unsigned *)pFunc, nVars, vCover, &vLeaves, Vec_IntSize(&pGia->vHTable) != 0 );
 //        assert( nVars <= 6 );
 //        Res = Dau_DsdToGiaCompose_rec( pGia, pFunc[0], Fanins, nVars );
         for ( i = nObjOld; i < Gia_ManObjNum(pGia); i++ )

src/proof/ssc/sscCore.c

@@ -85,7 +85,7 @@ Ssc_Man_t * Ssc_ManStart( Gia_Man_t * pAig, Gia_Man_t * pCare, Ssc_Pars_t * pPar
     p->pAig   = pAig;
     p->pCare  = pCare;
     p->pFraig = Gia_ManDupDfs( p->pCare );
-    assert( p->pFraig->pHTable == NULL );
+    assert( Vec_IntSize(&p->pFraig->vHTable) == 0 );
     assert( !Gia_ManHasDangling(p->pFraig) );
     Gia_ManInvertPos( p->pFraig );
     Ssc_ManStartSolver( p );