From: Tim King Date: Sun, 27 Feb 2011 17:34:37 +0000 (+0000) Subject: - Adds a buffer to the ReducedRowVector addRowTimesConstant operation to reduce the... X-Git-Tag: cvc5-1.0.0~8684 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8d52dbabb099cb66cfffe0d63397764d8a53b21c;p=cvc5.git - Adds a buffer to the ReducedRowVector addRowTimesConstant operation to reduce the number of allocations made. Compare cluster jobs 1585 and 1584 for the expected performance increase. --- 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 VarCoeffArray; typedef VarCoeffArray::const_iterator const_iterator; - typedef std::vector ArithVarContainsSet; - private: + typedef std::vector ArithVarContainsSet; typedef VarCoeffArray::iterator iterator; /** @@ -47,6 +46,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