From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Mon, 8 Feb 2021 19:32:18 +0000 (-0300)
Subject: Fix dumping of assertions for monolithic preprocessing passes (#5866)
X-Git-Tag: cvc5-1.0.0~2308
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b2a5854eb7409a9fa159ef67f93689543808aa2d;p=cvc5.git

Fix dumping of assertions for monolithic preprocessing passes (#5866)

Previously we were unable to dump assertions in ProcessAssertions::apply for the definition-expansion, simplify and repeat-simplify passes.
---

diff --git a/src/smt/dump.cpp b/src/smt/dump.cpp
index ceb0eb11f..b1fb0589c 100644
--- a/src/smt/dump.cpp
+++ b/src/smt/dump.cpp
@@ -105,7 +105,9 @@ void DumpC::setDumpFromString(const std::string& optarg) {
                                 + optargPtr
                                 + "'.  Please consult --dump help.");
         }
-        if (!strcmp(p, "everything"))
+        // hard-coded cases
+        if (!strcmp(p, "everything") || !strcmp(p, "definition-expansion")
+            || !strcmp(p, "simplify") || !strcmp(p, "repeat-simplify"))
         {
         }
         else if (preprocessing::PreprocessingPassRegistry::getInstance()
@@ -174,7 +176,8 @@ void DumpC::setDumpFromString(const std::string& optarg) {
   }
 }
 
-const std::string DumpC::s_dumpHelp = "\
+const std::string DumpC::s_dumpHelp =
+    "\
 Dump modes currently supported by the --dump option:\n\
 \n\
 benchmark\n\
@@ -225,10 +228,11 @@ bv-rewrites\n\
 theory::fullcheck\n\
 + Output completeness queries for all full-check effort-level theory checks\n\
 \n\
-Dump modes can be combined with multiple uses of --dump.  Generally you want\n\
-raw-benchmark or, alternatively, one from the assertions category (either\n\
-assertions or clauses), and perhaps one or more other modes\n\
-for checking correctness and completeness of decision procedure implementations.\n\
+Dump modes can be combined by concatenating the above values with \",\" in\n\
+between them.  Generally you want raw-benchmark or, alternatively, one from\n\
+the assertions category (either assertions or clauses), and perhaps one or more\n\
+other modes for checking correctness and completeness of decision procedure\n\
+implementations.\n\
 \n\
 The --output-language option controls the language used for dumping, and\n\
 this allows you to connect CVC4 to another solver implementation via a UNIX\n\