diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-09-14 18:19:42 -0700 |
---|---|---|
committer | Andres Noetzli <andres.noetzli@gmail.com> | 2018-09-14 18:57:18 -0700 |
commit | 5c22e392a9188dcd7b182622019354dad85d4c37 (patch) | |
tree | dbebc616f396e93c1fb31af6492b045a5a3ec93d | |
parent | f5d33852dbb11d7b9f8ad0b5ef655d127a839885 (diff) |
Fix dumping pre/post preprocessing passesfixPPDumpPR
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.
-rw-r--r-- | src/preprocessing/preprocessing_pass.cpp | 4 | ||||
-rw-r--r-- | src/smt/dump.cpp | 38 |
2 files changed, 19 insertions, 23 deletions
diff --git a/src/preprocessing/preprocessing_pass.cpp b/src/preprocessing/preprocessing_pass.cpp index 166508552..273215b50 100644 --- a/src/preprocessing/preprocessing_pass.cpp +++ b/src/preprocessing/preprocessing_pass.cpp @@ -75,7 +75,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())); @@ -88,7 +89,6 @@ PreprocessingPass::PreprocessingPass(PreprocessingPassContext* preprocContext, : d_name(name), d_timer("preprocessing::" + name) { d_preprocContext = preprocContext; smtStatisticsRegistry()->registerStat(&d_timer); - Dump.registerPreprocessingPass(d_name); } PreprocessingPass::~PreprocessingPass() { diff --git a/src/smt/dump.cpp b/src/smt/dump.cpp index 58a1e2912..eae11606f 100644 --- 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\ |