Draft of the new propagation code.

8 files changed, 378 insertions, 101 deletions

diff --git a/src/theory/arith/linear_equality.cpp b/src/theory/arith/linear_equality.cpp
index eda3bf682..4779b1012 100644
--- a/src/theory/arith/linear_equality.cpp
+++ b/src/theory/arith/linear_equality.cpp
@@ -421,19 +421,42 @@ bool LinearEqualityModule::debugEntireLinEqIsConsistent(const string& s){
   return result;
 }
 
-DeltaRational LinearEqualityModule::computeBound(ArithVar basic, bool upperBound){
+// DeltaRational LinearEqualityModule::computeBound(ArithVar basic, bool upperBound){
+//   DeltaRational sum(0,0);
+//   for(Tableau::RowIterator i = d_tableau.basicRowIterator(basic); !i.atEnd(); ++i){
+//     const Tableau::Entry& entry = (*i);
+//     ArithVar nonbasic = entry.getColVar();
+//     if(nonbasic == basic) continue;
+//     const Rational& coeff =  entry.getCoefficient();
+//     int sgn = coeff.sgn();
+//     bool ub = upperBound ? (sgn > 0) : (sgn < 0);
+
+//     const DeltaRational& bound = ub ?
+//       d_variables.getUpperBound(nonbasic):
+//       d_variables.getLowerBound(nonbasic);
+
+//     DeltaRational diff = bound * coeff;
+//     sum = sum + diff;
+//   }
+//   return sum;
+// }
+DeltaRational LinearEqualityModule::computeBound(ArithVar basic, bool upperBound) const {
+  RowIndex rid = d_tableau.basicToRowIndex(basic);
+  return computeRowBound(rid, upperBound, basic);
+}
+DeltaRational LinearEqualityModule::computeRowBound(RowIndex ridx, bool rowUb, ArithVar skip) const {
   DeltaRational sum(0,0);
-  for(Tableau::RowIterator i = d_tableau.basicRowIterator(basic); !i.atEnd(); ++i){
+  for(Tableau::RowIterator i = d_tableau.ridRowIterator(ridx); !i.atEnd(); ++i){
     const Tableau::Entry& entry = (*i);
-    ArithVar nonbasic = entry.getColVar();
-    if(nonbasic == basic) continue;
+    ArithVar v = entry.getColVar();
+    if(v == skip){ continue; }
+
     const Rational& coeff =  entry.getCoefficient();
-    int sgn = coeff.sgn();
-    bool ub = upperBound ? (sgn > 0) : (sgn < 0);
+    bool vUb = (rowUb == (coeff.sgn() > 0));
 
-    const DeltaRational& bound = ub ?
-      d_variables.getUpperBound(nonbasic):
-      d_variables.getLowerBound(nonbasic);
+    const DeltaRational& bound = vUb ?
+      d_variables.getUpperBound(v):
+      d_variables.getLowerBound(v);
 
     DeltaRational diff = bound * coeff;
     sum = sum + diff;
@@ -444,7 +467,7 @@ DeltaRational LinearEqualityModule::computeBound(ArithVar basic, bool upperBound
 /**
  * Computes the value of a basic variable using the current assignment.
  */
-DeltaRational LinearEqualityModule::computeRowValue(ArithVar x, bool useSafe){
+DeltaRational LinearEqualityModule::computeRowValue(ArithVar x, bool useSafe) const{
   Assert(d_tableau.isBasic(x));
   DeltaRational sum(0);
 
@@ -460,28 +483,54 @@ DeltaRational LinearEqualityModule::computeRowValue(ArithVar x, bool useSafe){
   return sum;
 }
 
+// bool LinearEqualityModule::hasBounds(ArithVar basic, bool upperBound){
+//   for(Tableau::RowIterator iter = d_tableau.basicRowIterator(basic); !iter.atEnd(); ++iter){
+//     const Tableau::Entry& entry = *iter;
+
+//     ArithVar var = entry.getColVar();
+//     if(var == basic) continue;
+//     int sgn = entry.getCoefficient().sgn();
+//     if(upperBound){
+//       if( (sgn < 0 && !d_variables.hasLowerBound(var)) ||
+//           (sgn > 0 && !d_variables.hasUpperBound(var))){
+//         return false;
+//       }
+//     }else{
+//       if( (sgn < 0 && !d_variables.hasUpperBound(var)) ||
+//           (sgn > 0 && !d_variables.hasLowerBound(var))){
+//         return false;
+//       }
+//     }
+//   }
+//   return true;
+// }
+
 bool LinearEqualityModule::hasBounds(ArithVar basic, bool upperBound){
-  for(Tableau::RowIterator iter = d_tableau.basicRowIterator(basic); !iter.atEnd(); ++iter){
+  RowIndex ridx = d_tableau.basicToRowIndex(basic);
+  return rowLacksBound(ridx, upperBound, basic) == NULL;
+}
+
+const Tableau::Entry* LinearEqualityModule::rowLacksBound(RowIndex ridx, bool rowUb, ArithVar skip){
+  Tableau::RowIterator iter = d_tableau.ridRowIterator(ridx);
+  for(; !iter.atEnd(); ++iter){
     const Tableau::Entry& entry = *iter;
 
     ArithVar var = entry.getColVar();
-    if(var == basic) continue;
+    if(var == skip) { continue; }
+
     int sgn = entry.getCoefficient().sgn();
-    if(upperBound){
-      if( (sgn < 0 && !d_variables.hasLowerBound(var)) ||
-          (sgn > 0 && !d_variables.hasUpperBound(var))){
-        return false;
-      }
-    }else{
-      if( (sgn < 0 && !d_variables.hasUpperBound(var)) ||
-          (sgn > 0 && !d_variables.hasLowerBound(var))){
-        return false;
-      }
+    bool selectUb = (rowUb == (sgn > 0));
+    bool hasBound = selectUb ?
+      d_variables.hasUpperBound(var):
+      d_variables.hasLowerBound(var);
+    if(!hasBound){
+      return &entry;
     }
   }
-  return true;
+  return NULL;
 }
 
+
 template <bool upperBound>
 void LinearEqualityModule::propagateNonbasics(ArithVar basic, Constraint c){
   Assert(d_tableau.isBasic(basic));
@@ -532,6 +581,40 @@ void LinearEqualityModule::propagateNonbasics(ArithVar basic, Constraint c){
                                    << basic << ") done" << endl;
 }
 
+void LinearEqualityModule::propagateRow(RowIndex ridx, bool rowUp, Constraint c){
+  Assert(!c->assertedToTheTheory());
+  Assert(c->canBePropagated());
+  Assert(!c->hasProof());
+
+  ArithVar v = c->getVariable();
+  Debug("arith::explainNonbasics") << "LinearEqualityModule::explainNonbasics("
+                                   << v <<") start" << endl;
+  vector<Constraint> bounds;
+
+  Tableau::RowIterator iter = d_tableau.ridRowIterator(ridx);
+  for(; !iter.atEnd(); ++iter){
+    const Tableau::Entry& entry = *iter;
+    ArithVar nonbasic = entry.getColVar();
+    if(nonbasic == v){ continue; }
+
+    const Rational& a_ij = entry.getCoefficient();
+
+    int sgn = a_ij.sgn();
+    Assert(sgn != 0);
+    bool selectUb = rowUp ? (sgn > 0) : (sgn < 0);
+    Constraint bound = selectUb
+      ? d_variables.getUpperBoundConstraint(nonbasic)
+      : d_variables.getLowerBoundConstraint(nonbasic);
+
+    Assert(bound != NullConstraint);
+    Debug("arith::explainNonbasics") << "explainNonbasics" << bound << " for " << c << endl;
+    bounds.push_back(bound);
+  }
+  c->impliedBy(bounds);
+  Debug("arith::explainNonbasics") << "LinearEqualityModule::explainNonbasics("
+                                   << v << ") done" << endl;
+}
+
 Constraint LinearEqualityModule::weakestExplanation(bool aboveUpper, DeltaRational& surplus, ArithVar v, const Rational& coeff, bool& anyWeakening, ArithVar basic) const {
 
   int sgn = coeff.sgn();
@@ -749,7 +832,8 @@ void LinearEqualityModule::trackRowIndex(RowIndex ridx){
 BoundsInfo LinearEqualityModule::computeRowBoundInfo(RowIndex ridx, bool inQueue) const{
   BoundsInfo bi;
 
-  for(Tableau::RowIterator iter = d_tableau.getRow(ridx).begin(); !iter.atEnd();  ++iter){
+  Tableau::RowIterator iter = d_tableau.ridRowIterator(ridx);
+  for(; !iter.atEnd();  ++iter){
     const Tableau::Entry& entry = *iter;
     ArithVar v = entry.getColVar();
     const Rational& a_ij = entry.getCoefficient();
diff --git a/src/theory/arith/linear_equality.h b/src/theory/arith/linear_equality.h
index bc653fdad..767c09340 100644
--- a/src/theory/arith/linear_equality.h
+++ b/src/theory/arith/linear_equality.h
@@ -255,20 +255,24 @@ public:
    * Updates the assignment of the other basic variables accordingly.
    */
   void pivotAndUpdate(ArithVar x_i, ArithVar x_j, const DeltaRational& v);
-  //void pivotAndUpdateAdj(ArithVar x_i, ArithVar x_j, const DeltaRational& v);
 
   ArithVariables& getVariables() const{ return d_variables; }
   Tableau& getTableau() const{ return d_tableau; }
 
   void forceNewBasis(const DenseSet& newBasis);
 
+#warning "Remove legacy code."
   bool hasBounds(ArithVar basic, bool upperBound);
-  bool hasLowerBounds(ArithVar basic){
-    return hasBounds(basic, false);
-  }
-  bool hasUpperBounds(ArithVar basic){
-    return hasBounds(basic, true);
-  }
+
+  /**
+   * Returns a pointer to the first Tableau entry on the row ridx that does not
+   * have an either a lower bound/upper bound for proving a bound on skip.
+   * The variable skip is always excluded. Returns NULL if there is no such element.
+   *
+   * If skip == ARITHVAR_SENTINEL, this is equivalent to considering the whole row.
+   */
+  const Tableau::Entry* rowLacksBound(RowIndex ridx, bool upperBound, ArithVar skip);
+
 
   void startTrackingBoundCounts();
   void stopTrackingBoundCounts();
@@ -412,10 +416,7 @@ private:
   BoundInfoMap& d_btracking;
   bool d_areTracking;
 
-  /**
-   * Exports either the explanation of an upperbound or a lower bound
-   * of the basic variable basic, using the non-basic variables in the row.
-   */
+#warning "Remove legacy code"
   template <bool upperBound>
   void propagateNonbasics(ArithVar basic, Constraint c);
 
@@ -426,6 +427,11 @@ public:
   void propagateNonbasicsUpperBound(ArithVar basic, Constraint c){
     propagateNonbasics<true>(basic, c);
   }
+  /**
+   * Exports either the explanation of an upperbound or a lower bound
+   * of the basic variable basic, using the non-basic variables in the row.
+   */
+  void propagateRow(RowIndex ridx, bool rowUp, Constraint c);
 
   /**
    * Computes the value of a basic variable using the assignments
@@ -434,12 +440,12 @@ public:
    * - the the current assignment (useSafe=false) or
    * - the safe assignment (useSafe = true).
    */
-  DeltaRational computeRowValue(ArithVar x, bool useSafe);
+  DeltaRational computeRowValue(ArithVar x, bool useSafe) const;
 
-  inline DeltaRational computeLowerBound(ArithVar basic){
+  inline DeltaRational computeLowerBound(ArithVar basic) const{
     return computeBound(basic, false);
   }
-  inline DeltaRational computeUpperBound(ArithVar basic){
+  inline DeltaRational computeUpperBound(ArithVar basic) const{
     return computeBound(basic, true);
   }
 
@@ -542,18 +548,22 @@ public:
    */
   bool basicsAtBounds(const UpdateInfo& u) const;
 private:
-  //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 debugBasicAtBoundCount(ArithVar x_i) const;
   void trackingCoefficientChange(RowIndex ridx, ArithVar nb, int oldSgn, int currSgn);
   void trackingMultiplyRow(RowIndex ridx, int sgn);
 
+  BoundCounts hasBoundCount(RowIndex ri) const {
+    Assert(d_variables.boundsQueueEmpty());
+    return d_btracking[ri].hasBounds();
+  }
+
+#warning "Remove legacy code"
   bool nonbasicsAtLowerBounds(ArithVar x_i) const;
   bool nonbasicsAtUpperBounds(ArithVar x_i) const;
 
+#warning "Remove legacy code"
   ArithVar _anySlackLowerBound(ArithVar x_i) const {
     return selectSlack<true>(x_i, &LinearEqualityModule::noPreference);
   }
@@ -606,8 +616,10 @@ public:
     return minimallyWeakConflict(false, conflictVar);
   }
 
+  DeltaRational computeRowBound(RowIndex ridx, bool rowUb, ArithVar skip) const;
+
 private:
-  DeltaRational computeBound(ArithVar basic, bool upperBound);
+  DeltaRational computeBound(ArithVar basic, bool upperBound) const;
 
 public:
   void substitutePlusTimesConstant(ArithVar to, ArithVar from, const Rational& mult);
diff --git a/src/theory/arith/options b/src/theory/arith/options
index 977d6cb32..cf0782a92 100644
--- a/src/theory/arith/options
+++ b/src/theory/arith/options
@@ -91,4 +91,7 @@ option fancyFinal --fancy-final bool :default false :read-write
 option exportDioDecompositions --dio-decomps bool :default false :read-write
  Let skolem variables for integer divisibility constraints leak from the dio solver.
 
+option newProp --new-prop bool :default false :read-write
+ Use the new row propagation system
+
 endmodule
diff --git a/src/theory/arith/partial_model.cpp b/src/theory/arith/partial_model.cpp
index b1c8d1b64..3fae3751c 100644
--- a/src/theory/arith/partial_model.cpp
+++ b/src/theory/arith/partial_model.cpp
@@ -524,8 +524,12 @@ BoundsInfo ArithVariables::selectBoundsInfo(ArithVar v, bool old) const {
   }
 }
 
+bool ArithVariables::boundsQueueEmpty() const {
+  return d_boundsQueue.empty();
+}
+
 void ArithVariables::processBoundsQueue(BoundUpdateCallback& changed){
-  while(!d_boundsQueue.empty()){
+  while(!boundsQueueEmpty()){
     ArithVar v = d_boundsQueue.back();
     BoundsInfo prev = d_boundsQueue[v];
     d_boundsQueue.pop_back();
diff --git a/src/theory/arith/partial_model.h b/src/theory/arith/partial_model.h
index f937fc241..953c8c0d3 100644
--- a/src/theory/arith/partial_model.h
+++ b/src/theory/arith/partial_model.h
@@ -403,6 +403,7 @@ public:
 
   BoundsInfo selectBoundsInfo(ArithVar v, bool old) const;
 
+  bool boundsQueueEmpty() const;
   void processBoundsQueue(BoundUpdateCallback& changed);
 
   void printEntireModel(std::ostream& out) const;
diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h
index 8b6ef1df6..deed7e7be 100644
--- a/src/theory/arith/tableau.h
+++ b/src/theory/arith/tableau.h
@@ -72,8 +72,12 @@ public:
     return getColumn(x).begin();
   }
 
+  RowIterator ridRowIterator(RowIndex rid) const {
+    return getRow(rid).begin();
+  }
+
   RowIterator basicRowIterator(ArithVar basic) const {
-    return getRow(basicToRowIndex(basic)).begin();
+    return ridRowIterator(basicToRowIndex(basic));
   }
 
   const Entry& basicFindEntry(ArithVar basic, ArithVar col) const {
diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp
index c39dab3cb..5b40e03bc 100644
--- a/src/theory/arith/theory_arith_private.cpp
+++ b/src/theory/arith/theory_arith_private.cpp
@@ -489,9 +489,7 @@ bool TheoryArithPrivate::AssertUpper(Constraint constraint){
         }else if(!lb->negationHasProof()){
           Constraint negLb = lb->getNegation();
           negLb->impliedBy(constraint, diseq);
-          //if(!negLb->canBePropagated()){
           d_learnedBounds.push_back(negLb);
-          //}//otherwise let this be propagated/asserted later
         }
       }
     }
@@ -1187,70 +1185,19 @@ ArithVar TheoryArithPrivate::requestArithVar(TNode x, bool slack){
   Assert(!d_partialModel.hasArithVar(x));
   Assert(x.getType().isReal()); // real or integer
 
-  // ArithVar varX = d_variables.size();
-  // d_variables.push_back(Node(x));
-
   ArithVar max = d_partialModel.getNumberOfVariables();
   ArithVar varX = d_partialModel.allocate(x, slack);
 
   bool reclaim =  max >= d_partialModel.getNumberOfVariables();;
 
-  if(reclaim){
-    // varX = d_pool.back();
-    // d_pool.pop_back();
-
-    // d_partialModel.setAssignment(varX, d_DELTA_ZERO, d_DELTA_ZERO);
-  }else{
-    // varX = d_numberOfVariables;
-    // ++d_numberOfVariables;
-
-    // d_slackVars.push_back(true);
-    // d_variableTypes.push_back(ATReal);
-
+  if(!reclaim){
     d_dualSimplex.increaseMax();
 
     d_tableau.increaseSize();
     d_tableauSizeHasBeenModified = true;
-
-    //d_partialModel.initialize(varX, d_DELTA_ZERO);
   }
-
-  // ArithType type;
-  // if(slack){
-  //   //The type computation is not quite accurate for Rationals that are integral.
-  //   //We'll use the isIntegral check from the polynomial package instead.
-  //   Polynomial p = Polynomial::parsePolynomial(x);
-  //   type = p.isIntegral() ? ATInteger : ATReal;
-  // }else{
-  //   type = nodeToArithType(x);
-  // }
-  // d_variableTypes[varX] = type;
-  // d_slackVars[varX] = slack;
-
   d_constraintDatabase.addVariable(varX);
 
-  //d_partialModel.setArithVar(x,varX);
-
-  // Debug("integers") << "isInteger[[" << x << "]]: " << x.getType().isInteger() << endl;
-
-  // if(slack){
-  //   //The type computation is not quite accurate for Rationals that are integral.
-  //   //We'll use the isIntegral check from the polynomial package instead.
-  //   Polynomial p = Polynomial::parsePolynomial(x);
-  //   d_variableTypes.push_back(p.isIntegral() ? ATInteger : ATReal);
-  // }else{
-  //   d_variableTypes.push_back(nodeToArithType(x));
-  // }
-
-  // d_slackVars.push_back(slack);
-
-  // d_simplex.increaseMax();
-
-  // d_tableau.increaseSize();
-  // d_tableauSizeHasBeenModified = true;
-
-  // d_constraintDatabase.addVariable(varX);
-
   Debug("arith::arithvar") << x << " |-> " << varX << endl;
 
   Assert(!d_partialModel.hasUpperBound(varX));
@@ -2160,7 +2107,11 @@ void TheoryArithPrivate::propagate(Theory::Effort e) {
      (options::arithPropagationMode() == BOUND_INFERENCE_PROP ||
       options::arithPropagationMode() == BOTH_PROP)
      && hasAnyUpdates()){
-    propagateCandidates();
+    if(options::newProp()){
+      propagateCandidatesNew();
+    }else{
+      propagateCandidates();
+    }
   }else{
     clearUpdates();
   }
@@ -2597,6 +2548,9 @@ bool TheoryArithPrivate::propagateCandidateBound(ArithVar basic, bool upperBound
         }
         // I think this can be skipped if canBePropagated is true
         //d_learnedBounds.push(bestImplied);
+        cout << "success " << bestImplied << endl;
+        d_partialModel.printModel(basic, cout);
+
         return true;
       }
       cout << "failed " << basic << " " << bound << assertedToTheTheory << " " <<
@@ -2612,10 +2566,10 @@ bool TheoryArithPrivate::propagateCandidateBound(ArithVar basic, bool upperBound
 
 void TheoryArithPrivate::propagateCandidate(ArithVar basic){
   bool success = false;
-  if(d_partialModel.strictlyAboveLowerBound(basic) && d_linEq.hasLowerBounds(basic)){
+  if(d_partialModel.strictlyAboveLowerBound(basic) && d_linEq.hasBounds(basic, false)){
     success |= propagateCandidateLowerBound(basic);
   }
-  if(d_partialModel.strictlyBelowUpperBound(basic) && d_linEq.hasUpperBounds(basic)){
+  if(d_partialModel.strictlyBelowUpperBound(basic) && d_linEq.hasBounds(basic, true)){
     success |= propagateCandidateUpperBound(basic);
   }
   if(success){
@@ -2626,6 +2580,8 @@ void TheoryArithPrivate::propagateCandidate(ArithVar basic){
 void TheoryArithPrivate::propagateCandidates(){
   TimerStat::CodeTimer codeTimer(d_statistics.d_boundComputationTime);
 
+  cout << "propagateCandidates begin" << endl;
+
   Assert(d_candidateBasics.empty());
 
   if(d_updatedBounds.empty()){ return; }
@@ -2659,6 +2615,7 @@ void TheoryArithPrivate::propagateCandidates(){
     Assert(d_tableau.isBasic(candidate));
     propagateCandidate(candidate);
   }
+  cout << "propagateCandidates end" << endl << endl << endl;
 }
 
 void TheoryArithPrivate::propagateCandidatesNew(){
@@ -2675,6 +2632,207 @@ void TheoryArithPrivate::propagateCandidatesNew(){
    * 4: The implied bound on x is strictly smaller/greater than the current bound.
    *    (This is O(n) to compute.)
    */
+
+  TimerStat::CodeTimer codeTimer(d_statistics.d_boundComputationTime);
+  cout << "propagateCandidatesNew begin" << endl;
+
+  Assert(d_qflraStatus == Result::SAT);
+  if(d_updatedBounds.empty()){ return; }
+  dumpUpdatedBoundsToRows();
+  Assert(d_updatedBounds.empty());
+
+  if(!d_candidateRows.empty()){
+    UpdateTrackingCallback utcb(&d_linEq);
+    d_partialModel.processBoundsQueue(utcb);
+  }
+
+  while(!d_candidateRows.empty()){
+    RowIndex candidate = d_candidateRows.back();
+    d_candidateRows.pop_back();
+    propagateCandidateRow(candidate);
+  }
+  cout << "propagateCandidatesNew end" << endl << endl << endl;
+}
+
+bool TheoryArithPrivate::propagateMightSucceed(ArithVar v, bool ub) const{
+  int cmp = ub ? d_partialModel.cmpAssignmentUpperBound(v)
+    : d_partialModel.cmpAssignmentLowerBound(v);
+  bool hasSlack = ub ? cmp < 0 : cmp > 0;
+  if(hasSlack){
+    ConstraintType t = ub ? UpperBound : LowerBound;
+    const DeltaRational& a = d_partialModel.getAssignment(v);
+
+    return NullConstraint != d_constraintDatabase.getBestImpliedBound(v, t, a);
+  }else{
+    return false;
+  }
+}
+
+bool TheoryArithPrivate::attemptSingleton(RowIndex ridx, bool rowUp){
+  cout << "  attemptSingleton" << ridx;
+
+  const Tableau::Entry* ep;
+  ep = d_linEq.rowLacksBound(ridx, rowUp, ARITHVAR_SENTINEL);
+  Assert(ep != NULL);
+
+  ArithVar v = ep->getColVar();
+  const Rational& coeff = ep->getCoefficient();
+
+  // 0 = c * v + \sum rest
+  // Suppose rowUp
+  // - c * v = \sum rest \leq D
+  // if c > 0, v \geq -D/c so !vUp
+  // if c < 0, v \leq -D/c so  vUp
+  // Suppose not rowUp
+  // - c * v = \sum rest \geq D
+  // if c > 0, v \leq -D/c so  vUp
+  // if c < 0, v \geq -D/c so !vUp
+  bool vUp = (rowUp == ( coeff.sgn() < 0));
+
+  cout << "  " << rowUp << " " << v << " " << coeff << " " << vUp << endl;
+  cout << "  " << propagateMightSucceed(v, vUp) << endl;
+
+  if(propagateMightSucceed(v, vUp)){
+    DeltaRational dr = d_linEq.computeRowBound(ridx, rowUp, v);
+    DeltaRational bound = dr / (- coeff);
+    return tryToPropagate(ridx, rowUp, v, vUp, bound);
+  }
+  return false;
+}
+
+bool TheoryArithPrivate::attemptFull(RowIndex ridx, bool rowUp){
+  cout << "  attemptFull" << ridx << endl;
+
+  vector<const Tableau::Entry*> candidates;
+
+  for(Tableau::RowIterator i = d_tableau.ridRowIterator(ridx); !i.atEnd(); ++i){
+    const Tableau::Entry& e =*i;
+    const Rational& c = e.getCoefficient();
+    ArithVar v = e.getColVar();
+    bool vUp = (rowUp == (c.sgn() < 0));
+    if(propagateMightSucceed(v, vUp)){
+      candidates.push_back(&e);
+    }
+  }
+  if(candidates.empty()){ return false; }
+
+  const DeltaRational slack =
+    d_linEq.computeRowBound(ridx, rowUp, ARITHVAR_SENTINEL);
+  bool any = false;
+  vector<const Tableau::Entry*>::const_iterator i, iend;
+  for(i = candidates.begin(), iend = candidates.end(); i != iend; ++i){
+    const Tableau::Entry* ep = *i;
+    const Rational& c = ep->getCoefficient();
+    ArithVar v = ep->getColVar();
+
+    // See the comment for attemptSingleton()
+    bool activeUp = (rowUp == (c.sgn() > 0));
+    bool vUb = (rowUp == (c.sgn() < 0));
+
+    const DeltaRational& activeBound = activeUp ?
+      d_partialModel.getUpperBound(v):
+      d_partialModel.getLowerBound(v);
+
+    DeltaRational contribution = activeBound * c;
+    DeltaRational impliedBound = (slack - contribution)/(-c);
+
+    bool success = tryToPropagate(ridx, rowUp, v, vUb, impliedBound);
+    if(success){
+      cout << " success " << v << endl;
+    }else{
+      cout << " fail " << v << endl;
+    }
+    any |= success;
+  }
+  return any;
+}
+
+bool TheoryArithPrivate::tryToPropagate(RowIndex ridx, bool rowUp, ArithVar v, bool vUb, const DeltaRational& bound){
+
+  bool weaker = vUb ? d_partialModel.strictlyLessThanUpperBound(v, bound):
+    d_partialModel.strictlyGreaterThanLowerBound(v, bound);
+  if(weaker){
+    ConstraintType t = vUb ? UpperBound : LowerBound;
+    Constraint implied = d_constraintDatabase.getBestImpliedBound(v, t, bound);
+    if(implied != NullConstraint){
+      return rowImplicationCanBeApplied(ridx, rowUp, implied);
+    }
+  }
+  return false;
+}
+
+bool TheoryArithPrivate::rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, Constraint implied){
+  Assert(implied != NullConstraint);
+  ArithVar v = implied->getVariable();
+
+  bool assertedToTheTheory = implied->assertedToTheTheory();
+  bool canBePropagated = implied->canBePropagated();
+  bool hasProof = implied->hasProof();
+
+  Debug("arith::prop") << "arith::prop" << v
+                       << " " << assertedToTheTheory
+                       << " " << canBePropagated
+                       << " " << hasProof
+                       << endl;
+
+  if(implied->negationHasProof()){
+    Warning() << "the negation of " <<  implied << " : " << endl
+              << "has proof " << implied->getNegation() << endl
+              << implied->getNegation()->explainForConflict() << endl;
+  }
+
+  if(!assertedToTheTheory && canBePropagated && !hasProof ){
+    d_linEq.propagateRow(ridx, rowUp, implied);
+    return true;
+  }
+  cout << "failed " << v << " " << assertedToTheTheory << " " <<
+    canBePropagated << " " << hasProof << " " << implied << endl;
+  d_partialModel.printModel(v, cout);
+  return false;
+}
+
+bool TheoryArithPrivate::propagateCandidateRow(RowIndex ridx){
+  BoundCounts hasCount = d_linEq.hasBoundCount(ridx);
+  uint32_t rowLength = d_tableau.getRowLength(ridx);
+
+  bool success = false;
+  static int instance = 0;
+  ++instance;
+  cout << "propagateCandidateRow " << instance << " attempt " << rowLength << " " <<  hasCount << endl;
+
+  if(hasCount.lowerBoundCount() == rowLength){
+    success |= attemptFull(ridx, false);
+  }else if(hasCount.lowerBoundCount() + 1 == rowLength){
+    success |= attemptSingleton(ridx, false);
+  }
+
+  if(hasCount.upperBoundCount() == rowLength){
+    success |= attemptFull(ridx, true);
+  }else if(hasCount.upperBoundCount() + 1 == rowLength){
+    success |= attemptSingleton(ridx, true);
+  }
+  return success;
+}
+
+void TheoryArithPrivate::dumpUpdatedBoundsToRows(){
+  Assert(d_candidateRows.empty());
+  DenseSet::const_iterator i = d_updatedBounds.begin();
+  DenseSet::const_iterator end = d_updatedBounds.end();
+  for(; i != end; ++i){
+    ArithVar var = *i;
+    if(d_tableau.isBasic(var)){
+      RowIndex ridx = d_tableau.basicToRowIndex(var);
+      d_candidateRows.softAdd(ridx);
+    }else{
+      Tableau::ColIterator basicIter = d_tableau.colIterator(var);
+      for(; !basicIter.atEnd(); ++basicIter){
+        const Tableau::Entry& entry = *basicIter;
+        RowIndex ridx = entry.getRowIndex();
+        d_candidateRows.softAdd(ridx);
+      }
+    }
+  }
+  d_updatedBounds.purge();
 }
 
 }/* CVC4::theory::arith namespace */
diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h
index 4de562d0a..e522bb8c8 100644
--- a/src/theory/arith/theory_arith_private.h
+++ b/src/theory/arith/theory_arith_private.h
@@ -463,6 +463,7 @@ private:
 
   /** Tracks the basic variables where propagation might be possible. */
   DenseSet d_candidateBasics;
+  DenseSet d_candidateRows;
 
   bool hasAnyUpdates() { return !d_updatedBounds.empty(); }
   void clearUpdates();
@@ -470,6 +471,16 @@ private:
   void revertOutOfConflict();
 
   void propagateCandidatesNew();
+  void dumpUpdatedBoundsToRows();
+  bool propagateCandidateRow(RowIndex rid);
+  bool propagateMightSucceed(ArithVar v, bool ub) const;
+  /** Attempt to perform a row propagation where there is at most 1 possible variable.*/
+  bool attemptSingleton(RowIndex ridx, bool rowUp);
+  /** Attempt to perform a row propagation where every variable is a potential candidate.*/
+  bool attemptFull(RowIndex ridx, bool rowUp);
+  bool tryToPropagate(RowIndex ridx, bool rowUp, ArithVar v, bool vUp, const DeltaRational& bound);
+  bool rowImplicationCanBeApplied(RowIndex ridx, bool rowUp, Constraint bestImplied);
+
 
   void propagateCandidates();
   void propagateCandidate(ArithVar basic);