diff options
Diffstat (limited to 'src/util/options.cpp')
-rw-r--r-- | src/util/options.cpp | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/util/options.cpp b/src/util/options.cpp index f68b64ab6..337eba9b6 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -82,7 +82,7 @@ Options::Options() : replayFilename(""), replayStream(NULL), replayLog(NULL), - rewriteArithEqualities(false), + variableRemovalEnabled(false), arithPropagation(false), satRandomFreq(0.0), satRandomSeed(91648253),// Minisat's default value @@ -123,7 +123,7 @@ static const string optionsDescription = "\ --pivot-rule=RULE change the pivot rule (see --pivot-rule help)\n\ --random-freq=P sets the frequency of random decisions in the sat solver(P=0.0 by default)\n\ --random-seed=S sets the random seed for the sat solver\n\ - --rewrite-arithmetic-equalities rewrite (= x y) to (and (<= x y) (>= x y)) in arithmetic\n\ + --variable-removal-enables enable permanent removal of variables in arithmetic (UNSAFE! experts only)\n\ --enable-arithmetic-propagation turns on arithmetic propagation\n\ --incremental enable incremental solving\n"; @@ -213,7 +213,7 @@ enum OptionValue { PIVOT_RULE, RANDOM_FREQUENCY, RANDOM_SEED, - REWRITE_ARITHMETIC_EQUALITIES, + ENABLE_VARIABLE_REMOVAL, ARITHMETIC_PROPAGATION };/* enum OptionValue */ @@ -282,7 +282,7 @@ static struct option cmdlineOptions[] = { { "pivot-rule" , required_argument, NULL, PIVOT_RULE }, { "random-freq" , required_argument, NULL, RANDOM_FREQUENCY }, { "random-seed" , required_argument, NULL, RANDOM_SEED }, - { "rewrite-arithmetic-equalities", no_argument, NULL, REWRITE_ARITHMETIC_EQUALITIES }, + { "enable-variable-removel", no_argument, NULL, ENABLE_VARIABLE_REMOVAL }, { "enable-arithmetic-propagation", no_argument, NULL, ARITHMETIC_PROPAGATION }, { NULL , no_argument , NULL, '\0' } };/* if you add things to the above, please remember to update usage.h! */ @@ -532,8 +532,8 @@ throw(OptionException) { #endif /* CVC4_REPLAY */ break; - case REWRITE_ARITHMETIC_EQUALITIES: - rewriteArithEqualities = true; + case ENABLE_VARIABLE_REMOVAL: + variableRemovalEnabled = true; break; case ARITHMETIC_PROPAGATION: |