From ea22ebcbd69b24906d2214b7d294261578ce67a7 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Wed, 19 Mar 2014 16:32:05 -0400
Subject: [PATCH] Set dumping options from (set-option..) and API more
 directly.

---
 src/main/driver_unified.cpp | 3 ---
 src/smt/options             | 4 ++--
 src/util/dump.h             | 2 +-
 3 files changed, 3 insertions(+), 6 deletions(-)

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index bf66629dd..adc40a9d1 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -42,7 +42,6 @@
 #include "smt/options.h"
 #include "theory/uf/options.h"
 #include "util/output.h"
-#include "util/dump.h"
 #include "util/result.h"
 #include "util/statistics_registry.h"
 
@@ -184,12 +183,10 @@ int runCvc4(int argc, char* argv[], Options& opts) {
     ChatChannel.setStream(CVC4::null_os);
     MessageChannel.setStream(CVC4::null_os);
     WarningChannel.setStream(CVC4::null_os);
-    DumpChannel.setStream(CVC4::null_os);
   }
 
   // important even for muzzled builds (to get result output right)
   *opts[options::out] << Expr::setlanguage(opts[options::outputLanguage]);
-  DumpChannel.getStream() << Expr::setlanguage(opts[options::outputLanguage]);
 
   // Create the expression manager using appropriate options
   ExprManager* exprMgr;
diff --git a/src/smt/options b/src/smt/options
index 873aec6d1..f3429287f 100644
--- a/src/smt/options
+++ b/src/smt/options
@@ -5,9 +5,9 @@
 
 module SMT "smt/options.h" SMT layer
 
-common-option - --dump=MODE argument :handler CVC4::smt::dumpMode :handler-include "smt/options_handlers.h"
+common-option - dump --dump=MODE argument :handler CVC4::smt::dumpMode :handler-include "smt/options_handlers.h"
  dump preprocessed assertions, etc., see --dump=help
-common-option - --dump-to=FILE argument :handler CVC4::smt::dumpToFile :handler-include "smt/options_handlers.h"
+common-option - dump-to --dump-to=FILE argument :handler CVC4::smt::dumpToFile :handler-include "smt/options_handlers.h"
  all dumping goes to FILE (instead of stdout)
 
 expert-option forceLogic force-logic --force-logic=LOGIC LogicInfo :include "theory/logic_info.h" :handler CVC4::smt::stringToLogicInfo :handler-include "smt/options_handlers.h" :default '""'
diff --git a/src/util/dump.h b/src/util/dump.h
index 0bde68d76..a85062af1 100644
--- a/src/util/dump.h
+++ b/src/util/dump.h
@@ -14,7 +14,7 @@
  ** Dump utility classes and functions.
  **/
 
-#include "cvc4_public.h"
+#include "cvc4_private.h"
 
 #ifndef __CVC4__DUMP_H
 #define __CVC4__DUMP_H
-- 
2.30.2