Adds a hueristic from Alberto's thesis. For a fixed window the row count is used...

diff --git a/src/theory/arith/row_vector.cpp b/src/theory/arith/row_vector.cpp
index 6835fc4352edf7274aa982cd8c732984e531f67d..f3b979bfd0326a60dc3d0d55767c8b33e2589822 100644 (file)
--- a/src/theory/arith/row_vector.cpp
+++ b/src/theory/arith/row_vector.cpp
@@ -5,6 +5,31 @@ using namespace CVC4;
 using namespace CVC4::theory;
 using namespace CVC4::theory::arith ;
 
+bool RowVector::isSorted(const VarCoeffArray& arr, bool strictlySorted) {
+  if(arr.size() >= 2){
+    NonZeroIterator curr = arr.begin();
+    NonZeroIterator end = arr.end();
+    ArithVar prev = getArithVar(*curr);
+    ++curr;
+    for(;curr != end; ++curr){
+      ArithVar v = getArithVar(*curr);
+      if(strictlySorted && prev > v) return false;
+      if(!strictlySorted && prev >= v) return false;
+      prev = v;
+    }
+  }
+  return true;
+}
+
+bool RowVector::noZeroCoefficients(const VarCoeffArray& arr){
+  for(NonZeroIterator curr = arr.begin(), end = arr.end();
+      curr != end; ++curr){
+    const Rational& coeff = getCoefficient(*curr);
+    if(coeff == 0) return false;
+  }
+  return true;
+}
+
 void RowVector::zip(const vector< ArithVar >& variables,
                     const vector< Rational >& coefficients,
                     VarCoeffArray& output){
@@ -24,16 +49,26 @@ void RowVector::zip(const vector< ArithVar >& variables,
 }
 
 RowVector::RowVector(const vector< ArithVar >& variables,
-                     const vector< Rational >& coefficients){
+                     const vector< Rational >& coefficients,
+                     std::vector<uint32_t>& counts):
+  d_rowCount(counts)
+{
   zip(variables, coefficients, d_entries);
 
   std::sort(d_entries.begin(), d_entries.end(), cmp);
 
+  for(NonZeroIterator i=beginNonZero(), end=endNonZero(); i != end; ++i){
+    ++d_rowCount[getArithVar(*i)];
+  }
+
   Assert(isSorted(d_entries, true));
   Assert(noZeroCoefficients(d_entries));
 }
 
-void RowVector::merge(VarCoeffArray& arr, const VarCoeffArray& other, const Rational& c){
+void RowVector::merge(VarCoeffArray& arr,
+                      const VarCoeffArray& other,
+                      const Rational& c,
+                      std::vector<uint32_t>& counts){
   VarCoeffArray copy = arr;
   arr.clear();
 
@@ -48,12 +83,18 @@ void RowVector::merge(VarCoeffArray& arr, const VarCoeffArray& other, const Rati
       arr.push_back(*curr1);
       ++curr1;
     }else if(getArithVar(*curr1) > getArithVar(*curr2)){
+      ++counts[getArithVar(*curr2)];
+
       arr.push_back( make_pair(getArithVar(*curr2), c * getCoefficient(*curr2)));
       ++curr2;
     }else{
       Rational res = getCoefficient(*curr1) + c * getCoefficient(*curr2);
       if(res != 0){
+        ++counts[getArithVar(*curr2)];
+
         arr.push_back(make_pair(getArithVar(*curr1), res));
+      }else{
+        --counts[getArithVar(*curr2)];
       }
       ++curr1;
       ++curr2;
@@ -64,6 +105,8 @@ void RowVector::merge(VarCoeffArray& arr, const VarCoeffArray& other, const Rati
     ++curr1;
   }
   while(curr2 != end2){
+    ++counts[getArithVar(*curr2)];
+
     arr.push_back(make_pair(getArithVar(*curr2), c * getCoefficient(*curr2)));
     ++curr2;
   }
@@ -80,7 +123,7 @@ void RowVector::multiply(const Rational& c){
 void RowVector::addRowTimesConstant(const Rational& c, const RowVector& other){
   Assert(c != 0);
 
-  merge(d_entries, other.d_entries, c);
+  merge(d_entries, other.d_entries, c, d_rowCount);
 }
 
 void RowVector::printRow(){
@@ -93,14 +136,15 @@ void RowVector::printRow(){
 
 ReducedRowVector::ReducedRowVector(ArithVar basic,
                                    const vector<ArithVar>& variables,
-                                   const vector<Rational>& coefficients):
-  RowVector(variables, coefficients), d_basic(basic){
+                                   const vector<Rational>& coefficients,
+                                   std::vector<uint32_t>& count):
+  RowVector(variables, coefficients, count), d_basic(basic){
 
 
   VarCoeffArray justBasic;
   justBasic.push_back(make_pair(basic, Rational(-1)));
 
-  merge(d_entries,justBasic, Rational(1));
+  merge(d_entries,justBasic, Rational(1), d_rowCount);
 
   Assert(wellFormed());
 }

diff --git a/src/theory/arith/row_vector.h b/src/theory/arith/row_vector.h
index d68f8bc30ba23c0e21c27f57d2995a4861b1e4a4..efb64d1c72d5c436df009ef5b1e187fb34403626 100644 (file)
--- a/src/theory/arith/row_vector.h
+++ b/src/theory/arith/row_vector.h
@@ -36,34 +36,13 @@ public:
    * isSorted(arr, strictlySorted) is then equivalent to
    * If i<j, cmp(getArithVar(d_entries[i]), getArithVar(d_entries[j])) <= c.
    */
-  static bool isSorted(const VarCoeffArray& arr, bool strictlySorted) {
-    if(arr.size() >= 2){
-      NonZeroIterator curr = arr.begin();
-      NonZeroIterator end = arr.end();
-      ArithVar prev = getArithVar(*curr);
-      ++curr;
-      for(;curr != end; ++curr){
-        ArithVar v = getArithVar(*curr);
-        if(strictlySorted && prev > v) return false;
-        if(!strictlySorted && prev >= v) return false;
-        prev = v;
-      }
-    }
-    return true;
-  }
+  static bool isSorted(const VarCoeffArray& arr, bool strictlySorted);
 
   /**
    * noZeroCoefficients(arr) is equivalent to
    *  0 != getCoefficient(arr[i]) for all i.
    */
-  static bool noZeroCoefficients(const VarCoeffArray& arr){
-    for(NonZeroIterator curr = arr.begin(), end = arr.end();
-        curr != end; ++curr){
-      const Rational& coeff = getCoefficient(*curr);
-      if(coeff == 0) return false;
-    }
-    return true;
-  }
+  static bool noZeroCoefficients(const VarCoeffArray& arr);
 
   /**
    * Zips together an array of variables and coefficients and appends
@@ -73,7 +52,7 @@ public:
                   const std::vector< Rational >& coefficients,
                   VarCoeffArray& output);
 
-  static void merge(VarCoeffArray& arr, const VarCoeffArray& other, const Rational& c);
+  static void merge(VarCoeffArray& arr, const VarCoeffArray& other, const Rational& c, std::vector<uint32_t>& count);
 
 
 protected:
@@ -84,6 +63,8 @@ protected:
    */
   VarCoeffArray d_entries;
 
+  std::vector<uint32_t>& d_rowCount;
+
   NonZeroIterator lower_bound(ArithVar x_j) const{
     return std::lower_bound(d_entries.begin(), d_entries.end(), make_pair(x_j,0), cmp);
   }
@@ -92,10 +73,11 @@ protected:
 
 public:
 
-  RowVector() : d_entries() {}
+  //RowVector() : d_entries() {}
 
   RowVector(const std::vector< ArithVar >& variables,
-            const std::vector< Rational >& coefficients);
+            const std::vector< Rational >& coefficients,
+            std::vector<uint32_t>& counts);
 
 
   //Iterates over the nonzero entries in the Vector
@@ -154,7 +136,8 @@ public:
 
   ReducedRowVector(ArithVar basic,
                    const std::vector< ArithVar >& variables,
-                   const std::vector< Rational >& coefficients);
+                   const std::vector< Rational >& coefficients,
+                   std::vector<uint32_t>& count);
 
 
   ArithVar basic() const{

diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index e435fd3dc9e9aabd5ebd91e0ea07242334c2a9be..e30d935f317e80e42b202deaf88d5a034aa9ade2 100644 (file)
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -306,6 +306,9 @@ template <bool above>
 ArithVar SimplexDecisionProcedure::selectSlack(ArithVar x_i){
   ReducedRowVector* row_i = d_tableau.lookup(x_i);
 
+  ArithVar slack = ARITHVAR_SENTINEL;
+  uint32_t numRows = std::numeric_limits<uint32_t>::max();
+
   for(ReducedRowVector::NonZeroIterator nbi = row_i->beginNonZero(), end = row_i->endNonZero();
       nbi != end; ++nbi){
     ArithVar nonbasic = getArithVar(*nbi);
@@ -315,24 +318,63 @@ ArithVar SimplexDecisionProcedure::selectSlack(ArithVar x_i){
     int cmp = a_ij.cmp(d_constants.d_ZERO);
     if(above){ // beta(x_i) > u_i
       if( cmp < 0 && d_partialModel.strictlyBelowUpperBound(nonbasic)){
-        return nonbasic;
+        if(d_pivotStage){
+          if(d_tableau.getRowCount(nonbasic) < numRows){
+            slack = nonbasic;
+            numRows = d_tableau.getRowCount(nonbasic);
+          }
+        }else{
+          slack = nonbasic; break;
+        }
       }else if( cmp > 0 && d_partialModel.strictlyAboveLowerBound(nonbasic)){
-        return nonbasic;
+        if(d_pivotStage){
+          if(d_tableau.getRowCount(nonbasic) < numRows){
+            slack = nonbasic;
+            numRows = d_tableau.getRowCount(nonbasic);
+          }
+        }else{
+          slack = nonbasic; break;
+        }
       }
     }else{ //beta(x_i) < l_i
       if(cmp > 0 && d_partialModel.strictlyBelowUpperBound(nonbasic)){
-        return nonbasic;
-      }else if(cmp < 0 && d_partialModel.strictlyAboveLowerBound(nonbasic)){
-        return nonbasic;
+        if(d_pivotStage){
+          if(d_tableau.getRowCount(nonbasic) < numRows){
+            slack = nonbasic;
+            numRows = d_tableau.getRowCount(nonbasic);
+          }
+        }else{
+          slack = nonbasic; break;
+        }
+      }else if(cmp < 0 && d_partialModel.strictlyAboveLowerBound(nonbasic)){if(d_pivotStage){
+          if(d_tableau.getRowCount(nonbasic) < numRows){
+            slack = nonbasic;
+            numRows = d_tableau.getRowCount(nonbasic);
+          }
+        }else{
+          slack = nonbasic; break;
+        }
       }
     }
   }
-  return ARITHVAR_SENTINEL;
+
+  return slack;
 }
 
 Node SimplexDecisionProcedure::updateInconsistentVars(){
+  Node possibleConflict = privateUpdateInconsistentVars();
+  Assert(!possibleConflict.isNull() || d_griggioRuleQueue.empty());
+  Assert(!possibleConflict.isNull() || d_possiblyInconsistent.empty());
   d_pivotStage = true;
-  return privateUpdateInconsistentVars();
+
+  while(!d_griggioRuleQueue.empty()){
+    d_griggioRuleQueue.pop();
+  }
+  while(!d_possiblyInconsistent.empty()){
+    d_possiblyInconsistent.pop();
+  }
+
+  return possibleConflict;
 }
 
 //corresponds to Check() in dM06

diff --git a/src/theory/arith/simplex.h b/src/theory/arith/simplex.h
index 440d7063cdf08d79ec9e43873e9913bd97cadd11..e753ebc28b7ab5918c5e114da4104aa94934fd0c 100644 (file)
--- a/src/theory/arith/simplex.h
+++ b/src/theory/arith/simplex.h
@@ -75,7 +75,8 @@ public:
     d_activityMonitor(am),
     d_out(out),
     d_tableau(tableau),
-    d_numVariables(0)
+    d_numVariables(0),
+    d_pivotStage(true)
   {}
 
   void increaseMax() {d_numVariables++;}

diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp
index 3c1cd36ba922db188e5135209667502ae4708ab6..1d58c5e1dd12475df876090c133c8269cd9db585 100644 (file)
--- a/src/theory/arith/tableau.cpp
+++ b/src/theory/arith/tableau.cpp
@@ -34,7 +34,7 @@ void Tableau::addRow(ArithVar basicVar,
   //The new basic variable cannot already be a basic variable
   Assert(!isActiveBasicVariable(basicVar));
   d_activeBasicVars.insert(basicVar);
-  ReducedRowVector* row_current = new ReducedRowVector(basicVar,variables, coeffs);
+  ReducedRowVector* row_current = new ReducedRowVector(basicVar,variables, coeffs,d_rowCount);
   d_rowsTable[basicVar] = row_current;
 
   //A variable in the row may have been made non-basic already.

diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
index 758e5d92d1ab262756ff15d584bd7a9139b529dc..5e34ac1a296e9efa33f5e02edc1a6fd9a329960a 100644 (file)
--- a/src/theory/arith/tableau.h
+++ b/src/theory/arith/tableau.h
@@ -97,6 +97,8 @@ private:
   ActivityMonitor& d_activityMonitor;
   ArithVarDenseSet& d_basicManager;
 
+  std::vector<uint32_t> d_rowCount;
+
 public:
   /**
    * Constructs an empty tableau.
@@ -111,6 +113,7 @@ public:
   void increaseSize(){
     d_activeBasicVars.increaseSize();
     d_rowsTable.push_back(NULL);
+    d_rowCount.push_back(0);
   }
 
   ArithVarSet::iterator begin(){
@@ -133,6 +136,11 @@ private:
   }
 public:
 
+  uint32_t getRowCount(ArithVar x){
+    Assert(x < d_rowCount.size());
+    return d_rowCount[x];
+  }
+
   void addRow(ArithVar basicVar,
               const std::vector<Rational>& coeffs,
               const std::vector<ArithVar>& variables);