diff options
| -rw-r--r-- | src/smt/dump.cpp | 25 | ||||
| -rw-r--r-- | 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(); |