diff options
author | Tim King <taking@cs.nyu.edu> | 2012-04-27 14:47:10 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-04-27 14:47:10 +0000 |
commit | f813ed144b0945334e03bfd769ea3c2cf8b75843 (patch) | |
tree | e70c9bddf5445aac50b5080c2b1719e6ffb478e0 /src/theory/arith/simplex.cpp | |
parent | 68237f7d39a03905be4cc133a42083fc3342adb4 (diff) |
This merges in the branch cvc4/branches/arithmetic/matrix into trunk.
- Splits the functionality of having a sparse matrix of Ts and a solved matrix of rationals in tableau.
- Splits ArithVarSet into DenseMap and CDDenseSet and simplifies the code.
- No performance loss!
Diffstat (limited to 'src/theory/arith/simplex.cpp')
-rw-r--r-- | src/theory/arith/simplex.cpp | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp index 9f48dad77..d3092c044 100644 --- a/src/theory/arith/simplex.cpp +++ b/src/theory/arith/simplex.cpp @@ -176,8 +176,8 @@ template <bool above> ArithVar SimplexDecisionProcedure::selectSlack(ArithVar x_i, SimplexDecisionProcedure::PreferenceFunction pref){ ArithVar slack = ARITHVAR_SENTINEL; - for(Tableau::RowIterator iter = d_tableau.rowIterator(x_i); !iter.atEnd(); ++iter){ - const TableauEntry& entry = *iter; + for(Tableau::RowIterator iter = d_tableau.basicRowIterator(x_i); !iter.atEnd(); ++iter){ + const Tableau::Entry& entry = *iter; ArithVar nonbasic = entry.getColVar(); if(nonbasic == x_i) continue; @@ -344,7 +344,7 @@ bool SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera bool useVarOrderPivot = d_pivotsInRound.count(x_i) >= Options::current()->arithPivotThreshold; if(!useVarOrderPivot){ - d_pivotsInRound.addMultiset(x_i); + d_pivotsInRound.add(x_i); } @@ -476,8 +476,8 @@ Node SimplexDecisionProcedure::weakenConflict(bool aboveUpper, ArithVar basicVar NodeBuilder<> conflict(kind::AND); bool anyWeakenings = false; - for(Tableau::RowIterator i = d_tableau.rowIterator(basicVar); !i.atEnd(); ++i){ - const TableauEntry& entry = *i; + for(Tableau::RowIterator i = d_tableau.basicRowIterator(basicVar); !i.atEnd(); ++i){ + const Tableau::Entry& entry = *i; ArithVar v = entry.getColVar(); const Rational& coeff = entry.getCoefficient(); bool weakening = false; |