diff options
author | Clark Barrett <barrett@cs.stanford.edu> | 2016-12-05 16:07:07 -0800 |
---|---|---|
committer | Clark Barrett <barrett@cs.stanford.edu> | 2016-12-05 16:07:07 -0800 |
commit | 14ec91ed77b816d77de60fbf6e77066da194d791 (patch) | |
tree | 4198f7cee37f0b14d991311ddfbf6367e5309811 /src/smt/dump.cpp | |
parent | 44c278ce99b7d84b070d260196c44569209f1528 (diff) |
Added "dump=raw-benchmark" option for dumping all user commands exactly as received.
Diffstat (limited to 'src/smt/dump.cpp')
-rw-r--r-- | src/smt/dump.cpp | 25 |
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\ |