From 5f8b41a0b896c2224ac4fc3b13eba7c370764df6 Mon Sep 17 00:00:00 2001
From: Tim King <taking@cs.nyu.edu>
Date: Thu, 30 Jun 2011 19:06:57 +0000
Subject: [PATCH] Changed the defaults for arithPivotThreshold and
 arithPropagateMaxLength to 16. Enabled arithmetic propagation and variable
 removal by default. Changed the command line arguments for both propagation
 and variable removal allow for disabling these.

---
 src/util/options.cpp | 24 ++++++++++++------------
 1 file 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:
-- 
2.30.2