From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Wed, 19 Mar 2014 20:32:05 +0000 (-0400)
Subject: Set dumping options from (set-option..) and API more directly.
X-Git-Tag: cvc5-1.0.0~7006
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ea22ebcbd69b24906d2214b7d294261578ce67a7;p=cvc5.git

Set dumping options from (set-option..) and API more directly.
---

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