From: Tim King <taking@cs.nyu.edu>
Date: Thu, 30 Jun 2011 19:06:57 +0000 (+0000)
Subject: Changed the defaults for arithPivotThreshold and arithPropagateMaxLength to 16. Enabl... 
X-Git-Tag: cvc5-1.0.0~8526
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5f8b41a0b896c2224ac4fc3b13eba7c370764df6;p=cvc5.git

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.
---

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: