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 bf66629dd9483327e1c287fc2c31a96ea3eec2fc..adc40a9d136f5bb6862111ac0d29412d91fe5f3c 100644 (file)
--- 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 873aec6d1f5c9ffa61ab7018558e1cc98490c82e..f3429287fa769f1c4ab886eda48b628f526e1a58 100644 (file)
--- 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 0bde68d762323254753dedbf25afd80185118620..a85062af1551f4d8ffcb03208a5be866822ae927 100644 (file)
--- 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