Remove now unused dumping infrastructure (#7703)

This PR removes the old dumping infrastructure. All dumping has already been migrated to -o.

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 6adb6241e6159718057ea9a5bea39105bebfdbb0..fb84058a3071e8ee61a553632db6ff7775bdd14d 100644 (file)
--- 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 04b377b123a7a5c15621d5cf8ab103eb3b3a2959..8ce9296ec1a82bd6342c490d0e1491001c8ef50e 100644 (file)
--- 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 bab629607d2c1f5b3f709db0f5be5ef96b11ac93..39ec7e77f14c017c1dc6a506d2e8e31ab593ac11 100644 (file)
--- 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 5d94f038e1fe3e0c4cd7c8ae619510899fd0d4dc..38cceea92ccb408387fc38568c888855e1668645 100644 (file)
--- 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 e1e1ef6f67291e2e9e37a6c9901c500dc2e3b75a..623c1a9dac8e07420e86133a4a53107e1798236e 100644 (file)
--- 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 18808f3c6d473bfb7351ec66eaa91838fca01d36..673df59dafd10db87a5d886d83a5db6607839540 100755 (executable)
--- 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 6a289ec92a02e8c376ff4ec40bd26a5a66019794..971bb7ea154967b40fb186bddb9df4d72d5311cb 100644 (file)
--- 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 a15a527847ecf3b321103997702e02a34969a425..816a70741a1785561291096c8de56f0a8cf01d83 100644 (file)
--- 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 0f4384dddc4115dcefc282b46d16f57fbc480c61..84b89cfbad8a365caeb73143c823afde4da23c0b 100644 (file)
--- 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 2e9fc64ee168b80b2608f91de151b810e097037f..ffbe6454c28238cbf61e05492403eabc02651391 100644 (file)
--- 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 44bde99832ab7c5785e384c018ba5d4b7295dbea..7bfae7bca64a7e466ffda64e90672041991b6bb9 100644 (file)
--- 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 b0a08b3593a8e08531d3e82c8dfbdff9b9dc08ad..68d1f2b64889a46b7e797d82316002714c4a2349 100644 (file)
--- 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 fbea9d1428d8671537099c73268add4201d3c7b7..8bfc34795f975e39413cd8d5cfd40a4f5324b361 100644 (file)
--- 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))))