From 303baf27cf34c2a57db97c4c567fd744241fa14b Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 2 Jul 2008 08:01:00 -0700 Subject: Version abc80702 --- src/sat/csat/csat_apis.c | 6 ++++-- src/sat/fraig/fraigFeed.c | 1 - src/sat/fraig/fraigInt.h | 2 +- src/sat/fraig/fraigMan.c | 9 ++++----- src/sat/msat/msatRead.c | 4 ++-- src/sat/msat/msatSolverCore.c | 2 -- src/sat/msat/msatVec.c | 4 ++-- 7 files changed, 13 insertions(+), 15 deletions(-) (limited to 'src/sat') diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c index 5872f5bc..e755d8d4 100644 --- a/src/sat/csat/csat_apis.c +++ b/src/sat/csat/csat_apis.c @@ -169,8 +169,10 @@ void ABC_UseOnlyCoreSatSolver( ABC_Manager mng ) ***********************************************************************/ int ABC_AddGate( ABC_Manager mng, enum GateType type, char * name, int nofi, char ** fanins, int dc_attr ) { - Abc_Obj_t * pObj, * pFanin; - char * pSop, * pNewName; + Abc_Obj_t * pObj = NULL; // Suppress "might be used uninitialized" + Abc_Obj_t * pFanin; + char * pSop = NULL; // Suppress "might be used uninitialized" + char * pNewName; int i; // save the name in the local memory manager diff --git a/src/sat/fraig/fraigFeed.c b/src/sat/fraig/fraigFeed.c index 8a3cc6c7..e1e8d12c 100644 --- a/src/sat/fraig/fraigFeed.c +++ b/src/sat/fraig/fraigFeed.c @@ -634,7 +634,6 @@ void Fraig_FeedBackCheckTable( Fraig_Man_t * p ) Fraig_HashTable_t * pT = p->pTableF; Fraig_Node_t * pEntF, * pEntD; int i, k, m, nPairs; - int clk = clock(); nPairs = 0; for ( i = 0; i < pT->nBins; i++ ) diff --git a/src/sat/fraig/fraigInt.h b/src/sat/fraig/fraigInt.h index dc7bc815..c13d7083 100644 --- a/src/sat/fraig/fraigInt.h +++ b/src/sat/fraig/fraigInt.h @@ -107,7 +107,7 @@ // copied from "extra.h" for stand-aloneness #define Fraig_PrintTime(a,t) printf( "%s = ", (a) ); printf( "%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC) ) -#define Fraig_HashKey2(a,b,TSIZE) (((unsigned)(a) + (unsigned)(b) * 12582917) % TSIZE) +#define Fraig_HashKey2(a,b,TSIZE) (((PORT_PTRUINT_T)(a) + (PORT_PTRUINT_T)(b) * 12582917) % TSIZE) //#define Fraig_HashKey2(a,b,TSIZE) (( ((unsigned)(a)->Num * 19) ^ ((unsigned)(b)->Num * 1999) ) % TSIZE) //#define Fraig_HashKey2(a,b,TSIZE) ( ((unsigned)((a)->Num + (b)->Num) * ((a)->Num + (b)->Num + 1) / 2) % TSIZE) // the other two hash functions give bad distribution of hash chain lengths (not clear why) diff --git a/src/sat/fraig/fraigMan.c b/src/sat/fraig/fraigMan.c index 12cb5c45..cbeef4c6 100644 --- a/src/sat/fraig/fraigMan.c +++ b/src/sat/fraig/fraigMan.c @@ -95,13 +95,13 @@ void Prove_ParamsPrint( Prove_Params_t * pParams ) printf( "Multiplicative coeficient for mitering: %.2f\n", pParams->nMiteringLimitMulti ); printf( "Starting number of rewriting iterations: %d\n", pParams->nRewritingLimitStart ); printf( "Multiplicative coeficient for rewriting: %.2f\n", pParams->nRewritingLimitMulti ); - printf( "Starting number of conflicts in fraiging: %d\n", pParams->nFraigingLimitMulti ); + printf( "Starting number of conflicts in fraiging: %.2f\n", pParams->nFraigingLimitMulti ); printf( "Multiplicative coeficient for fraiging: %.2f\n", pParams->nRewritingLimitMulti ); - printf( "BDD size limit for bailing out: %.2f\n", pParams->nBddSizeLimit ); + printf( "BDD size limit for bailing out: %d\n", pParams->nBddSizeLimit ); printf( "BDD reordering enabled: %s\n", pParams->fBddReorder? "yes":"no" ); printf( "Last-gasp mitering limit: %d\n", pParams->nMiteringLimitLast ); - printf( "Total conflict limit: %d\n", pParams->nTotalBacktrackLimit ); - printf( "Total inspection limit: %d\n", pParams->nTotalInspectLimit ); + printf( "Total conflict limit: %lld\n", pParams->nTotalBacktrackLimit ); + printf( "Total inspection limit: %lld\n", pParams->nTotalInspectLimit ); printf( "Parameter dump complete.\n" ); } @@ -347,7 +347,6 @@ void Fraig_ManCreateSolver( Fraig_Man_t * p ) void Fraig_ManPrintStats( Fraig_Man_t * p ) { double nMemory; - int clk = clock(); nMemory = ((double)(p->vInputs->nSize + p->vNodes->nSize) * (sizeof(Fraig_Node_t) + sizeof(unsigned)*(p->nWordsRand + p->nWordsDyna) /*+ p->nSuppWords*sizeof(unsigned)*/))/(1<<20); printf( "Words: Random = %d. Dynamic = %d. Used = %d. Memory = %0.2f Mb.\n", diff --git a/src/sat/msat/msatRead.c b/src/sat/msat/msatRead.c index 738562ef..20453fed 100644 --- a/src/sat/msat/msatRead.c +++ b/src/sat/msat/msatRead.c @@ -196,8 +196,8 @@ static void Msat_ReadClause( char ** pIn, Msat_Solver_t * p, Msat_IntVec_t * pLi ***********************************************************************/ static bool Msat_ReadDimacs( char * pText, Msat_Solver_t ** pS, bool fVerbose ) { - Msat_Solver_t * p; - Msat_IntVec_t * pLits; + Msat_Solver_t * p = NULL; // Suppress "might be used uninitialized" + Msat_IntVec_t * pLits = NULL; // Suppress "might be used uninitialized" char * pIn = pText; int nVars, nClas; while ( 1 ) diff --git a/src/sat/msat/msatSolverCore.c b/src/sat/msat/msatSolverCore.c index f9fee73c..e86ab511 100644 --- a/src/sat/msat/msatSolverCore.c +++ b/src/sat/msat/msatSolverCore.c @@ -138,8 +138,6 @@ bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTra double nConflictsLimit, nLearnedLimit; Msat_Type_t Status; int timeStart = clock(); - int64 nConflictsOld = p->Stats.nConflicts; - int64 nDecisionsOld = p->Stats.nDecisions; // p->pFreq = ALLOC( int, p->nVarsAlloc ); // memset( p->pFreq, 0, sizeof(int) * p->nVarsAlloc ); diff --git a/src/sat/msat/msatVec.c b/src/sat/msat/msatVec.c index 75f53047..36ad55ba 100644 --- a/src/sat/msat/msatVec.c +++ b/src/sat/msat/msatVec.c @@ -399,8 +399,8 @@ void Msat_IntVecPushUniqueOrder( Msat_IntVec_t * p, int Entry, int fIncrease ) { Entry1 = p->pArray[i ]; Entry2 = p->pArray[i-1]; - if ( fIncrease && Entry1 >= Entry2 || - !fIncrease && Entry1 <= Entry2 ) + if (( fIncrease && Entry1 >= Entry2) || + (!fIncrease && Entry1 <= Entry2) ) break; p->pArray[i ] = Entry2; p->pArray[i-1] = Entry1; -- cgit v1.2.3