diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-02-16 23:40:23 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-02-16 23:40:23 -0800 |
commit | 97856d021a1282cf3fb9a86701fff3ec403fe912 (patch) | |
tree | 7dbd5471eb417540ad39fa6079ac8c32a2e06222 /src/sat | |
parent | 791b107e7a225103ee76c921c3c4a96d0e1adae2 (diff) | |
download | abc-97856d021a1282cf3fb9a86701fff3ec403fe912.tar.gz abc-97856d021a1282cf3fb9a86701fff3ec403fe912.tar.bz2 abc-97856d021a1282cf3fb9a86701fff3ec403fe912.zip |
Silencing some of the gcc warnings.
Diffstat (limited to 'src/sat')
-rw-r--r-- | src/sat/bsat/satChecker.c | 3 | ||||
-rw-r--r-- | src/sat/bsat/satProof.c | 7 | ||||
-rw-r--r-- | src/sat/bsat/satSolver.c | 8 | ||||
-rw-r--r-- | src/sat/bsat/satSolver2.c | 8 | ||||
-rw-r--r-- | src/sat/cnf/cnfFast.c | 2 | ||||
-rw-r--r-- | src/sat/msat/msatOrderH.c | 8 | ||||
-rw-r--r-- | src/sat/msat/msatSolverCore.c | 10 |
7 files changed, 26 insertions, 20 deletions
diff --git a/src/sat/bsat/satChecker.c b/src/sat/bsat/satChecker.c index 7aec4a4d..f478928c 100644 --- a/src/sat/bsat/satChecker.c +++ b/src/sat/bsat/satChecker.c @@ -121,6 +121,7 @@ void Sat_ProofChecker( char * pFileName ) FILE * pFile; Vec_Vec_t * vClauses; int c, i, Num, RetValue, Counter, Counter2, Clause1, Clause2; + int RetValue; // open the file pFile = fopen( pFileName, "r" ); if ( pFile == NULL ) @@ -138,7 +139,7 @@ void Sat_ProofChecker( char * pFileName ) rewind( pFile ); for ( i = 1 ; ; i++ ) { - RetValue = fscanf( pFile, "%d", &Num ); + RetValue = RetValue = fscanf( pFile, "%d", &Num ); if ( RetValue != 1 ) break; assert( Num == i ); diff --git a/src/sat/bsat/satProof.c b/src/sat/bsat/satProof.c index 81adb18b..223c830b 100644 --- a/src/sat/bsat/satProof.c +++ b/src/sat/bsat/satProof.c @@ -524,7 +524,7 @@ void Sat_ProofCheck( sat_solver2 * s ) Vec_Int_t Roots = { 1, 1, &s->hProofLast }, * vRoots = &Roots; Vec_Set_t * vResolves; Vec_Int_t * vUsed, * vTemp; - satset * pSet, * pSet0, * pSet1; + satset * pSet, * pSet0 = NULL, * pSet1; int i, k, hRoot, Handle, Counter = 0, clk = clock(); hRoot = s->hProofLast; if ( hRoot == -1 ) @@ -537,6 +537,7 @@ void Sat_ProofCheck( sat_solver2 * s ) vResolves = Vec_SetAlloc(); Proof_ForeachNodeVec( vUsed, vProof, pSet, i ) { + Handle = -1; pSet0 = Sat_ProofCheckReadOne( vClauses, vProof, vResolves, pSet->pEnts[0] ); for ( k = 1; k < (int)pSet->nEnts; k++ ) { @@ -578,7 +579,7 @@ Vec_Int_t * Sat_ProofCollectCore( Vec_Int_t * vClauses, Vec_Set_t * vProof, Vec_ { Vec_Int_t * vCore; satset * pNode, * pFanin; - int i, k, clk = clock(); + int i, k;//, clk = clock(); vCore = Vec_IntAlloc( 1000 ); Proof_ForeachNodeVec( vUsed, vProof, pNode, i ) { @@ -669,7 +670,7 @@ void * Sat_ProofInterpolant( sat_solver2 * s, void * pGloVars ) Vec_Int_t * vUsed, * vCore, * vCoreNums, * vVarMap; satset * pNode, * pFanin; Aig_Man_t * pAig; - Aig_Obj_t * pObj; + Aig_Obj_t * pObj = NULL; int i, k, iVar, Lit, Entry, hRoot; // if ( s->hLearntLast < 0 ) // return NULL; diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index 181d152a..1f86f2d3 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -257,9 +257,9 @@ static inline void act_var_rescale(sat_solver* s) { s->var_inc *= 1e-100; } static inline void act_clause_rescale(sat_solver* s) { - static int Total = 0; +// static int Total = 0; clause** cs = (clause**)veci_begin(&s->learnts); - int i, clk = clock(); + int i;//, clk = clock(); for (i = 0; i < veci_size(&s->learnts); i++){ float a = clause_activity(cs[i]); clause_setactivity(cs[i], a * (float)1e-20); @@ -1300,8 +1300,8 @@ void luby_test() static lbool sat_solver_search(sat_solver* s, ABC_INT64_T nof_conflicts, ABC_INT64_T nof_learnts) { - double var_decay = 0.95; - double clause_decay = 0.999; +// double var_decay = 0.95; +// double clause_decay = 0.999; double random_var_freq = s->fNotUseRandom ? 0.0 : 0.02; ABC_INT64_T conflictC = 0; diff --git a/src/sat/bsat/satSolver2.c b/src/sat/bsat/satSolver2.c index a58cf22b..a02ecc3f 100644 --- a/src/sat/bsat/satSolver2.c +++ b/src/sat/bsat/satSolver2.c @@ -1402,8 +1402,8 @@ void sat_solver2_reducedb(sat_solver2* s) satset * c, * pivot; cla h,* pArray,* pArray2; int * pPerm, * pClaAct, nClaAct, ActCutOff; - int i, j, k, hTemp, hHandle, clk = clock(); - int Counter, CounterStart, LastSize; + int i, j, k, hTemp, hHandle, LastSize = 0; + int Counter, CounterStart, clk = clock(); // check if it is time to reduce if ( s->nLearntMax == 0 || s->stats.learnts < (unsigned)s->nLearntMax ) @@ -1483,7 +1483,7 @@ void sat_solver2_reducedb(sat_solver2* s) } // compact clauses pivot = satset_read( &s->learnts, s->hLearntPivot ); - s->hLearntPivot = hHandle; + s->hLearntPivot = hTemp = hHandle; satset_foreach_entry_vec( &s->learnt_live, &s->learnts, c, i ) { hTemp = c->Id; c->Id = i + 1; @@ -1631,7 +1631,7 @@ int sat_solver2_find_clause( sat_solver2* s, int Hand, int fVerbose ) if ( (pArray[k] >> 1) == Hand ) { if ( fVerbose ) - printf( "Clause found in list %d at position.\n", i, k ); + printf( "Clause found in list %d at position %d.\n", i, k ); Found = 1; break; } diff --git a/src/sat/cnf/cnfFast.c b/src/sat/cnf/cnfFast.c index 6ec2b6a6..840c923e 100644 --- a/src/sat/cnf/cnfFast.c +++ b/src/sat/cnf/cnfFast.c @@ -666,7 +666,7 @@ Cnf_Dat_t * Cnf_DeriveFastClauses( Aig_Man_t * p, int nOutputs ) Cnf_Dat_t * Cnf_DeriveFast( Aig_Man_t * p, int nOutputs ) { Cnf_Dat_t * pCnf = NULL; - int clk, clkTotal = clock(); + int clk;//, clkTotal = clock(); // printf( "\n" ); Aig_ManCleanMarkAB( p ); // create initial marking diff --git a/src/sat/msat/msatOrderH.c b/src/sat/msat/msatOrderH.c index 2904607f..61c4d4d3 100644 --- a/src/sat/msat/msatOrderH.c +++ b/src/sat/msat/msatOrderH.c @@ -282,8 +282,12 @@ timeSelect += clock() - clk; int Msat_HeapCheck_rec( Msat_Order_t * p, int i ) { return i >= HSIZE(p) || - ( HPARENT(i) == 0 || !HCOMPARE(p, HHEAP(p, i), HHEAP(p, HPARENT(i))) ) && - Msat_HeapCheck_rec( p, HLEFT(i) ) && Msat_HeapCheck_rec( p, HRIGHT(i) ); + ( HPARENT(i) == 0 || + ( + !HCOMPARE(p, HHEAP(p, i), HHEAP(p, HPARENT(i))) ) && + Msat_HeapCheck_rec( p, HLEFT(i) ) && + Msat_HeapCheck_rec( p, HRIGHT(i) ) + ); } /**Function************************************************************* diff --git a/src/sat/msat/msatSolverCore.c b/src/sat/msat/msatSolverCore.c index 3312c23d..4ef40ad0 100644 --- a/src/sat/msat/msatSolverCore.c +++ b/src/sat/msat/msatSolverCore.c @@ -111,11 +111,11 @@ void Msat_SolverPrintStats( Msat_Solver_t * p ) { printf("C solver (%d vars; %d clauses; %d learned):\n", p->nVars, Msat_ClauseVecReadSize(p->vClauses), Msat_ClauseVecReadSize(p->vLearned) ); - printf("starts : %lld\n", p->Stats.nStarts); - printf("conflicts : %lld\n", p->Stats.nConflicts); - printf("decisions : %lld\n", p->Stats.nDecisions); - printf("propagations : %lld\n", p->Stats.nPropagations); - printf("inspects : %lld\n", p->Stats.nInspects); + printf("starts : %d\n", (int)p->Stats.nStarts); + printf("conflicts : %d\n", (int)p->Stats.nConflicts); + printf("decisions : %d\n", (int)p->Stats.nDecisions); + printf("propagations : %d\n", (int)p->Stats.nPropagations); + printf("inspects : %d\n", (int)p->Stats.nInspects); } /**Function************************************************************* |