summaryrefslogtreecommitdiff
path: root/src/smt/options_handlers.h
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2012-11-27 05:52:21 +0000
committerMorgan Deters <mdeters@gmail.com>2012-11-27 05:52:21 +0000
commit41fc06dc6352a847f047970e63e46455eb4dd050 (patch)
tree92f08943a4782f24f0cb44935d612b400a612592 /src/smt/options_handlers.h
parentb122cec27ca27d0b48e786191448e0053be78ed0 (diff)
First chunk of boolean-terms support.
Passes simple tests and doesn't break existing functionality. Still need some work merged in for models. This version enables BV except for pure arithmetic (since we might otherwise need Boolean term support, which uses BV). Tonight's nightly regression run should tell us if/how that hurts performance. (this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/smt/options_handlers.h')
-rw-r--r--src/smt/options_handlers.h3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h
index 68b7222d7..a3065f29b 100644
--- a/src/smt/options_handlers.h
+++ b/src/smt/options_handlers.h
@@ -82,7 +82,7 @@ assertions\n\
+ Output the assertions after preprocessing and before clausification.\n\
Can also specify \"assertions:pre-PASS\" or \"assertions:post-PASS\",\n\
where PASS is one of the preprocessing passes: definition-expansion\n\
- constrain-subtypes substitution skolem-quant simplify\n\
+ boolean-terms constrain-subtypes substitution skolem-quant simplify\n\
static-learning ite-removal repeat-simplify theory-preprocessing.\n\
PASS can also be the special value \"everything\", in which case the\n\
assertions are printed before any preprocessing (with\n\
@@ -176,6 +176,7 @@ inline void dumpMode(std::string option, std::string optarg, SmtEngine* smt) {
}
if(!strcmp(p, "everything")) {
} else if(!strcmp(p, "definition-expansion")) {
+ } else if(!strcmp(p, "boolean-terms")) {
} else if(!strcmp(p, "constrain-subtypes")) {
} else if(!strcmp(p, "substitution")) {
} else if(!strcmp(p, "skolem-quant")) {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback