summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/aig/gia/gia.h7
-rw-r--r--src/aig/gia/giaDup.c6
-rw-r--r--src/aig/gia/giaHash.c123
-rw-r--r--src/aig/gia/giaMan.c6
-rw-r--r--src/aig/gia/giaSweeper.c4
-rw-r--r--src/base/abci/abcRec3.c4
-rw-r--r--src/opt/dau/dauGia.c8
-rw-r--r--src/proof/ssc/sscCore.c2
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 );
generated by cgit v1.2.3 (git 2.25.1) at 2025-11-04 11:04:48 +0000