Adds a hueristic from Alberto's thesis. For a fixed window the row count is used to select which non-basic variable is a row in made basic.

1 files changed, 8 insertions, 0 deletions

diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
index 758e5d92d..5e34ac1a2 100644
--- 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);