Merging the playground branch upto r1957 into trunk.

5 files changed, 212 insertions, 20 deletions

diff --git a/src/theory/arith/arithvar_set.h b/src/theory/arith/arithvar_set.h
index 4cd205172..f8a23fee0 100644
--- a/src/theory/arith/arithvar_set.h
+++ b/src/theory/arith/arithvar_set.h
@@ -179,6 +179,151 @@ public:
 typedef ArithVarSetImpl<false> ArithVarSet;
 typedef ArithVarSetImpl<true> PermissiveBackArithVarSet;
 
+
+/**
+ * ArithVarMultiset
+ */
+class ArithVarMultiset {
+public:
+  typedef std::vector<ArithVar> VarList;
+private:
+  //List of the ArithVars in the multi set.
+  VarList d_list;
+
+  //Each ArithVar in the set is mapped to its position in d_list.
+  //Each ArithVar not in the set is mapped to ARITHVAR_SENTINEL
+  std::vector<unsigned> d_posVector;
+
+  //Count of the number of elements in the array
+  std::vector<unsigned> d_counts;
+
+public:
+  typedef VarList::const_iterator const_iterator;
+
+  ArithVarMultiset() :  d_list(), d_posVector() {}
+
+  size_t size() const {
+    return d_list.size();
+  }
+
+  bool empty() const {
+    return d_list.empty();
+  }
+
+  size_t allocated() const {
+    Assert(d_posVector.size() == d_counts.size());
+    return d_posVector.size();
+  }
+
+  void purge() {
+    for(VarList::const_iterator i=d_list.begin(), endIter=d_list.end(); i!= endIter; ++i){
+      d_posVector[*i] = ARITHVAR_SENTINEL;
+      d_counts[*i] = 0;
+    }
+    d_list.clear();
+    Assert(empty());
+  }
+
+  void increaseSize(ArithVar max){
+    Assert(max >= allocated());
+    d_posVector.resize(max+1, ARITHVAR_SENTINEL);
+    d_counts.resize(max+1, 0);
+  }
+
+  void increaseSize(){
+    increaseSize(allocated());
+  }
+
+  bool isMember(ArithVar x) const{
+    if( x >=  allocated()){
+      return false;
+    }else{
+      Assert(x <  allocated());
+      return d_posVector[x] != ARITHVAR_SENTINEL;
+    }
+  }
+
+  /** Invalidates iterators */
+  /* void init(ArithVar x, bool val) { */
+  /*   Assert(x >= allocated()); */
+  /*   increaseSize(x); */
+  /*   if(val){ */
+  /*     add(x); */
+  /*   } */
+  /* } */
+
+  /**
+   * Invalidates iterators.
+   */
+  void addMultiset(ArithVar x){
+    if( x >=  allocated()){
+      increaseSize(x);
+    }
+    if(d_counts[x] == 0){
+      d_posVector[x] = size();
+      d_list.push_back(x);
+    }
+    d_counts[x]++;
+  }
+
+  unsigned count(ArithVar x){
+    if( x >=  allocated()){
+      return 0;
+    }else{
+      return d_counts[x];
+    }
+  }
+
+  const_iterator begin() const{ return d_list.begin(); }
+  const_iterator end() const{ return d_list.end(); }
+
+  const VarList& getList() const{
+    return d_list;
+  }
+
+  /** Invalidates iterators */
+  void remove(ArithVar x){
+    Assert(isMember(x));
+    swapToBack(x);
+    Assert(d_list.back() == x);
+    pop_back();
+  }
+
+  ArithVar pop_back() {
+    Assert(!empty());
+    ArithVar atBack = d_list.back();
+    d_posVector[atBack] = ARITHVAR_SENTINEL;
+    d_counts[atBack] = 0;
+    d_list.pop_back();
+    return atBack;
+  }
+
+ private:
+
+  /** This should be true of all x < allocated() after every operation. */
+  bool wellFormed(ArithVar x){
+    if(d_posVector[x] == ARITHVAR_SENTINEL){
+      return true;
+    }else{
+      return d_list[d_posVector[x]] == x;
+    }
+  }
+
+  /** Swaps a member x to the back of d_list. */
+  void swapToBack(ArithVar x){
+    Assert(isMember(x));
+
+    unsigned currentPos = d_posVector[x];
+    ArithVar atBack = d_list.back();
+
+    d_list[currentPos] = atBack;
+    d_posVector[atBack] = currentPos;
+
+    d_list[size() - 1] = x;
+    d_posVector[x] = size() - 1;
+  }
+};
+
 }; /* namespace arith */
 }; /* namespace theory */
 }; /* namespace CVC4 */
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index 113e80c27..3e2d90674 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -23,6 +23,7 @@ SimplexDecisionProcedure::SimplexDecisionProcedure(ArithPropManager& propManager
   d_propManager(propManager),
   d_numVariables(0),
   d_delayedLemmas(),
+  d_pivotsInRound(),
   d_ZERO(0),
   d_DELTA_ZERO(0,0)
 {
@@ -377,7 +378,8 @@ void SimplexDecisionProcedure::propagateCandidates(){
   PermissiveBackArithVarSet::const_iterator end = d_updatedBounds.end();
   for(; i != end; ++i){
     ArithVar var = *i;
-    if(d_tableau.isBasic(var)){
+    if(d_tableau.isBasic(var) &&
+       d_tableau.getRowLength(var) <= Options::current()->arithPropagateMaxLength){
       d_candidateBasics.softAdd(var);
     }else{
       Tableau::ColIterator basicIter = d_tableau.colIterator(var);
@@ -386,7 +388,9 @@ void SimplexDecisionProcedure::propagateCandidates(){
         ArithVar rowVar = entry.getRowVar();
         Assert(entry.getColVar() == var);
         Assert(d_tableau.isBasic(rowVar));
-        d_candidateBasics.softAdd(rowVar);
+        if(d_tableau.getRowLength(rowVar) <= Options::current()->arithPropagateMaxLength){
+          d_candidateBasics.softAdd(rowVar);
+        }
       }
     }
   }
@@ -395,7 +399,7 @@ void SimplexDecisionProcedure::propagateCandidates(){
   while(!d_candidateBasics.empty()){
     ArithVar candidate = d_candidateBasics.pop_back();
     Assert(d_tableau.isBasic(candidate));
-    propagateCandidate(candidate);
+    propagateCandidate(candidate); 
   }
 }
 
@@ -521,8 +525,8 @@ ArithVar SimplexDecisionProcedure::minBoundAndRowCount(const SimplexDecisionProc
   }
 }
 
-template <bool above, SimplexDecisionProcedure::PreferenceFunction pref>
-ArithVar SimplexDecisionProcedure::selectSlack(ArithVar x_i){
+template <bool above>
+ArithVar SimplexDecisionProcedure::selectSlack(ArithVar x_i, SimplexDecisionProcedure::PreferenceFunction pref){
   ArithVar slack = ARITHVAR_SENTINEL;
 
   for(Tableau::RowIterator iter = d_tableau.rowIterator(x_i); !iter.atEnd();  ++iter){
@@ -616,7 +620,7 @@ Node SimplexDecisionProcedure::updateInconsistentVars(){
           possibleConflict.isNull() &&
           pivotsRemaining > 0){
       uint32_t pivotsToDo = min(pivotsPerCheck, pivotsRemaining);
-      possibleConflict = searchForFeasibleSolution<minBoundAndRowCount>(pivotsToDo);
+      possibleConflict = searchForFeasibleSolution(pivotsToDo);
       pivotsRemaining -= pivotsToDo;
       //Once every CHECK_PERIOD examine the entire queue for conflicts
       if(possibleConflict.isNull()){
@@ -631,7 +635,7 @@ Node SimplexDecisionProcedure::updateInconsistentVars(){
     d_queue.transitionToVariableOrderMode();
 
     while(!d_queue.empty() && possibleConflict.isNull()){
-      possibleConflict = searchForFeasibleSolution<minVarOrder>(VARORDER_CHECK_PERIOD);
+      possibleConflict = searchForFeasibleSolution(VARORDER_CHECK_PERIOD);
 
       //Once every CHECK_PERIOD examine the entire queue for conflicts
       if(possibleConflict.isNull()){
@@ -647,6 +651,7 @@ Node SimplexDecisionProcedure::updateInconsistentVars(){
   // Curiously the invariant that we always do a full check
   // means that the assignment we can always empty these queues.
   d_queue.clear();
+  d_pivotsInRound.purge();
 
   Assert(!d_queue.inCollectionMode());
   d_queue.transitionToCollectionMode();
@@ -666,12 +671,12 @@ Node SimplexDecisionProcedure::checkBasicForConflict(ArithVar basic){
   const DeltaRational& beta = d_partialModel.getAssignment(basic);
 
   if(d_partialModel.belowLowerBound(basic, beta, true)){
-    ArithVar x_j = selectSlackUpperBound<minVarOrder>(basic);
+    ArithVar x_j = selectSlackUpperBound(basic);
     if(x_j == ARITHVAR_SENTINEL ){
       return generateConflictBelowLowerBound(basic);
     }
   }else if(d_partialModel.aboveUpperBound(basic, beta, true)){
-    ArithVar x_j = selectSlackLowerBound<minVarOrder>(basic);
+    ArithVar x_j = selectSlackLowerBound(basic);
     if(x_j == ARITHVAR_SENTINEL ){
       return generateConflictAboveUpperBound(basic);
     }
@@ -680,7 +685,7 @@ Node SimplexDecisionProcedure::checkBasicForConflict(ArithVar basic){
 }
 
 //corresponds to Check() in dM06
-template <SimplexDecisionProcedure::PreferenceFunction pf>
+//template <SimplexDecisionProcedure::PreferenceFunction pf>
 Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingIterations){
   Debug("arith") << "updateInconsistentVars" << endl;
   Assert(remainingIterations > 0);
@@ -697,11 +702,24 @@ Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera
 
     --remainingIterations;
 
+    bool useVarOrderPivot = d_pivotsInRound.count(x_i) >=  Options::current()->arithPivotThreshold;
+    if(!useVarOrderPivot){
+      d_pivotsInRound.addMultiset(x_i);
+    }
+
+
+    Debug("playground") << "pivots in rounds: " <<  d_pivotsInRound.count(x_i)
+                        << " use " << useVarOrderPivot
+                        << " threshold " << Options::current()->arithPivotThreshold
+                        << endl;
+
+    PreferenceFunction pf = useVarOrderPivot ? minVarOrder : minBoundAndRowCount;
+
     DeltaRational beta_i = d_partialModel.getAssignment(x_i);
     ArithVar x_j = ARITHVAR_SENTINEL;
 
     if(d_partialModel.belowLowerBound(x_i, beta_i, true)){
-      x_j = selectSlackUpperBound<pf>(x_i);
+      x_j = selectSlackUpperBound(x_i, pf);
       if(x_j == ARITHVAR_SENTINEL ){
         ++(d_statistics.d_statUpdateConflicts);
         return generateConflictBelowLowerBound(x_i); //unsat
@@ -710,7 +728,7 @@ Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera
       pivotAndUpdate(x_i, x_j, l_i);
 
     }else if(d_partialModel.aboveUpperBound(x_i, beta_i, true)){
-      x_j = selectSlackLowerBound<pf>(x_i);
+      x_j = selectSlackLowerBound(x_i, pf);
       if(x_j == ARITHVAR_SENTINEL ){
         ++(d_statistics.d_statUpdateConflicts);
         return generateConflictAboveUpperBound(x_i); //unsat
diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index f0dc5d62e..b3f43baf1 100644
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -43,6 +43,8 @@ private:
   PermissiveBackArithVarSet d_updatedBounds;
   PermissiveBackArithVarSet d_candidateBasics;
 
+  ArithVarMultiset d_pivotsInRound;
+
   Rational d_ZERO;
   DeltaRational d_DELTA_ZERO;
 
@@ -139,7 +141,7 @@ public:
    */
   Node updateInconsistentVars();
 private:
-  template <PreferenceFunction> Node searchForFeasibleSolution(uint32_t maxIterations);
+  Node searchForFeasibleSolution(uint32_t maxIterations);
 
   enum SearchPeriod {BeforeDiffSearch, DuringDiffSearch, AfterDiffSearch, DuringVarOrderSearch, AfterVarOrderSearch};
 
@@ -159,12 +161,12 @@ private:
    * - !lowerBound && a_ij < 0 && assignment(x_j) > lowerbound(x_j)
    *
    */
-  template <bool lowerBound, PreferenceFunction>  ArithVar selectSlack(ArithVar x_i);
-  template <PreferenceFunction pf> ArithVar selectSlackLowerBound(ArithVar x_i) {
-    return selectSlack<true, pf>(x_i);
+  template <bool lowerBound>  ArithVar selectSlack(ArithVar x_i, PreferenceFunction pf);
+  ArithVar selectSlackLowerBound(ArithVar x_i, PreferenceFunction pf = minVarOrder) {
+    return selectSlack<true>(x_i, pf);
   }
-  template <PreferenceFunction pf> ArithVar selectSlackUpperBound(ArithVar x_i) {
-    return selectSlack<false, pf>(x_i);
+  ArithVar selectSlackUpperBound(ArithVar x_i, PreferenceFunction pf = minVarOrder) {
+    return selectSlack<false>(x_i, pf);
   }
   /**
    * Returns the smallest basic variable whose assignment is not consistent
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");
diff --git a/src/util/options.h b/src/util/options.h
index b8d21f2b0..a5e03d21b 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -181,6 +181,17 @@ struct CVC4_PUBLIC Options {
   typedef enum { MINIMUM, BREAK_TIES, MAXIMUM } ArithPivotRule;
   ArithPivotRule pivotRule;
 
+  /**
+   * The number of pivots before Bland's pivot rule is used on a basic
+   * variable in arithmetic.
+   */
+  uint16_t arithPivotThreshold;
+
+  /**
+   * The maximum row length that arithmetic will use for propagation.
+   */
+  uint16_t arithPropagateMaxLength;
+
   Options();
 
   /**