Changed the defaults for arithPivotThreshold and arithPropagateMaxLength to 16. Enabl...

diff --git a/src/util/options.cpp b/src/util/options.cpp
index e49ed77e956dc9a51c2fa1226cd3327740504bc4..314d857187cd6f72de51e95e1203c2864a03cec5 100644 (file)
--- 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: