diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/util/options.cpp | 24 |
1 files changed, 12 insertions, 12 deletions
diff --git a/src/util/options.cpp b/src/util/options.cpp index e49ed77e9..314d85718 100644 --- a/src/util/options.cpp +++ b/src/util/options.cpp @@ -82,13 +82,13 @@ Options::Options() : replayFilename(""), replayStream(NULL), replayLog(NULL), - variableRemovalEnabled(false), - arithPropagation(false), + variableRemovalEnabled(true), + arithPropagation(true), satRandomFreq(0.0), satRandomSeed(91648253),// Minisat's default value pivotRule(MINIMUM), - arithPivotThreshold(10), - arithPropagateMaxLength(10) + arithPivotThreshold(16), + arithPropagateMaxLength(16) { } @@ -127,8 +127,8 @@ static const string optionsDescription = "\ --prop-row-length=N sets the maximum row length to be used in propagation\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\ - --enable-variable-removal enable permanent removal of variables in arithmetic (UNSAFE! experts only)\n\ - --enable-arithmetic-propagation turns on arithmetic propagation\n\ + --disable-variable-removal enable permanent removal of variables in arithmetic (UNSAFE! experts only)\n\ + --disable-arithmetic-propagation turns on arithmetic propagation\n\ --incremental enable incremental solving\n"; static const string languageDescription = "\ @@ -217,7 +217,7 @@ enum OptionValue { PIVOT_RULE, RANDOM_FREQUENCY, RANDOM_SEED, - ENABLE_VARIABLE_REMOVAL, + ARITHMETIC_VARIABLE_REMOVAL, ARITHMETIC_PROPAGATION, ARITHMETIC_PIVOT_THRESHOLD, ARITHMETIC_PROP_MAX_LENGTH @@ -290,8 +290,8 @@ static struct option cmdlineOptions[] = { { "prop-row-length" , required_argument, NULL, ARITHMETIC_PROP_MAX_LENGTH }, { "random-freq" , required_argument, NULL, RANDOM_FREQUENCY }, { "random-seed" , required_argument, NULL, RANDOM_SEED }, - { "enable-variable-removal", no_argument, NULL, ENABLE_VARIABLE_REMOVAL }, - { "enable-arithmetic-propagation", no_argument, NULL, ARITHMETIC_PROPAGATION }, + { "disable-variable-removal", no_argument, NULL, ARITHMETIC_VARIABLE_REMOVAL }, + { "disable-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! */ @@ -540,12 +540,12 @@ throw(OptionException) { #endif /* CVC4_REPLAY */ break; - case ENABLE_VARIABLE_REMOVAL: - variableRemovalEnabled = true; + case ARITHMETIC_VARIABLE_REMOVAL: + variableRemovalEnabled = false; break; case ARITHMETIC_PROPAGATION: - arithPropagation = true; + arithPropagation = false; break; case RANDOM_SEED: |