From f82d6315c5e7dbc988e4e8f0912314469542acea Mon Sep 17 00:00:00 2001
From: Gereon Kremer <gkremer@stanford.edu>
Date: Tue, 30 Nov 2021 07:37:38 -0800
Subject: [PATCH] Remove now unused dumping infrastructure (#7703)

This PR removes the old dumping infrastructure. All dumping has already been migrated to -o.
---
 CMakeLists.txt                                |  6 ---
 cmake/ConfigCompetition.cmake                 |  2 -
 cmake/ConfigDebug.cmake                       |  2 -
 cmake/ConfigProduction.cmake                  |  2 -
 cmake/ConfigTesting.cmake                     |  2 -
 configure.sh                                  |  7 ---
 src/base/configuration.cpp                    |  4 --
 src/base/configuration.h                      |  2 -
 src/base/configuration_private.h              |  6 ---
 src/base/output.cpp                           |  2 -
 src/base/output.h                             | 53 -------------------
 src/options/options_handler.cpp               |  1 -
 .../regress0/printer/let_shadowing.smt2       |  1 -
 13 files changed, 90 deletions(-)

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 6adb6241e..fb84058a3 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -78,7 +78,6 @@ cvc5_option(ENABLE_ASSERTIONS     "Enable assertions")
 cvc5_option(ENABLE_COMP_INC_TRACK
             "Enable optimizations for incremental SMT-COMP tracks")
 cvc5_option(ENABLE_DEBUG_SYMBOLS  "Enable debug symbols")
-cvc5_option(ENABLE_DUMPING        "Enable dumping")
 cvc5_option(ENABLE_MUZZLE         "Suppress ALL non-result output")
 cvc5_option(ENABLE_STATISTICS     "Enable statistics")
 cvc5_option(ENABLE_TRACING        "Enable tracing")
@@ -358,10 +357,6 @@ if(ENABLE_MUZZLE)
   add_definitions(-DCVC5_MUZZLE)
 endif()
 
-if(ENABLE_DUMPING)
-  add_definitions(-DCVC5_DUMPING)
-endif()
-
 if(ENABLE_PROFILING)
   add_definitions(-DCVC5_PROFILING)
   add_check_c_cxx_flag("-pg")
@@ -603,7 +598,6 @@ print_config("Assertions                " ${ENABLE_ASSERTIONS})
 print_config("Debug symbols             " ${ENABLE_DEBUG_SYMBOLS})
 print_config("Debug context mem mgr     " ${ENABLE_DEBUG_CONTEXT_MM})
 message("")
-print_config("Dumping                   " ${ENABLE_DUMPING})
 print_config("Muzzle                    " ${ENABLE_MUZZLE})
 print_config("Statistics                " ${ENABLE_STATISTICS})
 print_config("Tracing                   " ${ENABLE_TRACING})
diff --git a/cmake/ConfigCompetition.cmake b/cmake/ConfigCompetition.cmake
index 04b377b12..8ce9296ec 100644
--- a/cmake/ConfigCompetition.cmake
+++ b/cmake/ConfigCompetition.cmake
@@ -27,8 +27,6 @@ cvc5_set_option(ENABLE_ASSERTIONS OFF)
 cvc5_set_option(ENABLE_PROOFS OFF)
 # enable_tracing=no
 cvc5_set_option(ENABLE_TRACING OFF)
-# enable_dumping=no
-cvc5_set_option(ENABLE_DUMPING OFF)
 # enable_muzzle=yes
 cvc5_set_option(ENABLE_MUZZLE ON)
 # enable_valgrind=no
diff --git a/cmake/ConfigDebug.cmake b/cmake/ConfigDebug.cmake
index bab629607..39ec7e77f 100644
--- a/cmake/ConfigDebug.cmake
+++ b/cmake/ConfigDebug.cmake
@@ -24,8 +24,6 @@ cvc5_set_option(ENABLE_ASSERTIONS ON)
 cvc5_set_option(ENABLE_PROOFS ON)
 # enable_tracing=yes
 cvc5_set_option(ENABLE_TRACING ON)
-# enable_dumping=yes
-cvc5_set_option(ENABLE_DUMPING ON)
 # enable_muzzle=no
 cvc5_set_option(ENABLE_MUZZLE OFF)
 # enable_valgrind=optional
diff --git a/cmake/ConfigProduction.cmake b/cmake/ConfigProduction.cmake
index 5d94f038e..38cceea92 100644
--- a/cmake/ConfigProduction.cmake
+++ b/cmake/ConfigProduction.cmake
@@ -23,8 +23,6 @@ cvc5_set_option(ENABLE_ASSERTIONS OFF)
 cvc5_set_option(ENABLE_PROOFS ON)
 # enable_tracing=no
 cvc5_set_option(ENABLE_TRACING OFF)
-# enable_dumping=yes
-cvc5_set_option(ENABLE_DUMPING ON)
 # enable_muzzle=no
 cvc5_set_option(ENABLE_MUZZLE OFF)
 # enable_valgrind=no
diff --git a/cmake/ConfigTesting.cmake b/cmake/ConfigTesting.cmake
index e1e1ef6f6..623c1a9da 100644
--- a/cmake/ConfigTesting.cmake
+++ b/cmake/ConfigTesting.cmake
@@ -23,8 +23,6 @@ cvc5_set_option(ENABLE_ASSERTIONS ON)
 cvc5_set_option(ENABLE_PROOFS ON)
 # enable_tracing=yes
 cvc5_set_option(ENABLE_TRACING ON)
-# enable_dumping=yes
-cvc5_set_option(ENABLE_DUMPING ON)
 # enable_muzzle=no
 cvc5_set_option(ENABLE_MUZZLE OFF)
 # enable_valgrind=no
diff --git a/configure.sh b/configure.sh
index 18808f3c6..673df59da 100755
--- a/configure.sh
+++ b/configure.sh
@@ -39,7 +39,6 @@ The following flags enable optional features (disable with --no-<option name>).
   --statistics             include statistics
   --assertions             turn on assertions
   --tracing                include tracing code
-  --dumping                include dumping code
   --muzzle                 complete silence (no non-result output)
   --coverage               support for gcov coverage testing
   --profiling              support for gprof profiling
@@ -110,7 +109,6 @@ cryptominisat=default
 debug_context_mm=default
 debug_symbols=default
 docs=default
-dumping=default
 glpk=default
 gpl=default
 kissat=default
@@ -206,9 +204,6 @@ do
     --debug-context-mm) debug_context_mm=ON;;
     --no-debug-context-mm) debug_context_mm=OFF;;
 
-    --dumping) dumping=ON;;
-    --no-dumping) dumping=OFF;;
-
     --gpl) gpl=ON;;
     --no-gpl) gpl=OFF;;
 
@@ -329,8 +324,6 @@ fi
   && cmake_opts="$cmake_opts -DENABLE_DEBUG_SYMBOLS=$debug_symbols"
 [ $debug_context_mm != default ] \
   && cmake_opts="$cmake_opts -DENABLE_DEBUG_CONTEXT_MM=$debug_context_mm"
-[ $dumping != default ] \
-  && cmake_opts="$cmake_opts -DENABLE_DUMPING=$dumping"
 [ $gpl != default ] \
   && cmake_opts="$cmake_opts -DENABLE_GPL=$gpl"
 [ $win64 != default ] \
diff --git a/src/base/configuration.cpp b/src/base/configuration.cpp
index 6a289ec92..971bb7ea1 100644
--- a/src/base/configuration.cpp
+++ b/src/base/configuration.cpp
@@ -41,10 +41,6 @@ bool Configuration::isTracingBuild() {
   return IS_TRACING_BUILD;
 }
 
-bool Configuration::isDumpingBuild() {
-  return IS_DUMPING_BUILD && !IS_MUZZLED_BUILD;
-}
-
 bool Configuration::isMuzzledBuild() {
   return IS_MUZZLED_BUILD;
 }
diff --git a/src/base/configuration.h b/src/base/configuration.h
index a15a52784..816a70741 100644
--- a/src/base/configuration.h
+++ b/src/base/configuration.h
@@ -59,8 +59,6 @@ public:
 
   static bool isTracingBuild();
 
-  static bool isDumpingBuild();
-
   static bool isMuzzledBuild();
 
   static bool isAssertionBuild();
diff --git a/src/base/configuration_private.h b/src/base/configuration_private.h
index 0f4384ddd..84b89cfba 100644
--- a/src/base/configuration_private.h
+++ b/src/base/configuration_private.h
@@ -36,12 +36,6 @@ namespace cvc5 {
 #  define IS_TRACING_BUILD false
 #endif /* CVC5_TRACING */
 
-#ifdef CVC5_DUMPING
-#  define IS_DUMPING_BUILD true
-#else /* CVC5_DUMPING */
-#  define IS_DUMPING_BUILD false
-#endif /* CVC5_DUMPING */
-
 #ifdef CVC5_MUZZLE
 #  define IS_MUZZLED_BUILD true
 #else /* CVC5_MUZZLE */
diff --git a/src/base/output.cpp b/src/base/output.cpp
index 2e9fc64ee..ffbe6454c 100644
--- a/src/base/output.cpp
+++ b/src/base/output.cpp
@@ -32,7 +32,5 @@ const int Cvc5ostream::s_indentIosIndex = std::ios_base::xalloc();
 DebugC DebugChannel(&std::cout);
 WarningC WarningChannel(&std::cerr);
 TraceC TraceChannel(&std::cout);
-std::ostream DumpOutC::dump_cout(std::cout.rdbuf());  // copy cout stream buffer
-DumpOutC DumpOutChannel(&DumpOutC::dump_cout);
 
 }  // namespace cvc5
diff --git a/src/base/output.h b/src/base/output.h
index 44bde9983..7bfae7bca 100644
--- a/src/base/output.h
+++ b/src/base/output.h
@@ -304,57 +304,12 @@ public:
 
 }; /* class TraceC */
 
-/** The dump output class */
-class DumpOutC
-{
-  std::set<std::string> d_tags;
-  std::ostream* d_os;
-
-public:
-  /**
-   * A copy of cout for use by the dumper.  This is important because
-   * it has different settings (e.g., the expr printing depth is always
-   * unlimited). */
-  static std::ostream dump_cout;
-
-  explicit DumpOutC(std::ostream* os) : d_os(os) {}
-
-  Cvc5ostream operator()(std::string tag)
-  {
-    if(!d_tags.empty() && d_tags.find(tag) != d_tags.end()) {
-      return Cvc5ostream(d_os);
-    } else {
-      return Cvc5ostream();
-    }
-  }
-
-  bool on(const std::string& tag)
-  {
-    d_tags.insert(tag);
-    return true;
-  }
-  bool off(const std::string& tag)
-  {
-    d_tags.erase(tag);
-    return false;
-  }
-  bool off()                { d_tags.clear(); return false; }
-
-  bool isOn(std::string tag) const { return d_tags.find(tag) != d_tags.end(); }
-
-  std::ostream& setStream(std::ostream* os) { d_os = os; return *d_os; }
-  std::ostream& getStream() const { return *d_os; }
-  std::ostream* getStreamPointer() const { return d_os; }
-}; /* class DumpOutC */
-
 /** The debug output singleton */
 extern DebugC DebugChannel CVC5_EXPORT;
 /** The warning output singleton */
 extern WarningC WarningChannel CVC5_EXPORT;
 /** The trace output singleton */
 extern TraceC TraceChannel CVC5_EXPORT;
-/** The dump output singleton */
-extern DumpOutC DumpOutChannel CVC5_EXPORT;
 
 #ifdef CVC5_MUZZLE
 
@@ -364,8 +319,6 @@ extern DumpOutC DumpOutChannel CVC5_EXPORT;
 #define WarningOnce \
   ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::WarningChannel
 #define Trace ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::TraceChannel
-#define DumpOut \
-  ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::DumpOutChannel
 
 #else /* CVC5_MUZZLE */
 
@@ -386,12 +339,6 @@ extern DumpOutC DumpOutChannel CVC5_EXPORT;
 #else /* CVC5_TRACING */
 #define Trace ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::TraceChannel
 #endif /* CVC5_TRACING */
-#ifdef CVC5_DUMPING
-#define DumpOut ::cvc5::DumpOutChannel
-#else /* CVC5_DUMPING */
-#define DumpOut \
-  ::cvc5::__cvc5_true() ? ::cvc5::nullStream : ::cvc5::DumpOutChannel
-#endif /* CVC5_DUMPING */
 
 #endif /* CVC5_MUZZLE */
 
diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index b0a08b359..68d1f2b64 100644
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -389,7 +389,6 @@ void OptionsHandler::showConfiguration(const std::string& flag)
   print_config_cond("debug code", Configuration::isDebugBuild());
   print_config_cond("statistics", Configuration::isStatisticsBuild());
   print_config_cond("tracing", Configuration::isTracingBuild());
-  print_config_cond("dumping", Configuration::isDumpingBuild());
   print_config_cond("muzzled", Configuration::isMuzzledBuild());
   print_config_cond("assertions", Configuration::isAssertionBuild());
   print_config_cond("coverage", Configuration::isCoverageBuild());
diff --git a/test/regress/regress0/printer/let_shadowing.smt2 b/test/regress/regress0/printer/let_shadowing.smt2
index fbea9d142..8bfc34795 100644
--- a/test/regress/regress0/printer/let_shadowing.smt2
+++ b/test/regress/regress0/printer/let_shadowing.smt2
@@ -1,4 +1,3 @@
-; REQUIRES: dumping
 ; COMMAND-LINE: -o raw-benchmark --preprocess-only
 ; SCRUBBER: grep assert
 ; EXPECT: (assert (let ((_let_1 (* x y))) (and (= _let_1 _let_1) (= _let_1 _let_0))))
-- 
2.30.2