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!
 

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;