diff --git a/minisat/core/Dimacs.h b/minisat/core/Dimacs.h index d5db4139..eabffd4d 100644 --- a/minisat/core/Dimacs.h +++ b/minisat/core/Dimacs.h @@ -47,7 +47,6 @@ static void readClause(B& in, Solver& S, vec& lits) { template static void parse_DIMACS_main(B& in, Solver& S, bool strictp = false) { vec lits; - int vars = 0; int clauses = 0; int cnt = 0; for (;;){ @@ -55,7 +54,7 @@ static void parse_DIMACS_main(B& in, Solver& S, bool strictp = false) { if (*in == EOF) break; else if (*in == 'p'){ if (eagerMatch(in, "p cnf")){ - vars = parseInt(in); + (void)parseInt(in); // Variables clauses = parseInt(in); // SATRACE'06 hack // if (clauses > 4000000) diff --git a/minisat/core/Solver.cc b/minisat/core/Solver.cc index 0b4f77ad..6175cb4f 100644 --- a/minisat/core/Solver.cc +++ b/minisat/core/Solver.cc @@ -992,11 +992,11 @@ void Solver::printStats() const { double cpu_time = cpuTime(); double mem_used = memUsedPeak(); - printf("restarts : %"PRIu64"\n", starts); - printf("conflicts : %-12"PRIu64" (%.0f /sec)\n", conflicts , conflicts /cpu_time); - printf("decisions : %-12"PRIu64" (%4.2f %% random) (%.0f /sec)\n", decisions, (float)rnd_decisions*100 / (float)decisions, decisions /cpu_time); - printf("propagations : %-12"PRIu64" (%.0f /sec)\n", propagations, propagations/cpu_time); - printf("conflict literals : %-12"PRIu64" (%4.2f %% deleted)\n", tot_literals, (max_literals - tot_literals)*100 / (double)max_literals); + printf("restarts : %" PRIu64 "\n", starts); + printf("conflicts : %-12" PRIu64 " (%.0f /sec)\n", conflicts , conflicts /cpu_time); + printf("decisions : %-12" PRIu64 " (%4.2f %% random) (%.0f /sec)\n", decisions, (float)rnd_decisions*100 / (float)decisions, decisions /cpu_time); + printf("propagations : %-12" PRIu64 " (%.0f /sec)\n", propagations, propagations/cpu_time); + printf("conflict literals : %-12" PRIu64 " (%4.2f %% deleted)\n", tot_literals, (max_literals - tot_literals)*100 / (double)max_literals); if (mem_used != 0) printf("Memory used : %.2f MB\n", mem_used); printf("CPU time : %g s\n", cpu_time); } diff --git a/minisat/core/SolverTypes.h b/minisat/core/SolverTypes.h index 89986d1e..aa45ddb2 100644 --- a/minisat/core/SolverTypes.h +++ b/minisat/core/SolverTypes.h @@ -52,7 +52,7 @@ struct Lit { int x; // Use this as a constructor: - friend Lit mkLit(Var var, bool sign = false); + friend Lit mkLit(Var var, bool sign); bool operator == (Lit p) const { return x == p.x; } bool operator != (Lit p) const { return x != p.x; } @@ -60,7 +60,7 @@ struct Lit { }; -inline Lit mkLit (Var var, bool sign) { Lit p; p.x = var + var + (int)sign; return p; } +inline Lit mkLit (Var var, bool sign = false) { Lit p; p.x = var + var + (int)sign; return p; } inline Lit operator ~(Lit p) { Lit q; q.x = p.x ^ 1; return q; } inline Lit operator ^(Lit p, bool b) { Lit q; q.x = p.x ^ (unsigned int)b; return q; } inline bool sign (Lit p) { return p.x & 1; } diff --git a/minisat/utils/Options.h b/minisat/utils/Options.h index 4e71a18c..7d2e83a8 100644 --- a/minisat/utils/Options.h +++ b/minisat/utils/Options.h @@ -282,15 +282,15 @@ class Int64Option : public Option if (range.begin == INT64_MIN) fprintf(stderr, "imin"); else - fprintf(stderr, "%4"PRIi64, range.begin); + fprintf(stderr, "%4" PRIi64, range.begin); fprintf(stderr, " .. "); if (range.end == INT64_MAX) fprintf(stderr, "imax"); else - fprintf(stderr, "%4"PRIi64, range.end); + fprintf(stderr, "%4" PRIi64, range.end); - fprintf(stderr, "] (default: %"PRIi64")\n", value); + fprintf(stderr, "] (default: %" PRIi64 ")\n", value); if (verbose){ fprintf(stderr, "\n %s\n", description); fprintf(stderr, "\n");