Merging the playground branch upto r1957 into trunk.

1 files changed, 18 insertions, 2 deletions

diff --git a/src/util/options.cpp b/src/util/options.cpp
index 32be9d6c9..e49ed77e9 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -86,7 +86,9 @@ Options::Options() :
   arithPropagation(false),
   satRandomFreq(0.0),
   satRandomSeed(91648253),// Minisat's default value
-  pivotRule(MINIMUM)
+  pivotRule(MINIMUM),
+  arithPivotThreshold(10),
+  arithPropagateMaxLength(10)
 {
 }
 
@@ -121,6 +123,8 @@ static const string optionsDescription = "\
    --replay=file          replay decisions from file\n\
    --replay-log=file      log decisions and propagations to file\n\
    --pivot-rule=RULE      change the pivot rule (see --pivot-rule help)\n\
+   --pivot-threshold=N   sets the number of heuristic pivots per variable per simplex instance\n\
+   --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\
@@ -214,7 +218,9 @@ enum OptionValue {
   RANDOM_FREQUENCY,
   RANDOM_SEED,
   ENABLE_VARIABLE_REMOVAL,
-  ARITHMETIC_PROPAGATION
+  ARITHMETIC_PROPAGATION,
+  ARITHMETIC_PIVOT_THRESHOLD,
+  ARITHMETIC_PROP_MAX_LENGTH
 };/* enum OptionValue */
 
 /**
@@ -280,6 +286,8 @@ static struct option cmdlineOptions[] = {
   { "lazy-type-checking", no_argument, NULL, LAZY_TYPE_CHECKING },
   { "eager-type-checking", no_argument, NULL, EAGER_TYPE_CHECKING },
   { "pivot-rule" , required_argument, NULL, PIVOT_RULE  },
+  { "pivot-threshold" , required_argument, NULL, ARITHMETIC_PIVOT_THRESHOLD  },
+  { "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 },
@@ -574,6 +582,14 @@ throw(OptionException) {
       }
       break;
 
+    case ARITHMETIC_PIVOT_THRESHOLD:
+      arithPivotThreshold = atoi(optarg);
+      break;
+
+    case ARITHMETIC_PROP_MAX_LENGTH:
+      arithPropagateMaxLength = atoi(optarg);
+      break;
+
     case SHOW_CONFIG:
       fputs(Configuration::about().c_str(), stdout);
       printf("\n");