This commit merges the branch arithmetic/propagation-again into trunk.

	- This adds code for bounds refinement, and conflict weakening.
	- This adds util/boolean_simplification.h.
	- This adds a propagation manager to theory of arithmetic.
	- Propagation is disabled by default.
	- Propagation can be enabled by the command line flag "--enable-arithmetic-propagation"
	- Propagation interacts *heavily* with rewriting equalities, and will work best if the command line flag "--rewrite-arithmetic-equalities" is enabled.

1 files changed, 495 insertions, 119 deletions

diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index 1a9c39984..b804cb1aa 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -14,6 +14,33 @@ static const uint32_t NUM_CHECKS = 10;
 static const bool CHECK_AFTER_PIVOT = true;
 static const uint32_t VARORDER_CHECK_PERIOD = 200;
 
+SimplexDecisionProcedure::SimplexDecisionProcedure(ArithPropManager& propManager,
+                                                   ArithPartialModel& pm,
+                                                   Tableau& tableau) :
+  d_partialModel(pm),
+  d_tableau(tableau),
+  d_queue(pm, tableau),
+  d_propManager(propManager),
+  d_numVariables(0),
+  d_delayedLemmas(),
+  d_ZERO(0),
+  d_DELTA_ZERO(0,0)
+{
+  switch(Options::ArithPivotRule rule = Options::current()->pivotRule) {
+  case Options::MINIMUM:
+    d_queue.setPivotRule(ArithPriorityQueue::MINIMUM);
+    break;
+  case Options::BREAK_TIES:
+    d_queue.setPivotRule(ArithPriorityQueue::BREAK_TIES);
+    break;
+  case Options::MAXIMUM:
+    d_queue.setPivotRule(ArithPriorityQueue::MAXIMUM);
+    break;
+  default:
+    Unhandled(rule);
+  }
+}
+
 SimplexDecisionProcedure::Statistics::Statistics():
   d_statPivots("theory::arith::pivots",0),
   d_statUpdates("theory::arith::updates",0),
@@ -31,6 +58,13 @@ SimplexDecisionProcedure::Statistics::Statistics():
   d_successDuringVarOrderSearch("theory::arith::qi::DuringVarOrderSearch::success",0),
   d_attemptAfterVarOrderSearch("theory::arith::qi::AfterVarOrderSearch::attempt",0),
   d_successAfterVarOrderSearch("theory::arith::qi::AfterVarOrderSearch::success",0),
+  d_weakeningAttempts("theory::arith::weakening::attempts",0),
+  d_weakeningSuccesses("theory::arith::weakening::success",0),
+  d_weakenings("theory::arith::weakening::total",0),
+  d_weakenTime("theory::arith::weakening::time"),
+  d_boundComputationTime("theory::arith::bound::time"),
+  d_boundComputations("theory::arith::bound::boundComputations",0),
+  d_boundPropagations("theory::arith::bound::boundPropagations",0),
   d_delayedConflicts("theory::arith::delayedConflicts",0),
   d_pivotTime("theory::arith::pivotTime"),
   d_avgNumRowsNotContainingOnUpdate("theory::arith::avgNumRowsNotContainingOnUpdate"),
@@ -55,6 +89,15 @@ SimplexDecisionProcedure::Statistics::Statistics():
   StatisticsRegistry::registerStat(&d_attemptAfterVarOrderSearch);
   StatisticsRegistry::registerStat(&d_successAfterVarOrderSearch);
 
+  StatisticsRegistry::registerStat(&d_weakeningAttempts);
+  StatisticsRegistry::registerStat(&d_weakeningSuccesses);
+  StatisticsRegistry::registerStat(&d_weakenings);
+  StatisticsRegistry::registerStat(&d_weakenTime);
+
+  StatisticsRegistry::registerStat(&d_boundComputationTime);
+  StatisticsRegistry::registerStat(&d_boundComputations);
+  StatisticsRegistry::registerStat(&d_boundPropagations);
+
   StatisticsRegistry::registerStat(&d_delayedConflicts);
 
   StatisticsRegistry::registerStat(&d_pivotTime);
@@ -83,6 +126,15 @@ SimplexDecisionProcedure::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_attemptAfterVarOrderSearch);
   StatisticsRegistry::unregisterStat(&d_successAfterVarOrderSearch);
 
+  StatisticsRegistry::unregisterStat(&d_weakeningAttempts);
+  StatisticsRegistry::unregisterStat(&d_weakeningSuccesses);
+  StatisticsRegistry::unregisterStat(&d_weakenings);
+  StatisticsRegistry::unregisterStat(&d_weakenTime);
+
+  StatisticsRegistry::unregisterStat(&d_boundComputationTime);
+  StatisticsRegistry::unregisterStat(&d_boundComputations);
+  StatisticsRegistry::unregisterStat(&d_boundPropagations);
+
   StatisticsRegistry::unregisterStat(&d_delayedConflicts);
   StatisticsRegistry::unregisterStat(&d_pivotTime);
 
@@ -94,9 +146,21 @@ SimplexDecisionProcedure::Statistics::~Statistics(){
 Node SimplexDecisionProcedure::AssertLower(ArithVar x_i, const DeltaRational& c_i, TNode original){
   Debug("arith") << "AssertLower(" << x_i << " " << c_i << ")"<< std::endl;
 
-  if(d_partialModel.belowLowerBound(x_i, c_i, false)){
+  if(d_partialModel.belowLowerBound(x_i, c_i, true)){
     return Node::null();
   }
+  // if(d_partialModel.equalsLowerBound(x_i, c_i) && original.getKind() != AND){
+  //   TNode prevConstraint =  d_partialModel.getLowerConstraint(x_i);
+  //   if(prevConstraint.getKind() == EQUAL){
+  //     return Node::null();
+  //   }else{
+  //     Debug("beat::ya") << x_i << " "<< c_i << original << prevConstraint << endl;
+  //     Assert(prevConstraint.getKind() == AND);
+  //     d_partialModel.setLowerConstraint(x_i,original);
+  //     return Node::null();
+  //   }
+  // }
+
   if(d_partialModel.aboveUpperBound(x_i, c_i, true)){
     Node ubc = d_partialModel.getUpperConstraint(x_i);
     Node conflict =  NodeManager::currentNM()->mkNode(AND, ubc, original);
@@ -109,6 +173,8 @@ Node SimplexDecisionProcedure::AssertLower(ArithVar x_i, const DeltaRational& c_
   d_partialModel.setLowerConstraint(x_i,original);
   d_partialModel.setLowerBound(x_i, c_i);
 
+  d_updatedBounds.softAdd(x_i);
+
   if(!d_tableau.isBasic(x_i)){
     if(d_partialModel.getAssignment(x_i) < c_i){
       update(x_i, c_i);
@@ -127,23 +193,34 @@ Node SimplexDecisionProcedure::AssertUpper(ArithVar x_i, const DeltaRational& c_
 
   Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl;
 
-  if(d_partialModel.aboveUpperBound(x_i, c_i, false) ){ // \upperbound(x_i) <= c_i
-    //return false; //sat
-    return Node::null();
+  if(d_partialModel.aboveUpperBound(x_i, c_i, true) ){ // \upperbound(x_i) <= c_i
+    return Node::null(); //sat
   }
+
+  // if(d_partialModel.equalsUpperBound(x_i, c_i) && original.getKind() != AND){
+  //   TNode prevConstraint = d_partialModel.getUpperConstraint(x_i);
+  //   if(prevConstraint.getKind() == EQUAL){
+  //     return Node::null();
+  //   }else{
+  //     Debug("beat::ya") << x_i << " "<< c_i << original << prevConstraint  << endl;
+  //     Assert(prevConstraint.getKind() == AND);
+  //     d_partialModel.setUpperConstraint(x_i,original);
+  //     return Node::null();
+  //   }
+  // }
   if(d_partialModel.belowLowerBound(x_i, c_i, true)){// \lowerbound(x_i) > c_i
     Node lbc = d_partialModel.getLowerConstraint(x_i);
     Node conflict =  NodeManager::currentNM()->mkNode(AND, lbc, original);
     Debug("arith") << "AssertUpper conflict " << conflict << endl;
     ++(d_statistics.d_statAssertUpperConflicts);
-    //d_out->conflict(conflict);
     return conflict;
-    //return true;
   }
 
   d_partialModel.setUpperConstraint(x_i,original);
   d_partialModel.setUpperBound(x_i, c_i);
 
+  d_updatedBounds.softAdd(x_i);
+
   if(!d_tableau.isBasic(x_i)){
     if(d_partialModel.getAssignment(x_i) > c_i){
       update(x_i, c_i);
@@ -155,7 +232,6 @@ Node SimplexDecisionProcedure::AssertUpper(ArithVar x_i, const DeltaRational& c_
   if(Debug.isOn("model")) { d_partialModel.printModel(x_i); }
 
   return Node::null();
-  //return false;
 }
 
 
@@ -168,16 +244,13 @@ Node SimplexDecisionProcedure::AssertEquality(ArithVar x_i, const DeltaRational&
   // This can happen if both c_i <= x_i and x_i <= c_i are in the system.
   if(d_partialModel.belowLowerBound(x_i, c_i, false) &&
      d_partialModel.aboveUpperBound(x_i, c_i, false)){
-    //return false; //sat
-    return Node::null();
+    return Node::null(); //sat
   }
 
   if(d_partialModel.aboveUpperBound(x_i, c_i, true)){
     Node ubc = d_partialModel.getUpperConstraint(x_i);
     Node conflict =  NodeManager::currentNM()->mkNode(AND, ubc, original);
-    //d_out->conflict(conflict);
     Debug("arith") << "AssertLower conflict " << conflict << endl;
-    //return true;
     return conflict;
   }
 
@@ -185,8 +258,6 @@ Node SimplexDecisionProcedure::AssertEquality(ArithVar x_i, const DeltaRational&
     Node lbc = d_partialModel.getLowerConstraint(x_i);
     Node conflict =  NodeManager::currentNM()->mkNode(AND, lbc, original);
     Debug("arith") << "AssertUpper conflict " << conflict << endl;
-    //d_out->conflict(conflict);
-    //return true;
     return conflict;
   }
 
@@ -196,52 +267,18 @@ Node SimplexDecisionProcedure::AssertEquality(ArithVar x_i, const DeltaRational&
   d_partialModel.setUpperConstraint(x_i,original);
   d_partialModel.setUpperBound(x_i, c_i);
 
+  d_updatedBounds.softAdd(x_i);
+
   if(!d_tableau.isBasic(x_i)){
     if(!(d_partialModel.getAssignment(x_i) == c_i)){
       update(x_i, c_i);
     }
   }else{
     d_queue.enqueueIfInconsistent(x_i);
-    //checkBasicVariable(x_i);
   }
-
-  //return false;
   return Node::null();
 }
 
-// set<ArithVar> tableauAndHasSet(Tableau& tab, ArithVar v){
-//   set<ArithVar> has;
-//   for(ArithVarSet::const_iterator basicIter = tab.beginBasic();
-//       basicIter != tab.endBasic();
-//       ++basicIter){
-//     ArithVar basic = *basicIter;
-//     ReducedRowVector& row = tab.lookup(basic);
-
-//     if(row.has(v)){
-//       has.insert(basic);
-//     }
-//   }
-//   return has;
-// }
-
-// set<ArithVar> columnIteratorSet(Tableau& tab,ArithVar v){
-//   set<ArithVar> has;
-//   Column::iterator basicIter = tab.beginColumn(v);
-//   Column::iterator endIter = tab.endColumn(v);
-//   for(; basicIter != endIter; ++basicIter){
-//     ArithVar basic = *basicIter;
-//     has.insert(basic);
-//   }
-//   return has;
-// }
-
-
-/*
-bool matchingSets(Tableau& tab, ArithVar v){
-  return tableauAndHasSet(tab, v) == columnIteratorSet(tab, v);
-}
-*/
-
 void SimplexDecisionProcedure::update(ArithVar x_i, const DeltaRational& v){
   Assert(!d_tableau.isBasic(x_i));
   DeltaRational assignment_x_i = d_partialModel.getAssignment(x_i);
@@ -279,6 +316,116 @@ void SimplexDecisionProcedure::update(ArithVar x_i, const DeltaRational& v){
   if(Debug.isOn("paranoid:check_tableau")){  debugCheckTableau(); }
 }
 
+
+bool SimplexDecisionProcedure::propagateCandidateBound(ArithVar basic, bool upperBound){
+
+  DeltaRational bound = upperBound ?
+    computeUpperBound(basic):
+    computeLowerBound(basic);
+
+  if((upperBound && d_partialModel.strictlyBelowUpperBound(basic, bound)) ||
+     (!upperBound && d_partialModel.strictlyAboveLowerBound(basic, bound))){
+    Node bestImplied = upperBound ?
+      d_propManager.getBestImpliedUpperBound(basic, bound):
+      d_propManager.getBestImpliedLowerBound(basic, bound);
+
+    if(!bestImplied.isNull()){
+      bool asserted = d_propManager.isAsserted(bestImplied);
+      bool propagated = d_propManager.isPropagated(bestImplied);
+      if( !asserted && !propagated){
+
+        NodeBuilder<> nb(kind::AND);
+        if(upperBound){
+          explainNonbasicsUpperBound(basic, nb);
+        }else{
+          explainNonbasicsLowerBound(basic, nb);
+        }
+        Node explanation = nb;
+        d_propManager.propagate(bestImplied, explanation);
+        return true;
+      }else{
+        Debug("arith::prop") << basic << " " << asserted << " " << propagated << endl;
+      }
+    }
+  }
+  return false;
+}
+
+
+bool SimplexDecisionProcedure::hasBounds(ArithVar basic, bool upperBound){
+  for(Tableau::RowIterator iter = d_tableau.rowIterator(basic); !iter.atEnd(); ++iter){
+    const TableauEntry& entry = *iter;
+
+    ArithVar var = entry.getColVar();
+    if(var == basic) continue;
+    int sgn = entry.getCoefficient().sgn();
+    if(upperBound){
+      if( (sgn < 0 && !d_partialModel.hasLowerBound(var)) ||
+          (sgn > 0 && !d_partialModel.hasUpperBound(var))){
+        return false;
+      }
+    }else{
+      if( (sgn < 0 && !d_partialModel.hasUpperBound(var)) ||
+          (sgn > 0 && !d_partialModel.hasLowerBound(var))){
+        return false;
+      }
+    }
+  }
+  return true;
+}
+void SimplexDecisionProcedure::propagateCandidate(ArithVar basic){
+  bool success = false;
+  if(d_partialModel.strictlyAboveLowerBound(basic) &&
+     (!d_partialModel.hasLowerBound(basic) || d_propManager.hasStrongerLowerBound(d_partialModel.getLowerConstraint(basic))) &&
+     hasLowerBounds(basic)){
+    ++d_statistics.d_boundComputations;
+    success |= propagateCandidateLowerBound(basic);
+  }
+  if(d_partialModel.strictlyBelowUpperBound(basic) &&
+     (!d_partialModel.hasUpperBound(basic) || d_propManager.hasStrongerUpperBound(d_partialModel.getUpperConstraint(basic))) &&
+     hasUpperBounds(basic)){
+    ++d_statistics.d_boundComputations;
+    success |= propagateCandidateUpperBound(basic);
+  }
+  if(success){
+    ++d_statistics.d_boundPropagations;
+  }
+}
+
+void SimplexDecisionProcedure::propagateCandidates(){
+  TimerStat::CodeTimer codeTimer(d_statistics.d_boundComputationTime);
+
+  Assert(d_candidateBasics.empty());
+
+  if(d_updatedBounds.empty()){ return; }
+
+  PermissiveBackArithVarSet::const_iterator i = d_updatedBounds.begin();
+  PermissiveBackArithVarSet::const_iterator end = d_updatedBounds.end();
+  for(; i != end; ++i){
+    ArithVar var = *i;
+    if(d_tableau.isBasic(var)){
+      d_candidateBasics.softAdd(var);
+    }else{
+      Tableau::ColIterator basicIter = d_tableau.colIterator(var);
+      for(; !basicIter.atEnd(); ++basicIter){
+        const TableauEntry& entry = *basicIter;
+        ArithVar rowVar = entry.getRowVar();
+        Assert(entry.getColVar() == var);
+        Assert(d_tableau.isBasic(rowVar));
+        d_candidateBasics.softAdd(rowVar);
+      }
+    }
+  }
+  d_updatedBounds.purge();
+
+  while(!d_candidateBasics.empty()){
+    ArithVar candidate = d_candidateBasics.pop_back();
+    Assert(d_tableau.isBasic(candidate));
+    propagateCandidate(candidate);
+  }
+}
+
+
 void SimplexDecisionProcedure::debugPivotSimplex(ArithVar x_i, ArithVar x_j){
   Debug("arith::simplex:row") << "debugRowSimplex("
                               << x_i  << "|->" << x_j
@@ -545,14 +692,14 @@ Node SimplexDecisionProcedure::checkBasicForConflict(ArithVar basic){
   const DeltaRational& beta = d_partialModel.getAssignment(basic);
 
   if(d_partialModel.belowLowerBound(basic, beta, true)){
-    ArithVar x_j = selectSlackBelow<minVarOrder>(basic);
+    ArithVar x_j = selectSlackUpperBound<minVarOrder>(basic);
     if(x_j == ARITHVAR_SENTINEL ){
-      return generateConflictBelow(basic);
+      return generateConflictBelowLowerBound(basic);
     }
   }else if(d_partialModel.aboveUpperBound(basic, beta, true)){
-    ArithVar x_j = selectSlackAbove<minVarOrder>(basic);
+    ArithVar x_j = selectSlackLowerBound<minVarOrder>(basic);
     if(x_j == ARITHVAR_SENTINEL ){
-      return generateConflictAbove(basic);
+      return generateConflictAboveUpperBound(basic);
     }
   }
   return Node::null();
@@ -580,30 +727,43 @@ Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera
     ArithVar x_j = ARITHVAR_SENTINEL;
 
     if(d_partialModel.belowLowerBound(x_i, beta_i, true)){
-      x_j = selectSlackBelow<pf>(x_i);
+      x_j = selectSlackUpperBound<pf>(x_i);
       if(x_j == ARITHVAR_SENTINEL ){
         ++(d_statistics.d_statUpdateConflicts);
-        return generateConflictBelow(x_i); //unsat
+        return generateConflictBelowLowerBound(x_i); //unsat
       }
       DeltaRational l_i = d_partialModel.getLowerBound(x_i);
       pivotAndUpdate(x_i, x_j, l_i);
 
     }else if(d_partialModel.aboveUpperBound(x_i, beta_i, true)){
-      x_j = selectSlackAbove<pf>(x_i);
+      x_j = selectSlackLowerBound<pf>(x_i);
       if(x_j == ARITHVAR_SENTINEL ){
         ++(d_statistics.d_statUpdateConflicts);
-        return generateConflictAbove(x_i); //unsat
+        return generateConflictAboveUpperBound(x_i); //unsat
       }
       DeltaRational u_i = d_partialModel.getUpperBound(x_i);
       pivotAndUpdate(x_i, x_j, u_i);
     }
     Assert(x_j != ARITHVAR_SENTINEL);
+
     //Check to see if we already have a conflict with x_j to prevent wasteful work
     if(CHECK_AFTER_PIVOT){
-      Node earlyConflict = checkBasicForConflict(x_j);
-      if(!earlyConflict.isNull()){
-        return earlyConflict;
+      Node possibleConflict = checkBasicForConflict(x_j);
+      if(!possibleConflict.isNull()){
+        return possibleConflict;
       }
+      // if(selectSlackUpperBound<pf>(x_j) == ARITHVAR_SENTINEL){
+      //   Node possibleConflict  = deduceUpperBound(x_j);
+      //   if(!possibleConflict.isNull()){
+      //     return possibleConflict;
+      //   }
+      // }
+      // if(selectSlackLowerBound<pf>(x_j) == ARITHVAR_SENTINEL){
+      //   Node possibleConflict  = deduceLowerBound(x_j);
+      //   if(!possibleConflict.isNull()){
+      //     return possibleConflict;
+      //   }
+      // }
     }
   }
   Assert(remainingIterations == 0);
@@ -611,93 +771,289 @@ Node SimplexDecisionProcedure::searchForFeasibleSolution(uint32_t remainingItera
   return Node::null();
 }
 
+template <bool upperBound>
+void SimplexDecisionProcedure::explainNonbasics(ArithVar basic, NodeBuilder<>& output){
+  Assert(d_tableau.isBasic(basic));
 
-Node SimplexDecisionProcedure::generateConflictAbove(ArithVar conflictVar){
-
-  NodeBuilder<> nb(kind::AND);
-  TNode bound = d_partialModel.getUpperConstraint(conflictVar);
-
-  Debug("arith")  << "generateConflictAbove "
-                  << "conflictVar " << conflictVar
-                  << " " << d_partialModel.getAssignment(conflictVar)
-                  << " " << bound << endl;
+  Debug("arith::explainNonbasics") << "SimplexDecisionProcedure::explainNonbasics("
+                                   << basic <<") start" << endl;
 
-  nb << bound;
 
-  Tableau::RowIterator iter = d_tableau.rowIterator(conflictVar);
+  Tableau::RowIterator iter = d_tableau.rowIterator(basic);
   for(; !iter.atEnd(); ++iter){
     const TableauEntry& entry = *iter;
     ArithVar nonbasic = entry.getColVar();
-    if(nonbasic == conflictVar) continue;
+    if(nonbasic == basic) continue;
 
     const Rational& a_ij = entry.getCoefficient();
     Assert(a_ij != d_ZERO);
+    TNode bound = TNode::null();
 
     int sgn = a_ij.sgn();
     Assert(sgn != 0);
-    if(sgn < 0){
-      bound =  d_partialModel.getUpperConstraint(nonbasic);
-      Debug("arith") << "below 0 " << nonbasic << " "
-                     << d_partialModel.getAssignment(nonbasic)
-                     << " " << bound << endl;
-      nb << bound;
+    if(upperBound){
+      if(sgn < 0){
+        bound = d_partialModel.getLowerConstraint(nonbasic);
+      }else{
+        Assert(sgn > 0);
+        bound = d_partialModel.getUpperConstraint(nonbasic);
+      }
     }else{
-      Assert(sgn > 0);
-      bound =  d_partialModel.getLowerConstraint(nonbasic);
-      Debug("arith") << " above 0 " << nonbasic << " "
-                     << d_partialModel.getAssignment(nonbasic)
-                     << " " << bound << endl;
-      nb << bound;
+      if(sgn < 0){
+        bound =  d_partialModel.getUpperConstraint(nonbasic);
+      }else{
+        Assert(sgn > 0);
+        bound =  d_partialModel.getLowerConstraint(nonbasic);
+      }
     }
+    Assert(!bound.isNull());
+    Debug("arith::explainNonbasics") << "\t" << nonbasic << " " << sgn << " " << bound
+                                     << endl;
+    output << bound;
   }
-  Node conflict = nb;
-  return conflict;
+  Debug("arith::explainNonbasics") << "SimplexDecisionProcedure::explainNonbasics("
+                                   << basic << ") done" << endl;
 }
 
-Node SimplexDecisionProcedure::generateConflictBelow(ArithVar conflictVar){
-  NodeBuilder<> nb(kind::AND);
-  TNode bound = d_partialModel.getLowerConstraint(conflictVar);
-
-  Debug("arith") << "generateConflictBelow "
-                 << "conflictVar " << conflictVar
-                 << d_partialModel.getAssignment(conflictVar) << " "
-                 << " " << bound << endl;
-  nb << bound;
 
+TNode SimplexDecisionProcedure::weakestExplanation(bool aboveUpper, DeltaRational& surplus, ArithVar v, const Rational& coeff, bool& anyWeakening, ArithVar basic){
+
+  int sgn = coeff.sgn();
+  bool ub = aboveUpper?(sgn < 0) : (sgn > 0);
+  TNode exp = ub ?
+    d_partialModel.getUpperConstraint(v) :
+    d_partialModel.getLowerConstraint(v);
+  DeltaRational bound = ub?
+    d_partialModel.getUpperBound(v) :
+    d_partialModel.getLowerBound(v);
+
+  bool weakened;
+  do{
+    weakened = false;
+
+    Node weaker = ub?
+      d_propManager.strictlyWeakerAssertedUpperBound(v, bound):
+      d_propManager.strictlyWeakerAssertedLowerBound(v, bound);
+
+    if(!weaker.isNull()){
+      DeltaRational weakerBound = asDeltaRational(weaker);
+
+      DeltaRational diff = aboveUpper ? bound - weakerBound : weakerBound - bound;
+      //if var == basic,
+      //  if aboveUpper, weakerBound > bound, multiply by -1
+      //  if !aboveUpper, weakerBound < bound, multiply by -1
+      diff = diff * coeff;
+      if(surplus > diff){
+        ++d_statistics.d_weakenings;
+        weakened = true;
+        anyWeakening = true;
+        surplus = surplus - diff;
+
+        Debug("weak") << "found:" << endl;
+        if(v == basic){
+          Debug("weak") << "  basic: ";
+        }
+        Debug("weak") << "  " << surplus << " "<< diff  << endl
+                      << "  " << bound << exp << endl
+                      << "  " << weakerBound << weaker << endl;
 
-  Tableau::RowIterator iter = d_tableau.rowIterator(conflictVar);
-  for(; !iter.atEnd(); ++iter){
-    const TableauEntry& entry = *iter;
-    ArithVar nonbasic = entry.getColVar();
-    if(nonbasic == conflictVar) continue;
+        if(exp.getKind() == AND){
+          Debug("weak") << "VICTORY" << endl;
+        }
 
-    const Rational& a_ij = entry.getCoefficient();
+        Assert(diff > d_DELTA_ZERO);
+        exp = weaker;
+        bound = weakerBound;
+      }
+    }
+  }while(weakened);
 
-    int sgn = a_ij.sgn();
-    Assert(a_ij != d_ZERO);
-    Assert(sgn != 0);
+  if(exp.getKind() == AND){
+    Debug("weak") << "boo: " << exp << endl;
+  }
+  return exp;
+}
 
-    if(sgn < 0){
-      TNode bound = d_partialModel.getLowerConstraint(nonbasic);
-      Debug("arith") << "Lower "<< nonbasic << " "
-                     << d_partialModel.getAssignment(nonbasic) << " "
-                     << bound << endl;
+Node SimplexDecisionProcedure::weakenConflict(bool aboveUpper, ArithVar basicVar){
+  TimerStat::CodeTimer codeTimer(d_statistics.d_weakenTime);
 
-      nb << bound;
-    }else{
-      Assert(sgn > 0);
-      TNode bound = d_partialModel.getUpperConstraint(nonbasic);
-      Debug("arith") << "Upper "<< nonbasic << " "
-                     << d_partialModel.getAssignment(nonbasic) << " "
-                     << bound << endl;
+  const DeltaRational& assignment = d_partialModel.getAssignment(basicVar);
+  DeltaRational surplus;
+  if(aboveUpper){
+    Assert(d_partialModel.hasUpperBound(basicVar));
+    Assert(assignment > d_partialModel.getUpperBound(basicVar));
+    surplus = assignment - d_partialModel.getUpperBound(basicVar);
+  }else{
+    Assert(d_partialModel.hasLowerBound(basicVar));
+    Assert(assignment < d_partialModel.getLowerBound(basicVar));
+    surplus = d_partialModel.getLowerBound(basicVar) - assignment;
+  }
 
-      nb << bound;
-    }
+  NodeBuilder<> conflict(kind::AND);
+  bool anyWeakenings = false;
+  for(Tableau::RowIterator i = d_tableau.rowIterator(basicVar); !i.atEnd(); ++i){
+    const TableauEntry& entry = *i;
+    ArithVar v = entry.getColVar();
+    const Rational& coeff = entry.getCoefficient();
+    conflict << weakestExplanation(aboveUpper, surplus, v, coeff, anyWeakenings, basicVar);
+  }
+  ++d_statistics.d_weakeningAttempts;
+  if(anyWeakenings){
+    ++d_statistics.d_weakeningSuccesses;
   }
-  Node conflict (nb.constructNode());
   return conflict;
 }
 
+
+// Node SimplexDecisionProcedure::weakenLowerBoundConflict(ArithVar basicVar){
+//   TimerStat::CodeTimer codeTimer(d_statistics.d_weakenTime);
+
+//   bool anyWeakenings = false;
+//   const DeltaRational& assignment = d_partialModel.getAssignment(basicVar);
+//   Assert(d_partialModel.hasLowerBound(basicVar));
+//   Assert(assignment < d_partialModel.getLowerBound(basicVar));
+
+//   DeltaRational surplus = d_partialModel.getLowerBound(basicVar) - assignment;
+
+//   vector<WeakeningElem> weakeningElements;
+//   queue<uint32_t> potentialWeakingings;
+//   for(Tableau::RowIterator i = d_tableau.rowIterator(basicVar); !i.atEnd(); ++i){
+//     const TableauEntry& entry = *i;
+//     ArithVar v = entry.getColVar();
+//     const Rational& coeff = entry.getCoefficient();
+
+//     int sgn = coeff.sgn();
+//     bool ub = (sgn > 0);
+//     Node exp = ub ?
+//       d_partialModel.getUpperConstraint(v) :
+//       d_partialModel.getLowerConstraint(v);
+//     DeltaRational bound = ub?
+//       d_partialModel.getUpperBound(v) :
+//       d_partialModel.getLowerBound(v);
+//     potentialWeakingings.push(weakeningElements.size());
+//     weakeningElements.push_back(WeakeningElem(v, &coeff, ub, bound, exp));
+//   }
+
+//   vector<Node> conflict;
+
+//   Debug("weak") << "weakenLowerBoundConflict" << endl;
+//   while(!potentialWeakingings.empty()){
+//     uint32_t pos = potentialWeakingings.front();
+//     potentialWeakingings.pop();
+
+//     WeakeningElem& curr = weakeningElements[pos];
+
+//     Node weaker = curr.upperBound?
+//       d_propManager.strictlyWeakerAssertedUpperBound(curr.var, curr.bound):
+//       d_propManager.strictlyWeakerAssertedLowerBound(curr.var, curr.bound);
+
+//     bool weakened = false;
+//     if(!weaker.isNull()){
+//       DeltaRational weakerBound = asDeltaRational(weaker);
+//       DeltaRational diff = weakerBound -  curr.bound;
+//       //if var == basic, weakerBound < curr.bound
+//       // multiply by -1
+//       diff = diff * (*curr.coeff);
+
+//       if(surplus > diff){
+//         ++d_statistics.d_weakenings;
+//         anyWeakenings = true;
+//         weakened = true;
+//         surplus = surplus - diff;
+
+//         Debug("weak") << "found:" << endl;
+//         if(curr.var == basicVar){
+//           Debug("weak") << "  basic: ";
+//         }
+//         Debug("weak") << "  " << surplus << " "<< diff  << endl
+//                       << "  " << curr.bound << weakerBound << endl
+//                       << "  " << curr.explanation << weaker << endl;
+
+//         if(curr.explanation.getKind() == AND){
+//           Debug("weak") << "VICTORY" << endl;
+//         }
+
+//         Assert(diff > d_DELTA_ZERO);
+//         curr.explanation = weaker;
+//         curr.bound = weakerBound;
+//       }
+//     }
+
+//     if(weakened){
+//       potentialWeakingings.push(pos);
+//     }else{
+//       if(curr.explanation.getKind() == AND){
+//         Debug("weak") << "boo: " << curr.explanation << endl;
+//       }
+//       conflict.push_back(curr.explanation);
+//     }
+//   }
+
+//   ++d_statistics.d_weakeningAttempts;
+//   if(anyWeakenings){
+//     ++d_statistics.d_weakeningSuccesses;
+//   }
+
+//   NodeBuilder<> nb(AND);
+//   nb.append(conflict);
+//   return nb;
+// }
+
+// Node SimplexDecisionProcedure::deduceUpperBound(ArithVar basicVar){
+//   Assert(d_tableau.isBasic(basicVar));
+//   Assert(selectSlackUpperBound<minVarOrder>(basicVar) == ARITHVAR_SENTINEL);
+
+//   const DeltaRational& assignment = d_partialModel.getAssignment(basicVar);
+
+//   Assert(assignment.getInfinitesimalPart() <= 0);
+
+//   if(d_partialModel.strictlyBelowUpperBound(basicVar, assignment)){
+//     NodeBuilder<> nb(kind::AND);
+//     explainNonbasicsUpperBound(basicVar, nb);
+//     Node explanation = maybeUnaryConvert(nb);
+//     Debug("waka-waka") << basicVar << " ub " << assignment << " "<< explanation << endl;
+//     Node res = AssertUpper(basicVar, assignment, explanation);
+//     if(res.isNull()){
+//       d_propManager.propagateArithVar(true, basicVar, assignment, explanation);
+//     }
+//     return res;
+//   }else{
+//     return Node::null();
+//   }
+// }
+
+// Node SimplexDecisionProcedure::deduceLowerBound(ArithVar basicVar){
+//   Assert(d_tableau.isBasic(basicVar));
+//   Assert(selectSlackLowerBound<minVarOrder>(basicVar) == ARITHVAR_SENTINEL);
+//   const DeltaRational& assignment = d_partialModel.getAssignment(basicVar);
+
+//   if(Debug.isOn("paranoid:check_tableau")){ debugCheckTableau(); }
+
+//   Assert(assignment.getInfinitesimalPart() >= 0);
+
+//   if(d_partialModel.strictlyAboveLowerBound(basicVar, assignment)){
+//     NodeBuilder<> nb(kind::AND);
+//     explainNonbasicsLowerBound(basicVar, nb);
+//     Node explanation = maybeUnaryConvert(nb);
+//     Debug("waka-waka") << basicVar << " lb " << assignment << " "<< explanation << endl;
+//     Node res = AssertLower(basicVar, assignment, explanation);
+//     if(res.isNull()){
+//       d_propManager.propagateArithVar(false, basicVar, assignment, explanation);
+//     }
+//     return res;
+//   }else{
+//     return Node::null();
+//   }
+// }
+
+Node SimplexDecisionProcedure::generateConflictAboveUpperBound(ArithVar conflictVar){
+  return weakenConflict(true, conflictVar);
+}
+
+Node SimplexDecisionProcedure::generateConflictBelowLowerBound(ArithVar conflictVar){
+  return weakenConflict(false, conflictVar);
+}
+
 /**
  * Computes the value of a basic variable using the current assignment.
  */
@@ -717,6 +1073,26 @@ DeltaRational SimplexDecisionProcedure::computeRowValue(ArithVar x, bool useSafe
   return sum;
 }
 
+DeltaRational SimplexDecisionProcedure::computeBound(ArithVar basic, bool upperBound){
+  DeltaRational sum(0,0);
+  for(Tableau::RowIterator i = d_tableau.rowIterator(basic); !i.atEnd(); ++i){
+    const TableauEntry& 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_partialModel.getUpperBound(nonbasic):
+      d_partialModel.getLowerBound(nonbasic);
+
+    DeltaRational diff = bound * coeff;
+    sum = sum + diff;
+  }
+  return sum;
+}
+
 /**
  * This check is quite expensive.
  * It should be wrapped in a Debug.isOn() guard.