Small tableau optimization.

3 files changed, 87 insertions, 50 deletions

diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp
index df80c1118..aaeadb629 100644
--- a/src/theory/arith/tableau.cpp
+++ b/src/theory/arith/tableau.cpp
@@ -48,7 +48,6 @@ Row::Row(ArithVar basic,
     Assert(d_coeffs[var_i] != Rational(0,1));
   }
 }
-
 void Row::subsitute(Row& row_s){
   ArithVar x_s = row_s.basicVar();
 
@@ -115,7 +114,7 @@ void Tableau::addRow(ArithVar basicVar,
   Assert(!isActiveBasicVariable(basicVar));
   d_activeBasicVars.insert(basicVar);
   Row* row_current = new Row(basicVar,coeffs,variables);
-  d_activeRows[basicVar] = row_current;
+  d_rowsTable[basicVar] = row_current;
 
   //A variable in the row may have been made non-basic already.
   //If this is the case we fake pivoting this variable
@@ -143,23 +142,22 @@ void Tableau::pivot(ArithVar x_r, ArithVar x_s){
   Assert(d_basicManager.isBasic(x_r));
   Assert(!d_basicManager.isBasic(x_s));
 
-  RowsTable::iterator ptrRow_r = d_activeRows.find(x_r);
-  Assert(ptrRow_r != d_activeRows.end());
-
-  Row* row_s = (*ptrRow_r).second;
-
+  Row* row_s = lookup(x_r);
   Assert(row_s->has(x_s));
-  row_s->pivot(x_s);
 
-  d_activeRows.erase(ptrRow_r);
+  //Swap x_r and x_s in d_activeRows
+  d_rowsTable[x_s] = row_s;
+  d_rowsTable[x_r] = NULL;
+
   d_activeBasicVars.erase(x_r);
   d_basicManager.makeNonbasic(x_r);
 
-  d_activeRows.insert(std::make_pair(x_s,row_s));
   d_activeBasicVars.insert(x_s);
   d_basicManager.makeBasic(x_s);
 
-  for(VarSet::iterator basicIter = begin(), endIter = end();
+  row_s->pivot(x_s);
+
+  for(ArithVarSet::iterator basicIter = begin(), endIter = end();
       basicIter != endIter; ++basicIter){
     ArithVar basic = *basicIter;
     Row* row_k = lookup(basic);
@@ -169,19 +167,16 @@ void Tableau::pivot(ArithVar x_r, ArithVar x_s){
     }
   }
 }
-
 void Tableau::printTableau(){
-  for(VarSet::iterator basicIter = begin(), endIter = end();
-      basicIter != endIter; ++basicIter){
-    ArithVar basic = *basicIter;
-    Row* row_k = lookup(basic);
-    row_k->printRow();
-  }
-  for(RowsTable::iterator basicIter = d_inactiveRows.begin(), endIter =  d_inactiveRows.end();
-      basicIter != endIter; ++basicIter){
-    ArithVar basic = (*basicIter).first;
-    Row* row_k = lookupEjected(basic);
-    row_k->printRow();
+  Debug("tableau") << "Tableau::d_activeRows"  << endl;
+
+  typedef RowsTable::iterator table_iter;
+  for(table_iter rowIter = d_rowsTable.begin(), end = d_rowsTable.end();
+      rowIter != end; ++rowIter){
+    Row* row_k = *rowIter;
+    if(row_k != NULL){
+      row_k->printRow();
+    }
   }
 }
 
diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
index ed173a182..a69493ee0 100644
--- a/src/theory/arith/tableau.h
+++ b/src/theory/arith/tableau.h
@@ -88,49 +88,98 @@ public:
   void printRow();
 };
 
-class Tableau {
+class ArithVarSet {
+private:
+  typedef std::list<ArithVar> VarList;
+
 public:
-  typedef std::set<ArithVar> VarSet;
+  typedef VarList::const_iterator iterator;
 
 private:
-  typedef __gnu_cxx::hash_map<ArithVar, Row*> RowsTable;
+  VarList d_list;
+  std::vector< VarList::iterator > d_posVector;
+
+public:
+  ArithVarSet() : d_list(),  d_posVector() {}
+
+  iterator begin() const{ return d_list.begin(); }
+  iterator end() const{ return d_list.end(); }
+
+  void insert(ArithVar av){
+    Assert(inRange(av) );
+    Assert(!inSet(av) );
+
+    d_posVector[av] = d_list.insert(d_list.end(), av);
+  }
+
+  void erase(ArithVar var){
+    Assert( inRange(var) );
+    Assert( inSet(var) );
+
+    d_list.erase(d_posVector[var]);
+    d_posVector[var] = d_list.end();
+  }
 
-  VarSet d_activeBasicVars;
-  RowsTable d_activeRows, d_inactiveRows;
+  void increaseSize(){
+    d_posVector.push_back(d_list.end());
+  }
+
+  bool inSet(ArithVar v) const{
+    Assert(inRange(v) );
+
+    return d_posVector[v] != d_list.end();
+  }
+
+private:
+  bool inRange(ArithVar v) const{
+    return v < d_posVector.size();
+  }
+};
+
+class Tableau {
+private:
+
+  typedef std::vector< Row* > RowsTable;
+
+  ArithVarSet d_activeBasicVars;
+  RowsTable d_rowsTable;
 
   ActivityMonitor& d_activityMonitor;
   IsBasicManager& d_basicManager;
 
-
 public:
   /**
    * Constructs an empty tableau.
    */
   Tableau(ActivityMonitor &am, IsBasicManager& bm) :
     d_activeBasicVars(),
-    d_activeRows(),
-    d_inactiveRows(),
+    d_rowsTable(),
     d_activityMonitor(am),
     d_basicManager(bm)
   {}
 
-  VarSet::iterator begin(){
+  void increaseSize(){
+    d_activeBasicVars.increaseSize();
+    d_rowsTable.push_back(NULL);
+  }
+
+  ArithVarSet::iterator begin(){
     return d_activeBasicVars.begin();
   }
 
-  VarSet::iterator end(){
+  ArithVarSet::iterator end(){
     return d_activeBasicVars.end();
   }
 
   Row* lookup(ArithVar var){
     Assert(isActiveBasicVariable(var));
-    return d_activeRows[var];
+    return d_rowsTable[var];
   }
 
 private:
   Row* lookupEjected(ArithVar var){
     Assert(isEjected(var));
-    return d_inactiveRows[var];
+    return d_rowsTable[var];
   }
 public:
 
@@ -147,18 +196,14 @@ public:
   void printTableau();
 
   bool isEjected(ArithVar var){
-    return d_inactiveRows.find(var) != d_inactiveRows.end();
+    return d_basicManager.isBasic(var) && !isActiveBasicVariable(var);
   }
 
   void ejectBasic(ArithVar basic){
     Assert(d_basicManager.isBasic(basic));
     Assert(isActiveBasicVariable(basic));
 
-    Row* row = lookup(basic);
-    d_activeRows.erase(basic);
     d_activeBasicVars.erase(basic);
-
-    d_inactiveRows.insert(std::make_pair(basic, row));
   }
 
   void reinjectBasic(ArithVar basic){
@@ -166,16 +211,12 @@ public:
     Assert(isEjected(basic));
 
     Row* row = lookupEjected(basic);
-
-    d_inactiveRows.erase(basic);
     d_activeBasicVars.insert(basic);
-    d_activeRows.insert(std::make_pair(basic, row));
-
     updateRow(row);
   }
 private:
   inline bool isActiveBasicVariable(ArithVar var){
-    return d_activeBasicVars.find(var) != d_activeBasicVars.end();
+    return d_activeBasicVars.inSet(var);
   }
 
   void updateRow(Row* row);
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 4440a8e15..26bb58e90 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -138,7 +138,7 @@ bool TheoryArith::shouldEject(ArithVar var){
 }
 
 ArithVar TheoryArith::findBasicRow(ArithVar variable){
-  for(Tableau::VarSet::iterator basicIter = d_tableau.begin();
+  for(ArithVarSet::iterator basicIter = d_tableau.begin();
       basicIter != d_tableau.end();
       ++basicIter){
     ArithVar x_j = *basicIter;
@@ -241,6 +241,7 @@ ArithVar TheoryArith::requestArithVar(TNode x, bool basic){
 
   d_activityMonitor.initActivity(varX);
   d_basicManager.init(varX, basic);
+  d_tableau.increaseSize();
 
   Debug("arith::arithvar") << x << " |-> " << varX << endl;
 
@@ -501,7 +502,7 @@ void TheoryArith::update(ArithVar x_i, DeltaRational& v){
                  << assignment_x_i << "|-> " << v << endl;
   DeltaRational diff = v - assignment_x_i;
 
-  for(Tableau::VarSet::iterator basicIter = d_tableau.begin();
+  for(ArithVarSet::iterator basicIter = d_tableau.begin();
       basicIter != d_tableau.end();
       ++basicIter){
     ArithVar x_j = *basicIter;
@@ -545,7 +546,7 @@ void TheoryArith::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaRational& v){
   DeltaRational tmp = d_partialModel.getAssignment(x_j) + theta;
   d_partialModel.setAssignment(x_j, tmp);
 
-  for(Tableau::VarSet::iterator basicIter = d_tableau.begin();
+  for(ArithVarSet::iterator basicIter = d_tableau.begin();
       basicIter != d_tableau.end();
       ++basicIter){
     ArithVar x_k = *basicIter;
@@ -589,7 +590,7 @@ ArithVar TheoryArith::selectSmallestInconsistentVar(){
   }
 
   if(Debug.isOn("paranoid:variables")){
-    for(Tableau::VarSet::iterator basicIter = d_tableau.begin();
+    for(ArithVarSet::iterator basicIter = d_tableau.begin();
         basicIter != d_tableau.end();
         ++basicIter){
 
@@ -884,7 +885,7 @@ void TheoryArith::check(Effort level){
  */
 void TheoryArith::checkTableau(){
 
-  for(Tableau::VarSet::iterator basicIter = d_tableau.begin();
+  for(ArithVarSet::iterator basicIter = d_tableau.begin();
       basicIter != d_tableau.end(); ++basicIter){
     ArithVar basic = *basicIter;
     Row* row_k = d_tableau.lookup(basic);