Brings the tuning branch into trunk. This includes the changes from restricted-simplex.

2 files changed, 76 insertions, 18 deletions

diff --git a/src/util/options.cpp b/src/util/options.cpp
index 06dc6769b..8961d5b57 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -122,8 +122,14 @@ Options::Options() :
   satRestartInc(3.0),
   arithUnateLemmaMode(ALL_PRESOLVE_LEMMAS),
   arithPropagationMode(BOTH_PROP),
-  arithPivotRule(MINIMUM),
-  arithPivotThreshold(16),
+  arithHeuristicPivots(0),
+  arithHeuristicPivotsSetByUser(false),
+  arithStandardCheckVarOrderPivots(-1),
+  arithStandardCheckVarOrderPivotsSetByUser(false),
+  arithHeuristicPivotRule(MINIMUM),
+  arithSimplexCheckPeriod(200),
+  arithPivotThreshold(2),
+  arithPivotThresholdSetByUser(false),
   arithPropagateMaxLength(16),
   arithDioSolver(true),
   arithRewriteEq(false),
@@ -239,12 +245,17 @@ Additional CVC4 options:\n\
    --restart-int-inc=F    restart interval increase factor for the sat solver\n\
                           (F=3.0 by default)\n\
   ARITHMETIC:\n\
-   ---unate-lemmas=MODE   determines which lemmas to add before solving\n\
+   --unate-lemmas=MODE   determines which lemmas to add before solving\n\
                           (default is 'all', see --unate-lemmas=help)\n\
    --arith-prop=MODE      turns on arithmetic propagation\n\
                           (default is 'old', see --arith-prop=help)\n\
-   --pivot-rule=RULE      change the pivot rule for the basic variable\n\
-                          (default is 'min', see --pivot-rule help)\n\
+   --heuristic-pivot-rule=RULE change the pivot rule for the basic variable\n\
+                          (default is 'min', see --heuristic-pivot-rule help)\n\
+   --heuristic-pivots=N   the number of times to apply the heuristic pivot rule.\n\
+                          If N < 0, this defaults to the number of variables\n\
+                          If this is unset, this is tuned by the logic selection.\n\
+   --simplex-check-period=N The number of pivots to do in simplex before rechecking for\n\
+                          a conflict on all variables.\n\
    --pivot-threshold=N    sets the number of pivots using --pivot-rule\n\
                           per basic variable per simplex instance before\n\
                           using variable order\n\
@@ -528,7 +539,10 @@ enum OptionValue {
   SAT_RESTART_INC,
   ARITHMETIC_UNATE_LEMMA_MODE,
   ARITHMETIC_PROPAGATION_MODE,
+  ARITHMETIC_HEURISTIC_PIVOTS,
+  ARITHMETIC_VAR_ORDER_PIVOTS,
   ARITHMETIC_PIVOT_RULE,
+  ARITHMETIC_CHECK_PERIOD,
   ARITHMETIC_PIVOT_THRESHOLD,
   ARITHMETIC_PROP_MAX_LENGTH,
   ARITHMETIC_DIO_SOLVER,
@@ -653,7 +667,10 @@ static struct option cmdlineOptions[] = {
   { "print-winner", no_argument     , NULL, PRINT_WINNER  },
   { "unate-lemmas", required_argument, NULL, ARITHMETIC_UNATE_LEMMA_MODE },
   { "arith-prop", required_argument, NULL, ARITHMETIC_PROPAGATION_MODE },
-  { "pivot-rule" , required_argument, NULL, ARITHMETIC_PIVOT_RULE  },
+  { "heuristic-pivots", required_argument, NULL, ARITHMETIC_HEURISTIC_PIVOTS },
+  { "heuristic-pivot-rule" , required_argument, NULL, ARITHMETIC_PIVOT_RULE  },
+  { "standard-effort-variable-order-pivots", required_argument, NULL, ARITHMETIC_VAR_ORDER_PIVOTS },
+  { "simplex-check-period" , required_argument, NULL, ARITHMETIC_CHECK_PERIOD  },
   { "pivot-threshold" , required_argument, NULL, ARITHMETIC_PIVOT_THRESHOLD  },
   { "prop-row-length" , required_argument, NULL, ARITHMETIC_PROP_MAX_LENGTH  },
   { "disable-dio-solver", no_argument, NULL, ARITHMETIC_DIO_SOLVER },
@@ -1370,27 +1387,42 @@ throw(OptionException) {
       }
       break;
 
+    case ARITHMETIC_HEURISTIC_PIVOTS:
+      arithHeuristicPivots = atoi(optarg);
+      arithHeuristicPivotsSetByUser = true;
+      break;
+
+    case ARITHMETIC_VAR_ORDER_PIVOTS:
+      arithStandardCheckVarOrderPivots = atoi(optarg);
+      arithStandardCheckVarOrderPivotsSetByUser = true;
+      break;
+
     case ARITHMETIC_PIVOT_RULE:
       if(!strcmp(optarg, "min")) {
-        arithPivotRule = MINIMUM;
+        arithHeuristicPivotRule = MINIMUM;
         break;
       } else if(!strcmp(optarg, "min-break-ties")) {
-        arithPivotRule = BREAK_TIES;
+        arithHeuristicPivotRule = BREAK_TIES;
         break;
       } else if(!strcmp(optarg, "max")) {
-        arithPivotRule = MAXIMUM;
+        arithHeuristicPivotRule = MAXIMUM;
         break;
       } else if(!strcmp(optarg, "help")) {
         puts(pivotRulesHelp.c_str());
         exit(1);
       } else {
-        throw OptionException(string("unknown option for --pivot-rule: `") +
-                              optarg + "'.  Try --pivot-rule help.");
+        throw OptionException(string("unknown option for --heuristic-pivot-rule: `") +
+                              optarg + "'.  Try --heuristic-pivot-rule help.");
       }
       break;
 
+    case ARITHMETIC_CHECK_PERIOD:
+      arithSimplexCheckPeriod = atoi(optarg);
+      break;
+
     case ARITHMETIC_PIVOT_THRESHOLD:
       arithPivotThreshold = atoi(optarg);
+      arithPivotThresholdSetByUser = true;
       break;
 
     case ARITHMETIC_PROP_MAX_LENGTH:
@@ -1601,7 +1633,7 @@ void Options::setInputLanguage(const char* str) throw(OptionException) {
   languageHelp = true;
 }
 
-std::ostream& operator<<(std::ostream& out, Options::ArithPivotRule rule) {
+std::ostream& operator<<(std::ostream& out, Options::ArithHeuristicPivotRule rule) {
   switch(rule) {
   case Options::MINIMUM:
     out << "MINIMUM";
diff --git a/src/util/options.h b/src/util/options.h
index fb5f71060..7dbba2439 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -266,15 +266,41 @@ struct CVC4_PUBLIC Options {
   typedef enum { NO_PROP, UNATE_PROP, BOUND_INFERENCE_PROP, BOTH_PROP} ArithPropagationMode;
   ArithPropagationMode arithPropagationMode;
 
-  /** The pivot rule for arithmetic */
-  typedef enum { MINIMUM, BREAK_TIES, MAXIMUM } ArithPivotRule;
-  ArithPivotRule arithPivotRule;
+  /**
+   * The maximum number of difference pivots to do per invokation of simplex.
+   * If this is negative, the number of pivots done is the number of variables.
+   * If this is not set by the user, different logics are free to chose different
+   * defaults.
+   */
+  int16_t arithHeuristicPivots;
+  bool arithHeuristicPivotsSetByUser;
+
+  /**
+   * The maximum number of variable order pivots to do per invokation of simplex.
+   * If this is negative, the number of pivots done is unlimited.
+   * If this is not set by the user, different logics are free to chose different
+   * defaults.
+   */
+  int16_t arithStandardCheckVarOrderPivots;
+  bool arithStandardCheckVarOrderPivotsSetByUser;
+
+  /** The heuristic pivot rule for arithmetic. */
+  typedef enum { MINIMUM, BREAK_TIES, MAXIMUM } ArithHeuristicPivotRule;
+  ArithHeuristicPivotRule arithHeuristicPivotRule;
+
+  /**
+   * The number of pivots before simplex rechecks every basic variable for a conflict.
+   */
+  uint16_t arithSimplexCheckPeriod;
 
   /**
-   * The number of pivots before Bland's pivot rule is used on a basic
-   * variable in arithmetic.
+   * This is the pivots per basic variable that can be done using heuristic choices
+   * before variable order must be used.
+   * If this is not set by the user, different logics are free to chose different
+   * defaults.
    */
   uint16_t arithPivotThreshold;
+  bool arithPivotThresholdSetByUser;
 
   /**
    * The maximum row length that arithmetic will use for propagation.
@@ -529,7 +555,7 @@ inline std::ostream& operator<<(std::ostream& out,
   return out;
 }
 
-std::ostream& operator<<(std::ostream& out, Options::ArithPivotRule rule) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream& out, Options::ArithHeuristicPivotRule rule) CVC4_PUBLIC;
 
 }/* CVC4 namespace */