Added "dump=raw-benchmark" option for dumping all user commands exactly as received.

1 files changed, 15 insertions, 10 deletions

diff --git a/src/smt/dump.cpp b/src/smt/dump.cpp
index dc1ef792d..b1222a51e 100644
--- a/src/smt/dump.cpp
+++ b/src/smt/dump.cpp
@@ -39,7 +39,8 @@ void DumpC::setDumpFromString(const std::string& optarg) {
   char* toksave;
   while((optargPtr = strtok_r(tokstr, ",", &toksave)) != NULL) {
     tokstr = NULL;
-    if(!strcmp(optargPtr, "benchmark")) {
+    if(!strcmp(optargPtr, "raw-benchmark")) {
+    } else if(!strcmp(optargPtr, "benchmark")) {
     } else if(!strcmp(optargPtr, "declarations")) {
     } else if(!strcmp(optargPtr, "assertions")) {
       Dump.on("assertions:post-everything");
@@ -127,7 +128,7 @@ void DumpC::setDumpFromString(const std::string& optarg) {
     Dump.on("benchmark");
     if(strcmp(optargPtr, "benchmark")) {
       Dump.on("declarations");
-      if(strcmp(optargPtr, "declarations")) {
+      if(strcmp(optargPtr, "declarations") && strcmp(optargPtr, "raw-benchmark")) {
         Dump.on("skolems");
       }
     }
@@ -149,6 +150,10 @@ benchmark\n\
 declarations\n\
 + Dump user declarations.  Implied by all following modes.\n\
 \n\
+raw-benchmark\n\
++ Dump all user-commands as they are received (including assertions) without\n\
+  any preprocessing and without any internally-created commands.\n\
+\n\
 skolems\n\
 + Dump internally-created skolem variable declarations.  These can\n\
   arise from preprocessing simplifications, existential elimination,\n\
@@ -202,17 +207,17 @@ bv-abstraction [non-stateful]\n\
 bv-algebraic [non-stateful]\n\
 + Output correctness queries for bv algebraic solver. \n\
 \n\
-theory::fullcheck [non-stateful]\n                                      \
+theory::fullcheck [non-stateful]\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\
-one from the assertions category (either assertions or clauses), and\n\
-perhaps one or more stateful or non-stateful modes for checking correctness\n\
-and completeness of decision procedure implementations.  Stateful modes dump\n\
-the contextual assertions made by the core solver (all decisions and\n\
-propagations as assertions; that affects the validity of the resulting\n\
-correctness and completeness queries, so of course stateful and non-stateful\n\
-modes cannot be mixed in the same run.\n\
+raw-benchmark or, alternatively, one from the assertions category (either\n\
+assertions or clauses), and perhaps one or more stateful or non-stateful modes\n\
+for checking correctness and completeness of decision procedure implementations.\n\
+Stateful modes dump the contextual assertions made by the core solver (all\n\
+decisions and propagations as assertions); this affects the validity of the\n\
+resulting correctness and completeness queries, so of course stateful and\n\
+non-stateful modes cannot be mixed in the same run.\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\