diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-02-26 22:19:47 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-02-26 22:19:47 +0000 |
commit | 3548c7e5f6afed4e07bf9a70f0403952c9262519 (patch) | |
tree | 18f5ae49fe1ecdc9f3254074df0990dc1930fbf2 /src/prop/minisat | |
parent | edf6aaa87da179948e6b233d16fa37d2aea58bbb (diff) |
Commit to fix bug 241 (improper "using namespace std" in a header). This caused a number of latent errors in sources and headers to come up. Those are now fixed (by adding "using" or "std::" depending on the context). Took the opportunity to bring many rewriter sources in line with coding conventions.
Diffstat (limited to 'src/prop/minisat')
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 18ed9b5da..28a90d741 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -197,13 +197,13 @@ bool Solver::addClause_(vec<Lit>& ps, ClauseType type) } else { // Lemma vec<Lit> assigned_lits; - Debug("minisat::lemmas") << "Asserting lemma with " << ps.size() << " literals." << endl; + Debug("minisat::lemmas") << "Asserting lemma with " << ps.size() << " literals." << std::endl; bool lemmaSatisfied = false; for (i = j = 0, p = lit_Undef; i < ps.size(); i++) { if (ps[i] == ~p) { // We don't add clauses that represent splits directly, they are decision literals // so they will get decided upon and sent to the theory - Debug("minisat::lemmas") << "Lemma is a tautology." << endl; + Debug("minisat::lemmas") << "Lemma is a tautology." << std::endl; return true; } if (value(ps[i]) == l_Undef) { @@ -216,7 +216,7 @@ bool Solver::addClause_(vec<Lit>& ps, ClauseType type) p = ps[i]; if (value(p) == l_True) lemmaSatisfied = true; assigned_lits.push(p); - Debug("minisat::lemmas") << proxy->getNode(p) << " has value " << value(p) << endl; + Debug("minisat::lemmas") << proxy->getNode(p) << " has value " << value(p) << std::endl; } } Assert(j >= 1 || lemmaSatisfied, "You are asserting a falsified lemma, produce a conflict instead!"); @@ -232,7 +232,7 @@ bool Solver::addClause_(vec<Lit>& ps, ClauseType type) } } if (value(ps[1]) != l_Undef && max_level != -1) { - swap(ps[1], ps[max_level_j]); + std::swap(ps[1], ps[max_level_j]); } ps.shrink(i - j); } @@ -249,7 +249,7 @@ bool Solver::addClause_(vec<Lit>& ps, ClauseType type) clauses.push(cr); attachClause(cr); if (propagate_first_literal) { - Debug("minisat::lemmas") << "Lemma propagating: " << (theory[var(ps[0])] ? proxy->getNode(ps[0]).toString() : "bool") << endl; + Debug("minisat::lemmas") << "Lemma propagating: " << (theory[var(ps[0])] ? proxy->getNode(ps[0]).toString() : "bool") << std::endl; lemma_propagated_literals.push(ps[0]); lemma_propagated_reasons.push(cr); propagating_lemmas.push(cr); @@ -915,11 +915,11 @@ lbool Solver::search(int nof_conflicts) // If we have more assertions from lemmas, we continue if (problem_extended) { - Debug("minisat::lemmas") << "Problem extended with lemmas, adding propagations." << endl; + Debug("minisat::lemmas") << "Problem extended with lemmas, adding propagations." << std::endl; for (int i = 0, i_end = lemma_propagated_literals.size(); i < i_end; ++ i) { if (value(var(lemma_propagated_literals[i])) == l_Undef) { - Debug("minisat::lemmas") << "Lemma propagating: " << proxy->getNode(lemma_propagated_literals[i]) << endl; + Debug("minisat::lemmas") << "Lemma propagating: " << proxy->getNode(lemma_propagated_literals[i]) << std::endl; uncheckedEnqueue(lemma_propagated_literals[i], lemma_propagated_reasons[i]); } } @@ -1080,7 +1080,7 @@ static double luby(double y, int x){ // NOTE: assumptions passed in member-variable 'assumptions'. lbool Solver::solve_() { - Debug("minisat") << "nvars = " << nVars() << endl; + Debug("minisat") << "nvars = " << nVars() << std::endl; in_solve = true; @@ -1123,7 +1123,7 @@ lbool Solver::solve_() model.growTo(nVars()); for (int i = 0; i < nVars(); i++) { model[i] = value(i); - Debug("minisat") << i << " = " << model[i] << endl; + Debug("minisat") << i << " = " << model[i] << std::endl; } }else if (status == l_False && conflict.size() == 0) ok = false; |