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

8 files changed, 82 insertions, 78 deletions

diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 4d58992c..e5e5b303 100644
--- a/src/aig/gia/gia.h
+++ b/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);
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index 2e45fe2b..2be08453 100644
--- a/src/aig/gia/giaDup.c
+++ b/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) );
 } 
diff --git a/src/aig/gia/giaHash.c b/src/aig/gia/giaHash.c
index c6067312..d9873d76 100644
--- a/src/aig/gia/giaHash.c
+++ b/src/aig/gia/giaHash.c
@@ -53,15 +53,17 @@ static inline int Gia_ManHashOne( int iLit0, int iLit1, int iLitC, int TableSize
 }
 static inline int * Gia_ManHashFind( Gia_Man_t * p, int iLit0, int iLit1, int iLitC )
 {
-    Gia_Obj_t * pThis;
-    int * pPlace = p->pHTable + Gia_ManHashOne( iLit0, iLit1, iLitC, p->nHTable );
+    int iThis, * pPlace = Vec_IntEntryP( &p->vHTable, Gia_ManHashOne( iLit0, iLit1, iLitC, Vec_IntSize(&p->vHTable) ) );
+    assert( Vec_IntSize(&p->vHash) == Gia_ManObjNum(p) );
     assert( p->pMuxes || iLit0 < iLit1 );
     assert( iLit0 < iLit1 || (!Abc_LitIsCompl(iLit0) && !Abc_LitIsCompl(iLit1)) );
     assert( iLitC == -1 || !Abc_LitIsCompl(iLit1) );
-    for ( pThis = (*pPlace)? Gia_ManObj(p, Abc_Lit2Var(*pPlace)) : NULL; pThis; 
-          pPlace = (int *)&pThis->Value, pThis = (*pPlace)? Gia_ManObj(p, Abc_Lit2Var(*pPlace)) : NULL )
-              if ( Gia_ObjFaninLit0p(p, pThis) == iLit0 && Gia_ObjFaninLit1p(p, pThis) == iLit1 && (p->pMuxes == NULL || Gia_ObjFaninLit2p(p, pThis) == iLitC) )
-                  break;
+    for ( ; (iThis = *pPlace); pPlace = Vec_IntEntryP(&p->vHash, iThis) )
+    {
+        Gia_Obj_t * pThis = Gia_ManObj( p, iThis );
+        if ( Gia_ObjFaninLit0(pThis, iThis) == iLit0 && Gia_ObjFaninLit1(pThis, iThis) == iLit1 && (p->pMuxes == NULL || Gia_ObjFaninLit2p(p, pThis) == iLitC) )
+            break;
+    }
     return pPlace;
 }
 
@@ -80,7 +82,7 @@ int Gia_ManHashLookupInt( Gia_Man_t * p, int iLit0, int iLit1 )
 {
     if ( iLit0 > iLit1 )
         iLit0 ^= iLit1, iLit1 ^= iLit0, iLit0 ^= iLit1;
-    return *Gia_ManHashFind( p, iLit0, iLit1, -1 );
+    return Abc_Var2Lit( *Gia_ManHashFind( p, iLit0, iLit1, -1 ), 0 );
 }
 int Gia_ManHashLookup( Gia_Man_t * p, Gia_Obj_t * p0, Gia_Obj_t * p1 )
 {
@@ -102,9 +104,11 @@ int Gia_ManHashLookup( Gia_Man_t * p, Gia_Obj_t * p0, Gia_Obj_t * p1 )
 ***********************************************************************/
 void Gia_ManHashAlloc( Gia_Man_t * p )  
 {
-    assert( p->pHTable == NULL );
-    p->nHTable = Abc_PrimeCudd( Gia_ManAndNum(p) ? Gia_ManAndNum(p) + 1000 : p->nObjsAlloc );
-    p->pHTable = ABC_CALLOC( int, p->nHTable );
+    assert( Vec_IntSize(&p->vHTable) == 0 );
+    Vec_IntFill( &p->vHTable, Abc_PrimeCudd( Gia_ManAndNum(p) ? Gia_ManAndNum(p) + 1000 : p->nObjsAlloc ), 0 );
+    Vec_IntGrow( &p->vHash, Abc_MaxInt(Vec_IntSize(&p->vHTable), Gia_ManObjNum(p)) );
+    Vec_IntFill( &p->vHash, Gia_ManObjNum(p), 0 );
+//printf( "Alloced table with %d entries.\n", Vec_IntSize(&p->vHTable) );
 }
 
 /**Function*************************************************************
@@ -123,12 +127,11 @@ void Gia_ManHashStart( Gia_Man_t * p )
     Gia_Obj_t * pObj;
     int * pPlace, i;
     Gia_ManHashAlloc( p );
-    Gia_ManCleanValue( p );
     Gia_ManForEachAnd( p, pObj, i )
     {
         pPlace = Gia_ManHashFind( p, Gia_ObjFaninLit0(pObj, i), Gia_ObjFaninLit1(pObj, i), Gia_ObjFaninLit2(p, i) );
         assert( *pPlace == 0 );
-        *pPlace = Abc_Var2Lit( i, 0 );
+        *pPlace = i;
     }
 }
 
@@ -145,8 +148,8 @@ void Gia_ManHashStart( Gia_Man_t * p )
 ***********************************************************************/
 void Gia_ManHashStop( Gia_Man_t * p )  
 {
-    ABC_FREE( p->pHTable );
-    p->nHTable = 0;
+    Vec_IntErase( &p->vHTable );
+    Vec_IntErase( &p->vHash );
 }
 
 /**Function*************************************************************
@@ -162,35 +165,32 @@ void Gia_ManHashStop( Gia_Man_t * p )
 ***********************************************************************/
 void Gia_ManHashResize( Gia_Man_t * p )
 {
-    Gia_Obj_t * pThis;
-    int * pHTableOld, * pPlace;
-    int nHTableOld, iNext, Counter, Counter2, i;
-    assert( p->pHTable != NULL );
+    int i, iThis, iNext, Counter, Counter2, * pPlace;
+    Vec_Int_t vOld = p->vHTable;
+    assert( Vec_IntSize(&vOld) > 0 );
     // replace the table
-    pHTableOld = p->pHTable;
-    nHTableOld = p->nHTable;
-    p->nHTable = Abc_PrimeCudd( 2 * Gia_ManAndNum(p) ); 
-    p->pHTable = ABC_CALLOC( int, p->nHTable );
+    Vec_IntZero( &p->vHTable );
+    Vec_IntFill( &p->vHTable, Abc_PrimeCudd( 2 * Gia_ManAndNum(p) ), 0 ); 
     // rehash the entries from the old table
     Counter = 0;
-    for ( i = 0; i < nHTableOld; i++ )
-    for ( pThis = (pHTableOld[i]? Gia_ManObj(p, Abc_Lit2Var(pHTableOld[i])) : NULL),
-          iNext = (pThis? pThis->Value : 0);  
-          pThis;  pThis = (iNext? Gia_ManObj(p, Abc_Lit2Var(iNext)) : NULL),   
-          iNext = (pThis? pThis->Value : 0)  )
-    {
-        pThis->Value = 0;
-        pPlace = Gia_ManHashFind( p, Gia_ObjFaninLit0p(p, pThis), Gia_ObjFaninLit1p(p, pThis), Gia_ObjFaninLit2p(p, pThis) );
-        assert( *pPlace == 0 ); // should not be there
-        *pPlace = Abc_Var2Lit( Gia_ObjId(p, pThis), 0 );
-        assert( *pPlace != 0 );
-        Counter++;
-    }
+    Vec_IntForEachEntry( &vOld, iThis, i )
+        for ( iNext = Vec_IntEntry(&p->vHash, iThis);  
+              iThis;  iThis = iNext,   
+              iNext = Vec_IntEntry(&p->vHash, iThis)  )
+        {
+            Gia_Obj_t * pThis0 = Gia_ManObj( p, iThis );
+            Vec_IntWriteEntry( &p->vHash, iThis, 0 );
+            pPlace = Gia_ManHashFind( p, Gia_ObjFaninLit0(pThis0, iThis), Gia_ObjFaninLit1(pThis0, iThis), Gia_ObjFaninLit2p(p, pThis0) );
+            assert( *pPlace == 0 ); // should not be there
+            *pPlace = iThis;
+            assert( *pPlace != 0 );
+            Counter++;
+        }
     Counter2 = Gia_ManAndNum(p) - Gia_ManBufNum(p);
     assert( Counter == Counter2 );
-    ABC_FREE( pHTableOld );
 //    if ( p->fVerbose )
-//        printf( "Resizing GIA hash table: %d -> %d.\n", nHTableOld, p->nHTable );
+//        printf( "Resizing GIA hash table: %d -> %d.\n", Vec_IntSize(&vOld), Vec_IntSize(&p->vHTable) );
+    Vec_IntErase( &vOld );
 }
 
 /**Function********************************************************************
@@ -206,17 +206,17 @@ void Gia_ManHashResize( Gia_Man_t * p )
 ******************************************************************************/
 void Gia_ManHashProfile( Gia_Man_t * p )
 {
-    Gia_Obj_t * pEntry;
+    int iEntry;
     int i, Counter, Limit;
-    printf( "Table size = %d. Entries = %d. ", p->nHTable, Gia_ManAndNum(p) );
+    printf( "Table size = %d. Entries = %d. ", Vec_IntSize(&p->vHTable), Gia_ManAndNum(p) );
     printf( "Hits = %d. Misses = %d.\n", (int)p->nHashHit, (int)p->nHashMiss );
-    Limit = Abc_MinInt( 1000, p->nHTable );
+    Limit = Abc_MinInt( 1000, Vec_IntSize(&p->vHTable) );
     for ( i = 0; i < Limit; i++ )
     {
         Counter = 0;
-        for ( pEntry = (p->pHTable[i]? Gia_ManObj(p, Abc_Lit2Var(p->pHTable[i])) : NULL); 
-              pEntry; 
-              pEntry = (pEntry->Value? Gia_ManObj(p, Abc_Lit2Var(pEntry->Value)) : NULL) )
+        for ( iEntry = Vec_IntEntry(&p->vHTable, i); 
+              iEntry; 
+              iEntry = iEntry? Vec_IntEntry(&p->vHash, iEntry) : 0 )
             Counter++;
         if ( Counter ) 
             printf( "%d ", Counter );
@@ -478,7 +478,7 @@ int Gia_ManHashXorReal( Gia_Man_t * p, int iLit0, int iLit1 )
         return 0;
     if ( iLit0 == Abc_LitNot(iLit1) )
         return 1;
-    if ( (p->nObjs & 0xFF) == 0 && 2 * p->nHTable < Gia_ManAndNum(p) )
+    if ( (p->nObjs & 0xFF) == 0 && 2 * Vec_IntSize(&p->vHTable) < Gia_ManAndNum(p) )
         Gia_ManHashResize( p );
     if ( iLit0 < iLit1 )
         iLit0 ^= iLit1, iLit1 ^= iLit0, iLit0 ^= iLit1;
@@ -491,19 +491,19 @@ int Gia_ManHashXorReal( Gia_Man_t * p, int iLit0, int iLit1 )
         if ( *pPlace )
         {
             p->nHashHit++;
-            return Abc_LitNotCond( *pPlace, fCompl );
+            return Abc_Var2Lit( *pPlace, fCompl );
         }
         p->nHashMiss++;
-        if ( p->nObjs < p->nObjsAlloc )
-            *pPlace = Gia_ManAppendXorReal( p, iLit0, iLit1 );
+        if ( Vec_IntSize(&p->vHash) < Vec_IntCap(&p->vHash) )
+            *pPlace = Abc_Lit2Var( Gia_ManAppendXorReal( p, iLit0, iLit1 ) );
         else
         {
             int iNode = Gia_ManAppendXorReal( p, iLit0, iLit1 );
             pPlace = Gia_ManHashFind( p, iLit0, iLit1, -1 );
             assert( *pPlace == 0 );
-            *pPlace = iNode;
+            *pPlace = Abc_Lit2Var( iNode );
         }
-        return Abc_LitNotCond( *pPlace, fCompl );
+        return Abc_Var2Lit( *pPlace, fCompl );
     }
 }
 
@@ -546,19 +546,19 @@ int Gia_ManHashMuxReal( Gia_Man_t * p, int iLitC, int iLit1, int iLit0 )
         if ( *pPlace )
         {
             p->nHashHit++;
-            return Abc_LitNotCond( *pPlace, fCompl );
+            return Abc_Var2Lit( *pPlace, fCompl );
         }
         p->nHashMiss++;
-        if ( p->nObjs < p->nObjsAlloc )
-            *pPlace = Gia_ManAppendMuxReal( p, iLitC, iLit1, iLit0 );
+        if ( Vec_IntSize(&p->vHash) < Vec_IntCap(&p->vHash) )
+            *pPlace = Abc_Lit2Var( Gia_ManAppendMuxReal( p, iLitC, iLit1, iLit0 ) );
         else
         {
             int iNode = Gia_ManAppendMuxReal( p, iLitC, iLit1, iLit0 );
             pPlace = Gia_ManHashFind( p, iLit0, iLit1, iLitC );
             assert( *pPlace == 0 );
-            *pPlace = iNode;
+            *pPlace = Abc_Lit2Var( iNode );
         }
-        return Abc_LitNotCond( *pPlace, fCompl );
+        return Abc_Var2Lit( *pPlace, fCompl );
     }
 }
 
@@ -585,10 +585,10 @@ int Gia_ManHashAnd( Gia_Man_t * p, int iLit0, int iLit1 )
         return 0;
     if ( p->fGiaSimple )
     {
-        assert( p->nHTable == 0 );
+        assert( Vec_IntSize(&p->vHTable) == 0 );
         return Gia_ManAppendAnd( p, iLit0, iLit1 );
     }
-    if ( (p->nObjs & 0xFF) == 0 && 2 * p->nHTable < Gia_ManAndNum(p) )
+    if ( (p->nObjs & 0xFF) == 0 && 2 * Vec_IntSize(&p->vHTable) < Gia_ManAndNum(p) )
         Gia_ManHashResize( p );
     if ( p->fAddStrash )
     {
@@ -603,18 +603,19 @@ int Gia_ManHashAnd( Gia_Man_t * p, int iLit0, int iLit1 )
         if ( *pPlace )
         {
             p->nHashHit++;
-            return *pPlace;
+            return Abc_Var2Lit( *pPlace, 0 );
         }
         p->nHashMiss++;
-        if ( p->nObjs < p->nObjsAlloc )
-            return *pPlace = Gia_ManAppendAnd( p, iLit0, iLit1 );
+        if ( Vec_IntSize(&p->vHash) < Vec_IntCap(&p->vHash) )
+            *pPlace = Abc_Lit2Var( Gia_ManAppendAnd( p, iLit0, iLit1 ) );
         else
         {
             int iNode = Gia_ManAppendAnd( p, iLit0, iLit1 );
             pPlace = Gia_ManHashFind( p, iLit0, iLit1, -1 );
             assert( *pPlace == 0 );
-            return *pPlace = iNode;
+            *pPlace = Abc_Lit2Var( iNode );
         }
+        return Abc_Var2Lit( *pPlace, 0 );
     }
 }
 int Gia_ManHashOr( Gia_Man_t * p, int iLit0, int iLit1 )  
@@ -648,7 +649,7 @@ int Gia_ManHashAndTry( Gia_Man_t * p, int iLit0, int iLit1 )
     {
         int * pPlace = Gia_ManHashFind( p, iLit0, iLit1, -1 );
         if ( *pPlace ) 
-            return *pPlace;
+            return Abc_Var2Lit( *pPlace, 0 );
         return -1;
     }
 }
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index 5278c5cc..48ae25a0 100644
--- a/src/aig/gia/giaMan.c
+++ b/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 );
diff --git a/src/aig/gia/giaSweeper.c b/src/aig/gia/giaSweeper.c
index b4a53f44..c1ce596d 100644
--- a/src/aig/gia/giaSweeper.c
+++ b/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!!!
 
diff --git a/src/base/abci/abcRec3.c b/src/base/abci/abcRec3.c
index 6d2d58eb..43da4839 100644
--- a/src/base/abci/abcRec3.c
+++ b/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
diff --git a/src/opt/dau/dauGia.c b/src/opt/dau/dauGia.c
index fa757e62..b1df5db0 100644
--- a/src/opt/dau/dauGia.c
+++ b/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++ )
diff --git a/src/proof/ssc/sscCore.c b/src/proof/ssc/sscCore.c
index caad8d48..a6c6f494 100644
--- a/src/proof/ssc/sscCore.c
+++ b/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 );