diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-09-07 19:54:12 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-09-07 19:54:12 -0700 |
| commit | 8a11c911ab2a746eddfc05d5cc22d5a6b2aff73d (patch) | |
| tree | 42d8239ad5b56e40640730e23889866870737f1c /src/sat/glucose | |
| parent | 7ce7e9ec310db430078b7cbec538ea2a29b6d539 (diff) | |
| download | abc-8a11c911ab2a746eddfc05d5cc22d5a6b2aff73d.tar.gz abc-8a11c911ab2a746eddfc05d5cc22d5a6b2aff73d.tar.bz2 abc-8a11c911ab2a746eddfc05d5cc22d5a6b2aff73d.zip | |
Compiler warnings.
Diffstat (limited to 'src/sat/glucose')
| -rw-r--r-- | src/sat/glucose/Glucose.cpp | 22 | ||||
| -rw-r--r-- | src/sat/glucose/Options.cpp | 3 | ||||
| -rw-r--r-- | src/sat/glucose/SimpSolver.cpp | 10 |
3 files changed, 19 insertions, 16 deletions
diff --git a/src/sat/glucose/Glucose.cpp b/src/sat/glucose/Glucose.cpp index b3df0c82..6301a0f8 100644 --- a/src/sat/glucose/Glucose.cpp +++ b/src/sat/glucose/Glucose.cpp @@ -92,8 +92,8 @@ Solver::Solver() : SolverType(0) , pCnfFunc(NULL) , nCallConfl(1000) - , verbEveryConflicts(10000) , terminate_search_early(false) + , verbEveryConflicts(10000) , pstop(NULL) , nRuntimeLimit(0) @@ -1188,16 +1188,16 @@ double Solver::progressEstimate() const void Solver::printIncrementalStats() { printf("c---------- Glucose Stats -------------------------\n"); - printf("c restarts : %lld\n", starts); - printf("c nb ReduceDB : %lld\n", nbReduceDB); - printf("c nb removed Clauses : %lld\n", nbRemovedClauses); - printf("c nb learnts DL2 : %lld\n", nbDL2); - printf("c nb learnts size 2 : %lld\n", nbBin); - printf("c nb learnts size 1 : %lld\n", nbUn); - - printf("c conflicts : %lld\n", conflicts); - printf("c decisions : %lld\n", decisions); - printf("c propagations : %lld\n", propagations); + printf("c restarts : %ld\n", starts); + printf("c nb ReduceDB : %ld\n", nbReduceDB); + printf("c nb removed Clauses : %ld\n", nbRemovedClauses); + printf("c nb learnts DL2 : %ld\n", nbDL2); + printf("c nb learnts size 2 : %ld\n", nbBin); + printf("c nb learnts size 1 : %ld\n", nbUn); + + printf("c conflicts : %ld\n", conflicts); + printf("c decisions : %ld\n", decisions); + printf("c propagations : %ld\n", propagations); printf("c SAT Calls : %d in %g seconds\n", nbSatCalls, totalTime4Sat); printf("c UNSAT Calls : %d in %g seconds\n", nbUnsatCalls, totalTime4Unsat); diff --git a/src/sat/glucose/Options.cpp b/src/sat/glucose/Options.cpp index c4729b04..d9521c52 100644 --- a/src/sat/glucose/Options.cpp +++ b/src/sat/glucose/Options.cpp @@ -42,11 +42,12 @@ void Gluco::parseOptions(int& argc, char** argv, bool strict) // fprintf(stderr, "checking %d: %s against flag <%s> (%s)\n", i, argv[i], Option::getOptionList()[k]->name, parsed_ok ? "ok" : "skip"); } - if (!parsed_ok) + if (!parsed_ok) { if (strict && match(argv[i], "-")) fprintf(stderr, "ERROR! Unknown flag \"%s\". Use '--%shelp' for help.\n", argv[i], Option::getHelpPrefixString()), exit(1); else argv[j++] = argv[i]; + } } } diff --git a/src/sat/glucose/SimpSolver.cpp b/src/sat/glucose/SimpSolver.cpp index 1c3ee67b..566472fe 100644 --- a/src/sat/glucose/SimpSolver.cpp +++ b/src/sat/glucose/SimpSolver.cpp @@ -241,15 +241,16 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& ou const Clause& ps = ps_smallest ? _qs : _ps; const Clause& qs = ps_smallest ? _ps : _qs; - int i; + int i, j; for (i = 0; i < qs.size(); i++){ if (var(qs[i]) != v){ - for (int j = 0; j < ps.size(); j++) - if (var(ps[j]) == var(qs[i])) + for (j = 0; j < ps.size(); j++) + if (var(ps[j]) == var(qs[i])) { if (ps[j] == ~qs[i]) return false; else goto next; + } out_clause.push(qs[i]); } next:; @@ -279,11 +280,12 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, int& size) for (int i = 0; i < qs.size(); i++){ if (var(__qs[i]) != v){ for (int j = 0; j < ps.size(); j++) - if (var(__ps[j]) == var(__qs[i])) + if (var(__ps[j]) == var(__qs[i])) { if (__ps[j] == ~__qs[i]) return false; else goto next; + } size++; } next:; |