diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-03-09 21:10:17 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-03-09 21:10:17 +0000 |
commit | 84f26af22566f7c10dea45b399b944cb50b5e317 (patch) | |
tree | 68fbe22665cc09f46c321c6132e49dabbc15c337 /src/prop | |
parent | f29ea80fb3e238278a721d79077c9087bccbac0b (diff) |
Some work on the dump infrastructure to support portfolio work.
Dump("foo") << FooCommand(...);
now "dumps" the textual representation of the command (in the current
output language) to a file, IF dumping is on at configure-time, AND the
"muzzle" feature is off, AND the "foo" flag is turned on for the dump
stream during this run.
If it's a portfolio build, the above will also store the command in a
CommandSequence, IF the "foo" flag is turned on for the dump stream
during this run. This is done even if the muzzle is on.
This commit also cleans up some code that used the dump feature (in arrays,
particularly).
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 |