2 files changed, 60 insertions, 41 deletions

diff --git a/src/theory/arith/row_vector.cpp b/src/theory/arith/row_vector.cpp
index 6980188a1..78ec55c2a 100644
--- a/src/theory/arith/row_vector.cpp
+++ b/src/theory/arith/row_vector.cpp
@@ -91,20 +91,29 @@ void ReducedRowVector::removeArithVar(ArithVarContainsSet& contains, ArithVar v)
   contains[v] = false;
 }
 
-void ReducedRowVector::merge(const VarCoeffArray& other,
-                             const Rational& c){
-  VarCoeffArray copy = d_entries;
-  d_entries.clear();
+void ReducedRowVector::multiply(const Rational& c){
+  Assert(c != 0);
+
+  for(iterator i = d_entries.begin(), end = d_entries.end(); i != end; ++i){
+    getCoefficient(*i) *= c;
+  }
+}
+
+void ReducedRowVector::addRowTimesConstant(const Rational& c, const ReducedRowVector& other){
+  Assert(c != 0);
+  Assert(d_buffer.empty());
+
+  d_buffer.reserve(other.d_entries.size());
 
-  iterator curr1 = copy.begin();
-  iterator end1 = copy.end();
+  iterator curr1 = d_entries.begin();
+  iterator end1 = d_entries.end();
 
-  const_iterator curr2 = other.begin();
-  const_iterator end2 = other.end();
+  const_iterator curr2 = other.d_entries.begin();
+  const_iterator end2 = other.d_entries.end();
 
   while(curr1 != end1 && curr2 != end2){
     if(getArithVar(*curr1) < getArithVar(*curr2)){
-      d_entries.push_back(*curr1);
+      d_buffer.push_back(*curr1);
       ++curr1;
     }else if(getArithVar(*curr1) > getArithVar(*curr2)){
 
@@ -114,14 +123,14 @@ void ReducedRowVector::merge(const VarCoeffArray& other,
       }
 
       addArithVar(d_contains, getArithVar(*curr2));
-      d_entries.push_back( make_pair(getArithVar(*curr2), c * getCoefficient(*curr2)));
+      d_buffer.push_back( make_pair(getArithVar(*curr2), c * getCoefficient(*curr2)));
       ++curr2;
     }else{
       Rational res = getCoefficient(*curr1) + c * getCoefficient(*curr2);
       if(res != 0){
         //The variable is not new so the count stays the same
 
-        d_entries.push_back(make_pair(getArithVar(*curr1), res));
+        d_buffer.push_back(make_pair(getArithVar(*curr1), res));
       }else{
         removeArithVar(d_contains, getArithVar(*curr2));
 
@@ -135,7 +144,7 @@ void ReducedRowVector::merge(const VarCoeffArray& other,
     }
   }
   while(curr1 != end1){
-    d_entries.push_back(*curr1);
+    d_buffer.push_back(*curr1);
     ++curr1;
   }
   while(curr2 != end2){
@@ -146,23 +155,14 @@ void ReducedRowVector::merge(const VarCoeffArray& other,
 
     addArithVar(d_contains, getArithVar(*curr2));
 
-    d_entries.push_back(make_pair(getArithVar(*curr2), c * getCoefficient(*curr2)));
+    d_buffer.push_back(make_pair(getArithVar(*curr2), c * getCoefficient(*curr2)));
     ++curr2;
   }
-}
-
-void ReducedRowVector::multiply(const Rational& c){
-  Assert(c != 0);
 
-  for(iterator i = d_entries.begin(), end = d_entries.end(); i != end; ++i){
-    getCoefficient(*i) *= c;
-  }
-}
-
-void ReducedRowVector::addRowTimesConstant(const Rational& c, const ReducedRowVector& other){
-  Assert(c != 0);
+  d_buffer.swap(d_entries);
+  d_buffer.clear();
 
-  merge(other.d_entries, c);
+  Assert(d_buffer.empty());
 }
 
 void ReducedRowVector::printRow(){
diff --git a/src/theory/arith/row_vector.h b/src/theory/arith/row_vector.h
index 829cecd7e..983e19a0a 100644
--- a/src/theory/arith/row_vector.h
+++ b/src/theory/arith/row_vector.h
@@ -35,9 +35,8 @@ public:
   typedef std::vector<VarCoeffPair> VarCoeffArray;
   typedef VarCoeffArray::const_iterator const_iterator;
 
-  typedef std::vector<bool> ArithVarContainsSet;
-
 private:
+  typedef std::vector<bool> ArithVarContainsSet;
   typedef VarCoeffArray::iterator iterator;
 
   /**
@@ -48,6 +47,11 @@ private:
   VarCoeffArray d_entries;
 
   /**
+   * Buffer for d_entries to reduce allocations by addRowTimesConstant.
+   */
+  VarCoeffArray d_buffer;
+
+  /**
    * The basic variable associated with the row.
    * Must have a coefficient of -1.
    */
@@ -74,6 +78,7 @@ public:
 
   ~ReducedRowVector();
 
+  /** Returns the basic variable.*/
   ArithVar basic() const{
     Assert(basicIsSet());
     return d_basic;
@@ -84,7 +89,7 @@ public:
     return d_entries.size();
   }
 
-  //Iterates over the nonzero entries in the Vector
+  /** Iterates over the nonzero entries in the vector. */
   const_iterator begin() const { return d_entries.begin(); }
   const_iterator end() const { return d_entries.end(); }
 
@@ -107,22 +112,25 @@ public:
     return getCoefficient(*lb);
   }
 
-  /** Multiplies the coefficients of the RowVector by c (where c != 0). */
-  void multiply(const Rational& c);
-
-  /**
-   * \sum(this->entries) += c * (\sum(other.d_entries) )
-   *
-   * Updates the current row to be the sum of itself and
-   * another vector times c (c != 0).
-   */
-  void addRowTimesConstant(const Rational& c, const ReducedRowVector& other);
 
+  /** Prints the row to the buffer Debug("row::print"). */
   void printRow();
 
-
+  /**
+   * Changes the basic variable to x_j.
+   * Precondition: has(x_j)
+   */
   void pivot(ArithVar x_j);
 
+  /**
+   * Replaces other.basic() in the current row using the other row.
+   * This assumes the other row represents an equality equal to zero.
+   *
+   *   \sum(this->entries) -= this->lookup(other.basic()) * (\sum(other.d_entries))
+   * Precondition:
+   *  has(other.basic())
+   *  basic != other.basic()
+   */
   void substitute(const ReducedRowVector& other);
 
   /**
@@ -133,6 +141,19 @@ public:
   Node asEquality(const ArithVarToNodeMap& map) const;
 
 private:
+
+  /**
+   * \sum(this->entries) += c * (\sum(other.d_entries) )
+   *
+   * Updates the current row to be the sum of itself and
+   * another vector times c (c != 0).
+   */
+  void addRowTimesConstant(const Rational& c, const ReducedRowVector& other);
+
+
+  /** Multiplies the coefficients of the RowVector by c (where c != 0). */
+  void multiply(const Rational& c);
+
   /**
    * Adds v to d_contains.
    * This may resize d_contains.
@@ -158,8 +179,6 @@ private:
                   const std::vector< Rational >& coefficients,
                   VarCoeffArray& output);
 
-  void merge(const VarCoeffArray& other, const Rational& c);
-
   /**
    * Debugging code.
    * noZeroCoefficients(arr) is equivalent to