diff options
Diffstat (limited to 'src/theory/arith/matrix.h')
-rw-r--r-- | src/theory/arith/matrix.h | 76 |
1 files changed, 38 insertions, 38 deletions
diff --git a/src/theory/arith/matrix.h b/src/theory/arith/matrix.h index ea6c389b9..027397b6a 100644 --- a/src/theory/arith/matrix.h +++ b/src/theory/arith/matrix.h @@ -25,6 +25,7 @@ #include "util/dense_map.h" #include "theory/arith/arithvar.h" +#include "theory/arith/arithvar_node_map.h" #include "theory/arith/normal_form.h" #include <queue> @@ -377,6 +378,8 @@ protected: uint32_t d_entriesInUse; MatrixEntryVector<T> d_entries; + std::vector<RowIndex> d_pool; + T d_zero; public: @@ -446,6 +449,23 @@ protected: d_entries.freeEntry(id); } + private: + RowIndex requestRowIndex(){ + if(d_pool.empty()){ + RowIndex ridx = d_rows.size(); + d_rows.push_back(RowVectorT(&d_entries)); + return ridx; + }else{ + RowIndex rid = d_pool.back(); + d_pool.pop_back(); + return rid; + } + } + + void releaseRowIndex(RowIndex rid){ + d_pool.push_back(rid); + } + public: size_t getNumRows() const { @@ -485,8 +505,11 @@ public: */ RowIndex addRow(const std::vector<T>& coeffs, const std::vector<ArithVar>& variables){ - RowIndex ridx = d_rows.size(); - d_rows.push_back(RowVectorT(&d_entries)); + + RowIndex ridx = requestRowIndex(); + + //RowIndex ridx = d_rows.size(); + //d_rows.push_back(RowVectorT(&d_entries)); std::vector<Rational>::const_iterator coeffIter = coeffs.begin(); std::vector<ArithVar>::const_iterator varsIter = variables.begin(); @@ -701,36 +724,7 @@ public: EntryID id = i.getID(); removeEntry(id); } - } - - - Node rowAsEquality(RowIndex rid, const ArithVarToNodeMap& map){ - using namespace CVC4::kind; - - Assert(getRowLength(rid) >= 2); - - std::vector<Node> pairs; - for(RowIterator i = getRow(rid); !i.atEnd(); ++i){ - const Entry& entry = *i; - ArithVar colVar = entry.getColVar(); - - Node var = (map.find(colVar))->second; - Node coeff = mkRationalNode(entry.getCoefficient()); - - Node mult = NodeBuilder<2>(MULT) << coeff << var; - pairs.push_back(mult); - } - - Node sum = Node::null(); - if(pairs.size() == 1 ){ - sum = pairs.front(); - }else{ - Assert(pairs.size() >= 2); - NodeBuilder<> sumBuilder(PLUS); - sumBuilder.append(pairs); - sum = sumBuilder; - } - return NodeBuilder<2>(EQUAL) << sum << mkRationalNode(d_zero); + releaseRowIndex(rid); } double densityMeasure() const{ @@ -754,6 +748,15 @@ public: } } + void loadSignQueries(RowIndex rid, DenseMap<int>& target) const{ + + RowIterator i = getRow(rid).begin(), i_end = getRow(rid).end(); + for(; i != i_end; ++i){ + const MatrixEntry<T>& entry = *i; + target.set(entry.getColVar(), entry.getCoefficient().sgn()); + } + } + protected: uint32_t numNonZeroEntries() const { return size(); } @@ -833,8 +836,10 @@ private: // Set of all of the basic variables in the tableau. // ArithVarMap<RowIndex> : ArithVar |-> RowIndex BasicToRowMap d_basic2RowIndex; + // RowIndex |-> Basic Variable - std::vector<ArithVar> d_rowIndex2basic; + typedef DenseMap<ArithVar> RowIndexToBasicMap; + RowIndexToBasicMap d_rowIndex2basic; public: @@ -882,10 +887,6 @@ public: return getRow(basicToRowIndex(basic)).begin(); } - // RowIterator rowIterator(RowIndex r) const { - // return getRow(r).begin(); - // } - /** * Adds a row to the tableau. * The new row is equivalent to: @@ -911,7 +912,6 @@ public: void removeBasicRow(ArithVar basic); - private: /* Changes the basic variable on the row for basicOld to basicNew. */ void rowPivot(ArithVar basicOld, ArithVar basicNew); |