Fix dumping pre/post preprocessing passes (#2469)

This commit changes the hard-coded list of checks for
preprocessing-related dump tags to take advantage of the new
preprocessing pass registration mechanism from PR #2468. It also fixes a
typo in the `Dump.isOn()` check in `PreprocessingPass::dumpAssertions()`
and adds a list of available passes to the `--dump help` output.

diff --git a/src/preprocessing/preprocessing_pass.cpp b/src/preprocessing/preprocessing_pass.cpp
index 6a1d89d33a39a687ffc09e0a5a0f02d6d3b8d62d..120c68a914868168599f509837ce2b4eca46e453 100644 (file)
--- a/src/preprocessing/preprocessing_pass.cpp
+++ b/src/preprocessing/preprocessing_pass.cpp
@@ -36,7 +36,8 @@ PreprocessingPassResult PreprocessingPass::apply(
 
 void PreprocessingPass::dumpAssertions(const char* key,
                                        const AssertionPipeline& assertionList) {
-  if (Dump.isOn("assertions") && Dump.isOn(std::string("assertions::") + key)) {
+  if (Dump.isOn("assertions") && Dump.isOn(std::string("assertions:") + key))
+  {
     // Push the simplified assertions to the dump output stream
     for (const auto& n : assertionList) {
       Dump("assertions") << AssertCommand(Expr(n.toExpr()));

diff --git a/src/smt/dump.cpp b/src/smt/dump.cpp
index 58a1e2912604c9350f4c4d8f7d461dee552ee394..eae11606f5e31c59c04e990a86e3afbf9ed1d9bb 100644 (file)
--- a/src/smt/dump.cpp
+++ b/src/smt/dump.cpp
@@ -15,8 +15,10 @@
  **/
 
 #include "smt/dump.h"
-#include "lib/strtok_r.h"
+
 #include "base/output.h"
+#include "lib/strtok_r.h"
+#include "preprocessing/preprocessing_pass_registry.h"
 
 namespace CVC4 {
 
@@ -55,25 +57,10 @@ void DumpC::setDumpFromString(const std::string& optarg) {
                               optargPtr + "'.  Please consult --dump help.");
       }
       if(!strcmp(p, "everything")) {
-      } else if(!strcmp(p, "definition-expansion")) {
-      } else if(!strcmp(p, "boolean-terms")) {
-      } else if(!strcmp(p, "constrain-subtypes")) {
-      } else if(!strcmp(p, "substitution")) {
-      } else if(!strcmp(p, "bv-to-bool")) {
-      } else if(!strcmp(p, "bool-to-bv")) {
-      } else if(!strcmp(p, "strings-pp")) {
-      } else if(!strcmp(p, "skolem-quant")) {
-      } else if(!strcmp(p, "simplify")) {
-      } else if(!strcmp(p, "static-learning")) {
-      } else if(!strcmp(p, "ite-removal")) {
-      } else if(!strcmp(p, "repeat-simplify")) {
-      } else if(!strcmp(p, "rewrite-apply-to-const")) {
-      } else if(!strcmp(p, "theory-preprocessing")) {
-      } else if(!strcmp(p, "nonclausal")) {
-      } else if(!strcmp(p, "theorypp")) {
-      } else if(!strcmp(p, "itesimp")) {
-      } else if(!strcmp(p, "unconstrained")) {
-      } else if(!strcmp(p, "repeatsimp")) {
+      }
+      else if (preprocessing::PreprocessingPassRegistry::getInstance().hasPass(
+                   p))
+      {
       } else {
         throw OptionException(std::string("don't know how to dump `") +
                               optargPtr + "'.  Please consult --dump help.");
@@ -116,6 +103,16 @@ void DumpC::setDumpFromString(const std::string& optarg) {
       }
     } else if(!strcmp(optargPtr, "help")) {
       puts(s_dumpHelp.c_str());
+
+      std::stringstream ss;
+      ss << "Available preprocessing passes:\n";
+      for (const std::string& pass :
+           preprocessing::PreprocessingPassRegistry::getInstance()
+               .getAvailablePasses())
+      {
+        ss << "- " << pass << "\n";
+      }
+      puts(ss.str().c_str());
       exit(1);
     } else if(!strcmp(optargPtr, "bv-abstraction")) {
       Dump.on("bv-abstraction");
@@ -140,7 +137,6 @@ void DumpC::setDumpFromString(const std::string& optarg) {
 #endif /* CVC4_DUMPING */
 }
 
-
 const std::string DumpC::s_dumpHelp = "\
 Dump modes currently supported by the --dump option:\n\
 \n\

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index b133f3a364aad2858b7132aa6ac518f630af46fb..11c03de6cbf4ed2a9ad13372aa1e07dc1299733a 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2742,8 +2742,6 @@ static void dumpAssertions(const char* key,
 // returns false if simplification led to "false"
 bool SmtEnginePrivate::simplifyAssertions()
 {
-  PreprocessingPassRegistry& ppReg = PreprocessingPassRegistry::getInstance();
-
   spendResource(options::preprocessStep());
   Assert(d_smt.d_pendingPops == 0);
   try {
@@ -2972,8 +2970,6 @@ void SmtEnginePrivate::processAssertions() {
   SubstitutionMap& top_level_substs =
       d_preprocessingPassContext->getTopLevelSubstitutions();
 
-  PreprocessingPassRegistry& ppReg = PreprocessingPassRegistry::getInstance();
-
   // Dump the assertions
   dumpAssertions("pre-everything", d_assertions);