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, 10 insertions, 58 deletions

diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
index 588b521b1..758e5d92d 100644
--- a/src/theory/arith/tableau.h
+++ b/src/theory/arith/tableau.h
@@ -25,8 +25,9 @@
 #include "theory/arith/arithvar_dense_set.h"
 #include "theory/arith/normal_form.h"
 
+#include "theory/arith/row_vector.h"
+
 #include <ext/hash_map>
-#include <map>
 #include <set>
 
 #ifndef __CVC4__THEORY__ARITH__TABLEAU_H
@@ -36,57 +37,6 @@ namespace CVC4 {
 namespace theory {
 namespace arith {
 
-
-class Row {
-  ArithVar d_x_i;
-
-  typedef std::map<ArithVar, Rational, std::greater<ArithVar> > CoefficientTable;
-
-  CoefficientTable d_coeffs;
-
-public:
-
-  typedef CoefficientTable::iterator iterator;
-
-  /**
-   * Construct a row equal to:
-   *   basic = \sum_{x_i} c_i * x_i
-   */
-  Row(ArithVar basic,
-      const std::vector< Rational >& coefficients,
-      const std::vector< ArithVar >& variables);
-
-
-  iterator begin(){
-    return d_coeffs.begin();
-  }
-
-  iterator end(){
-    return d_coeffs.end();
-  }
-
-  ArithVar basicVar(){
-    return d_x_i;
-  }
-
-  bool has(ArithVar x_j){
-    CoefficientTable::iterator x_jPos = d_coeffs.find(x_j);
-    return x_jPos != d_coeffs.end();
-  }
-
-  const Rational& lookup(ArithVar x_j){
-    CoefficientTable::iterator x_jPos = d_coeffs.find(x_j);
-    Assert(x_jPos !=  d_coeffs.end());
-    return (*x_jPos).second;
-  }
-
-  void pivot(ArithVar x_j);
-
-  void substitute(Row& row_s);
-
-  void printRow();
-};
-
 class ArithVarSet {
 private:
   typedef std::list<ArithVar> VarList;
@@ -138,7 +88,7 @@ private:
 class Tableau {
 private:
 
-  typedef std::vector< Row* > RowsTable;
+  typedef std::vector< ReducedRowVector* > RowsTable;
 
   ArithVarSet d_activeBasicVars;
   RowsTable d_rowsTable;
@@ -171,19 +121,21 @@ public:
     return d_activeBasicVars.end();
   }
 
-  Row* lookup(ArithVar var){
+  ReducedRowVector* lookup(ArithVar var){
     Assert(isActiveBasicVariable(var));
     return d_rowsTable[var];
   }
 
 private:
-  Row* lookupEjected(ArithVar var){
+  ReducedRowVector* lookupEjected(ArithVar var){
     Assert(isEjected(var));
     return d_rowsTable[var];
   }
 public:
 
-  void addRow(ArithVar basicVar, const std::vector<Rational>& coeffs, const std::vector<ArithVar>& variables);
+  void addRow(ArithVar basicVar,
+              const std::vector<Rational>& coeffs,
+              const std::vector<ArithVar>& variables);
 
   /**
    * preconditions:
@@ -210,7 +162,7 @@ public:
     Assert(d_basicManager.isMember(basic));
     Assert(isEjected(basic));
 
-    Row* row = lookupEjected(basic);
+    ReducedRowVector* row = lookupEjected(basic);
     d_activeBasicVars.insert(basic);
     updateRow(row);
   }
@@ -219,7 +171,7 @@ private:
     return d_activeBasicVars.inSet(var);
   }
 
-  void updateRow(Row* row);
+  void updateRow(ReducedRowVector* row);
 };
 
 }; /* namespace arith  */