This commit merges in the branch arithmetic/cprop.

5 files changed, 388 insertions, 50 deletions

diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index d2a0d9bfa..d451e9597 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -66,7 +66,11 @@ ConstraintValue::ConstraintValue(ArithVar x,  ConstraintType t, const DeltaRatio
 
 
 std::ostream& operator<<(std::ostream& o, const Constraint c){
-  return o << *c;
+  if(c == NullConstraint){
+    return o << "NullConstraint";
+  }else{
+    return o << *c;
+  }
 }
 
 std::ostream& operator<<(std::ostream& o, const ConstraintType t){
@@ -530,6 +534,19 @@ ConstraintDatabase::~ConstraintDatabase(){
   Assert(d_nodetoConstraintMap.empty());
 }
 
+ConstraintDatabase::Statistics::Statistics():
+  d_unatePropagateCalls("theory::arith::cd::unatePropagateCalls", 0),
+  d_unatePropagateImplications("theory::arith::cd::unatePropagateImplications", 0)
+{
+  StatisticsRegistry::registerStat(&d_unatePropagateCalls);
+  StatisticsRegistry::registerStat(&d_unatePropagateImplications);
+
+}
+ConstraintDatabase::Statistics::~Statistics(){
+  StatisticsRegistry::unregisterStat(&d_unatePropagateCalls);
+  StatisticsRegistry::unregisterStat(&d_unatePropagateImplications);
+}
+
 void ConstraintDatabase::addVariable(ArithVar v){
   Assert(v == d_varDatabases.size());
   d_varDatabases.push_back(new PerVariableDatabase(v));
@@ -1050,29 +1067,15 @@ void mutuallyExclusive(std::vector<Node>& out, Constraint a, Constraint b){
   out.push_back(orderOr);
 }
 
-void ConstraintDatabase::outputAllUnateLemmas(std::vector<Node>& out, ArithVar v) const{
+void ConstraintDatabase::outputUnateInequalityLemmas(std::vector<Node>& out, ArithVar v) const{
   SortedConstraintMap& scm = getVariableSCM(v);
-
-  SortedConstraintMapConstIterator outer;
+  SortedConstraintMapConstIterator scm_iter = scm.begin();
   SortedConstraintMapConstIterator scm_end = scm.end();
-
-  vector<Constraint> equalities;
-  for(outer = scm.begin(); outer != scm_end; ++outer){
-    const ValueCollection& vc = outer->second;
-    if(vc.hasEquality()){
-      Constraint eq = vc.getEquality();
-      if(eq->hasLiteral()){
-        equalities.push_back(eq);
-      }
-    }
-  }
-
   Constraint prev = NullConstraint;
   //get transitive unates
   //Only lower bounds or upperbounds should be done.
-  for(outer = scm.begin(); outer != scm_end; ++outer){
-    const ValueCollection& vc = outer->second;
-
+  for(; scm_iter != scm_end; ++scm_iter){
+    const ValueCollection& vc = scm_iter->second;
     if(vc.hasUpperBound()){
       Constraint ub = vc.getUpperBound();
       if(ub->hasLiteral()){
@@ -1083,6 +1086,26 @@ void ConstraintDatabase::outputAllUnateLemmas(std::vector<Node>& out, ArithVar v
       }
     }
   }
+}
+
+void ConstraintDatabase::outputUnateEqualityLemmas(std::vector<Node>& out, ArithVar v) const{
+
+  vector<Constraint> equalities;
+
+  SortedConstraintMap& scm = getVariableSCM(v);
+  SortedConstraintMapConstIterator scm_iter = scm.begin();
+  SortedConstraintMapConstIterator scm_end = scm.end();
+
+  for(; scm_iter != scm_end; ++scm_iter){
+    const ValueCollection& vc = scm_iter->second;
+    if(vc.hasEquality()){
+      Constraint eq = vc.getEquality();
+      if(eq->hasLiteral()){
+        equalities.push_back(eq);
+      }
+    }
+  }
+
   vector<Constraint>::const_iterator i, j, eq_end = equalities.end();
   for(i = equalities.begin(); i != eq_end; ++i){
     Constraint at_i = *i;
@@ -1116,14 +1139,190 @@ void ConstraintDatabase::outputAllUnateLemmas(std::vector<Node>& out, ArithVar v
       implies(out, eq, ub);
     }
   }
+}
+
+void ConstraintDatabase::outputUnateEqualityLemmas(std::vector<Node>& lemmas) const{
+  for(ArithVar v = 0, N = d_varDatabases.size(); v < N; ++v){
+    outputUnateEqualityLemmas(lemmas, v);
   }
+}
 
-void ConstraintDatabase::outputAllUnateLemmas(std::vector<Node>& lemmas) const{
+void ConstraintDatabase::outputUnateInequalityLemmas(std::vector<Node>& lemmas) const{
   for(ArithVar v = 0, N = d_varDatabases.size(); v < N; ++v){
-    outputAllUnateLemmas(lemmas, v);
+    outputUnateInequalityLemmas(lemmas, v);
   }
 }
 
+void ConstraintDatabase::unatePropLowerBound(Constraint curr, Constraint prev){
+  Debug("arith::unate") << "unatePropLowerBound " << curr << " " << prev << endl;
+  Assert(curr != prev);
+  Assert(curr != NullConstraint);
+  bool hasPrev = ! (prev == NullConstraint);
+  Assert(!hasPrev || curr->getValue() > prev->getValue());
+
+  ++d_statistics.d_unatePropagateCalls;
+
+  const SortedConstraintMap& scm = curr->constraintSet();
+  const SortedConstraintMapConstIterator scm_begin = scm.begin();
+  SortedConstraintMapConstIterator scm_i = curr->d_variablePosition;
+
+  //Ignore the first ValueCollection
+  // NOPE: (>= p c) then (= p c) NOPE
+  // NOPE: (>= p c) then (not (= p c)) NOPE
+
+  while(scm_i != scm_begin){
+    --scm_i; // move the iterator back
+
+    const ValueCollection& vc = scm_i->second;
+
+    //If it has the previous element, do nothing and stop!
+    if(hasPrev &&
+       vc.hasConstraintOfType(prev->getType())
+       && vc.getConstraintOfType(prev->getType()) == prev){
+      break;
+    }
+
+    //Don't worry about implying the negation of upperbound.
+    //These should all be handled by propagating the LowerBounds!
+    if(vc.hasLowerBound()){
+      Constraint lb = vc.getLowerBound();
+      if(!lb->isTrue()){
+        ++d_statistics.d_unatePropagateImplications;
+        Debug("arith::unate") << "unatePropLowerBound " << curr << " implies " << lb << endl;
+        lb->impliedBy(curr);
+      }
+    }
+    if(vc.hasDisequality()){
+      Constraint dis = vc.getDisequality();
+      if(!dis->isTrue()){
+        ++d_statistics.d_unatePropagateImplications;
+        Debug("arith::unate") << "unatePropLowerBound " << curr << " implies " << dis << endl;
+        dis->impliedBy(curr);
+      }
+    }
+  }
+}
+
+void ConstraintDatabase::unatePropUpperBound(Constraint curr, Constraint prev){
+  Debug("arith::unate") << "unatePropUpperBound " << curr << " " << prev << endl;
+  Assert(curr != prev);
+  Assert(curr != NullConstraint);
+  bool hasPrev = ! (prev == NullConstraint);
+  Assert(!hasPrev || curr->getValue() < prev->getValue());
+
+  ++d_statistics.d_unatePropagateCalls;
+
+  const SortedConstraintMap& scm = curr->constraintSet();
+  const SortedConstraintMapConstIterator scm_end = scm.end();
+  SortedConstraintMapConstIterator scm_i = curr->d_variablePosition;
+  ++scm_i;
+  for(; scm_i != scm_end; ++scm_i){
+    const ValueCollection& vc = scm_i->second;
+
+    //If it has the previous element, do nothing and stop!
+    if(hasPrev &&
+       vc.hasConstraintOfType(prev->getType()) &&
+       vc.getConstraintOfType(prev->getType()) == prev){
+      break;
+    }
+    //Don't worry about implying the negation of upperbound.
+    //These should all be handled by propagating the UpperBounds!
+    if(vc.hasUpperBound()){
+      Constraint ub = vc.getUpperBound();
+      if(!ub->isTrue()){
+        ++d_statistics.d_unatePropagateImplications;
+        Debug("arith::unate") << "unatePropUpperBound " << curr << " implies " << ub << endl;
+        ub->impliedBy(curr);
+      }
+    }
+    if(vc.hasDisequality()){
+      Constraint dis = vc.getDisequality();
+      if(!dis->isTrue()){
+        Debug("arith::unate") << "unatePropUpperBound " << curr << " implies " << dis << endl;
+        ++d_statistics.d_unatePropagateImplications;
+        dis->impliedBy(curr);
+      }
+    }
+  }
+}
+
+void ConstraintDatabase::unatePropEquality(Constraint curr, Constraint prevLB, Constraint prevUB){
+  Debug("arith::unate") << "unatePropEquality " << curr << " " << prevLB << " " << prevUB << endl;
+  Assert(curr != prevLB);
+  Assert(curr != prevUB);
+  Assert(curr != NullConstraint);
+  bool hasPrevLB = ! (prevLB == NullConstraint);
+  bool hasPrevUB = ! (prevUB == NullConstraint);
+  Assert(!hasPrevLB || curr->getValue() >= prevLB->getValue());
+  Assert(!hasPrevUB || curr->getValue() <= prevUB->getValue());
+
+  ++d_statistics.d_unatePropagateCalls;
+
+  const SortedConstraintMap& scm = curr->constraintSet();
+  SortedConstraintMapConstIterator scm_curr = curr->d_variablePosition;
+  SortedConstraintMapConstIterator scm_last = hasPrevUB ? prevUB->d_variablePosition : scm.end();
+  SortedConstraintMapConstIterator scm_i;
+  if(hasPrevLB){
+    scm_i = prevLB->d_variablePosition;
+    if(scm_i != scm_curr){ // If this does not move this past scm_curr, move it one forward
+      ++scm_i;
+    }
+  }else{
+    scm_i = scm.begin();
+  }
+
+  for(; scm_i != scm_curr; ++scm_i){
+    // between the previous LB and the curr
+    const ValueCollection& vc = scm_i->second;
+
+    //Don't worry about implying the negation of upperbound.
+    //These should all be handled by propagating the LowerBounds!
+    if(vc.hasLowerBound()){
+      Constraint lb = vc.getLowerBound();
+      if(!lb->isTrue()){
+        ++d_statistics.d_unatePropagateImplications;
+        Debug("arith::unate") << "unatePropUpperBound " << curr << " implies " << lb << endl;
+        lb->impliedBy(curr);
+      }
+    }
+    if(vc.hasDisequality()){
+      Constraint dis = vc.getDisequality();
+      if(!dis->isTrue()){
+        ++d_statistics.d_unatePropagateImplications;
+        Debug("arith::unate") << "unatePropUpperBound " << curr << " implies " << dis << endl;
+        dis->impliedBy(curr);
+      }
+    }
+  }
+  Assert(scm_i == scm_curr);
+  if(!hasPrevUB || scm_i != scm_last){
+    ++scm_i;
+  } // hasPrevUB implies scm_i != scm_last
+
+  for(; scm_i != scm_last; ++scm_i){
+    // between the curr and the previous UB imply the upperbounds and disequalities.
+    const ValueCollection& vc = scm_i->second;
+
+    //Don't worry about implying the negation of upperbound.
+    //These should all be handled by propagating the UpperBounds!
+    if(vc.hasUpperBound()){
+      Constraint ub = vc.getUpperBound();
+      if(!ub->isTrue()){
+        ++d_statistics.d_unatePropagateImplications;
+        Debug("arith::unate") << "unateProp " << curr << " implies " << ub << endl;
+        ub->impliedBy(curr);
+      }
+    }
+    if(vc.hasDisequality()){
+      Constraint dis = vc.getDisequality();
+      if(!dis->isTrue()){
+        ++d_statistics.d_unatePropagateImplications;
+        Debug("arith::unate") << "unateProp " << curr << " implies " << dis << endl;
+        dis->impliedBy(curr);
+      }
+    }
+  }
+}
 
 }/* arith namespace */
 }/* theory namespace */
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index fe10ecc4a..5b49dd54d 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -828,14 +828,38 @@ public:
    */
   Constraint getConstraint(ArithVar v, ConstraintType t, const DeltaRational& r);
 
+  /**
+   * Outputs a minimal set of unate implications onto the vector for the variable.
+   * This outputs lemmas of the general forms
+   *     (= p c) implies (<= p d) for c < d, or
+   *     (= p c) implies (not (= p d)) for c != d.
+   */
+  void outputUnateEqualityLemmas(std::vector<Node>& lemmas) const;
+  void outputUnateEqualityLemmas(std::vector<Node>& lemmas, ArithVar v) const;
 
   /**
-   * Outputs a minimal set of unate implications on the output channel
-   * for all variables.
+   * Outputs a minimal set of unate implications onto the vector for the variable.
+   *
+   * If ineqs is true, this outputs lemmas of the general form
+   *     (<= p c) implies (<= p d) for c < d.
    */
-  void outputAllUnateLemmas(std::vector<Node>& lemmas) const;
+  void outputUnateInequalityLemmas(std::vector<Node>& lemmas) const;
+  void outputUnateInequalityLemmas(std::vector<Node>& lemmas, ArithVar v) const;
+
+
+  void unatePropLowerBound(Constraint curr, Constraint prev);
+  void unatePropUpperBound(Constraint curr, Constraint prev);
+  void unatePropEquality(Constraint curr, Constraint prevLB, Constraint prevUB);
+
+private:
+  class Statistics {
+  public:
+    IntStat d_unatePropagateCalls;
+    IntStat d_unatePropagateImplications;
 
-  void outputAllUnateLemmas(std::vector<Node>& lemmas, ArithVar v) const;
+    Statistics();
+    ~Statistics();
+  } d_statistics;
 
 }; /* ConstraintDatabase */
 
diff --git a/src/theory/arith/simplex.cpp b/src/theory/arith/simplex.cpp
index 31187afd1..b5475586a 100644
--- a/src/theory/arith/simplex.cpp
+++ b/src/theory/arith/simplex.cpp
@@ -44,7 +44,7 @@ SimplexDecisionProcedure::SimplexDecisionProcedure(LinearEqualityModule& linEq,
   d_pivotsInRound(),
   d_DELTA_ZERO(0,0)
 {
-  switch(Options::ArithPivotRule rule = Options::current()->pivotRule) {
+  switch(Options::ArithPivotRule rule = Options::current()->arithPivotRule) {
   case Options::MINIMUM:
     d_queue.setPivotRule(ArithPriorityQueue::MINIMUM);
     break;
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 524079938..ac9796986 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -92,6 +92,7 @@ TheoryArith::Statistics::Statistics():
   d_simplifyTimer("theory::arith::simplifyTimer"),
   d_staticLearningTimer("theory::arith::staticLearningTimer"),
   d_presolveTime("theory::arith::presolveTime"),
+  d_newPropTime("::newPropTimer"),
   d_externalBranchAndBounds("theory::arith::externalBranchAndBounds",0),
   d_initialTableauSize("theory::arith::initialTableauSize", 0),
   d_currSetToSmaller("theory::arith::currSetToSmaller", 0),
@@ -112,6 +113,7 @@ TheoryArith::Statistics::Statistics():
   StatisticsRegistry::registerStat(&d_staticLearningTimer);
 
   StatisticsRegistry::registerStat(&d_presolveTime);
+  StatisticsRegistry::registerStat(&d_newPropTime);
 
   StatisticsRegistry::registerStat(&d_externalBranchAndBounds);
 
@@ -137,6 +139,7 @@ TheoryArith::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_staticLearningTimer);
 
   StatisticsRegistry::unregisterStat(&d_presolveTime);
+  StatisticsRegistry::unregisterStat(&d_newPropTime);
 
   StatisticsRegistry::unregisterStat(&d_externalBranchAndBounds);
 
@@ -150,6 +153,16 @@ TheoryArith::Statistics::~Statistics(){
   StatisticsRegistry::unregisterStat(&d_boundPropagations);
 }
 
+void TheoryArith::revertOutOfConflict(){
+  d_partialModel.revertAssignmentChanges();
+  clearUpdates();
+  d_currentPropagationList.clear();
+}
+
+void TheoryArith::clearUpdates(){
+  d_updatedBounds.purge();
+}
+
 void TheoryArith::zeroDifferenceDetected(ArithVar x){
   Assert(d_congruenceManager.isWatchedVariable(x));
   Assert(d_partialModel.upperBoundIsZero(x));
@@ -223,6 +236,9 @@ Node TheoryArith::AssertLower(Constraint constraint){
     }
   }
 
+  d_currentPropagationList.push_back(constraint);
+  d_currentPropagationList.push_back(d_partialModel.getLowerBoundConstraint(x_i));
+
   d_partialModel.setLowerBoundConstraint(constraint);
 
   if(d_congruenceManager.isWatchedVariable(x_i)){
@@ -306,6 +322,10 @@ Node TheoryArith::AssertUpper(Constraint constraint){
 
   }
 
+  d_currentPropagationList.push_back(constraint);
+  d_currentPropagationList.push_back(d_partialModel.getUpperBoundConstraint(x_i));
+  //It is fine if this is NullConstraint
+
   d_partialModel.setUpperBoundConstraint(constraint);
 
   if(d_congruenceManager.isWatchedVariable(x_i)){
@@ -380,6 +400,9 @@ Node TheoryArith::AssertEquality(Constraint constraint){
 
   // Don't bother to check whether x_i != c_i is in d_diseq
   // The a and (not a) should never be on the fact queue
+  d_currentPropagationList.push_back(constraint);
+  d_currentPropagationList.push_back(d_partialModel.getLowerBoundConstraint(x_i));
+  d_currentPropagationList.push_back(d_partialModel.getUpperBoundConstraint(x_i));
 
   d_partialModel.setUpperBoundConstraint(constraint);
   d_partialModel.setLowerBoundConstraint(constraint);
@@ -1128,6 +1151,7 @@ bool TheoryArith::hasIntegerModel(){
 
 
 void TheoryArith::check(Effort effortLevel){
+  Assert(d_currentPropagationList.empty());
   Debug("arith") << "TheoryArith::check begun" << std::endl;
 
   d_hasDoneWorkSinceCut = d_hasDoneWorkSinceCut || !done();
@@ -1137,17 +1161,16 @@ void TheoryArith::check(Effort effortLevel){
     Node possibleConflict = assertionCases(assertion);
 
     if(!possibleConflict.isNull()){
-      d_partialModel.revertAssignmentChanges();
+      revertOutOfConflict();
+
       Debug("arith::conflict") << "conflict   " << possibleConflict << endl;
-      clearUpdates();
       d_out->conflict(possibleConflict);
       return;
     }
     if(d_congruenceManager.inConflict()){
       Node c = d_congruenceManager.conflict();
-      d_partialModel.revertAssignmentChanges();
+      revertOutOfConflict();
       Debug("arith::conflict") << "difference manager conflict   " << c << endl;
-      clearUpdates();
       d_out->conflict(c);
       return;
     }
@@ -1162,38 +1185,84 @@ void TheoryArith::check(Effort effortLevel){
   Assert(d_conflicts.empty());
   bool foundConflict = d_simplex.findModel();
   if(foundConflict){
-    d_partialModel.revertAssignmentChanges();
-    clearUpdates();
+    revertOutOfConflict();
 
     Assert(!d_conflicts.empty());
     for(size_t i = 0, i_end = d_conflicts.size(); i < i_end; ++i){
       Node conflict = d_conflicts[i];
       Debug("arith::conflict") << "d_conflicts[" << i << "] " << conflict << endl;
-      d_out->conflict(conflict);      
+      d_out->conflict(conflict);
     }
     emmittedConflictOrSplit = true;
   }else{
     d_partialModel.commitAssignmentChanges();
   }
 
+  if(!emmittedConflictOrSplit &&
+     (Options::current()->arithPropagationMode == Options::UNATE_PROP ||
+      Options::current()->arithPropagationMode == Options::BOTH_PROP)){
+    TimerStat::CodeTimer codeTimer(d_statistics.d_newPropTime);
+
+    while(!d_currentPropagationList.empty()){
+      Constraint curr = d_currentPropagationList.front();
+      d_currentPropagationList.pop_front();
+
+      ConstraintType t = curr->getType();
+      Assert(t != Disequality, "Disequalities are not allowed in d_currentPropagation");
+
+
+      switch(t){
+      case LowerBound:
+        {
+          Constraint prev = d_currentPropagationList.front();
+          d_currentPropagationList.pop_front();
+          d_constraintDatabase.unatePropLowerBound(curr, prev);
+          break;
+        }
+      case UpperBound:
+        {
+          Constraint prev = d_currentPropagationList.front();
+          d_currentPropagationList.pop_front();
+          d_constraintDatabase.unatePropUpperBound(curr, prev);
+          break;
+        }
+      case Equality:
+        {
+          Constraint prevLB = d_currentPropagationList.front();
+          d_currentPropagationList.pop_front();
+          Constraint prevUB = d_currentPropagationList.front();
+          d_currentPropagationList.pop_front();
+          d_constraintDatabase.unatePropEquality(curr, prevLB, prevUB);
+          break;
+        }
+      default:
+        Unhandled(curr->getType());
+      }
+    }
+  }else{
+    TimerStat::CodeTimer codeTimer(d_statistics.d_newPropTime);
+    d_currentPropagationList.clear();
+  }
+  Assert( d_currentPropagationList.empty());
+
 
   if(!emmittedConflictOrSplit && fullEffort(effortLevel)){
     emmittedConflictOrSplit = splitDisequalities();
   }
 
-  Node possibleConflict = Node::null();
   if(!emmittedConflictOrSplit && fullEffort(effortLevel) && !hasIntegerModel()){
-
-    if(!emmittedConflictOrSplit && Options::current()->dioSolver){
+    Node possibleConflict = Node::null();
+    if(!emmittedConflictOrSplit && Options::current()->arithDioSolver){
       possibleConflict = callDioSolver();
       if(possibleConflict != Node::null()){
+        revertOutOfConflict();
         Debug("arith::conflict") << "dio conflict   " << possibleConflict << endl;
         d_out->conflict(possibleConflict);
         emmittedConflictOrSplit = true;
       }
     }
 
-    if(!emmittedConflictOrSplit && d_hasDoneWorkSinceCut && Options::current()->dioSolver){
+    if(!emmittedConflictOrSplit && d_hasDoneWorkSinceCut && Options::current()->arithDioSolver){
       Node possibleLemma = dioCutting();
       if(!possibleLemma.isNull()){
         Debug("arith") << "dio cut   " << possibleLemma << endl;
@@ -1358,7 +1427,9 @@ Node TheoryArith::explain(TNode n) {
 
 
 void TheoryArith::propagate(Effort e) {
-  if(Options::current()->arithPropagation && hasAnyUpdates()){
+  if((Options::current()->arithPropagationMode == Options::BOUND_INFERENCE_PROP ||
+      Options::current()->arithPropagationMode == Options::BOTH_PROP)
+     && hasAnyUpdates()){
     propagateCandidates();
   }else{
     clearUpdates();
@@ -1616,17 +1687,42 @@ void TheoryArith::presolve(){
     callCount = callCount + 1;
   }
 
-  if(Options::current()->arithPropagation ){
-    vector<Node> lemmas;
-    d_constraintDatabase.outputAllUnateLemmas(lemmas);
-    vector<Node>::const_iterator i = lemmas.begin(), i_end = lemmas.end();
-    for(; i != i_end; ++i){
-      Node lem = *i;
-      Debug("arith::oldprop") << " lemma lemma duck " <<lem << endl;
-      d_out->lemma(lem);
-    }
+  vector<Node> lemmas;
+  switch(Options::current()->arithUnateLemmaMode){
+  case Options::NO_PRESOLVE_LEMMAS:
+    break;
+  case Options::INEQUALITY_PRESOLVE_LEMMAS:
+    d_constraintDatabase.outputUnateInequalityLemmas(lemmas);
+    break;
+  case Options::EQUALITY_PRESOLVE_LEMMAS:
+    d_constraintDatabase.outputUnateEqualityLemmas(lemmas);
+    break;
+  case Options::ALL_PRESOLVE_LEMMAS:
+    d_constraintDatabase.outputUnateInequalityLemmas(lemmas);
+    d_constraintDatabase.outputUnateEqualityLemmas(lemmas);
+    break;
+  default:
+    Unhandled(Options::current()->arithUnateLemmaMode);
   }
 
+  vector<Node>::const_iterator i = lemmas.begin(), i_end = lemmas.end();
+  for(; i != i_end; ++i){
+    Node lem = *i;
+    Debug("arith::oldprop") << " lemma lemma duck " <<lem << endl;
+    d_out->lemma(lem);
+  }
+
+  // if(Options::current()->arithUnateLemmaMode == Options::ALL_UNATE){
+  //   vector<Node> lemmas;
+  //   d_constraintDatabase.outputAllUnateLemmas(lemmas);
+  //   vector<Node>::const_iterator i = lemmas.begin(), i_end = lemmas.end();
+  //   for(; i != i_end; ++i){
+  //     Node lem = *i;
+  //     Debug("arith::oldprop") << " lemma lemma duck " <<lem << endl;
+  //     d_out->lemma(lem);
+  //   }
+  // }
+
   d_learner.clear();
 }
 
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 431c82476..ebc131b60 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -160,11 +160,26 @@ private:
   Comparison mkIntegerEqualityFromAssignment(ArithVar v);
 
   /**
-   * List of all of the inequalities asserted in the current context.
+   * List of all of the disequalities asserted in the current context that are not known
+   * to be satisfied.
    */
-  //context::CDHashSet<Node, NodeHashFunction> d_diseq;
   context::CDQueue<Constraint> d_diseqQueue;
 
+  /**
+   * Constraints that have yet to be processed by proagation work list.
+   * All of the elements have type of LowerBound, UpperBound, or
+   * Equality.
+   *
+   * This is empty at the beginning of every check call.
+   *
+   * If head()->getType() == LowerBound or UpperBound,
+   * then d_cPL[1] is the previous constraint in d_partialModel for the
+   * corresponding bound.
+   * If head()->getType() == Equality,
+   * then d_cPL[1] is the previous lowerBound in d_partialModel,
+   * and d_cPL[2] is the previous upperBound in d_partialModel.
+   */
+  std::deque<Constraint> d_currentPropagationList;
 
   /**
    * Manages information about the assignment and upper and lower bounds on
@@ -380,7 +395,9 @@ private:
   DenseSet d_candidateBasics;
 
   bool hasAnyUpdates() { return !d_updatedBounds.empty(); }
-  void clearUpdates(){ d_updatedBounds.purge(); }
+  void clearUpdates();
+
+  void revertOutOfConflict();
 
   void propagateCandidates();
   void propagateCandidate(ArithVar basic);
@@ -445,6 +462,8 @@ private:
 
     TimerStat d_presolveTime;
 
+    TimerStat d_newPropTime;
+
     IntStat d_externalBranchAndBounds;
 
     IntStat d_initialTableauSize;