diff options
author | Tim King <taking@cs.nyu.edu> | 2011-03-30 15:07:02 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2011-03-30 15:07:02 +0000 |
commit | 6495988f28ad6c9b318fc506e5d85d8613b03640 (patch) | |
tree | f8679ffdf53b9d38f307e03b34aed251ba37bfbd /src/util/options.cpp | |
parent | 10cabf82a20258da80be53eb6d23b1a536e82eb5 (diff) |
Added the command line flag --rewrite-arithmetic-equalities. This sets a static flag in Options that the ArithRewriter uses to determine the equality rewriting policy.
Diffstat (limited to 'src/util/options.cpp')
-rw-r--r-- | src/util/options.cpp | 11 |
1 files changed, 10 insertions, 1 deletions
diff --git a/src/util/options.cpp b/src/util/options.cpp index 6fc71bae3..94d479166 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -67,6 +67,7 @@ static const string optionsDescription = "\ --produce-models support the get-value command\n\ --produce-assignments support the get-assignment command\n\ --lazy-definition-expansion expand define-fun lazily\n\ + --rewrite-arithmetic-equalities rewrite (= x y) to (and (<= x y) (>= x y)) in arithmetic \n\ --incremental enable incremental solving\n"; static const string languageDescription = "\ @@ -121,7 +122,8 @@ enum OptionValue { LAZY_TYPE_CHECKING, EAGER_TYPE_CHECKING, INCREMENTAL, - PIVOT_RULE + PIVOT_RULE, + REWRITE_ARITHMETIC_EQUALITIES };/* enum OptionValue */ /** @@ -179,6 +181,7 @@ static struct option cmdlineOptions[] = { { "eager-type-checking", no_argument, NULL, EAGER_TYPE_CHECKING}, { "incremental", no_argument, NULL, INCREMENTAL}, { "pivot-rule" , required_argument, NULL, PIVOT_RULE }, + { "rewrite-arithmetic-equalities" , no_argument, NULL, REWRITE_ARITHMETIC_EQUALITIES}, { NULL , no_argument , NULL, '\0' } };/* if you add things to the above, please remember to update usage.h! */ @@ -376,6 +379,10 @@ throw(OptionException) { incrementalSolving = true; break; + case REWRITE_ARITHMETIC_EQUALITIES: + rewriteArithEqualities = true; + break; + case PIVOT_RULE: if(!strcmp(optarg, "min")) { pivotRule = MINIMUM; @@ -438,4 +445,6 @@ throw(OptionException) { return optind; } +bool Options::rewriteArithEqualities = false; + }/* CVC4 namespace */ |