The Row implementation has no been replaced by RowVector and ReducedRowVector. A RowVector is an array of ArithVar and Rational pairs. (This replaces a map based implementation in Row.) ReducedRowVector is a RowVector with a notion of having a basic variable. The Tableau is now a collection of ReduceRowVector's. A major difference between ReducedRowVectors and Rows is that the iterator now includes the basic variable and its coefficient (always -1). Before only nonbasic members were accessible by the iterator.

1 files changed, 17 insertions, 93 deletions

diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp
index 2490ed51b..c22c21a46 100644
--- a/src/theory/arith/tableau.cpp
+++ b/src/theory/arith/tableau.cpp
@@ -24,85 +24,6 @@ using namespace CVC4;
 using namespace CVC4::theory;
 using namespace CVC4::theory::arith;
 
-Row::Row(ArithVar basic,
-         const std::vector< Rational >& coefficients,
-         const std::vector< ArithVar >& variables):
-  d_x_i(basic),
-  d_coeffs(){
-
-  Assert(coefficients.size() == variables.size() );
-
-  std::vector<Rational>::const_iterator coeffIter = coefficients.begin();
-  std::vector<Rational>::const_iterator coeffEnd = coefficients.end();
-  std::vector<ArithVar>::const_iterator varIter = variables.begin();
-
-  for(; coeffIter != coeffEnd; ++coeffIter, ++varIter){
-    const Rational& coeff = *coeffIter;
-    ArithVar var_i = *varIter;
-
-    Assert(var_i != d_x_i);
-    Assert(!has(var_i));
-    Assert(coeff != Rational(0,1));
-
-    d_coeffs[var_i] = coeff;
-    Assert(d_coeffs[var_i] != Rational(0,1));
-  }
-}
-void Row::substitute(Row& row_s){
-  ArithVar x_s = row_s.basicVar();
-
-  Assert(has(x_s));
-  Assert(x_s != d_x_i);
-
-  Rational zero(0,1);
-
-  Rational a_rs = lookup(x_s);
-  Assert(a_rs != zero);
-  d_coeffs.erase(x_s);
-
-  for(iterator iter = row_s.begin(), iter_end = row_s.end();
-      iter != iter_end; ++iter){
-    ArithVar x_j = iter->first;
-    Rational a_sj = iter->second;
-    a_sj *= a_rs;
-    CoefficientTable::iterator coeff_iter = d_coeffs.find(x_j);
-
-    if(coeff_iter != d_coeffs.end()){
-      coeff_iter->second += a_sj;
-      if(coeff_iter->second == zero){
-        d_coeffs.erase(coeff_iter);
-      }
-    }else{
-      d_coeffs.insert(std::make_pair(x_j,a_sj));
-    }
-  }
-}
-
-void Row::pivot(ArithVar x_j){
-  Rational negInverseA_rs = -(lookup(x_j).inverse());
-  d_coeffs[d_x_i] = Rational(Integer(-1));
-  d_coeffs.erase(x_j);
-
-  d_x_i = x_j;
-
-  for(iterator nonbasicIter = begin(), nonbasicIter_end = end();
-      nonbasicIter != nonbasicIter_end; ++nonbasicIter){
-    nonbasicIter->second *= negInverseA_rs;
-  }
-
-}
-
-void Row::printRow(){
-  Debug("tableau") << d_x_i << " ";
-  for(iterator nonbasicIter = d_coeffs.begin();
-      nonbasicIter != d_coeffs.end();
-      ++nonbasicIter){
-    ArithVar nb = nonbasicIter->first;
-    Debug("tableau") << "{" << nb << "," << d_coeffs[nb] << "}";
-  }
-  Debug("tableau") << std::endl;
-}
-
 void Tableau::addRow(ArithVar basicVar,
                      const std::vector<Rational>& coeffs,
                      const std::vector<ArithVar>& variables){
@@ -113,15 +34,15 @@ void Tableau::addRow(ArithVar basicVar,
   //The new basic variable cannot already be a basic variable
   Assert(!isActiveBasicVariable(basicVar));
   d_activeBasicVars.insert(basicVar);
-  Row* row_current = new Row(basicVar,coeffs,variables);
+  ReducedRowVector* row_current = new ReducedRowVector(basicVar,variables, coeffs);
   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
-  std::vector<Rational>::const_iterator coeffsIter = coeffs.begin();
-  std::vector<Rational>::const_iterator coeffsEnd = coeffs.end();
+  vector<Rational>::const_iterator coeffsIter = coeffs.begin();
+  vector<Rational>::const_iterator coeffsEnd = coeffs.end();
 
-  std::vector<ArithVar>::const_iterator varsIter = variables.begin();
+  vector<ArithVar>::const_iterator varsIter = variables.begin();
 
   for( ; coeffsIter != coeffsEnd; ++coeffsIter, ++ varsIter){
     ArithVar var = *varsIter;
@@ -132,7 +53,7 @@ void Tableau::addRow(ArithVar basicVar,
       }
       Assert(isActiveBasicVariable(var));
 
-      Row* row_var = lookup(var);
+      ReducedRowVector* row_var = lookup(var);
       row_current->substitute(*row_var);
     }
   }
@@ -142,7 +63,7 @@ void Tableau::pivot(ArithVar x_r, ArithVar x_s){
   Assert(d_basicManager.isMember(x_r));
   Assert(!d_basicManager.isMember(x_s));
 
-  Row* row_s = lookup(x_r);
+  ReducedRowVector* row_s = lookup(x_r);
   Assert(row_s->has(x_s));
 
   //Swap x_r and x_s in d_activeRows
@@ -160,7 +81,9 @@ void Tableau::pivot(ArithVar x_r, ArithVar x_s){
   for(ArithVarSet::iterator basicIter = begin(), endIter = end();
       basicIter != endIter; ++basicIter){
     ArithVar basic = *basicIter;
-    Row* row_k = lookup(basic);
+    if(basic == x_s) continue;
+
+    ReducedRowVector* row_k = lookup(basic);
     if(row_k->has(x_s)){
       d_activityMonitor[basic] += 30;
       row_k->substitute(*row_s);
@@ -173,7 +96,7 @@ void Tableau::printTableau(){
   typedef RowsTable::iterator table_iter;
   for(table_iter rowIter = d_rowsTable.begin(), end = d_rowsTable.end();
       rowIter != end; ++rowIter){
-    Row* row_k = *rowIter;
+    ReducedRowVector* row_k = *rowIter;
     if(row_k != NULL){
       row_k->printRow();
     }
@@ -181,18 +104,19 @@ void Tableau::printTableau(){
 }
 
 
-void Tableau::updateRow(Row* row){
-  for(Row::iterator i=row->begin(), endIter = row->end(); i != endIter; ){
+void Tableau::updateRow(ReducedRowVector* row){
+  ArithVar basic = row->basic();
+  for(ReducedRowVector::NonZeroIterator i=row->beginNonZero(), endIter = row->endNonZero(); i != endIter; ){
     ArithVar var = i->first;
     ++i;
-    if(d_basicManager.isMember(var)){
-      Row* row_var = isActiveBasicVariable(var) ? lookup(var) : lookupEjected(var);
+    if(var != basic && d_basicManager.isMember(var)){
+      ReducedRowVector* row_var = isActiveBasicVariable(var) ? lookup(var) : lookupEjected(var);
 
       Assert(row_var != row);
       row->substitute(*row_var);
 
-      i = row->begin();
-      endIter = row->end();
+      i = row->beginNonZero();
+      endIter = row->endNonZero();
     }
   }
 }