diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-01 15:27:28 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-01 15:27:28 -0700 |
| commit | bd4b2521e779d963affd4af3805cc240ab4fdc3a (patch) | |
| tree | 2f75cada69f2b6ba0419a40ab74a6c3b5f723945 /src/aig/saig | |
| parent | 2cc51b4f75a1f418cee8145c9f1bc7ba8ea5a1dc (diff) | |
| download | abc-bd4b2521e779d963affd4af3805cc240ab4fdc3a.tar.gz abc-bd4b2521e779d963affd4af3805cc240ab4fdc3a.tar.bz2 abc-bd4b2521e779d963affd4af3805cc240ab4fdc3a.zip | |
Other improvements to bmc2 and bmc3.
Diffstat (limited to 'src/aig/saig')
| -rw-r--r-- | src/aig/saig/saigBmc3.c | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c index fac50264..aeb1a34d 100644 --- a/src/aig/saig/saigBmc3.c +++ b/src/aig/saig/saigBmc3.c @@ -700,7 +700,7 @@ Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig ) p->nWordNum = Abc_BitWordNum( 2 * Aig_ManObjNumMax(pAig) ); // hash table p->nTable = 1000003; - p->pTable = ABC_CALLOC( unsigned, 6 * p->nTable ); // 2.4 Mb + p->pTable = ABC_CALLOC( int, 6 * p->nTable ); // 2.4 Mb return p; } @@ -1001,7 +1001,7 @@ static inline void Saig_ManBmcAddClauses( Gia_ManBmc_t * p, int uTruth, int Lits SeeAlso [] ***********************************************************************/ -static inline unsigned Saig_ManBmcHashKey( unsigned * pArray ) +static inline unsigned Saig_ManBmcHashKey( int * pArray ) { static int s_Primes[5] = { 12582917, 25165843, 50331653, 100663319, 201326611 }; unsigned i, Key = 0; @@ -1097,11 +1097,12 @@ int Saig_ManBmcCreateCnf_rec( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame ) { *pLookup = toLit( p->nSatVars++ ); Saig_ManBmcAddClauses( p, uTruth, Lits, *pLookup ); - +/* if ( (Lits[0] > 1 && (Lits[0] == Lits[1] || Lits[0] == Lits[2] || Lits[0] == Lits[3])) || (Lits[1] > 1 && (Lits[1] == Lits[2] || Lits[1] == Lits[2])) || (Lits[2] > 1 && (Lits[2] == Lits[3])) ) p->nDupNum++; +*/ } iLit = *pLookup; } |