From: Morgan Deters <mdeters@gmail.com>
Date: Wed, 29 Feb 2012 17:49:44 +0000 (+0000)
Subject: consistency in how the Dump output stream is used
X-Git-Tag: cvc5-1.0.0~8296
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=39af3d2f0391aba90a1941433dfd57e37218f3c2;p=cvc5.git

consistency in how the Dump output stream is used
---

diff --git a/src/main/driver_portfolio.cpp b/src/main/driver_portfolio.cpp
index 7b0c70a8a..d17d00c5d 100644
--- a/src/main/driver_portfolio.cpp
+++ b/src/main/driver_portfolio.cpp
@@ -275,6 +275,7 @@ int runCvc4(int argc, char *argv[], Options& options) {
     Chat.setStream(CVC4::null_os);
     Message.setStream(CVC4::null_os);
     Warning.setStream(CVC4::null_os);
+    Dump.setStream(CVC4::null_os);
   } else {
     if(options.verbosity < 2) {
       Chat.setStream(CVC4::null_os);
@@ -294,6 +295,9 @@ int runCvc4(int argc, char *argv[], Options& options) {
     Chat.getStream() << Expr::setlanguage(language);
     Message.getStream() << Expr::setlanguage(language);
     Warning.getStream() << Expr::setlanguage(language);
+    Dump.getStream() << Expr::setlanguage(options.outputLanguage)
+                     << Expr::setdepth(-1)
+                     << Expr::printtypes(false);
   }
 
   vector<Options> threadOptions;
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);