- Merged RowVector and ReducedRowVector.

- Renamed NonZeroIterator to const_iterator.
- Both of these changes are in response to the code review.

1 files changed, 78 insertions, 100 deletions

diff --git a/src/theory/arith/row_vector.h b/src/theory/arith/row_vector.h
index bed33349d..829cecd7e 100644
--- a/src/theory/arith/row_vector.h
+++ b/src/theory/arith/row_vector.h
@@ -15,58 +15,30 @@ namespace theory {
 namespace arith {
 
 typedef std::pair<ArithVar, Rational> VarCoeffPair;
+
 inline ArithVar getArithVar(const VarCoeffPair& v) { return v.first; }
 inline Rational& getCoefficient(VarCoeffPair& v) { return v.second; }
 inline const Rational& getCoefficient(const VarCoeffPair& v) { return v.second; }
 
 inline bool cmp(const VarCoeffPair& a, const VarCoeffPair& b){
-  return CVC4::theory::arith::getArithVar(a) < CVC4::theory::arith::getArithVar(b);
+  return getArithVar(a) < getArithVar(b);
 }
 
 /**
- * RowVector is a sparse vector representation that represents the
+ * ReducedRowVector is a sparse vector representation that represents the
  * row as a strictly sorted array of "VarCoeffPair"s.
+ * The row has a notion of a basic variable.
+ * This is a variable that must have a coefficient of -1 in the array.
  */
-class RowVector {
+class ReducedRowVector {
 public:
   typedef std::vector<VarCoeffPair> VarCoeffArray;
-  typedef VarCoeffArray::const_iterator NonZeroIterator;
+  typedef VarCoeffArray::const_iterator const_iterator;
 
   typedef std::vector<bool> ArithVarContainsSet;
 
-  /**
-   * Let c be -1 if strictlySorted is true and c be 0 otherwise.
-   * 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);
-
-  /**
-   * Zips together an array of variables and coefficients and appends
-   * it to the end of an output vector.
-   */
-  static void zip(const std::vector< ArithVar >& variables,
-                  const std::vector< Rational >& coefficients,
-                  VarCoeffArray& output);
-
-  static void merge(VarCoeffArray& arr,
-                    ArithVarContainsSet& contains,
-                    const VarCoeffArray& other,
-                    const Rational& c,
-                    std::vector<uint32_t>& count,
-                    std::vector<ArithVarSet>& columnMatrix,
-                    ArithVar basic);
-
-protected:
-  /**
-   * Debugging code.
-   * noZeroCoefficients(arr) is equivalent to
-   *  0 != getCoefficient(arr[i]) for all i.
-   */
-  static bool noZeroCoefficients(const VarCoeffArray& arr);
-
-  /** Debugging code.*/
-  bool matchingCounts() const;
+private:
+  typedef VarCoeffArray::iterator iterator;
 
   /**
    * Invariants:
@@ -76,6 +48,13 @@ protected:
   VarCoeffArray d_entries;
 
   /**
+   * The basic variable associated with the row.
+   * Must have a coefficient of -1.
+   */
+  ArithVar d_basic;
+
+
+  /**
    * Invariants:
    * - This set is the same as the set maintained in d_entries.
    */
@@ -84,20 +63,21 @@ protected:
   std::vector<uint32_t>& d_rowCount;
   std::vector<ArithVarSet>& d_columnMatrix;
 
-  NonZeroIterator lower_bound(ArithVar x_j) const{
-    return std::lower_bound(d_entries.begin(), d_entries.end(), std::make_pair(x_j,0), cmp);
-  }
-
-  typedef VarCoeffArray::iterator iterator;
 
 public:
 
-  RowVector(const std::vector< ArithVar >& variables,
-            const std::vector< Rational >& coefficients,
-            std::vector<uint32_t>& counts,
-            std::vector<ArithVarSet>& columnMatrix);
+  ReducedRowVector(ArithVar basic,
+                   const std::vector< ArithVar >& variables,
+                   const std::vector< Rational >& coefficients,
+                   std::vector<uint32_t>& count,
+                   std::vector<ArithVarSet>& columnMatrix);
 
-  ~RowVector();
+  ~ReducedRowVector();
+
+  ArithVar basic() const{
+    Assert(basicIsSet());
+    return d_basic;
+  }
 
   /** Returns the number of nonzero variables in the vector. */
   uint32_t size() const {
@@ -105,8 +85,8 @@ public:
   }
 
   //Iterates over the nonzero entries in the Vector
-  NonZeroIterator beginNonZero() const { return d_entries.begin(); }
-  NonZeroIterator endNonZero() const { return d_entries.end(); }
+  const_iterator begin() const { return d_entries.begin(); }
+  const_iterator end() const { return d_entries.end(); }
 
   /** Returns true if the variable is in the row. */
   bool has(ArithVar x_j) const{
@@ -117,20 +97,13 @@ public:
     }
   }
 
-private:
-  /** Debugging code. */
-  bool hasInEntries(ArithVar x_j) const {
-    return std::binary_search(d_entries.begin(), d_entries.end(), std::make_pair(x_j,0), cmp);
-  }
-public:
-
   /**
    * Returns the coefficient of a variable in the row.
    */
   const Rational& lookup(ArithVar x_j) const{
     Assert(has(x_j));
     Assert(hasInEntries(x_j));
-    NonZeroIterator lb = lower_bound(x_j);
+    const_iterator lb = lower_bound(x_j);
     return getCoefficient(*lb);
   }
 
@@ -143,11 +116,23 @@ public:
    * Updates the current row to be the sum of itself and
    * another vector times c (c != 0).
    */
-  void addRowTimesConstant(const Rational& c, const RowVector& other, ArithVar basic);
+  void addRowTimesConstant(const Rational& c, const ReducedRowVector& other);
 
   void printRow();
 
-protected:
+
+  void pivot(ArithVar x_j);
+
+  void substitute(const ReducedRowVector& other);
+
+  /**
+   * Returns the reduced row as an equality with
+   * the basic variable on the lhs equal to the sum of the non-basics variables.
+   * The mapped from ArithVars to Nodes is specificied by map.
+   */
+  Node asEquality(const ArithVarToNodeMap& map) const;
+
+private:
   /**
    * Adds v to d_contains.
    * This may resize d_contains.
@@ -157,17 +142,39 @@ protected:
   /** Removes v from d_contains. */
   static void removeArithVar(ArithVarContainsSet& contains, ArithVar v);
 
-}; /* class RowVector */
 
-/**
- * A reduced row is similar to a normal row except
- * that it also has a notion of a basic variable.
- * This variable that must have a coefficient of -1 in the array.
- */
-class ReducedRowVector : public RowVector{
-private:
-  ArithVar d_basic;
+  /**
+   * Let c be -1 if strictlySorted is true and c be 0 otherwise.
+   * 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);
 
+  /**
+   * Zips together an array of variables and coefficients and appends
+   * it to the end of an output vector.
+   */
+  static void zip(const std::vector< ArithVar >& variables,
+                  const std::vector< Rational >& coefficients,
+                  VarCoeffArray& output);
+
+  void merge(const VarCoeffArray& other, const Rational& c);
+
+  /**
+   * Debugging code.
+   * noZeroCoefficients(arr) is equivalent to
+   *  0 != getCoefficient(arr[i]) for all i.
+   */
+  static bool noZeroCoefficients(const VarCoeffArray& arr);
+
+  /** Debugging code.*/
+  bool matchingCounts() const;
+
+  const_iterator lower_bound(ArithVar x_j) const{
+    return std::lower_bound(d_entries.begin(), d_entries.end(), std::make_pair(x_j,0), cmp);
+  }
+
+  /** Debugging code */
   bool wellFormed() const{
     return
       isSorted(d_entries, true) &&
@@ -177,42 +184,13 @@ private:
       lookup(basic()) == Rational(-1);
   }
 
-public:
-
   bool basicIsSet() const { return d_basic != ARITHVAR_SENTINEL; }
 
-  ReducedRowVector(ArithVar basic,
-                   const std::vector< ArithVar >& variables,
-                   const std::vector< Rational >& coefficients,
-                   std::vector<uint32_t>& count,
-                   std::vector<ArithVarSet>& columnMatrix);
-
-  ~ReducedRowVector();
-
-  ArithVar basic() const{
-    Assert(basicIsSet());
-    return d_basic;
-  }
-
-  /** Return true if x is in the row and is not the basic variable. */
-  bool hasNonBasic(ArithVar x) const {
-    if(x == basic()){
-      return false;
-    }else{
-      return has(x);
-    }
+  /** Debugging code. */
+  bool hasInEntries(ArithVar x_j) const {
+    return std::binary_search(d_entries.begin(), d_entries.end(), std::make_pair(x_j,0), cmp);
   }
 
-  void pivot(ArithVar x_j);
-
-  void substitute(const ReducedRowVector& other);
-
-  /**
-   * Returns the reduced row as an equality with
-   * the basic variable on the lhs equal to the sum of the non-basics variables.
-   * The mapped from ArithVars to Nodes is specificied by map.
-   */
-  Node asEquality(const ArithVarToNodeMap& map) const;
 }; /* class ReducedRowVector */