From: Tim King <taking@cs.nyu.edu>
Date: Tue, 30 Apr 2013 04:46:14 +0000 (-0400)
Subject: Adding has bound counts and tracking for rows.
X-Git-Tag: cvc5-1.0.0~7287^2~163^2~3
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2b9e032cc93a96dccab8757326645da82b5866e5;p=cvc5.git

Adding has bound counts and tracking for rows.
---

diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am
index c5b07c3a5..466f8626f 100644
--- a/src/theory/arith/Makefile.am
+++ b/src/theory/arith/Makefile.am
@@ -11,6 +11,7 @@ libarith_la_SOURCES = \
 	arithvar.h \
 	arithvar.cpp \
 	bound_counts.h \
+	bound_counts.cpp \
 	arith_rewriter.h \
 	arith_rewriter.cpp \
 	arith_static_learner.h \
diff --git a/src/theory/arith/bound_counts.cpp b/src/theory/arith/bound_counts.cpp
new file mode 100644
index 000000000..27e9a35dc
--- /dev/null
+++ b/src/theory/arith/bound_counts.cpp
@@ -0,0 +1,16 @@
+#include "theory/arith/bound_counts.h"
+#include "theory/arith/tableau.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+const BoundsInfo& BoundCountingLookup::boundsInfo(ArithVar basic) const {
+  RowIndex ridx = d_tab->basicToRowIndex(basic);
+  Assert(d_bc->isKey(ridx));
+  return (*d_bc)[ridx];
+}
+
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/arith/bound_counts.h b/src/theory/arith/bound_counts.h
index 954cc056a..d82fff3eb 100644
--- a/src/theory/arith/bound_counts.h
+++ b/src/theory/arith/bound_counts.h
@@ -10,62 +10,92 @@ namespace CVC4 {
 namespace theory {
 namespace arith {
 
-/**
- * x = \sum_{a < 0} a_i i + \sum_{b > 0} b_j j
- *
- * AtUpperBound = {assignment(i) = lb(i)} \cup {assignment(j) = ub(j)}
- * AtLowerBound = {assignment(i) = ub(i)} \cup {assignment(j) = lb(j)}
- */
 class BoundCounts {
 private:
-  uint32_t d_atLowerBounds;
-  uint32_t d_atUpperBounds;
+  uint32_t d_lowerBoundCount;
+  uint32_t d_upperBoundCount;
 
 public:
-  BoundCounts() : d_atLowerBounds(0), d_atUpperBounds(0) {}
+  BoundCounts() : d_lowerBoundCount(0), d_upperBoundCount(0) {}
   BoundCounts(uint32_t lbs, uint32_t ubs)
-  : d_atLowerBounds(lbs), d_atUpperBounds(ubs) {}
+  : d_lowerBoundCount(lbs), d_upperBoundCount(ubs) {}
 
   bool operator==(BoundCounts bc) const {
-    return d_atLowerBounds == bc.d_atLowerBounds
-      && d_atUpperBounds == bc.d_atUpperBounds;
+    return d_lowerBoundCount == bc.d_lowerBoundCount
+      && d_upperBoundCount == bc.d_upperBoundCount;
   }
   bool operator!=(BoundCounts bc) const {
-    return  d_atLowerBounds != bc.d_atLowerBounds
-      || d_atUpperBounds != bc.d_atUpperBounds;
+    return  d_lowerBoundCount != bc.d_lowerBoundCount
+      || d_upperBoundCount != bc.d_upperBoundCount;
   }
-  inline bool isZero() const{ return d_atLowerBounds == 0 && d_atUpperBounds == 0; }
-  inline uint32_t atLowerBounds() const{
-    return d_atLowerBounds;
+  /** This is not a total order! */
+  bool operator>=(BoundCounts bc) const {
+    return d_lowerBoundCount >= bc.d_lowerBoundCount &&
+      d_upperBoundCount >= bc.d_upperBoundCount;
   }
-  inline uint32_t atUpperBounds() const{
-    return d_atUpperBounds;
+
+  inline bool isZero() const{ return d_lowerBoundCount == 0 && d_upperBoundCount == 0; }
+  inline uint32_t lowerBoundCount() const{
+    return d_lowerBoundCount;
+  }
+  inline uint32_t upperBoundCount() const{
+    return d_upperBoundCount;
   }
 
   inline BoundCounts operator+(BoundCounts bc) const{
-    return BoundCounts(d_atLowerBounds + bc.d_atLowerBounds,
-                       d_atUpperBounds + bc.d_atUpperBounds);
+    return BoundCounts(d_lowerBoundCount + bc.d_lowerBoundCount,
+                       d_upperBoundCount + bc.d_upperBoundCount);
   }
 
   inline BoundCounts operator-(BoundCounts bc) const {
-    Assert(d_atLowerBounds >= bc.d_atLowerBounds);
-    Assert(d_atUpperBounds >= bc.d_atUpperBounds);
-    return BoundCounts(d_atLowerBounds - bc.d_atLowerBounds,
-                       d_atUpperBounds - bc.d_atUpperBounds);
+    Assert( *this >= bc );
+    return BoundCounts(d_lowerBoundCount - bc.d_lowerBoundCount,
+                       d_upperBoundCount - bc.d_upperBoundCount);
+  }
+
+
+  inline BoundCounts& operator+=(BoundCounts bc) {
+    d_upperBoundCount += bc.d_upperBoundCount;
+    d_lowerBoundCount += bc.d_lowerBoundCount;
+    return *this;
+  }
+
+  inline BoundCounts& operator-=(BoundCounts bc) {
+    Assert(d_lowerBoundCount >= bc.d_lowerBoundCount);
+    Assert(d_upperBoundCount >= bc.d_upperBoundCount);
+    d_upperBoundCount -= bc.d_upperBoundCount;
+    d_lowerBoundCount -= bc.d_lowerBoundCount;
+
+    return *this;
+  }
+
+  /** Based on the sign coefficient a variable is multiplied by,
+   * the effects the bound counts either has no effect (sgn == 0),
+   * the lower bounds and upper bounds flip (sgn < 0), or nothing (sgn >0).
+   */
+  inline BoundCounts multiplyBySgn(int sgn) const{
+    if(sgn > 0){
+      return *this;
+    }else if(sgn == 0){
+      return BoundCounts(0,0);
+    }else{
+      return BoundCounts(d_upperBoundCount, d_lowerBoundCount);
+    }
   }
 
   inline void addInChange(int sgn, BoundCounts before, BoundCounts after){
-    Assert(before != after);
-    if(sgn < 0){
-      Assert(d_atUpperBounds >= before.d_atLowerBounds);
-      Assert(d_atLowerBounds >= before.d_atUpperBounds);
-      d_atUpperBounds += after.d_atLowerBounds - before.d_atLowerBounds;
-      d_atLowerBounds += after.d_atUpperBounds - before.d_atUpperBounds;
+    if(before == after){
+      return;
+    }else if(sgn < 0){
+      Assert(d_upperBoundCount >= before.d_lowerBoundCount);
+      Assert(d_lowerBoundCount >= before.d_upperBoundCount);
+      d_upperBoundCount += after.d_lowerBoundCount - before.d_lowerBoundCount;
+      d_lowerBoundCount += after.d_upperBoundCount - before.d_upperBoundCount;
     }else if(sgn > 0){
-      Assert(d_atUpperBounds >= before.d_atUpperBounds);
-      Assert(d_atLowerBounds >= before.d_atLowerBounds);
-      d_atUpperBounds += after.d_atUpperBounds - before.d_atUpperBounds;
-      d_atLowerBounds += after.d_atLowerBounds - before.d_atLowerBounds;
+      Assert(d_upperBoundCount >= before.d_upperBoundCount);
+      Assert(d_lowerBoundCount >= before.d_lowerBoundCount);
+      d_upperBoundCount += after.d_upperBoundCount - before.d_upperBoundCount;
+      d_lowerBoundCount += after.d_lowerBoundCount - before.d_lowerBoundCount;
     }
   }
 
@@ -74,69 +104,129 @@ public:
     Assert(!bc.isZero());
 
     if(before < 0){
-      d_atUpperBounds -= bc.d_atLowerBounds;
-      d_atLowerBounds -= bc.d_atUpperBounds;
+      d_upperBoundCount -= bc.d_lowerBoundCount;
+      d_lowerBoundCount -= bc.d_upperBoundCount;
     }else if(before > 0){
-      d_atUpperBounds -= bc.d_atUpperBounds;
-      d_atLowerBounds -= bc.d_atLowerBounds;
+      d_upperBoundCount -= bc.d_upperBoundCount;
+      d_lowerBoundCount -= bc.d_lowerBoundCount;
     }
     if(after < 0){
-      d_atUpperBounds += bc.d_atLowerBounds;
-      d_atLowerBounds += bc.d_atUpperBounds;
+      d_upperBoundCount += bc.d_lowerBoundCount;
+      d_lowerBoundCount += bc.d_upperBoundCount;
     }else if(after > 0){
-      d_atUpperBounds += bc.d_atUpperBounds;
-      d_atLowerBounds += bc.d_atLowerBounds;
+      d_upperBoundCount += bc.d_upperBoundCount;
+      d_lowerBoundCount += bc.d_lowerBoundCount;
     }
   }
+};
 
-  inline BoundCounts& operator+=(BoundCounts bc) {
-    d_atUpperBounds += bc.d_atUpperBounds;
-    d_atLowerBounds += bc.d_atLowerBounds;
-    return *this;
+class BoundsInfo {
+private:
+
+  /**
+   * x = \sum_{a < 0} a_i i + \sum_{b > 0} b_j j
+   *
+   * AtUpperBound = {assignment(i) = lb(i)} \cup {assignment(j) = ub(j)}
+   * AtLowerBound = {assignment(i) = ub(i)} \cup {assignment(j) = lb(j)}
+   */
+  BoundCounts d_atBounds;
+
+  /** This is for counting how many upper and lower bounds a row has. */
+  BoundCounts d_hasBounds;
+
+public:
+  BoundsInfo() : d_atBounds(), d_hasBounds() {}
+  BoundsInfo(BoundCounts atBounds, BoundCounts hasBounds)
+    : d_atBounds(atBounds), d_hasBounds(hasBounds) {}
+
+  BoundCounts atBounds() const { return d_atBounds; }
+  BoundCounts hasBounds() const { return d_hasBounds; }
+
+  /** This corresponds to adding in another variable to the row. */
+  inline BoundsInfo operator+(const BoundsInfo& bc) const{
+    return BoundsInfo(d_atBounds + bc.d_atBounds,
+                      d_hasBounds + bc.d_hasBounds);
+  }
+  /** This corresponds to removing a variable from the row. */
+  inline BoundsInfo operator-(const BoundsInfo& bc) const {
+    Assert(*this >= bc);
+    return BoundsInfo(d_atBounds - bc.d_atBounds,
+                      d_hasBounds - bc.d_hasBounds);
   }
 
-  inline BoundCounts& operator-=(BoundCounts bc) {
-    Assert(d_atLowerBounds >= bc.d_atLowerBounds);
-    Assert(d_atUpperBounds >= bc.d_atUpperBounds);
-    d_atUpperBounds -= bc.d_atUpperBounds;
-    d_atLowerBounds -= bc.d_atLowerBounds;
+  inline BoundsInfo& operator+=(const BoundsInfo& bc) {
+    d_atBounds += bc.d_atBounds;
+    d_hasBounds += bc.d_hasBounds;
+    return (*this);
+  }
 
-    return *this;
+  /** Based on the sign coefficient a variable is multiplied by,
+   * the effects the bound counts either has no effect (sgn == 0),
+   * the lower bounds and upper bounds flip (sgn < 0), or nothing (sgn >0).
+   */
+  inline BoundsInfo multiplyBySgn(int sgn) const{
+    return BoundsInfo(d_atBounds.multiplyBySgn(sgn), d_hasBounds.multiplyBySgn(sgn));
   }
 
-  inline BoundCounts multiplyBySgn(int sgn) const{
-    if(sgn > 0){
-      return *this;
-    }else if(sgn == 0){
-      return BoundCounts(0,0);
-    }else{
-      return BoundCounts(d_atUpperBounds, d_atLowerBounds);
-    }
+  bool operator==(const BoundsInfo& other) const{
+    return d_atBounds == other.d_atBounds && d_hasBounds == other.d_hasBounds;
+  }
+  bool operator!=(const BoundsInfo& other) const{
+    return !(*this == other);
+  }
+  /** This is not a total order! */
+  bool operator>=(const BoundsInfo& other) const{
+    return d_atBounds >= other.d_atBounds && d_hasBounds >= other.d_hasBounds;
+  }
+  void addInChange(int sgn, const BoundsInfo& before, const BoundsInfo& after){
+    addInAtBoundChange(sgn, before.d_atBounds, after.d_atBounds);
+    addInHasBoundChange(sgn, before.d_hasBounds, after.d_hasBounds);
+  }
+  void addInAtBoundChange(int sgn, BoundCounts before, BoundCounts after){
+    d_atBounds.addInChange(sgn, before, after);
+  }
+  void addInHasBoundChange(int sgn, BoundCounts before, BoundCounts after){
+    d_hasBounds.addInChange(sgn, before, after);
+  }
+
+  inline void addInSgn(const BoundsInfo& bc, int before, int after){
+    if(!bc.d_atBounds.isZero()){ d_atBounds.addInSgn(bc.d_atBounds, before, after);}
+    if(!bc.d_hasBounds.isZero()){ d_hasBounds.addInSgn(bc.d_hasBounds, before, after);}
   }
 };
 
-typedef DenseMap<BoundCounts> BoundCountingVector;
+/** This is intended to map each row to its relevant bound information. */
+typedef DenseMap<BoundsInfo> BoundInfoMap;
+
+class Tableau;
 
 class BoundCountingLookup {
 private:
-  BoundCountingVector* d_bc;
+  BoundInfoMap* d_bc;
+  Tableau* d_tab;
 public:
-  BoundCountingLookup(BoundCountingVector* bc) : d_bc(bc) {}
-  BoundCounts boundCounts(ArithVar v) const {
-    Assert(d_bc->isKey(v));
-    return (*d_bc)[v];
+  BoundCountingLookup(BoundInfoMap* bc, Tableau* tab) : d_bc(bc), d_tab(tab) {}
+  const BoundsInfo& boundsInfo(ArithVar basic) const;
+  BoundCounts atBounds(ArithVar basic) const{
+    return boundsInfo(basic).atBounds();
+  }
+  BoundCounts hasBounds(ArithVar basic) const {
+    return boundsInfo(basic).hasBounds();
   }
 };
 
 inline std::ostream& operator<<(std::ostream& os, const BoundCounts& bc){
-  os << "[bc " << bc.atLowerBounds() << ", "
-     << bc.atUpperBounds() << "]";
+  os << "[bc " << bc.lowerBoundCount() << ", " << bc.upperBoundCount() << "]";
   return os;
 }
 
-class BoundCountsCallback {
+inline std::ostream& operator<<(std::ostream& os, const BoundsInfo& inf){
+  os << "[bi : @ " << inf.atBounds() << ", " << inf.hasBounds() << "]";
+  return os;
+}
+class BoundUpdateCallback {
 public:
-  virtual void operator()(ArithVar v, BoundCounts bc) = 0;
+  virtual void operator()(ArithVar v, const BoundsInfo&  up) = 0;
 };
 
 }/* CVC4::theory::arith namespace */
diff --git a/src/theory/arith/error_set.h b/src/theory/arith/error_set.h
index ce6412573..0d24fa099 100644
--- a/src/theory/arith/error_set.h
+++ b/src/theory/arith/error_set.h
@@ -361,8 +361,8 @@ public:
 
   uint32_t sumMetric(ArithVar a) const{
     Assert(inError(a));
-    BoundCounts bcs = d_boundLookup.boundCounts(a);
-    uint32_t count = getSgn(a) > 0 ? bcs.atUpperBounds() : bcs.atLowerBounds();
+    BoundCounts bcs = d_boundLookup.atBounds(a);
+    uint32_t count = getSgn(a) > 0 ? bcs.upperBoundCount() : bcs.lowerBoundCount();
 
     uint32_t length = d_tableauSizes.getRowLength(a);
 
diff --git a/src/theory/arith/fc_simplex.cpp b/src/theory/arith/fc_simplex.cpp
index ac4625ba3..d264be978 100644
--- a/src/theory/arith/fc_simplex.cpp
+++ b/src/theory/arith/fc_simplex.cpp
@@ -289,7 +289,7 @@ UpdateInfo FCSimplexDecisionProcedure::selectPrimalUpdate(ArithVar basic, Linear
   Debug("arith::selectPrimalUpdate")
     << "selectPrimalUpdate " << instance << endl
     << basic << " " << d_tableau.basicRowLength(basic)
-    << " " << d_linEq._countBounds(basic) << endl;
+    << " " << d_linEq.debugBasicAtBoundCount(basic) << endl;
 
   static const int s_maxCandidatesAfterImprove = 3;
   bool isFocus = basic == d_focusErrorVar;
@@ -505,7 +505,7 @@ void FCSimplexDecisionProcedure::debugPrintSignal(ArithVar updated) const{
   int dir = !d_variables.assignmentIsConsistent(updated) ?
     d_errorSet.getSgn(updated) : 0;
   Debug("updateAndSignal") << " dir " << dir;
-  Debug("updateAndSignal") << " _countBounds " << d_linEq._countBounds(updated) << endl;
+  Debug("updateAndSignal") << " debugBasicAtBoundCount " << d_linEq.debugBasicAtBoundCount(updated) << endl;
 }
 
 bool debugUpdatedBasic(const UpdateInfo& selected, ArithVar updated){
@@ -530,7 +530,7 @@ void FCSimplexDecisionProcedure::updateAndSignal(const UpdateInfo& selected, Wit
       ArithVar leaving = selected.leaving();
       ss << "leaving " << leaving
          << " " << d_tableau.basicRowLength(leaving)
-         << " " << d_linEq._countBounds(leaving)
+         << " " << d_linEq.debugBasicAtBoundCount(leaving)
          << endl;
     }
     if(degenerate(w) && selected.describesPivot()){
@@ -539,7 +539,7 @@ void FCSimplexDecisionProcedure::updateAndSignal(const UpdateInfo& selected, Wit
         << "degenerate " << leaving
         << ", atBounds " << d_linEq.basicsAtBounds(selected)
         << ", len " << d_tableau.basicRowLength(leaving)
-        << ", bc " << d_linEq._countBounds(leaving)
+        << ", bc " << d_linEq.debugBasicAtBoundCount(leaving)
         << endl;
     }
   }
diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp
index 42d8b41f8..eda3bf682 100644
--- a/src/theory/arith/linear_equality.cpp
+++ b/src/theory/arith/linear_equality.cpp
@@ -31,12 +31,6 @@ template void LinearEqualityModule::propagateNonbasics<false>(ArithVar basic, Co
 template ArithVar LinearEqualityModule::selectSlack<true>(ArithVar x_i, VarPreferenceFunction pf) const;
 template ArithVar LinearEqualityModule::selectSlack<false>(ArithVar x_i, VarPreferenceFunction pf) const;
 
-// template bool LinearEqualityModule::preferNonDegenerate<true>(const UpdateInfo& a, const UpdateInfo& b) const;
-// template bool LinearEqualityModule::preferNonDegenerate<false>(const UpdateInfo& a, const UpdateInfo& b) const;
-
-// template bool LinearEqualityModule::preferErrorsFixed<true>(const UpdateInfo& a, const UpdateInfo& b) const;
-// template bool LinearEqualityModule::preferErrorsFixed<false>(const UpdateInfo& a, const UpdateInfo& b) const;
-
 template bool LinearEqualityModule::preferWitness<true>(const UpdateInfo& a, const UpdateInfo& b) const;
 template bool LinearEqualityModule::preferWitness<false>(const UpdateInfo& a, const UpdateInfo& b) const;
 
@@ -57,14 +51,14 @@ void Border::output(std::ostream& out) const{
       << "}";
 }
 
-LinearEqualityModule::LinearEqualityModule(ArithVariables& vars, Tableau& t, BoundCountingVector& boundTracking, BasicVarModelUpdateCallBack f):
+LinearEqualityModule::LinearEqualityModule(ArithVariables& vars, Tableau& t, BoundInfoMap& boundsTracking, BasicVarModelUpdateCallBack f):
   d_variables(vars),
   d_tableau(t),
   d_basicVariableUpdates(f),
   d_increasing(1),
   d_decreasing(-1),
   d_relevantErrorBuffer(),
-  d_boundTracking(boundTracking),
+  d_btracking(boundsTracking),
   d_areTracking(false),
   d_trackCallback(this)
 {}
@@ -103,31 +97,24 @@ LinearEqualityModule::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_weakenings);
   StatisticsRegistry::unregisterStat(&d_weakenTime);
 }
-void LinearEqualityModule::includeBoundCountChange(ArithVar nb, BoundCounts prev){
-  if(d_tableau.isBasic(nb)){
-    return;
-  }
-  Assert(!d_tableau.isBasic(nb));
+void LinearEqualityModule::includeBoundUpdate(ArithVar v, const BoundsInfo& prev){
   Assert(!d_areTracking);
 
-  BoundCounts curr = d_variables.boundCounts(nb);
+  BoundsInfo curr = d_variables.boundsInfo(v);
 
   Assert(prev != curr);
-  Tableau::ColIterator basicIter = d_tableau.colIterator(nb);
+  Tableau::ColIterator basicIter = d_tableau.colIterator(v);
   for(; !basicIter.atEnd(); ++basicIter){
     const Tableau::Entry& entry = *basicIter;
-    Assert(entry.getColVar() == nb);
+    Assert(entry.getColVar() == v);
     int a_ijSgn = entry.getCoefficient().sgn();
 
-    ArithVar basic = d_tableau.rowIndexToBasic(entry.getRowIndex());
-
-    BoundCounts& counts = d_boundTracking.get(basic);
-    Debug("includeBoundCountChange") << basic << " " << counts << " to " ;
-    counts -= prev.multiplyBySgn(a_ijSgn);
-    counts += curr.multiplyBySgn(a_ijSgn);
-    Debug("includeBoundCountChange") << counts << " " << a_ijSgn << std::endl;
+    RowIndex ridx = entry.getRowIndex();
+    BoundsInfo& counts = d_btracking.get(ridx);
+    Debug("includeBoundUpdate") << d_tableau.rowIndexToBasic(ridx) << " " << counts << " to " ;
+    counts.addInChange(a_ijSgn, prev, curr);
+    Debug("includeBoundUpdate") << counts << " " << a_ijSgn << std::endl;
   }
-  d_boundTracking.set(nb, curr);
 }
 
 void LinearEqualityModule::updateMany(const DenseMap<DeltaRational>& many){
@@ -231,9 +218,9 @@ void LinearEqualityModule::updateTracked(ArithVar x_i, const DeltaRational& v){
                  << d_variables.getAssignment(x_i) << "|-> " << v << endl;
 
 
-  BoundCounts before = d_variables.boundCounts(x_i);
+  BoundCounts before = d_variables.atBoundCounts(x_i);
   d_variables.setAssignment(x_i, v);
-  BoundCounts after = d_variables.boundCounts(x_i);
+  BoundCounts after = d_variables.atBoundCounts(x_i);
 
   bool anyChange = before != after;
 
@@ -242,17 +229,24 @@ void LinearEqualityModule::updateTracked(ArithVar x_i, const DeltaRational& v){
     const Tableau::Entry& entry = *colIter;
     Assert(entry.getColVar() == x_i);
 
-    ArithVar x_j = d_tableau.rowIndexToBasic(entry.getRowIndex());
+    RowIndex ridx = entry.getRowIndex();
+    ArithVar x_j = d_tableau.rowIndexToBasic(ridx);
     const Rational& a_ji = entry.getCoefficient();
 
     const DeltaRational& assignment = d_variables.getAssignment(x_j);
     DeltaRational  nAssignment = assignment+(diff * a_ji);
     Debug("update") << x_j << " " << a_ji << assignment << " -> " << nAssignment << endl;
+    BoundCounts xjBefore = d_variables.atBoundCounts(x_j);
     d_variables.setAssignment(x_j, nAssignment);
+    BoundCounts xjAfter = d_variables.atBoundCounts(x_j);
 
-    if(anyChange && basicIsTracked(x_j)){
-      BoundCounts& next_bc_k = d_boundTracking.get(x_j);
-      next_bc_k.addInChange(a_ji.sgn(), before, after);
+    Assert(rowIndexIsTracked(ridx));
+    BoundsInfo& next_bc_k = d_btracking.get(ridx);
+    if(anyChange){
+      next_bc_k.addInAtBoundChange(a_ji.sgn(), before, after);
+    }
+    if(xjBefore != xjAfter){
+      next_bc_k.addInAtBoundChange(-1, xjBefore, xjAfter);
     }
 
     d_basicVariableUpdates(x_j);
@@ -332,7 +326,7 @@ void LinearEqualityModule::debugCheckTracking(){
       ArithVar var = entry.getColVar();
       const Rational& coeff = entry.getCoefficient();
       DeltaRational beta = d_variables.getAssignment(var);
-      Debug("arith::tracking") << var << " " << d_variables.boundCounts(var)
+      Debug("arith::tracking") << var << " " << d_variables.boundsInfo(var)
                                << " " << beta << coeff;
       if(d_variables.hasLowerBound(var)){
         Debug("arith::tracking") << "(lb " << d_variables.getLowerBound(var) << ")";
@@ -345,11 +339,12 @@ void LinearEqualityModule::debugCheckTracking(){
     Debug("arith::tracking") << "end row"<< endl;
 
     if(basicIsTracked(basic)){
-      BoundCounts computed = computeBoundCounts(basic);
+      RowIndex ridx = d_tableau.basicToRowIndex(basic);
+      BoundsInfo computed = computeRowBoundInfo(ridx, false);
       Debug("arith::tracking")
         << "computed " << computed
-        << " tracking " << d_boundTracking[basic] << endl;
-      Assert(computed == d_boundTracking[basic]);
+        << " tracking " << d_btracking[ridx] << endl;
+      Assert(computed == d_btracking[ridx]);
 
     }
   }
@@ -745,60 +740,34 @@ void LinearEqualityModule::stopTrackingBoundCounts(){
 }
 
 
-void LinearEqualityModule::trackVariable(ArithVar x_i){
-  Assert(!basicIsTracked(x_i));
-  BoundCounts counts(0,0);
-
-  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;
-
-    const Rational& a_ij = entry.getCoefficient();
-    counts += (d_variables.oldBoundCounts(nonbasic)).multiplyBySgn(a_ij.sgn());
-  }
-  d_boundTracking.set(x_i, counts);
+void LinearEqualityModule::trackRowIndex(RowIndex ridx){
+  Assert(!rowIndexIsTracked(ridx));
+  BoundsInfo bi = computeRowBoundInfo(ridx, true);
+  d_btracking.set(ridx, bi);
 }
 
-BoundCounts LinearEqualityModule::computeBoundCounts(ArithVar x_i) const{
-  BoundCounts counts(0,0);
+BoundsInfo LinearEqualityModule::computeRowBoundInfo(RowIndex ridx, bool inQueue) const{
+  BoundsInfo bi;
 
-  for(Tableau::RowIterator iter = d_tableau.basicRowIterator(x_i); !iter.atEnd();  ++iter){
+  for(Tableau::RowIterator iter = d_tableau.getRow(ridx).begin(); !iter.atEnd();  ++iter){
     const Tableau::Entry& entry = *iter;
-    ArithVar nonbasic = entry.getColVar();
-    if(nonbasic == x_i) continue;
-
+    ArithVar v = entry.getColVar();
     const Rational& a_ij = entry.getCoefficient();
-    counts += (d_variables.boundCounts(nonbasic)).multiplyBySgn(a_ij.sgn());
+    bi += (d_variables.selectBoundsInfo(v, inQueue)).multiplyBySgn(a_ij.sgn());
   }
-
-  return counts;
+  return bi;
 }
 
-// BoundCounts LinearEqualityModule::cachingCountBounds(ArithVar x_i) const{
-//   if(d_boundTracking.isKey(x_i)){
-//     return d_boundTracking[x_i];
-//   }else{
-//     return computeBoundCounts(x_i);
-//   }
-// }
-BoundCounts LinearEqualityModule::_countBounds(ArithVar x_i) const {
-  Assert(d_boundTracking.isKey(x_i));
-  return d_boundTracking[x_i];
+BoundCounts LinearEqualityModule::debugBasicAtBoundCount(ArithVar x_i) const {
+  return d_btracking[d_tableau.basicToRowIndex(x_i)].atBounds();
 }
 
-// BoundCounts LinearEqualityModule::countBounds(ArithVar x_i){
-//   if(d_boundTracking.isKey(x_i)){
-//     return d_boundTracking[x_i];
-//   }else{
-//     BoundCounts bc = computeBoundCounts(x_i);
-//     if(d_areTracking){
-//       d_boundTracking.set(x_i,bc);
-//     }
-//     return bc;
-//   }
-// }
-
+/**
+ * If the pivot described in u were performed,
+ * then the row would qualify as being either at the minimum/maximum
+ * to the non-basics being at their bounds.
+ * The minimum/maximum is determined by the direction the non-basic is changing.
+ */
 bool LinearEqualityModule::basicsAtBounds(const UpdateInfo& u) const {
   Assert(u.describesPivot());
 
@@ -814,79 +783,78 @@ bool LinearEqualityModule::basicsAtBounds(const UpdateInfo& u) const {
   int toLB = (c->getType() == LowerBound ||
               c->getType() == Equality) ? 1 : 0;
 
+  RowIndex ridx = d_tableau.basicToRowIndex(basic);
 
-  BoundCounts bcs = d_boundTracking[basic];
+  BoundCounts bcs = d_btracking[ridx].atBounds();
   // x = c*n + \sum d*m
-  // n = 1/c * x + -1/c * (\sum d*m)  
-  BoundCounts nonb = bcs - d_variables.boundCounts(nonbasic).multiplyBySgn(coeffSgn);
+  // 0 = -x + c*n + \sum d*m
+  // n = 1/c * x + -1/c * (\sum d*m)
+  BoundCounts nonb = bcs - d_variables.atBoundCounts(nonbasic).multiplyBySgn(coeffSgn);
+  nonb.addInChange(-1, d_variables.atBoundCounts(basic), BoundCounts(toLB, toUB));
   nonb = nonb.multiplyBySgn(-coeffSgn);
-  nonb += BoundCounts(toLB, toUB).multiplyBySgn(coeffSgn);
 
   uint32_t length = d_tableau.basicRowLength(basic);
   Debug("basicsAtBounds")
     << "bcs " << bcs
     << "nonb " << nonb
     << "length " << length << endl;
-
+  // nonb has nb excluded.
   if(nbdir < 0){
-    return bcs.atLowerBounds() + 1 == length;
+    return nonb.lowerBoundCount() + 1 == length;
   }else{
     Assert(nbdir > 0);
-    return bcs.atUpperBounds() + 1 == length;
+    return nonb.upperBoundCount() + 1 == length;
   }
 }
 
 bool LinearEqualityModule::nonbasicsAtLowerBounds(ArithVar basic) const {
   Assert(basicIsTracked(basic));
-  BoundCounts bcs = d_boundTracking[basic];
+  RowIndex ridx = d_tableau.basicToRowIndex(basic);
+
+  BoundCounts bcs = d_btracking[ridx].atBounds();
   uint32_t length = d_tableau.basicRowLength(basic);
 
-  return bcs.atLowerBounds() + 1 == length;
+  // return true if excluding the basic is every element is at its "lowerbound"
+  // The psuedo code is:
+  //   bcs -= basic.count(basic, basic's sgn)
+  //   return bcs.lowerBoundCount() + 1 == length
+  // As basic's sign is always -1, we can pull out the pieces of the count:
+  //   bcs.lowerBoundCount() - basic.atUpperBoundInd() + 1 == length
+  // basic.atUpperBoundInd() is either 0 or 1
+  uint32_t lbc = bcs.lowerBoundCount();
+  return  (lbc == length) ||
+    (lbc + 1 == length && d_variables.cmpAssignmentUpperBound(basic) != 0);
 }
 
 bool LinearEqualityModule::nonbasicsAtUpperBounds(ArithVar basic) const {
   Assert(basicIsTracked(basic));
-  BoundCounts bcs = d_boundTracking[basic];
+  RowIndex ridx = d_tableau.basicToRowIndex(basic);
+  BoundCounts bcs = d_btracking[ridx].atBounds();
   uint32_t length = d_tableau.basicRowLength(basic);
+  uint32_t ubc = bcs.upperBoundCount();
+  // See the comment for nonbasicsAtLowerBounds()
 
-  return bcs.atUpperBounds() + 1 == length;
+  return (ubc == length) ||
+    (ubc + 1 == length && d_variables.cmpAssignmentLowerBound(basic) != 0);
 }
 
-void LinearEqualityModule::trackingSwap(ArithVar basic, ArithVar nb, int nbSgn) {
-  Assert(basicIsTracked(basic));
-
-  // z = a*x + \sum b*y
-  // x = (1/a) z + \sum (-1/a)*b*y
-  // basicCount(z) = bc(a*x) +  bc(\sum b y)
-  // basicCount(x) = bc(z/a) + bc(\sum -b/a * y)
-
-  // sgn(1/a) = sgn(a)
-  // bc(a*x) = bc(x).multiply(sgn(a))
-  // bc(z/a) = bc(z).multiply(sgn(a))
-  // bc(\sum -b/a * y) = bc(\sum b y).multiplyBySgn(-sgn(a))
-  // bc(\sum b y) = basicCount(z) - bc(a*x)
-  // basicCount(x) =
-  //  = bc(z).multiply(sgn(a)) + (basicCount(z) - bc(a*x)).multiplyBySgn(-sgn(a))
-
-  BoundCounts bc = d_boundTracking[basic];
-  bc -= (d_variables.boundCounts(nb)).multiplyBySgn(nbSgn);
-  bc = bc.multiplyBySgn(-nbSgn);
-  bc += d_variables.boundCounts(basic).multiplyBySgn(nbSgn);
-  d_boundTracking.set(nb, bc);
-  d_boundTracking.remove(basic);
+void LinearEqualityModule::trackingMultiplyRow(RowIndex ridx, int sgn) {
+  Assert(rowIndexIsTracked(ridx));
+  Assert(sgn != 0);
+  if(sgn < 0){
+    BoundsInfo& bi = d_btracking.get(ridx);
+    bi = bi.multiplyBySgn(sgn);
+  }
 }
 
 void LinearEqualityModule::trackingCoefficientChange(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn){
   Assert(oldSgn != currSgn);
-  BoundCounts nb_bc = d_variables.boundCounts(nb);
+  BoundsInfo nb_inf = d_variables.boundsInfo(nb);
 
-  if(!nb_bc.isZero()){
-    ArithVar basic = d_tableau.rowIndexToBasic(ridx);
-    Assert(basicIsTracked(basic));
+  Assert(rowIndexIsTracked(ridx));
 
-    BoundCounts& basic_bc = d_boundTracking.get(basic);
-    basic_bc.addInSgn(nb_bc, oldSgn, currSgn);
-  }
+  BoundsInfo& row_bi = d_btracking.get(ridx);
+  row_bi.addInSgn(nb_inf, oldSgn, currSgn);
 }
 
 void LinearEqualityModule::computeSafeUpdate(UpdateInfo& inf, VarPreferenceFunction pref){
@@ -895,9 +863,6 @@ void LinearEqualityModule::computeSafeUpdate(UpdateInfo& inf, VarPreferenceFunct
   Assert(sgn != 0);
   Assert(!d_tableau.isBasic(nb));
 
-  //inf.setErrorsChange(0);
-  //inf.setlimiting = NullConstraint;
-
 
   // Error variables moving in the correct direction
   Assert(d_relevantErrorBuffer.empty());
@@ -1188,8 +1153,9 @@ bool LinearEqualityModule::willBeInConflictAfterPivot(const Tableau::Entry& entr
 
   // Assume past this point, nb will be in error if this pivot is done
   ArithVar nb = entry.getColVar();
-  ArithVar basic = d_tableau.rowIndexToBasic(entry.getRowIndex());
-  Assert(basicIsTracked(basic));
+  RowIndex ridx = entry.getRowIndex();
+  ArithVar basic = d_tableau.rowIndexToBasic(ridx);
+  Assert(rowIndexIsTracked(ridx));
   int coeffSgn = entry.getCoefficient().sgn();
 
 
@@ -1201,12 +1167,11 @@ bool LinearEqualityModule::willBeInConflictAfterPivot(const Tableau::Entry& entr
   // 2) -a * x = -y + \sum b * z
   // 3) x = (-1/a) * ( -y + \sum b * z)
 
-  Assert(basicIsTracked(basic));
-  BoundCounts bc = d_boundTracking[basic];
+  BoundCounts bc = d_btracking[ridx].atBounds();
 
   // 1) y = a * x + \sum b * z
   // Get bc(\sum b * z)
-  BoundCounts sumOnly = bc - d_variables.boundCounts(nb).multiplyBySgn(coeffSgn);
+  BoundCounts sumOnly = bc - d_variables.atBoundCounts(nb).multiplyBySgn(coeffSgn);
 
   // y's bounds in the proposed model
   int yWillBeAtUb = (bToUB || d_variables.boundsAreEqual(basic)) ? 1 : 0;
@@ -1215,19 +1180,19 @@ bool LinearEqualityModule::willBeInConflictAfterPivot(const Tableau::Entry& entr
 
   // 2) -a * x = -y + \sum b * z
   // Get bc(-y + \sum b * z)
-  BoundCounts withNegY = sumOnly + ysBounds.multiplyBySgn(-1);
+  sumOnly.addInChange(-1, d_variables.atBoundCounts(basic), ysBounds);
 
   // 3) x = (-1/a) * ( -y + \sum b * z)
   // Get bc((-1/a) * ( -y + \sum b * z))
-  BoundCounts xsBoundsAfterPivot = withNegY.multiplyBySgn(-coeffSgn);
+  BoundCounts xsBoundsAfterPivot = sumOnly.multiplyBySgn(-coeffSgn);
 
   uint32_t length = d_tableau.basicRowLength(basic);
   if(nbSgn > 0){
     // Only check for the upper bound being violated
-    return xsBoundsAfterPivot.atLowerBounds() + 1 == length;
+    return xsBoundsAfterPivot.lowerBoundCount() + 1 == length;
   }else{
     // Only check for the lower bound being violated
-    return xsBoundsAfterPivot.atUpperBounds() + 1 == length;
+    return xsBoundsAfterPivot.upperBoundCount() + 1 == length;
   }
 }
 
diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h
index 8b9b888f2..bc653fdad 100644
--- a/src/theory/arith/linear_equality.h
+++ b/src/theory/arith/linear_equality.h
@@ -192,9 +192,6 @@ public:
 };
 
 
-
-
-
 class LinearEqualityModule {
 public:
   typedef ArithVar (LinearEqualityModule::*VarPreferenceFunction)(ArithVar, ArithVar) const;
@@ -226,14 +223,12 @@ public:
    * Initializes a LinearEqualityModule with a partial model, a tableau,
    * and a callback function for when basic variables update their values.
    */
-  LinearEqualityModule(ArithVariables& vars, Tableau& t, BoundCountingVector& boundTracking, BasicVarModelUpdateCallBack f);
+  LinearEqualityModule(ArithVariables& vars, Tableau& t, BoundInfoMap& boundTracking, BasicVarModelUpdateCallBack f);
 
   /**
    * Updates the assignment of a nonbasic variable x_i to v.
    * Also updates the assignment of basic variables accordingly.
    */
-  void updateUntracked(ArithVar x_i, const DeltaRational& v);
-  void updateTracked(ArithVar x_i, const DeltaRational& v);
   void update(ArithVar x_i, const DeltaRational& v){
     if(d_areTracking){
       updateTracked(x_i,v);
@@ -241,6 +236,17 @@ public:
       updateUntracked(x_i,v);
     }
   }
+
+  /** Specialization of update if the module is not tracking yet (for Assert*). */
+  void updateUntracked(ArithVar x_i, const DeltaRational& v);
+
+  /** Specialization of update if the module is not tracking yet (for Simplex). */
+  void updateTracked(ArithVar x_i, const DeltaRational& v);
+
+  /**
+   * Updates every non-basic to reflect the assignment in many.
+   * For use with ApproximateSimplex.
+   */
   void updateMany(const DenseMap<DeltaRational>& many);
 
   /**
@@ -268,7 +274,7 @@ public:
   void stopTrackingBoundCounts();
 
 
-  void includeBoundCountChange(ArithVar nb, BoundCounts prev);
+  void includeBoundUpdate(ArithVar nb, const BoundsInfo& prev);
 
   void computeSafeUpdate(UpdateInfo& inf, VarPreferenceFunction basic);
 
@@ -334,40 +340,6 @@ public:
     }
   }
 
-  // template<bool heuristic>
-  // bool preferNonDegenerate(const UpdateInfo& a, const UpdateInfo& b) const{
-  //   if(a.focusDirection() == b.focusDirection()){
-  //     if(heuristic){
-  //       return preferNeitherBound(a,b);
-  //     }else{
-  //       return minNonBasicVarOrder(a,b);
-  //     }
-  //   }else{
-  //     return a.focusDirection() < b.focusDirection();
-  //   }
-  // }
-
-  // template <bool heuristic>
-  // bool preferErrorsFixed(const UpdateInfo& a, const UpdateInfo& b) const{
-  //   if( a.errorsChange() == b.errorsChange() ){
-  //     return preferNonDegenerate<heuristic>(a,b);
-  //   }else{
-  //     return a.errorsChange() > b.errorsChange();
-  //   }
-  // }
-
-  // template <bool heuristic>
-  // bool preferConflictFound(const UpdateInfo& a, const UpdateInfo& b) const{
-  //   if(a.d_foundConflict && b.d_foundConflict){
-  //     // if both are true, determinize the preference
-  //     return minNonBasicVarOrder(a,b);
-  //   }else if( a.d_foundConflict || b.d_foundConflict ){
-  //     return b.d_foundConflict;
-  //   }else{
-  //     return preferErrorsFixed<heuristic>(a,b);
-  //   }
-  // }
-
   bool modifiedBlands(const UpdateInfo& a, const UpdateInfo& b) const {
     Assert(a.focusDirection() == 0 && b.focusDirection() == 0);
     Assert(a.describesPivot());
@@ -434,8 +406,10 @@ private:
   //uint32_t computedFixed(ArithVar nb, int sgn, const DeltaRational& am);
   void computedFixed(UpdateInfo&);
 
-  // RowIndex -> BoundCount
-  BoundCountingVector& d_boundTracking;
+  /**
+   * This maps each row index to its relevant bounds info.
+   * This tracks the */
+  BoundInfoMap& d_btracking;
   bool d_areTracking;
 
   /**
@@ -548,31 +522,34 @@ public:
 
   const Tableau::Entry* selectSlackEntry(ArithVar x_i, bool above) const;
 
+  inline bool rowIndexIsTracked(RowIndex ridx) const {
+    return d_btracking.isKey(ridx);
+  }
   inline bool basicIsTracked(ArithVar v) const {
-    return d_boundTracking.isKey(v);
+    return rowIndexIsTracked(d_tableau.basicToRowIndex(v));
   }
-  void trackVariable(ArithVar x_i);
-
-  void maybeRemoveTracking(ArithVar v){
-    Assert(!d_tableau.isBasic(v));
-    if(d_boundTracking.isKey(v)){
-      d_boundTracking.remove(v);
-    }
+  void trackRowIndex(RowIndex ridx);
+  void stopTrackingRowIndex(RowIndex ridx){
+    Assert(rowIndexIsTracked(ridx));
+    d_btracking.remove(ridx);
   }
 
-  // void trackVariable(ArithVar x_i){
-  //   Assert(!basicIsTracked(x_i));
-  //   d_boundTracking.set(x_i,computeBoundCounts(x_i));
-  // }
+  /**
+   * If the pivot described in u were performed,
+   * then the row would qualify as being either at the minimum/maximum
+   * to the non-basics being at their bounds.
+   * The minimum/maximum is determined by the direction the non-basic is changing.
+   */
   bool basicsAtBounds(const UpdateInfo& u) const;
 private:
-  BoundCounts computeBoundCounts(ArithVar x_i) const;
+  //BoundCounts computeBasicAtBoundCounts(ArithVar x_i) const;
+  //BoundCounts computeRowAtBoundCounts(RowIndex ridx) const;
+  BoundsInfo computeRowBoundInfo(RowIndex ridx, bool inQueue) const;
 public:
   //BoundCounts cachingCountBounds(ArithVar x_i) const;
-  BoundCounts _countBounds(ArithVar x_i) const;
+  BoundCounts debugBasicAtBoundCount(ArithVar x_i) const;
   void trackingCoefficientChange(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn);
-
-  void trackingSwap(ArithVar basic, ArithVar nb, int sgn);
+  void trackingMultiplyRow(RowIndex ridx, int sgn);
 
   bool nonbasicsAtLowerBounds(ArithVar x_i) const;
   bool nonbasicsAtUpperBounds(ArithVar x_i) const;
@@ -593,8 +570,8 @@ private:
     void update(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn){
       d_linEq->trackingCoefficientChange(ridx, nb, oldSgn, currSgn);
     }
-    void swap(ArithVar basic, ArithVar nb, int oldNbSgn){
-      d_linEq->trackingSwap(basic, nb, oldNbSgn);
+    void multiplyRow(RowIndex ridx, int sgn){
+      d_linEq->trackingMultiplyRow(ridx, sgn);
     }
     bool canUseRow(RowIndex ridx) const {
       ArithVar basic = d_linEq->getTableau().rowIndexToBasic(ridx);
@@ -737,13 +714,13 @@ public:
   }
 };
 
-class UpdateTrackingCallback : public BoundCountsCallback {
+class UpdateTrackingCallback : public BoundUpdateCallback {
 private:
   LinearEqualityModule* d_mod;
 public:
   UpdateTrackingCallback(LinearEqualityModule* mod): d_mod(mod){}
-  void operator()(ArithVar v, BoundCounts bc){
-    d_mod->includeBoundCountChange(v, bc);
+  void operator()(ArithVar v, const BoundsInfo& bi){
+    d_mod->includeBoundUpdate(v, bi);
   }
 };
 
diff --git a/src/theory/arith/matrix.cpp b/src/theory/arith/matrix.cpp
index 7136c3fa8..b8bd68488 100644
--- a/src/theory/arith/matrix.cpp
+++ b/src/theory/arith/matrix.cpp
@@ -24,7 +24,7 @@ namespace theory {
 namespace arith {
 
 void NoEffectCCCB::update(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn) {}
-void NoEffectCCCB::swap(ArithVar basic, ArithVar nb, int nbSgn){}
+void NoEffectCCCB::multiplyRow(RowIndex ridx, int sgn){}
 bool NoEffectCCCB::canUseRow(RowIndex ridx) const { return false; }
 
 }/* CVC4::theory::arith namespace */
diff --git a/src/theory/arith/matrix.h b/src/theory/arith/matrix.h
index 100f999e0..d93b6986e 100644
--- a/src/theory/arith/matrix.h
+++ b/src/theory/arith/matrix.h
@@ -39,15 +39,15 @@ const RowIndex ROW_INDEX_SENTINEL  = std::numeric_limits<RowIndex>::max();
 
 class CoefficientChangeCallback {
 public:
-  virtual void update(RowIndex basic, ArithVar nb, int oldSgn, int currSgn) = 0;
-  virtual void swap(ArithVar basic, ArithVar nb, int nbSgn) = 0;
+  virtual void update(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn) = 0;
+  virtual void multiplyRow(RowIndex ridx, int Sgn) = 0;
   virtual bool canUseRow(RowIndex ridx) const = 0;
 };
 
 class NoEffectCCCB : public CoefficientChangeCallback {
 public:
   void update(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn);
-  void swap(ArithVar basic, ArithVar nb, int nbSgn);
+  void multiplyRow(RowIndex ridx, int Sgn);
   bool canUseRow(RowIndex ridx) const;
 };
 
diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp
index 695d9df25..b1c8d1b64 100644
--- a/src/theory/arith/partial_model.cpp
+++ b/src/theory/arith/partial_model.cpp
@@ -35,12 +35,13 @@ ArithVariables::ArithVariables(context::Context* c, DeltaComputeCallback deltaCo
    d_released(),
    d_releasedIterator(d_released.begin()),
    d_nodeToArithVarMap(),
+   d_boundsQueue(),
+   d_enqueueingBoundCounts(true),
    d_lbRevertHistory(c, true, LowerBoundCleanUp(this)),
    d_ubRevertHistory(c, true, UpperBoundCleanUp(this)),
    d_deltaIsSafe(false),
    d_delta(-1,1),
-   d_deltaComputingFunc(deltaComputingFunc),
-   d_enqueueingBoundCounts(true)
+   d_deltaComputingFunc(deltaComputingFunc)
 { }
 
 ArithVariables::VarInfo::VarInfo()
@@ -55,6 +56,10 @@ ArithVariables::VarInfo::VarInfo()
     d_slack(false)
 { }
 
+bool ArithVariables::VarInfo::initialized() const {
+  return d_var != ARITHVAR_SENTINEL;
+}
+
 void ArithVariables::VarInfo::initialize(ArithVar v, Node n, bool slack){
   Assert(!initialized());
   Assert(d_lb == NullConstraint);
@@ -82,7 +87,7 @@ void ArithVariables::VarInfo::uninitialize(){
   d_node = Node::null();
 }
 
-bool ArithVariables::VarInfo::setAssignment(const DeltaRational& a, BoundCounts & prev){
+bool ArithVariables::VarInfo::setAssignment(const DeltaRational& a, BoundsInfo& prev){
   Assert(initialized());
   d_assignment = a;
   int cmpUB = (d_ub == NullConstraint) ? -1 :
@@ -97,7 +102,7 @@ bool ArithVariables::VarInfo::setAssignment(const DeltaRational& a, BoundCounts
     (cmpUB == 0 || d_cmpAssignmentUB == 0);
 
   if(lbChanged || ubChanged){
-    prev = boundCounts();
+    prev = boundsInfo();
   }
 
   d_cmpAssignmentUB = cmpUB;
@@ -119,33 +124,59 @@ void ArithVariables::releaseArithVar(ArithVar v){
   }
 }
 
-bool ArithVariables::VarInfo::setUpperBound(Constraint ub, BoundCounts& prev){
+bool ArithVariables::VarInfo::setUpperBound(Constraint ub, BoundsInfo& prev){
   Assert(initialized());
-  d_ub = ub;
-  int cmpUB = (d_ub == NullConstraint) ? -1 : d_assignment.cmp(d_ub->getValue());
-  bool ubChanged = cmpUB != d_cmpAssignmentUB &&
-    (cmpUB == 0 || d_cmpAssignmentUB == 0);
+  bool wasNull = d_ub == NullConstraint;
+  bool isNull = ub == NullConstraint;
+
+  int cmpUB = isNull ? -1 : d_assignment.cmp(ub->getValue());
+  bool ubChanged = (wasNull != isNull) ||
+    (cmpUB != d_cmpAssignmentUB && (cmpUB == 0 || d_cmpAssignmentUB == 0));
   if(ubChanged){
-    prev = boundCounts();
+    prev = boundsInfo();
   }
+  d_ub = ub;
   d_cmpAssignmentUB = cmpUB;
   return ubChanged;
 }
 
-bool ArithVariables::VarInfo::setLowerBound(Constraint lb, BoundCounts& prev){
+bool ArithVariables::VarInfo::setLowerBound(Constraint lb, BoundsInfo& prev){
   Assert(initialized());
-  d_lb = lb;
-  int cmpLB = (d_lb == NullConstraint) ? 1 : d_assignment.cmp(d_lb->getValue());
+  bool wasNull = d_lb == NullConstraint;
+  bool isNull = lb == NullConstraint;
 
-  bool lbChanged = cmpLB != d_cmpAssignmentLB &&
-    (cmpLB == 0 || d_cmpAssignmentLB == 0);
+  int cmpLB = isNull ? 1 : d_assignment.cmp(lb->getValue());
+
+  bool lbChanged = (wasNull != isNull) ||
+    (cmpLB != d_cmpAssignmentLB && (cmpLB == 0 || d_cmpAssignmentLB == 0));
   if(lbChanged){
-    prev = boundCounts();
+    prev = boundsInfo();
   }
+  d_lb = lb;
   d_cmpAssignmentLB = cmpLB;
   return lbChanged;
 }
 
+BoundCounts ArithVariables::VarInfo::atBoundCounts() const {
+  uint32_t lbIndc = (d_cmpAssignmentLB == 0) ? 1 : 0;
+  uint32_t ubIndc = (d_cmpAssignmentUB == 0) ? 1 : 0;
+  return BoundCounts(lbIndc, ubIndc);
+}
+
+BoundCounts ArithVariables::VarInfo::hasBoundCounts() const {
+  uint32_t lbIndc = (d_lb != NullConstraint) ? 1 : 0;
+  uint32_t ubIndc = (d_ub != NullConstraint) ? 1 : 0;
+  return BoundCounts(lbIndc, ubIndc);
+}
+
+BoundsInfo ArithVariables::VarInfo::boundsInfo() const{
+  return BoundsInfo(atBoundCounts(), hasBoundCounts());
+}
+
+bool ArithVariables::VarInfo::canBeReclaimed() const{
+  return d_pushCount == 0;
+}
+
 void ArithVariables::attemptToReclaimReleased(){
   std::list<ArithVar>::iterator i_end = d_released.end();
   for(int iter = 0; iter < 20 && d_releasedIterator != i_end; ++d_releasedIterator){
@@ -170,7 +201,7 @@ ArithVar ArithVariables::allocateVariable(){
     attemptToReclaimReleased();
   }
   bool reclaim = !d_pool.empty();
-  
+
   ArithVar varX;
   if(reclaim){
     varX = d_pool.back();
@@ -210,7 +241,7 @@ void ArithVariables::setAssignment(ArithVar x, const DeltaRational& r){
   }
   invalidateDelta();
 
-  BoundCounts prev;
+  BoundsInfo prev;
   if(vi.setAssignment(r, prev)){
     addToBoundQueue(x, prev);
   }
@@ -229,7 +260,7 @@ void ArithVariables::setAssignment(ArithVar x, const DeltaRational& safe, const
 
   invalidateDelta();
   VarInfo& vi = d_vars.get(x);
-  BoundCounts prev;
+  BoundsInfo prev;
   if(vi.setAssignment(r, prev)){
     addToBoundQueue(x, prev);
   }
@@ -314,7 +345,7 @@ void ArithVariables::setLowerBoundConstraint(Constraint c){
   invalidateDelta();
   VarInfo& vi = d_vars.get(x);
   pushLowerBound(vi);
-  BoundCounts prev;
+  BoundsInfo prev;
   if(vi.setLowerBound(c, prev)){
     addToBoundQueue(x, prev);
   }
@@ -333,37 +364,12 @@ void ArithVariables::setUpperBoundConstraint(Constraint c){
   invalidateDelta();
   VarInfo& vi = d_vars.get(x);
   pushUpperBound(vi);
-  BoundCounts prev;
+  BoundsInfo prev;
   if(vi.setUpperBound(c, prev)){
     addToBoundQueue(x, prev);
   }
 }
 
-// void ArithVariables::forceRelaxLowerBound(ArithVar v){
-//   AssertArgument(inMaps(v), "Calling forceRelaxLowerBound on a variable that is not properly setup.");
-//   AssertArgument(hasLowerBound(v), "Calling forceRelaxLowerBound on a variable without a lowerbound.");
-
-//   Debug("partial_model") << "forceRelaxLowerBound(" << v << ") dropping :" << getLowerBoundConstraint(v) << endl;
-
-//   invalidateDelta();
-//   VarInfo& vi = d_vars.get(v);
-//   pushLowerBound(vi);
-//   vi.setLowerBound(NullConstraint);
-// }
-
-
-// void ArithVariables::forceRelaxUpperBound(ArithVar v){
-//   AssertArgument(inMaps(v), "Calling forceRelaxUpperBound on a variable that is not properly setup.");
-//   AssertArgument(hasUpperBound(v), "Calling forceRelaxUpperBound on a variable without an upper bound.");
-
-//   Debug("partial_model") << "forceRelaxUpperBound(" << v << ") dropping :" << getUpperBoundConstraint(v) << endl;
-
-//   invalidateDelta();
-//   VarInfo& vi = d_vars.get(v);
-//   pushUpperBound(vi);
-//   vi.setUpperBound(NullConstraint);
-// }
-
 int ArithVariables::cmpToLowerBound(ArithVar x, const DeltaRational& c) const{
   if(!hasLowerBound(x)){
     // l = -\intfy
@@ -405,30 +411,16 @@ bool ArithVariables::hasEitherBound(ArithVar x) const{
 
 bool ArithVariables::strictlyBelowUpperBound(ArithVar x) const{
   return d_vars[x].d_cmpAssignmentUB < 0;
-  // if(!hasUpperBound(x)){ // u = \infty
-  //   return true;
-  // }else{
-  //   return d_assignment[x] < getUpperBound(x);
-  // }
 }
 
 bool ArithVariables::strictlyAboveLowerBound(ArithVar x) const{
   return d_vars[x].d_cmpAssignmentLB > 0;
-  // if(!hasLowerBound(x)){ // l = -\infty
-  //   return true;
-  // }else{
-  //   return getLowerBound(x) < d_assignment[x];
-  // }
 }
 
 bool ArithVariables::assignmentIsConsistent(ArithVar x) const{
   return
     d_vars[x].d_cmpAssignmentLB >= 0 &&
     d_vars[x].d_cmpAssignmentUB <= 0;
-  // const DeltaRational& beta = getAssignment(x);
-
-  // //l_i <= beta(x_i) <= u_i
-  // return  greaterThanLowerBound(x,beta) && lessThanUpperBound(x,beta);
 }
 
 
@@ -442,7 +434,7 @@ void ArithVariables::clearSafeAssignments(bool revert){
     ArithVar atBack = d_safeAssignment.back();
     if(revert){
       VarInfo& vi = d_vars.get(atBack);
-      BoundCounts prev;
+      BoundsInfo prev;
       if(vi.setAssignment(d_safeAssignment[atBack], prev)){
         addToBoundQueue(atBack, prev);
       }
@@ -489,33 +481,6 @@ void ArithVariables::printModel(ArithVar x) const{
   printModel(x,  Debug("model"));
 }
 
-// BoundRelationship ArithVariables::boundRelationship(Constraint lb, const DeltaRational& d, Constraint ub){
-//   if(lb == NullConstraint && ub == NullConstraint){
-//     return BetweenBounds;
-//   }else if(lb == NullConstraint){
-//     int cmp = d.cmp(ub->getValue());
-//     return (cmp < 0) ? BetweenBounds :
-//       (cmp == 0 ? AtUpperBound  : AboveUpperBound);
-//   }else if(ub == NullConstraint){
-//     int cmp = d.cmp(lb->getValue());
-//     return (cmp > 0) ? BetweenBounds :
-//       (cmp == 0 ? AtLowerBound  : BelowLowerBound);    
-//   }else{
-//     Assert(lb->getValue() <= ub->getValue());
-//     int cmpToLB = d.cmp(lb->getValue());
-//     if(cmpToLB < 0){
-//       return BelowLowerBound;
-//     }else if(cmpToLB == 0){
-//       return (d == ub->getValue()) ? AtBothBounds : AtLowerBound;
-//     }else{
-//       // d > 0
-//       int cmpToUB = d.cmp(ub->getValue());
-//       return (cmpToUB > 0) ? BetweenBounds :
-//         (cmpToUB == 0 ? AtLowerBound  : BelowLowerBound);    
-//     }
-//   }
-// }
-
 void ArithVariables::pushUpperBound(VarInfo& vi){
   ++vi.d_pushCount;
   d_ubRevertHistory.push_back(make_pair(vi.d_var, vi.d_ub));
@@ -528,7 +493,7 @@ void ArithVariables::pushLowerBound(VarInfo& vi){
 void ArithVariables::popUpperBound(AVCPair* c){
   ArithVar x = c->first;
   VarInfo& vi = d_vars.get(x);
-  BoundCounts prev;
+  BoundsInfo prev;
   if(vi.setUpperBound(c->second, prev)){
     addToBoundQueue(x, prev);
   }
@@ -538,62 +503,38 @@ void ArithVariables::popUpperBound(AVCPair* c){
 void ArithVariables::popLowerBound(AVCPair* c){
   ArithVar x = c->first;
   VarInfo& vi = d_vars.get(x);
-  BoundCounts prev;
+  BoundsInfo prev;
   if(vi.setLowerBound(c->second, prev)){
     addToBoundQueue(x, prev);
   }
   --vi.d_pushCount;
 }
 
-/* To ensure that the final deallocation stuff works,
- * we need to ensure that we need to not reference any of the other vectors
- */
-// void ArithVariables::relaxUpperBound(Constraint curr, Constraint afterPop){
-//   BoundRelation next = Undefined;
-//   switch(d_boundRel[x]){
-//   case BelowLowerBound:
-//   case BetweenBounds:
-//   case AtLowerBound:
-//     return; // do nothing
-//   case AtUpperBound:
-//     if(afterPop != NullConstraint
-//        && curr->getValue() == afterPop->getValue()){
-//       next = AtUpperBound;
-//     }else{
-//       next = BetweenBounds;
-//     }
-//     break;
-//   case AtBothBounds:
-//     if(afterPop != NullConstraint
-//        && curr->getValue() == afterPop->getValue()){
-//       next = AtUpperBound;
-//     }else{
-//       next = AtLowerBound;
-//     }
-//     break;
-//   case AboveUpperBound:
-//     if(afterPop == NullConstraint){
-//       next = BetweenBounds;
-//     }else{
-//       int cmp = d_assignment[x].cmp(afterPop->getValue());
-//       next = (cmp < 0) ? BetweenBounds :
-//         (cmp == 0) ? AtUpperBound  : AboveUpperBound;
-//     }
-//     break;
-//   default:
-//     Unreachable();
-//   }
-//   d_boundRel[x] = next;
-// }
-
+void ArithVariables::addToBoundQueue(ArithVar v, const BoundsInfo& prev){
+  if(d_enqueueingBoundCounts && !d_boundsQueue.isKey(v)){
+    d_boundsQueue.set(v, prev);
+  }
+}
 
+BoundsInfo ArithVariables::selectBoundsInfo(ArithVar v, bool old) const {
+  if(old && d_boundsQueue.isKey(v)){
+    return d_boundsQueue[v];
+  }else{
+    return boundsInfo(v);
+  }
+}
 
-// void ArithVariables::relaxLowerBound(Constraint curr, Constraint afterPop){
-//   // TODO this can be optimized using the automata induced by d_boundRel and
-//   // the knowledge that lb <= ub
-//   ArithVar x = curr->getVariable();
-//   d_boundRel[x] = boundRelationship(afterPop, d_assignment[x], d_ubc[x]);    
-// }
+void ArithVariables::processBoundsQueue(BoundUpdateCallback& changed){
+  while(!d_boundsQueue.empty()){
+    ArithVar v = d_boundsQueue.back();
+    BoundsInfo prev = d_boundsQueue[v];
+    d_boundsQueue.pop_back();
+    BoundsInfo curr = boundsInfo(v);
+    if(prev != curr){
+      changed(v, prev);
+    }
+  }
+}
 
 void ArithVariables::LowerBoundCleanUp::operator()(AVCPair* p){
   d_pm->popLowerBound(p);
diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h
index dcfe97079..f937fc241 100644
--- a/src/theory/arith/partial_model.h
+++ b/src/theory/arith/partial_model.h
@@ -44,6 +44,7 @@ namespace arith {
 
 class ArithVariables {
 private:
+
   class VarInfo {
     friend class ArithVariables;
     ArithVar d_var;
@@ -62,29 +63,36 @@ private:
   public:
     VarInfo();
 
-    bool setAssignment(const DeltaRational& r, BoundCounts& prev);
-    bool setLowerBound(Constraint c, BoundCounts& prev);
-    bool setUpperBound(Constraint c, BoundCounts& prev);
+    bool setAssignment(const DeltaRational& r, BoundsInfo& prev);
+    bool setLowerBound(Constraint c, BoundsInfo& prev);
+    bool setUpperBound(Constraint c, BoundsInfo& prev);
 
-    bool initialized() const {
-      return d_var != ARITHVAR_SENTINEL;
-    }
+    /** Returns true if this VarInfo has been initialized. */
+    bool initialized() const;
+
+    /**
+     * Initializes the VarInfo with the ArithVar index it is associated with,
+     * the node that the variable represents, and whether it is a slack variable.
+     */
     void initialize(ArithVar v, Node n, bool slack);
+    /** Uninitializes the VarInfo. */
     void uninitialize();
 
-    bool canBeReclaimed() const{
-      return d_pushCount == 0;
-    }
+    bool canBeReclaimed() const;
 
-    BoundCounts boundCounts() const {
-      uint32_t lbIndc = (d_cmpAssignmentLB == 0) ? 1 : 0;
-      uint32_t ubIndc = (d_cmpAssignmentUB == 0) ? 1 : 0;
-      return BoundCounts(lbIndc, ubIndc);
-    }
+    /** Indicator variables for if the assignment is equal to the upper and lower bounds. */
+    BoundCounts atBoundCounts() const;
+
+    /** Combination of indicator variables for whether it has upper and lower bounds.  */
+    BoundCounts hasBoundCounts() const;
+
+    /** Stores both atBoundCounts() and hasBoundCounts().  */
+    BoundsInfo boundsInfo() const;
   };
 
-  //Maps from ArithVar -> VarInfo
+  /**Maps from ArithVar -> VarInfo */
   typedef DenseMap<VarInfo> VarInfoVec;
+  /** This maps an ArithVar to its Variable information.*/
   VarInfoVec d_vars;
 
   // Partial Map from Arithvar -> PreviousAssignment
@@ -104,7 +112,15 @@ private:
   // Inverse of d_vars[x].d_node
   NodeToArithVarMap d_nodeToArithVarMap;
 
-  DenseMap<BoundCounts> d_atBoundsQueue;
+
+  /** The queue of constraints where the assignment is at the bound.*/
+  DenseMap<BoundsInfo> d_boundsQueue;
+
+  /**
+   * If this is true, record the incoming changes to the bound information.
+   * If this is false, the responsibility of recording the changes is LinearEqualities's.
+   */
+  bool d_enqueueingBoundCounts;
 
  public:
 
@@ -225,7 +241,6 @@ private:
   // Function to call if the value of delta needs to be recomputed.
   DeltaComputeCallback d_deltaComputingFunc;
 
-  bool d_enqueueingBoundCounts;
 
 public:
 
@@ -252,22 +267,7 @@ public:
     return d_vars[x].d_lb;
   }
 
-  /**
-   * This forces the lower bound for a variable to be relaxed in the current context.
-   * This is done by forcing the lower bound to be NullConstraint.
-   * This is an expert only operation! (See primal simplex for an example.)
-   */
-  //void forceRelaxLowerBound(ArithVar x);
-
-  /**
-   * This forces the upper bound for a variable to be relaxed in the current context.
-   * This is done by forcing the upper bound to be NullConstraint.
-   * This is an expert only operation! (See primal simplex for an example.)
-   */
-  //void forceRelaxUpperBound(ArithVar x);
-
   /* Initializes a variable to a safe value.*/
-  //void initialize(ArithVar x, const DeltaRational& r);
   void initialize(ArithVar x, Node n, bool slack);
 
   ArithVar allocate(Node n, bool slack = false);
@@ -360,8 +360,14 @@ public:
     return d_vars[x].d_cmpAssignmentUB;
   }
 
-  inline BoundCounts boundCounts(ArithVar x) const {
-    return d_vars[x].boundCounts();
+  inline BoundCounts atBoundCounts(ArithVar x) const {
+    return d_vars[x].atBoundCounts();
+  }
+  inline BoundCounts hasBoundCounts(ArithVar x) const {
+    return d_vars[x].hasBoundCounts();
+  }
+  inline BoundsInfo boundsInfo(ArithVar x) const{
+    return d_vars[x].boundsInfo();
   }
 
   bool strictlyBelowUpperBound(ArithVar x) const;
@@ -391,38 +397,13 @@ public:
     d_deltaIsSafe = true;
   }
 
-  // inline bool initialized(ArithVar x) const {
-  //   return d_vars[x].initialized();
-  // }
-
-  void addToBoundQueue(ArithVar v, BoundCounts prev){
-    if(d_enqueueingBoundCounts && !d_atBoundsQueue.isKey(v)){
-      d_atBoundsQueue.set(v, prev);
-    }
-  }
+  void startQueueingBoundCounts(){ d_enqueueingBoundCounts = true; }
+  void stopQueueingBoundCounts(){ d_enqueueingBoundCounts = false; }
+  void addToBoundQueue(ArithVar v, const BoundsInfo& prev);
 
-  BoundCounts oldBoundCounts(ArithVar v) const {
-    if(d_atBoundsQueue.isKey(v)){
-      return d_atBoundsQueue[v];
-    }else{
-      return boundCounts(v);
-    }
-  }
+  BoundsInfo selectBoundsInfo(ArithVar v, bool old) const;
 
-  void startQueueingAtBoundQueue(){ d_enqueueingBoundCounts = true; }
-  void stopQueueingAtBoundQueue(){ d_enqueueingBoundCounts = false; }
-
-  void processAtBoundQueue(BoundCountsCallback& changed){
-    while(!d_atBoundsQueue.empty()){
-      ArithVar v = d_atBoundsQueue.back();
-      BoundCounts prev = d_atBoundsQueue[v];
-      d_atBoundsQueue.pop_back();
-      BoundCounts curr = boundCounts(v);
-      if(prev != curr){
-        changed(v, prev);
-      }
-    }
-  }
+  void processBoundsQueue(BoundUpdateCallback& changed);
 
   void printEntireModel(std::ostream& out) const;
 
diff --git a/src/theory/arith/pure_update_simplex.cpp b/src/theory/arith/pure_update_simplex.cpp
index 9b3edfa6f..233fc292f 100644
--- a/src/theory/arith/pure_update_simplex.cpp
+++ b/src/theory/arith/pure_update_simplex.cpp
@@ -175,7 +175,7 @@ bool PureUpdateSimplexDecisionProcedure::attemptPureUpdates(){
 
       worthwhile = proposal.errorsChange() < 0 ||
         (proposal.focusDirection() > 0 &&
-         d_variables.boundCounts(curr).isZero() &&
+         d_variables.atBoundCounts(curr).isZero() &&
          !proposal.describesPivot());
 
       Debug("pu::refined")
@@ -188,11 +188,11 @@ bool PureUpdateSimplexDecisionProcedure::attemptPureUpdates(){
     if(worthwhile){
       Debug("pu") << d_variables.getAssignment(d_focusErrorVar) << endl;
 
-      BoundCounts before = d_variables.boundCounts(curr);
+      BoundCounts before = d_variables.atBoundCounts(curr);
       DeltaRational newAssignment =
         d_variables.getAssignment(curr) + proposal.nonbasicDelta();
       d_linEq.updateTracked(curr, newAssignment);
-      BoundCounts after = d_variables.boundCounts(curr);
+      BoundCounts after = d_variables.atBoundCounts(curr);
 
       ++d_statistics.d_pureUpdates;
       ++boundImprovements;
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index 02e49258c..707c8d029 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -130,6 +130,8 @@ void SimplexDecisionProcedure::tearDownInfeasiblityFunction(TimerStat& timer, Ar
   Assert(tmp != ARITHVAR_SENTINEL);
   Assert(d_tableau.isBasic(tmp));
 
+  RowIndex ri = d_tableau.basicToRowIndex(tmp);
+  d_linEq.stopTrackingRowIndex(ri);
   d_tableau.removeBasicRow(tmp);
   releaseVariable(tmp);
 }
@@ -193,9 +195,10 @@ ArithVar SimplexDecisionProcedure::constructInfeasiblityFunction(TimerStat& time
   DeltaRational newAssignment = d_linEq.computeRowValue(inf, false);
   d_variables.setAssignment(inf, newAssignment);
 
-  d_linEq.trackVariable(inf);
+  //d_linEq.trackVariable(inf);
+  d_linEq.trackRowIndex(d_tableau.basicToRowIndex(inf));
 
-  Debug("Inf") << inf << " " << newAssignment << endl;
+  Debug("constructInfeasiblityFunction") << inf << " " << newAssignment << endl;
 
   return inf;
 }
diff --git a/src/theory/arith/soi_simplex.cpp b/src/theory/arith/soi_simplex.cpp
index f19b13fa5..ef00807f7 100644
--- a/src/theory/arith/soi_simplex.cpp
+++ b/src/theory/arith/soi_simplex.cpp
@@ -237,7 +237,7 @@ UpdateInfo SumOfInfeasibilitiesSPD::selectUpdate(LinearEqualityModule::UpdatePre
   Debug("soi::selectPrimalUpdate")
     << "selectPrimalUpdate " << instance << endl
     << d_soiVar << " " << d_tableau.basicRowLength(d_soiVar)
-    << " " << d_linEq._countBounds(d_soiVar) << endl;
+    << " " << d_linEq.debugBasicAtBoundCount(d_soiVar) << endl;
 
   typedef std::vector<Cand> CandVector;
   CandVector candidates;
@@ -349,7 +349,7 @@ void SumOfInfeasibilitiesSPD::debugPrintSignal(ArithVar updated) const{
   int dir = !d_variables.assignmentIsConsistent(updated) ?
     d_errorSet.getSgn(updated) : 0;
   Debug("updateAndSignal") << " dir " << dir;
-  Debug("updateAndSignal") << " _countBounds " << d_linEq._countBounds(updated) << endl;
+  Debug("updateAndSignal") << " debugBasicAtBoundCount " << d_linEq.debugBasicAtBoundCount(updated) << endl;
 }
 
 
@@ -367,7 +367,7 @@ void SumOfInfeasibilitiesSPD::updateAndSignal(const UpdateInfo& selected, Witnes
       ArithVar leaving = selected.leaving();
       ss << "leaving " << leaving
          << " " << d_tableau.basicRowLength(leaving)
-         << " " << d_linEq._countBounds(leaving)
+         << " " << d_linEq.debugBasicAtBoundCount(leaving)
          << endl;
     }
     if(degenerate(w) && selected.describesPivot()){
@@ -376,7 +376,7 @@ void SumOfInfeasibilitiesSPD::updateAndSignal(const UpdateInfo& selected, Witnes
         << "degenerate " << leaving
         << ", atBounds " << d_linEq.basicsAtBounds(selected)
         << ", len " << d_tableau.basicRowLength(leaving)
-        << ", bc " << d_linEq._countBounds(leaving)
+        << ", bc " << d_linEq.debugBasicAtBoundCount(leaving)
         << endl;
     }
   }
diff --git a/src/theory/arith/tableau.cpp b/src/theory/arith/tableau.cpp
index c54b0857a..9d06fadc4 100644
--- a/src/theory/arith/tableau.cpp
+++ b/src/theory/arith/tableau.cpp
@@ -75,7 +75,7 @@ void Tableau::rowPivot(ArithVar basicOld, ArithVar basicNew, CoefficientChangeCa
   d_basic2RowIndex.set(basicNew, rid);
   d_rowIndex2basic.set(rid, basicNew);
 
-  cb.swap(basicOld, basicNew, a_rs_sgn);
+  cb.multiplyRow(rid, -a_rs_sgn);
 }
 
 
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index 263f9536b..c39dab3cb 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -83,7 +83,7 @@ namespace arith {
 TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo, QuantifiersEngine* qe) :
   d_containing(containing),
   d_nlIncomplete( false),
-  d_boundTracking(),
+  d_rowTracking(),
   d_constraintDatabase(c, u, d_partialModel, d_congruenceManager, RaiseConflict(*this)),
   d_qflraStatus(Result::SAT_UNKNOWN),
   d_unknownsInARow(0),
@@ -96,9 +96,9 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, context::Context
   d_currentPropagationList(),
   d_learnedBounds(c),
   d_partialModel(c, DeltaComputeCallback(*this)),
-  d_errorSet(d_partialModel, TableauSizes(&d_tableau), BoundCountingLookup(&d_boundTracking)),
+  d_errorSet(d_partialModel, TableauSizes(&d_tableau), BoundCountingLookup(&d_rowTracking, &d_tableau)),
   d_tableau(),
-  d_linEq(d_partialModel, d_tableau, d_boundTracking, BasicVarModelUpdateCallBack(*this)),
+  d_linEq(d_partialModel, d_tableau, d_rowTracking, BasicVarModelUpdateCallBack(*this)),
   d_diosolver(c),
   d_restartsCounter(0),
   d_tableauSizeHasBeenModified(false),
@@ -1100,7 +1100,7 @@ void TheoryArithPrivate::setupPolynomial(const Polynomial& poly) {
     ArithVar varSlack = requestArithVar(polyNode, true);
     d_tableau.addRow(varSlack, coefficients, variables);
     setupBasicValue(varSlack);
-    d_linEq.trackVariable(varSlack);
+    d_linEq.trackRowIndex(d_tableau.basicToRowIndex(varSlack));
 
     //Add differences to the difference manager
     Polynomial::iterator i = poly.begin(), end = poly.end();
@@ -1176,7 +1176,6 @@ void TheoryArithPrivate::releaseArithVar(ArithVar v){
 
   d_constraintDatabase.removeVariable(v);
   d_partialModel.releaseArithVar(v);
-  d_linEq.maybeRemoveTracking(v);
 }
 
 ArithVar TheoryArithPrivate::requestArithVar(TNode x, bool slack){
@@ -1609,9 +1608,9 @@ void TheoryArithPrivate::branchVector(const std::vector<ArithVar>& lemmas){
 bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){
   Assert(d_qflraStatus != Result::SAT);
 
-  d_partialModel.stopQueueingAtBoundQueue();
+  d_partialModel.stopQueueingBoundCounts();
   UpdateTrackingCallback utcb(&d_linEq);
-  d_partialModel.processAtBoundQueue(utcb);
+  d_partialModel.processBoundsQueue(utcb);
   d_linEq.startTrackingBoundCounts();
 
   bool noPivotLimit = Theory::fullEffort(effortLevel) ||
@@ -1701,7 +1700,7 @@ bool TheoryArithPrivate::solveRealRelaxation(Theory::Effort effortLevel){
 
   // TODO Save zeroes with no conflicts
   d_linEq.stopTrackingBoundCounts();
-  d_partialModel.startQueueingAtBoundQueue();
+  d_partialModel.startQueueingBoundCounts();
 
   return emmittedConflictOrSplit;
 }
@@ -2432,37 +2431,6 @@ void TheoryArithPrivate::notifyRestart(){
   if(Debug.isOn("paranoid:check_tableau")){ d_linEq.debugCheckTableau(); }
 
   ++d_restartsCounter;
-#warning "removing restart"
-  // return;
-
-  // uint32_t currSize = d_tableau.size();
-  // uint32_t copySize = d_smallTableauCopy.size();
-
-  // Debug("arith::reset") << "resetting" << d_restartsCounter << endl;
-  // Debug("arith::reset") << "curr " << currSize << " copy " << copySize << endl;
-  // Debug("arith::reset") << "tableauSizeHasBeenModified " << d_tableauSizeHasBeenModified << endl;
-
-  // if(d_tableauSizeHasBeenModified){
-  //   Debug("arith::reset") << "row has been added must copy " << d_restartsCounter << endl;
-  //   d_smallTableauCopy = d_tableau;
-  //   d_tableauSizeHasBeenModified = false;
-  // }else if( d_restartsCounter >= RESET_START){
-  //   if(copySize >= currSize * 1.1 ){
-  //     Debug("arith::reset") << "size has shrunk " << d_restartsCounter << endl;
-  //     ++d_statistics.d_smallerSetToCurr;
-  //     d_smallTableauCopy = d_tableau;
-  //   }else if(d_tableauResetDensity * copySize <=  currSize){
-  //     d_errorSet.popAllSignals();
-  //     if(safeToReset()){
-  //       Debug("arith::reset") << "resetting " << d_restartsCounter << endl;
-  //       ++d_statistics.d_currSetToSmaller;
-  //       d_tableau = d_smallTableauCopy;
-  //     }else{
-  //       Debug("arith::reset") << "not safe to reset at the moment " << d_restartsCounter << endl;
-  //     }
-  //   }
-  // }
-  // Assert(unenqueuedVariablesAreConsistent());
 }
 
 bool TheoryArithPrivate::entireStateIsConsistent(const string& s){
@@ -2631,7 +2599,13 @@ bool TheoryArithPrivate::propagateCandidateBound(ArithVar basic, bool upperBound
         //d_learnedBounds.push(bestImplied);
         return true;
       }
+      cout << "failed " << basic << " " << bound << assertedToTheTheory << " " <<
+        canBePropagated << " " << hasProof << endl;
+      d_partialModel.printModel(basic, cout);
     }
+  }else{
+    cout << "false " << bound << " ";
+    d_partialModel.printModel(basic, cout);
   }
   return false;
 }
@@ -2687,6 +2661,22 @@ void TheoryArithPrivate::propagateCandidates(){
   }
 }
 
+void TheoryArithPrivate::propagateCandidatesNew(){
+  /* Four criteria must be met for progagation on a variable to happen using a row:
+   * 0: A new bound has to have been added to the row.
+   * 1: The hasBoundsCount for the row must be "full" or be full minus one variable
+   *    (This is O(1) to check, but requires book keeping.)
+   * 2: The current assignment must be strictly smaller/greater than the current bound.
+   *    assign(x) < upper(x)
+   *    (This is O(1) to compute.)
+   * 3: There is a bound that is strictly smaller/greater than the current assignment.
+   *    assign(x) < c for some x <= c literal
+   *    (This is O(log n) to compute.)
+   * 4: The implied bound on x is strictly smaller/greater than the current bound.
+   *    (This is O(n) to compute.)
+   */
+}
+
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 7b37a813f..4de562d0a 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -105,7 +105,7 @@ private:
   // TODO A better would be:
   //context::CDO<bool> d_nlIncomplete;
 
-  BoundCountingVector d_boundTracking;
+  BoundInfoMap d_rowTracking;
 
   /**
    * The constraint database associated with the theory.
@@ -469,6 +469,8 @@ private:
 
   void revertOutOfConflict();
 
+  void propagateCandidatesNew();
+
   void propagateCandidates();
   void propagateCandidate(ArithVar basic);
   bool propagateCandidateBound(ArithVar basic, bool upperBound);