Skip to content

A
abc
Commit 2cc51b4f by Alan Mishchenko
Options

Other improvements to bmc2 and bmc3.

parent 71f67ef9
Showing with 4 additions and 4 deletions
src/aig/saig/saigBmc3.c
...@@ -43,7 +43,7 @@ struct Gia_ManBmc_t_ ...@@ -43,7 +43,7 @@ struct Gia_ManBmc_t_
Vec_Ptr_t * vTerInfo; // ternary information Vec_Ptr_t * vTerInfo; // ternary information
Vec_Ptr_t * vId2Var; // SAT vars for each object Vec_Ptr_t * vId2Var; // SAT vars for each object
// hash table // hash table
unsigned * pTable; int * pTable;
int nTable; int nTable;
int nHashHit; int nHashHit;
int nHashMiss; int nHashMiss;
...@@ -1009,9 +1009,9 @@ static inline unsigned Saig_ManBmcHashKey( unsigned * pArray ) ...@@ -1009,9 +1009,9 @@ static inline unsigned Saig_ManBmcHashKey( unsigned * pArray )
Key += pArray[i] * s_Primes[i]; Key += pArray[i] * s_Primes[i];
return Key; return Key;
} }
static inline int * Saig_ManBmcLookup( Gia_ManBmc_t * p, unsigned * pArray ) static inline int * Saig_ManBmcLookup( Gia_ManBmc_t * p, int * pArray )
{ {
unsigned * pTable = p->pTable + 6 * (Saig_ManBmcHashKey(pArray) % p->nTable); int * pTable = p->pTable + 6 * (Saig_ManBmcHashKey(pArray) % p->nTable);
if ( memcmp( pTable, pArray, 20 ) ) if ( memcmp( pTable, pArray, 20 ) )
{ {
if ( pTable[0] == 0 ) if ( pTable[0] == 0 )
...@@ -1024,7 +1024,7 @@ static inline int * Saig_ManBmcLookup( Gia_ManBmc_t * p, unsigned * pArray ) ...@@ -1024,7 +1024,7 @@ static inline int * Saig_ManBmcLookup( Gia_ManBmc_t * p, unsigned * pArray )
else else
p->nHashHit++; p->nHashHit++;
assert( pTable + 5 < pTable + 6 * p->nTable ); assert( pTable + 5 < pTable + 6 * p->nTable );
return (int *)(pTable + 5); return pTable + 5;
} }
/**Function************************************************************* /**Function*************************************************************
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment