diff options
author | Tim King <taking@cs.nyu.edu> | 2011-02-26 23:32:34 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2011-02-26 23:32:34 +0000 |
commit | 181333d85ccf9daea71285299493c4b0b0008f49 (patch) | |
tree | c3bc0fd1f3d1610a1778749ee721e2b8ae58c63e /src/theory/arith/row_vector.h | |
parent | 3548c7e5f6afed4e07bf9a70f0403952c9262519 (diff) |
- Merged RowVector and ReducedRowVector.
- Renamed NonZeroIterator to const_iterator.
- Both of these changes are in response to the code review.
Diffstat (limited to 'src/theory/arith/row_vector.h')
-rw-r--r-- | src/theory/arith/row_vector.h | 178 |
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 */ |