From 14ec91ed77b816d77de60fbf6e77066da194d791 Mon Sep 17 00:00:00 2001
From: Clark Barrett <barrett@cs.stanford.edu>
Date: Mon, 5 Dec 2016 16:07:07 -0800
Subject: [PATCH] Added "dump=raw-benchmark" option for dumping all user
 commands exactly as received.

---
 src/smt/dump.cpp       | 25 +++++++++++++++----------
 src/smt/smt_engine.cpp | 17 ++++++++++++-----
 2 files changed, 27 insertions(+), 15 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\
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index f5b769984..30da29813 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1099,11 +1099,14 @@ void SmtEngine::finishInit() {
 
   // dump out a set-logic command
   if(Dump.isOn("benchmark")) {
-    // Dump("benchmark") << SetBenchmarkLogicCommand(logic.getLogicString());
-    LogicInfo everything;
-    everything.lock();
-    Dump("benchmark") << CommentCommand("CVC4 always dumps the most general, all-supported logic (below), as some internals might require the use of a logic more general than the input.")
-                      << SetBenchmarkLogicCommand(everything.getLogicString());
+    if (Dump.isOn("raw-benchmark")) {
+      Dump("raw-benchmark") << SetBenchmarkLogicCommand(d_logic.getLogicString());
+    } else {
+      LogicInfo everything;
+      everything.lock();
+      Dump("benchmark") << CommentCommand("CVC4 always dumps the most general, all-supported logic (below), as some internals might require the use of a logic more general than the input.")
+                        << SetBenchmarkLogicCommand(everything.getLogicString());
+    }
   }
 
   Trace("smt-debug") << "Dump declaration commands..." << std::endl;
@@ -4497,6 +4500,10 @@ Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore) throw(TypeChec
 
   Trace("smt") << "SmtEngine::assertFormula(" << ex << ")" << endl;
 
+  if (Dump.isOn("raw-benchmark")) {
+    Dump("raw-benchmark") << AssertCommand(ex);
+  }
+
   // Substitute out any abstract values in ex
   Expr e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr();
 
-- 
2.30.2