From 181333d85ccf9daea71285299493c4b0b0008f49 Mon Sep 17 00:00:00 2001 From: Tim King Date: Sat, 26 Feb 2011 23:32:34 +0000 Subject: [PATCH] - Merged RowVector and ReducedRowVector. - Renamed NonZeroIterator to const_iterator. - Both of these changes are in response to the code review. --- src/theory/arith/row_vector.cpp | 165 ++++++++++++----------------- src/theory/arith/row_vector.h | 178 ++++++++++++++------------------ src/theory/arith/simplex.cpp | 33 +++--- 3 files changed, 161 insertions(+), 215 deletions(-) diff --git a/src/theory/arith/row_vector.cpp b/src/theory/arith/row_vector.cpp index 0dc483126..6980188a1 100644 --- a/src/theory/arith/row_vector.cpp +++ b/src/theory/arith/row_vector.cpp @@ -7,10 +7,10 @@ using namespace CVC4::theory::arith; using namespace std; -bool RowVector::isSorted(const VarCoeffArray& arr, bool strictlySorted) { +bool ReducedRowVector::isSorted(const VarCoeffArray& arr, bool strictlySorted) { if(arr.size() >= 2){ - NonZeroIterator curr = arr.begin(); - NonZeroIterator end = arr.end(); + const_iterator curr = arr.begin(); + const_iterator end = arr.end(); ArithVar prev = getArithVar(*curr); ++curr; for(;curr != end; ++curr){ @@ -23,20 +23,26 @@ bool RowVector::isSorted(const VarCoeffArray& arr, bool strictlySorted) { return true; } -RowVector::~RowVector(){ - NonZeroIterator curr = beginNonZero(); - NonZeroIterator end = endNonZero(); - for(;curr != end; ++curr){ +ReducedRowVector::~ReducedRowVector(){ + //This executes before the super classes destructor RowVector, + // which will set this to 0. + Assert(d_rowCount[basic()] == 1); + + const_iterator curr = begin(); + const_iterator endEntries = end(); + for(;curr != endEntries; ++curr){ ArithVar v = getArithVar(*curr); Assert(d_rowCount[v] >= 1); + d_columnMatrix[v].remove(basic()); --(d_rowCount[v]); } Assert(matchingCounts()); } -bool RowVector::matchingCounts() const{ - for(NonZeroIterator i=beginNonZero(), end=endNonZero(); i != end; ++i){ + +bool ReducedRowVector::matchingCounts() const{ + for(const_iterator i=begin(), endEntries=end(); i != endEntries; ++i){ ArithVar v = getArithVar(*i); if(d_columnMatrix[v].size() != d_rowCount[v]){ return false; @@ -45,18 +51,18 @@ bool RowVector::matchingCounts() const{ return true; } -bool RowVector::noZeroCoefficients(const VarCoeffArray& arr){ - for(NonZeroIterator curr = arr.begin(), end = arr.end(); - curr != end; ++curr){ +bool ReducedRowVector::noZeroCoefficients(const VarCoeffArray& arr){ + for(const_iterator curr = arr.begin(), endEntries = arr.end(); + curr != endEntries; ++curr){ const Rational& coeff = getCoefficient(*curr); if(coeff == 0) return false; } return true; } -void RowVector::zip(const std::vector< ArithVar >& variables, - const std::vector< Rational >& coefficients, - VarCoeffArray& output){ +void ReducedRowVector::zip(const std::vector< ArithVar >& variables, + const std::vector< Rational >& coefficients, + VarCoeffArray& output){ Assert(coefficients.size() == variables.size() ); @@ -72,81 +78,56 @@ void RowVector::zip(const std::vector< ArithVar >& variables, } } - -RowVector::RowVector(const std::vector< ArithVar >& variables, - const std::vector< Rational >& coefficients, - std::vector& counts, - std::vector& cm): - d_rowCount(counts), d_columnMatrix(cm) -{ - zip(variables, coefficients, d_entries); - - std::sort(d_entries.begin(), d_entries.end(), cmp); - - for(NonZeroIterator i=beginNonZero(), end=endNonZero(); i != end; ++i){ - ++d_rowCount[getArithVar(*i)]; - addArithVar(d_contains, getArithVar(*i)); - } - - Assert(isSorted(d_entries, true)); - Assert(noZeroCoefficients(d_entries)); -} - -void RowVector::addArithVar(ArithVarContainsSet& contains, ArithVar v){ +void ReducedRowVector::addArithVar(ArithVarContainsSet& contains, ArithVar v){ if(v >= contains.size()){ contains.resize(v+1, false); } contains[v] = true; } -void RowVector::removeArithVar(ArithVarContainsSet& contains, ArithVar v){ +void ReducedRowVector::removeArithVar(ArithVarContainsSet& contains, ArithVar v){ Assert(v < contains.size()); Assert(contains[v]); contains[v] = false; } -void RowVector::merge(VarCoeffArray& arr, - ArithVarContainsSet& contains, - const VarCoeffArray& other, - const Rational& c, - std::vector& counts, - std::vector& columnMatrix, - ArithVar basic){ - VarCoeffArray copy = arr; - arr.clear(); +void ReducedRowVector::merge(const VarCoeffArray& other, + const Rational& c){ + VarCoeffArray copy = d_entries; + d_entries.clear(); iterator curr1 = copy.begin(); iterator end1 = copy.end(); - NonZeroIterator curr2 = other.begin(); - NonZeroIterator end2 = other.end(); + const_iterator curr2 = other.begin(); + const_iterator end2 = other.end(); while(curr1 != end1 && curr2 != end2){ if(getArithVar(*curr1) < getArithVar(*curr2)){ - arr.push_back(*curr1); + d_entries.push_back(*curr1); ++curr1; }else if(getArithVar(*curr1) > getArithVar(*curr2)){ - ++counts[getArithVar(*curr2)]; - if(basic != ARITHVAR_SENTINEL){ - columnMatrix[getArithVar(*curr2)].add(basic); + ++d_rowCount[getArithVar(*curr2)]; + if(d_basic != ARITHVAR_SENTINEL){ + d_columnMatrix[getArithVar(*curr2)].add(d_basic); } - addArithVar(contains, getArithVar(*curr2)); - arr.push_back( make_pair(getArithVar(*curr2), c * getCoefficient(*curr2))); + addArithVar(d_contains, getArithVar(*curr2)); + d_entries.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 - arr.push_back(make_pair(getArithVar(*curr1), res)); + d_entries.push_back(make_pair(getArithVar(*curr1), res)); }else{ - removeArithVar(contains, getArithVar(*curr2)); + removeArithVar(d_contains, getArithVar(*curr2)); - --counts[getArithVar(*curr2)]; - if(basic != ARITHVAR_SENTINEL){ - columnMatrix[getArithVar(*curr2)].remove(basic); + --d_rowCount[getArithVar(*curr2)]; + if(d_basic != ARITHVAR_SENTINEL){ + d_columnMatrix[getArithVar(*curr2)].remove(d_basic); } } ++curr1; @@ -154,23 +135,23 @@ void RowVector::merge(VarCoeffArray& arr, } } while(curr1 != end1){ - arr.push_back(*curr1); + d_entries.push_back(*curr1); ++curr1; } while(curr2 != end2){ - ++counts[getArithVar(*curr2)]; - if(basic != ARITHVAR_SENTINEL){ - columnMatrix[getArithVar(*curr2)].add(basic); + ++d_rowCount[getArithVar(*curr2)]; + if(d_basic != ARITHVAR_SENTINEL){ + d_columnMatrix[getArithVar(*curr2)].add(d_basic); } - addArithVar(contains, getArithVar(*curr2)); + addArithVar(d_contains, getArithVar(*curr2)); - arr.push_back(make_pair(getArithVar(*curr2), c * getCoefficient(*curr2))); + d_entries.push_back(make_pair(getArithVar(*curr2), c * getCoefficient(*curr2))); ++curr2; } } -void RowVector::multiply(const Rational& c){ +void ReducedRowVector::multiply(const Rational& c){ Assert(c != 0); for(iterator i = d_entries.begin(), end = d_entries.end(); i != end; ++i){ @@ -178,14 +159,14 @@ void RowVector::multiply(const Rational& c){ } } -void RowVector::addRowTimesConstant(const Rational& c, const RowVector& other, ArithVar basic){ +void ReducedRowVector::addRowTimesConstant(const Rational& c, const ReducedRowVector& other){ Assert(c != 0); - merge(d_entries, d_contains, other.d_entries, c, d_rowCount, d_columnMatrix, basic); + merge(other.d_entries, c); } -void RowVector::printRow(){ - for(NonZeroIterator i = beginNonZero(); i != endNonZero(); ++i){ +void ReducedRowVector::printRow(){ + for(const_iterator i = begin(); i != end(); ++i){ ArithVar nb = getArithVar(*i); Debug("row::print") << "{" << nb << "," << getCoefficient(*i) << "}"; } @@ -196,21 +177,23 @@ void RowVector::printRow(){ ReducedRowVector::ReducedRowVector(ArithVar basic, const std::vector& variables, const std::vector& coefficients, - std::vector& count, - std::vector& columnMatrix): - RowVector(variables, coefficients, count, columnMatrix), d_basic(basic){ + std::vector& counts, + std::vector& cm): + d_basic(basic), d_rowCount(counts), d_columnMatrix(cm) +{ + zip(variables, coefficients, d_entries); + d_entries.push_back(make_pair(basic, Rational(-1))); + std::sort(d_entries.begin(), d_entries.end(), cmp); - for(NonZeroIterator i=beginNonZero(), end=endNonZero(); i != end; ++i){ - //basic is not yet in d_entries - Assert(getArithVar(*i) != d_basic); + for(const_iterator i=begin(), endEntries=end(); i != endEntries; ++i){ + ++d_rowCount[getArithVar(*i)]; + addArithVar(d_contains, getArithVar(*i)); d_columnMatrix[getArithVar(*i)].add(d_basic); } - VarCoeffArray justBasic; - justBasic.push_back(make_pair(basic, Rational(-1))); - - merge(d_entries, d_contains, justBasic, Rational(1), d_rowCount, d_columnMatrix, d_basic); + Assert(isSorted(d_entries, true)); + Assert(noZeroCoefficients(d_entries)); Assert(matchingCounts()); Assert(wellFormed()); @@ -226,7 +209,7 @@ void ReducedRowVector::substitute(const ReducedRowVector& row_s){ Rational a_rs = lookup(x_s); Assert(a_rs != 0); - addRowTimesConstant(a_rs, row_s, basic()); + addRowTimesConstant(a_rs, row_s); Assert(!has(x_s)); @@ -241,7 +224,7 @@ void ReducedRowVector::pivot(ArithVar x_j){ Rational negInverseA_rs = -(lookup(x_j).inverse()); multiply(negInverseA_rs); - for(NonZeroIterator i=beginNonZero(), end=endNonZero(); i != end; ++i){ + for(const_iterator i=begin(), endEntries=end(); i != endEntries; ++i){ d_columnMatrix[getArithVar(*i)].remove(d_basic); d_columnMatrix[getArithVar(*i)].add(x_j); } @@ -264,7 +247,7 @@ Node ReducedRowVector::asEquality(const ArithVarToNodeMap& map) const{ if(size() > 2){ NodeBuilder<> sumBuilder(PLUS); - for(NonZeroIterator i = beginNonZero(); i != endNonZero(); ++i){ + for(const_iterator i = begin(); i != end(); ++i){ ArithVar nb = getArithVar(*i); if(nb == basic()) continue; Node var = (map.find(nb))->second; @@ -276,7 +259,7 @@ Node ReducedRowVector::asEquality(const ArithVarToNodeMap& map) const{ sum = sumBuilder; }else{ Assert(size() == 2); - NonZeroIterator i = beginNonZero(); + const_iterator i = begin(); if(getArithVar(*i) == basic()){ ++i; } @@ -289,17 +272,3 @@ Node ReducedRowVector::asEquality(const ArithVarToNodeMap& map) const{ return NodeBuilder<2>(EQUAL) << basicVar << sum; } - -ReducedRowVector::~ReducedRowVector(){ - //This executes before the super classes destructor RowVector, - // which will set this to 0. - Assert(d_rowCount[basic()] == 1); - - NonZeroIterator curr = beginNonZero(); - NonZeroIterator end = endNonZero(); - for(;curr != end; ++curr){ - ArithVar v = getArithVar(*curr); - Assert(d_rowCount[v] >= 1); - d_columnMatrix[v].remove(basic()); - } -} 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 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 VarCoeffArray; - typedef VarCoeffArray::const_iterator NonZeroIterator; + typedef VarCoeffArray::const_iterator const_iterator; typedef std::vector ArithVarContainsSet; - /** - * Let c be -1 if strictlySorted is true and c be 0 otherwise. - * isSorted(arr, strictlySorted) is then equivalent to - * If i& variables, - const std::vector< Rational >& coefficients, - VarCoeffArray& output); - - static void merge(VarCoeffArray& arr, - ArithVarContainsSet& contains, - const VarCoeffArray& other, - const Rational& c, - std::vector& count, - std::vector& 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: @@ -75,6 +47,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& d_rowCount; std::vector& 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& counts, - std::vector& columnMatrix); + ReducedRowVector(ArithVar basic, + const std::vector< ArithVar >& variables, + const std::vector< Rational >& coefficients, + std::vector& count, + std::vector& 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& 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& count, - std::vector& 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 */ diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index c8f1ce3e8..02ce310ff 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -253,8 +253,8 @@ void SimplexDecisionProcedure::pivotAndUpdate(ArithVar x_i, ArithVar x_j, DeltaR if(Debug.isOn("arith::pivotAndUpdate")){ Debug("arith::pivotAndUpdate") << "x_i " << "|->" << x_j << endl; ReducedRowVector& row_k = d_tableau.lookup(x_i); - for(ReducedRowVector::NonZeroIterator varIter = row_k.beginNonZero(); - varIter != row_k.endNonZero(); + for(ReducedRowVector::const_iterator varIter = row_k.begin(); + varIter != row_k.end(); ++varIter){ ArithVar var = varIter->first; @@ -332,7 +332,7 @@ ArithVar SimplexDecisionProcedure::selectSlack(ArithVar x_i, bool first){ bool pivotStage = !first; - for(ReducedRowVector::NonZeroIterator nbi = row_i.beginNonZero(), end = row_i.endNonZero(); + for(ReducedRowVector::const_iterator nbi = row_i.begin(), end = row_i.end(); nbi != end; ++nbi){ ArithVar nonbasic = getArithVar(*nbi); if(nonbasic == x_i) continue; @@ -494,7 +494,7 @@ template Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingIterations){ Debug("arith") << "updateInconsistentVars" << endl; - static const uint32_t CHECK_PERIOD = 1000; + static const uint32_t CHECK_PERIOD = 100; while(!limitIterations || remainingIterations > 0){ if(Debug.isOn("paranoid:check_tableau")){ checkTableau(); } @@ -536,12 +536,12 @@ Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera return earlyConflict; } //Once every CHECK_PERIOD examine the entire queue for conflicts - // if(!limitIterations && remainingIterations % CHECK_PERIOD == 0){ - // Node earlyConflict = findConflictOnTheQueue(DuringVarOrderSearch); - // if(!earlyConflict.isNull()){ - // return earlyConflict; - // } - // } + if(!limitIterations && remainingIterations % CHECK_PERIOD == 0){ + Node earlyConflict = findConflictOnTheQueue(DuringVarOrderSearch); + if(!earlyConflict.isNull()){ + return earlyConflict; + } + } } AlwaysAssert(limitIterations && remainingIterations == 0); @@ -563,8 +563,7 @@ Node SimplexDecisionProcedure::generateConflictAbove(ArithVar conflictVar){ nb << bound; - typedef ReducedRowVector::NonZeroIterator RowIterator; - RowIterator nbi = row_i.beginNonZero(), end = row_i.endNonZero(); + ReducedRowVector::const_iterator nbi = row_i.begin(), end = row_i.end(); for(; nbi != end; ++nbi){ ArithVar nonbasic = getArithVar(*nbi); @@ -604,8 +603,8 @@ Node SimplexDecisionProcedure::generateConflictBelow(ArithVar conflictVar){ << " " << bound << endl; nb << bound; - typedef ReducedRowVector::NonZeroIterator RowIterator; - RowIterator nbi = row_i.beginNonZero(), end = row_i.endNonZero(); + + ReducedRowVector::const_iterator nbi = row_i.begin(), end = row_i.end(); for(; nbi != end; ++nbi){ ArithVar nonbasic = getArithVar(*nbi); if(nonbasic == conflictVar) continue; @@ -642,7 +641,7 @@ DeltaRational SimplexDecisionProcedure::computeRowValue(ArithVar x, bool useSafe DeltaRational sum = d_constants.d_ZERO_DELTA; ReducedRowVector& row = d_tableau.lookup(x); - for(ReducedRowVector::NonZeroIterator i = row.beginNonZero(), end = row.endNonZero(); + for(ReducedRowVector::const_iterator i = row.begin(), end = row.end(); i != end;++i){ ArithVar nonbasic = getArithVar(*i); if(nonbasic == row.basic()) continue; @@ -669,8 +668,8 @@ void SimplexDecisionProcedure::checkTableau(){ ReducedRowVector& row_k = d_tableau.lookup(basic); DeltaRational sum; Debug("paranoid:check_tableau") << "starting row" << basic << endl; - for(ReducedRowVector::NonZeroIterator nonbasicIter = row_k.beginNonZero(); - nonbasicIter != row_k.endNonZero(); + for(ReducedRowVector::const_iterator nonbasicIter = row_k.begin(); + nonbasicIter != row_k.end(); ++nonbasicIter){ ArithVar nonbasic = nonbasicIter->first; if(basic == nonbasic) continue; -- 2.30.2