diff options
| author | Haniel Barbosa <hanielbbarbosa@gmail.com> | 2021-02-08 16:32:18 -0300 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-08 13:32:18 -0600 |
| commit | b2a5854eb7409a9fa159ef67f93689543808aa2d (patch) | |
| tree | 27bae8e4258cd7dfa365da956aba5fef060e624d /src | |
| parent | 57919ba7271a6c2b36173f2ba0f580b84f962b1b (diff) | |
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.
Diffstat (limited to 'src')
| -rw-r--r-- | src/smt/dump.cpp | 16 |
1 files changed, 10 insertions, 6 deletions
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\ |