diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-02-29 17:49:44 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-02-29 17:49:44 +0000 |
commit | 39af3d2f0391aba90a1941433dfd57e37218f3c2 (patch) | |
tree | 5a6dc0dd2f3b64a7cd924de92aac0a0f37888b2c /src/prop | |
parent | eefe0b63e564320eb135eb66d6c02c9dc6e9e8de (diff) |
consistency in how the Dump output stream is used
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/cnf_stream.cpp | 20 |
1 files changed, 9 insertions, 11 deletions
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp index 74feebd03..f2557a303 100644 --- a/src/prop/cnf_stream.cpp +++ b/src/prop/cnf_stream.cpp @@ -63,18 +63,16 @@ TseitinCnfStream::TseitinCnfStream(SatSolverInterface* satSolver, Registrar* reg void CnfStream::assertClause(TNode node, SatClause& c) { Debug("cnf") << "Inserting into stream " << c << endl; if(Dump.isOn("clauses")) { - if(Message.isOn()) { - if(c.size() == 1) { - Message() << AssertCommand(BoolExpr(getNode(c[0]).toExpr())) << endl; - } else { - Assert(c.size() > 1); - NodeBuilder<> b(kind::OR); - for(int i = 0; i < c.size(); ++i) { - b << getNode(c[i]); - } - Node n = b; - Message() << AssertCommand(BoolExpr(n.toExpr())) << endl; + if(c.size() == 1) { + Dump("clauses") << AssertCommand(BoolExpr(getNode(c[0]).toExpr())) << endl; + } else { + Assert(c.size() > 1); + NodeBuilder<> b(kind::OR); + for(int i = 0; i < c.size(); ++i) { + b << getNode(c[i]); } + Node n = b; + Dump("clauses") << AssertCommand(BoolExpr(n.toExpr())) << endl; } } d_satSolver->addClause(c, d_removable); |