diff options
Diffstat (limited to 'src/prop')
| -rw-r--r-- | src/prop/cnf_stream.cpp | 4 | ||||
| -rw-r--r-- | src/prop/minisat/core/Solver.cc | 2 | ||||
| -rw-r--r-- | src/prop/minisat/core/Solver.h | 2 | ||||
| -rw-r--r-- | src/prop/prop_engine.cpp | 4 |
4 files changed, 6 insertions, 6 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 396454fac..661221441 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -74,7 +74,7 @@ void CnfStream::assertClause(TNode node, SatClause& c) { Debug("cnf") << "Inserting into stream " << c << endl; if(Dump.isOn("clauses")) { if(c.size() == 1) { - Dump("clauses") << AssertCommand(BoolExpr(getNode(c[0]).toExpr())) << endl; + Dump("clauses") << AssertCommand(BoolExpr(getNode(c[0]).toExpr())); } else { Assert(c.size() > 1); NodeBuilder<> b(kind::OR); @@ -82,7 +82,7 @@ void CnfStream::assertClause(TNode node, SatClause& c) { b << getNode(c[i]); } Node n = b; - Dump("clauses") << AssertCommand(BoolExpr(n.toExpr())) << endl; + Dump("clauses") << AssertCommand(BoolExpr(n.toExpr())); } } d_satSolver->addClause(c, d_removable); diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index ac3c5e101..980cb1b3f 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -322,7 +322,7 @@ void Solver::cancelUntil(int level) { for (int l = trail_lim.size() - level; l > 0; --l) { context->pop(); if(Dump.isOn("state")) { - Dump("state") << PopCommand() << std::endl; + Dump("state") << PopCommand(); } } for (int c = trail.size()-1; c >= trail_lim[level]; c--){ diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h index 8a5472725..ca5b2c30f 100644 --- a/src/prop/minisat/core/Solver.h +++ b/src/prop/minisat/core/Solver.h @@ -454,7 +454,7 @@ inline bool Solver::addClause (Lit p, bool removable) inline bool Solver::addClause (Lit p, Lit q, bool removable) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable); } inline bool Solver::addClause (Lit p, Lit q, Lit r, bool removable) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable); } inline bool Solver::locked (const Clause& c) const { return value(c[0]) == l_True && isPropagatedBy(var(c[0]), c); } -inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); context->push(); if(Dump.isOn("state")) { Dump("state") << CVC4::PushCommand() << std::endl; } } +inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); context->push(); if(Dump.isOn("state")) { Dump("state") << CVC4::PushCommand(); } } inline int Solver::decisionLevel () const { return trail_lim.size(); } inline uint32_t Solver::abstractLevel (Var x) const { return 1 << (level(x) & 31); } diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 2538e6d0c..b7b3c685f 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -97,9 +97,9 @@ void PropEngine::assertLemma(TNode node, bool negated, bool removable) { Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl; if(!d_inCheckSat && Dump.isOn("learned")) { - Dump("learned") << AssertCommand(BoolExpr(node.toExpr())) << endl; + Dump("learned") << AssertCommand(BoolExpr(node.toExpr())); } else if(Dump.isOn("lemmas")) { - Dump("lemmas") << AssertCommand(BoolExpr(node.toExpr())) << endl; + Dump("lemmas") << AssertCommand(BoolExpr(node.toExpr())); } //TODO This comment is now false |