diff options
author | Tim King <taking@cs.nyu.edu> | 2011-03-07 19:10:16 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2011-03-07 19:10:16 +0000 |
commit | 423dafb4b4a34d0c99274a7619b062997342179a (patch) | |
tree | 409ac25256c64fb90c0e867f611ce495107bc940 /src/theory/arith/tableau.cpp | |
parent | c01318241e5082478090cba15ff71f82b3f6da6a (diff) |
Merges branches/arithmetic/tableau-reset into the trunk. The tableau is now heuristically reset to its initial state during restarts.
Diffstat (limited to 'src/theory/arith/tableau.cpp')
-rw-r--r-- | src/theory/arith/tableau.cpp | 28 |
1 files changed, 26 insertions, 2 deletions
diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp index a8bcd28cc..cb1364488 100644 --- a/src/theory/arith/tableau.cpp +++ b/src/theory/arith/tableau.cpp @@ -45,11 +45,14 @@ void Tableau::internalCopy(const Tableau& tab){ d_rowCount.insert(d_rowCount.end(), N, 0); } + ColumnMatrix::const_iterator otherIter = tab.d_columnMatrix.begin(); ColumnMatrix::iterator i_colIter = d_columnMatrix.begin(); ColumnMatrix::iterator end_colIter = d_columnMatrix.end(); - for(; i_colIter != end_colIter; ++i_colIter){ + for(; i_colIter != end_colIter; ++i_colIter, ++otherIter){ + Assert(otherIter != tab.d_columnMatrix.end()); Column& col = *i_colIter; - col.increaseSize(d_columnMatrix.size()); + const Column& otherCol = *otherIter; + col.increaseSize(otherCol.allocated()); } ArithVarSet::iterator i_basicIter = tab.d_basicVariables.begin(); @@ -183,3 +186,24 @@ void Tableau::printTableau(){ } } } + +uint32_t Tableau::numNonZeroEntries() const { + uint32_t colSum = 0; + ColumnMatrix::const_iterator i = d_columnMatrix.begin(), end = d_columnMatrix.end(); + for(; i != end; ++i){ + const Column& col = *i; + colSum += col.size(); + } + return colSum; +} + +uint32_t Tableau::numNonZeroEntriesByRow() const { + uint32_t rowSum = 0; + ArithVarSet::iterator i = d_basicVariables.begin(), end = d_basicVariables.end(); + for(; i != end; ++i){ + ArithVar basic = *i; + const ReducedRowVector& row = *(d_rowsTable[basic]); + rowSum += row.size(); + } + return rowSum; +} |