diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2006-06-11 08:01:00 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2006-06-11 08:01:00 -0700 |
| commit | 3db1557f45b03875a0a0b8adddcc15c4565895d2 (patch) | |
| tree | 2896d20ddcb85ae4aa7245ca28bc585f567fea54 /src/sat/aig | |
| parent | 7d0921330b1f4e789901b4c2450920e7c412f95f (diff) | |
| download | abc-3db1557f45b03875a0a0b8adddcc15c4565895d2.tar.gz abc-3db1557f45b03875a0a0b8adddcc15c4565895d2.tar.bz2 abc-3db1557f45b03875a0a0b8adddcc15c4565895d2.zip | |
Version abc60611
Diffstat (limited to 'src/sat/aig')
| -rw-r--r-- | src/sat/aig/aig.h | 4 | ||||
| -rw-r--r-- | src/sat/aig/fraigCore.c | 2 | ||||
| -rw-r--r-- | src/sat/aig/rwrTruth.c | 6 |
3 files changed, 7 insertions, 5 deletions
diff --git a/src/sat/aig/aig.h b/src/sat/aig/aig.h index 5d2547ea..a0d63ce9 100644 --- a/src/sat/aig/aig.h +++ b/src/sat/aig/aig.h @@ -64,9 +64,11 @@ extern "C" { //////////////////////////////////////////////////////////////////////// //typedef int bool; +#ifndef __cplusplus #ifndef bool #define bool int #endif +#endif typedef struct Aig_Param_t_ Aig_Param_t; typedef struct Aig_Man_t_ Aig_Man_t; @@ -215,7 +217,7 @@ struct Aig_SimInfo_t_ /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// -static inline int Aig_BitWordNum( int nBits ) { return nBits/32 + ((nBits%32) > 0); } +static inline int Aig_BitWordNum( int nBits ) { return (nBits>>5) + ((nBits&31) > 0); } static inline int Aig_InfoHasBit( unsigned * p, int i ) { return (p[(i)>>5] & (1<<((i) & 31))) > 0; } static inline void Aig_InfoSetBit( unsigned * p, int i ) { p[(i)>>5] |= (1<<((i) & 31)); } static inline void Aig_InfoXorBit( unsigned * p, int i ) { p[(i)>>5] ^= (1<<((i) & 31)); } diff --git a/src/sat/aig/fraigCore.c b/src/sat/aig/fraigCore.c index 525d4a14..03781180 100644 --- a/src/sat/aig/fraigCore.c +++ b/src/sat/aig/fraigCore.c @@ -92,7 +92,7 @@ Aig_ProofType_t Aig_FraigProveOutput( Aig_Man_t * pMan ) // solve the miter clk = clock(); pMan->pSat->verbosity = pMan->pParam->fSatVerbose; - status = solver_solve( pMan->pSat, NULL, NULL, 0, 0 );//pMan->pParam->nConfLimit, pMan->pParam->nImpLimit ); + status = solver_solve( pMan->pSat, NULL, NULL, 0, 0 );//pMan->pParam->nConfLimit, pMan->pParam->nInsLimit ); if ( status == l_Undef ) { // printf( "The problem timed out.\n" ); diff --git a/src/sat/aig/rwrTruth.c b/src/sat/aig/rwrTruth.c index 92a39f0a..cb8d03e0 100644 --- a/src/sat/aig/rwrTruth.c +++ b/src/sat/aig/rwrTruth.c @@ -167,7 +167,7 @@ void Aig_TruthCount( Aig_Truth_t * p ) ***********************************************************************/ static inline unsigned Aig_WordGetPart( unsigned * p, int Start, int Size ) { - return (p[Start/5] >> (Start%32)) & (~0u >> (32-Size)); + return (p[Start/5] >> (Start&31)) & (~0u >> (32-Size)); } /**Function************************************************************* @@ -183,7 +183,7 @@ static inline unsigned Aig_WordGetPart( unsigned * p, int Start, int Size ) ***********************************************************************/ static inline void Aig_WordSetPart( unsigned * p, int Start, unsigned Part ) { - p[Start/5] |= (Part << (Start%32)); + p[Start/5] |= (Part << (Start&31)); } /**Function************************************************************* @@ -254,7 +254,7 @@ DdNode * Aig_TruthToBdd_rec( DdManager * dd, unsigned * pTruth, int Shift, int n } if ( nVars == 5 ) { - unsigned * pWord = pTruth + Shift/32; + unsigned * pWord = pTruth + (Shift>>5); assert( Shift % 32 == 0 ); if ( *pWord == 0 ) return Cudd_ReadLogicZero(dd); |