diff options
Diffstat (limited to 'src/theory/arith/matrix.h')
-rw-r--r-- | src/theory/arith/matrix.h | 44 |
1 files changed, 39 insertions, 5 deletions
diff --git a/src/theory/arith/matrix.h b/src/theory/arith/matrix.h index d93b6986e..084281c04 100644 --- a/src/theory/arith/matrix.h +++ b/src/theory/arith/matrix.h @@ -362,16 +362,18 @@ public: template <class T> class Matrix { -protected: - +public: typedef MatrixEntry<T> Entry; +protected: typedef CVC4::theory::arith::RowVector<T> RowVectorT; - typedef typename RowVectorT::const_iterator RowIterator; - typedef CVC4::theory::arith::ColumnVector<T> ColumnVectorT; + +public: + typedef typename RowVectorT::const_iterator RowIterator; typedef typename ColumnVectorT::const_iterator ColIterator; +protected: // RowTable : RowID |-> RowVector typedef std::vector< RowVectorT > RowTable; RowTable d_rows; @@ -532,6 +534,12 @@ public: d_columns.push_back(ColumnVector<T>(&d_entries)); } + void increaseSizeTo(size_t s){ + while(getNumColumns() < s){ + increaseSize(); + } + } + const RowVector<T>& getRow(RowIndex r) const { Assert(r < d_rows.size()); return d_rows[r]; @@ -600,7 +608,33 @@ public: d_mergeBuffer.purge(); } - /** to += mult * buffer. */ + /* to *= mult */ + void multiplyRowByConstant(RowIndex to, const T& mult){ + RowIterator i = getRow(to).begin(); + RowIterator i_end = getRow(to).end(); + for( ; i != i_end; ++i){ + EntryID id = i.getID(); + Entry& entry = d_entries.get(id); + T& coeff = entry.getCoefficient(); + coeff *= mult; + } + } + + /** to += mult * from. + * Use the more efficient rowPlusBufferTimesConstant() for + * repeated use. + */ + void rowPlusRowTimesConstant(RowIndex to, RowIndex from, const T& mult){ + Assert(to != from); + loadRowIntoBuffer(from); + rowPlusBufferTimesConstant(to, mult); + clearBuffer(); + } + + /** to += mult * buffer. + * Invalidates coefficients on the row. + * (mult should never be a direct copy of a coefficient!) + */ void rowPlusBufferTimesConstant(RowIndex to, const T& mult){ Assert(d_rowInMergeBuffer != ROW_INDEX_SENTINEL); Assert(to != ROW_INDEX_SENTINEL); |