This commit merges in the branch arithmetic/cprop.

7 files changed, 565 insertions, 120 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;
diff --git a/src/util/options.cpp b/src/util/options.cpp
index e41959da2..a510f35f8 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -101,21 +101,22 @@ Options::Options() :
   replayFilename(""),
   replayStream(NULL),
   replayLog(NULL),
-  arithPropagation(true),
   satRandomFreq(0.0),
   satRandomSeed(91648253),// Minisat's default value
   satVarDecay(0.95),
   satClauseDecay(0.999),
   satRestartFirst(25),
   satRestartInc(3.0),
-  pivotRule(MINIMUM),
+  arithUnateLemmaMode(ALL_PRESOLVE_LEMMAS),
+  arithPropagationMode(BOTH_PROP),
+  arithPivotRule(MINIMUM),
   arithPivotThreshold(16),
   arithPropagateMaxLength(16),
-  ufSymmetryBreaker(false),
-  ufSymmetryBreakerSetByUser(false),
-  dioSolver(true),
+  arithDioSolver(true),
   arithRewriteEq(false),
   arithRewriteEqSetByUser(false),
+  ufSymmetryBreaker(false),
+  ufSymmetryBreakerSetByUser(false),
   lemmaOutputChannel(NULL),
   lemmaInputChannel(NULL),
   threads(2),// default should be 1 probably, but say 2 for now
@@ -134,8 +135,10 @@ static const string mostCommonOptionsDescription = "\
 Most commonly-used CVC4 options:\n\
    --version | -V         identify this CVC4 binary\n\
    --help | -h            full command line reference\n\
-   --lang | -L            force input language (default is `auto'; see --lang help)\n\
-   --output-lang          force output language (default is `auto'; see --lang help)\n\
+   --lang | -L            force input language\n\
+                          (default is `auto'; see --lang help)\n\
+   --output-lang          force output language\n\
+                          (default is `auto'; see --lang help)\n\
    --verbose | -v         increase verbosity (may be repeated)\n\
    --quiet | -q           decrease verbosity (may be repeated)\n\
    --stats                give statistics on exit\n\
@@ -165,7 +168,8 @@ Additional CVC4 options:\n\
    --mmap                 memory map file input\n\
    --segv-nospin          don't spin on segfault waiting for gdb\n\
    --lazy-type-checking   type check expressions only when necessary (default)\n\
-   --eager-type-checking  type check expressions immediately on creation (debug builds only)\n\
+   --eager-type-checking  type check expressions immediately on creation\n\
+                          (debug builds only)\n\
    --no-type-checking     never type check expressions\n\
    --no-checking          disable ALL semantic checks, including type checks\n\
    --no-theory-registration disable theory reg (not safe for some theories)\n\
@@ -185,18 +189,35 @@ Additional CVC4 options:\n\
    --no-ite-simp          turn off ite simplification (Kim (and Somenzi) et al., SAT 2009)\n\
    --replay=file          replay decisions from file\n\
    --replay-log=file      log decisions and propagations to file\n\
-   --pivot-rule=RULE      change the pivot rule (see --pivot-rule help)\n\
-   --pivot-threshold=N   sets the number of heuristic pivots per variable per simplex instance\n\
-   --prop-row-length=N    sets the maximum row length to be used in propagation\n\
-   --random-freq=P        sets the frequency of random decisions in the sat solver(P=0.0 by default)\n\
+  SAT:\n\
+   --random-freq=P        frequency of random decisions in the sat solver\n\
+                          (P=0.0 by default)\n\
    --random-seed=S        sets the random seed for the sat solver\n\
-   --restart-int-base=I   sets the base restart interval for the sat solver (I=25 by default)\n\
-   --restart-int-inc=F    sets the restart interval increase factor for the sat solver (F=3.0 by default)\n\
-   --disable-arithmetic-propagation turns on arithmetic propagation\n\
-   --enable-symmetry-breaker turns on UF symmetry breaker (Deharbe et al., CADE 2011) [on by default only for QF_UF]\n\
+   --restart-int-base=I   sets the base restart interval for the sat solver\n\
+                          (I=25 by default)\n\
+   --restart-int-inc=F    restart interval increase factor for the sat solver\n\
+                          (F=3.0 by default)\n\
+  ARITHMETIC:\n\
+   --arith-presolve-lemmas=MODE  determines which lemmas to add before solving\n\
+                          (default is 'all', see --arith-presolve-lemmas=help)\n\
+   --arith-prop=MODE      turns on arithmetic propagation\n\
+                          (default is 'old', see --arith-prop=help)\n\
+   --pivot-rule=RULE      change the pivot rule for the basic variable\n\
+                          (default is 'min', see --pivot-rule help)\n\
+   --pivot-threshold=N    sets the number of pivots using --pivot-rule\n\
+                          per basic variable per simplex instance before\n\
+                          using variable order\n\
+   --prop-row-length=N    sets the maximum row length to be used in propagation\n\
+   --disable-dio-solver   turns off Linear Diophantine Equation solver \n\
+                          (Griggio, JSAT 2012)\n\
+   --enable-arith-rewrite-equalities   turns on the preprocessing rewrite\n\
+                          turning equalities into a conjunction of inequalities.\n \
+   --disable-arith-rewrite-equalities   turns off the preprocessing rewrite\n\
+                          turning equalities into a conjunction of inequalities.\n \
+ UF:\n\
+   --enable-symmetry-breaker turns on UF symmetry breaker (Deharbe et al.,\n\
+                          CADE 2011) [on by default only for QF_UF]\n\
    --disable-symmetry-breaker turns off UF symmetry breaker\n\
-   --disable-dio-solver   turns off Linear Diophantine Equation solver (Griggio, JSAT 2012)\n\
-   --disable-arith-rewrite-equalities   turns off the preprocessing rewrite turning equalities into a conjunction of inequalities.\n\
    --threads=N            sets the number of solver threads\n\
    --threadN=string       configures thread N (0..#threads-1)\n\
    --filter-lemma-length=N don't share lemmas strictly longer than N\n\
@@ -315,6 +336,44 @@ pipe to perform on-line checking.  The --dump-to option can be used to dump\n\
 to a file.\n\
 ";
 
+static const string arithPresolveLemmasHelp = "\
+Presolve lemmas are generated before SAT search begins using the relationship\n\
+of constant terms and polynomials.\n\
+Modes currently supported by the --arith-presolve-lemmas option:\n\
++ none \n\
++ ineqs \n\
+  Outputs lemmas of the general form (<= p c) implies (<= p d) for c < d.\n\
++ eqs \n\
+  Outputs lemmas of the general forms\n\
+  (= p c) implies (<= p d) for c < d, or\n\
+  (= p c) implies (not (= p d)) for c != d.\n\
++ all \n\
+  A combination of inequalities and equalities.\n\
+";
+
+static const string propagationModeHelp = "\
+This decides on kind of propagation arithmetic attempts to do during the search.\n\
++ none\n\
++ unate\n\
+ use constraints to do unate propagation\n\
++ bi (Bounds Inference)\n\
+  infers bounds on basic variables using the upper and lower bounds of the\n\
+  non-basic variables in the tableau.\n\
++both\n\
+";
+
+static const string pivotRulesHelp = "\
+This decides on the rule used by simplex during hueristic rounds\n\
+for deciding the next basic variable to select.\n\
+Pivot rules available:\n\
++min\n\
+  The minimum abs() value of the variable's violation of its bound. (default)\n\
++min-break-ties\n\
+  The minimum violation with ties broken by variable order (total)\n\
++max\n\
+  The maximum violation the bound\n\
+";
+
 string Options::getDescription() const {
   return optionsDescription;
 }
@@ -341,7 +400,8 @@ void Options::printLanguageHelp(std::ostream& out) {
  * any collision.
  */
 enum OptionValue {
-  SMTCOMP = 256, /* avoid clashing with char options */
+  OPTION_VALUE_BEGIN = 256, /* avoid clashing with char options */
+  SMTCOMP, 
   STATS,
   SEGV_NOSPIN,
   OUTPUT_LANGUAGE,
@@ -377,13 +437,14 @@ enum OptionValue {
   EAGER_TYPE_CHECKING,
   REPLAY,
   REPLAY_LOG,
-  PIVOT_RULE,
   PRINT_WINNER,
   RANDOM_FREQUENCY,
   RANDOM_SEED,
   SAT_RESTART_FIRST,
   SAT_RESTART_INC,
-  ARITHMETIC_PROPAGATION,
+  ARITHMETIC_UNATE_LEMMA_MODE,
+  ARITHMETIC_PROPAGATION_MODE,
+  ARITHMETIC_PIVOT_RULE,
   ARITHMETIC_PIVOT_THRESHOLD,
   ARITHMETIC_PROP_MAX_LENGTH,
   ARITHMETIC_DIO_SOLVER,
@@ -401,7 +462,8 @@ enum OptionValue {
   BITVECTOR_EAGER_BITBLAST,
   BITVECTOR_SHARE_LEMMAS,
   BITVECTOR_EAGER_FULLCHECK,
-  SAT_REFINE_CONFLICTS
+  SAT_REFINE_CONFLICTS,
+  OPTION_VALUE_END
 };/* enum OptionValue */
 
 /**
@@ -475,15 +537,16 @@ static struct option cmdlineOptions[] = {
   { "incremental", no_argument      , NULL, 'i' },
   { "replay"     , required_argument, NULL, REPLAY      },
   { "replay-log" , required_argument, NULL, REPLAY_LOG  },
-  { "pivot-rule" , required_argument, NULL, PIVOT_RULE  },
-  { "pivot-threshold" , required_argument, NULL, ARITHMETIC_PIVOT_THRESHOLD  },
-  { "prop-row-length" , required_argument, NULL, ARITHMETIC_PROP_MAX_LENGTH  },
   { "random-freq" , required_argument, NULL, RANDOM_FREQUENCY  },
   { "random-seed" , required_argument, NULL, RANDOM_SEED  },
   { "restart-int-base", required_argument, NULL, SAT_RESTART_FIRST },
   { "restart-int-inc", required_argument, NULL, SAT_RESTART_INC },
   { "print-winner", no_argument     , NULL, PRINT_WINNER  },
-  { "disable-arithmetic-propagation", no_argument, NULL, ARITHMETIC_PROPAGATION },
+  { "unate-lemmas", required_argument, NULL, ARITHMETIC_UNATE_LEMMA_MODE },
+  { "arith-prop", required_argument, NULL, ARITHMETIC_PROPAGATION_MODE },
+  { "pivot-rule" , required_argument, NULL, ARITHMETIC_PIVOT_RULE  },
+  { "pivot-threshold" , required_argument, NULL, ARITHMETIC_PIVOT_THRESHOLD  },
+  { "prop-row-length" , required_argument, NULL, ARITHMETIC_PROP_MAX_LENGTH  },
   { "disable-dio-solver", no_argument, NULL, ARITHMETIC_DIO_SOLVER },
   { "enable-arith-rewrite-equalities", no_argument, NULL, ENABLE_ARITHMETIC_REWRITE_EQUALITIES },
   { "disable-arith-rewrite-equalities", no_argument, NULL, DISABLE_ARITHMETIC_REWRITE_EQUALITIES },
@@ -878,24 +941,6 @@ throw(OptionException) {
 #endif /* CVC4_REPLAY */
       break;
 
-    case ARITHMETIC_PROPAGATION:
-      arithPropagation = false;
-      break;
-
-    case ARITHMETIC_DIO_SOLVER:
-      dioSolver = false;
-      break;
-
-    case ENABLE_ARITHMETIC_REWRITE_EQUALITIES:
-      arithRewriteEq = true;
-      arithRewriteEqSetByUser = true;
-      break;
-
-    case DISABLE_ARITHMETIC_REWRITE_EQUALITIES:
-      arithRewriteEq = false;
-      arithRewriteEqSetByUser = true;
-      break;
-
     case ENABLE_SYMMETRY_BREAKER:
       ufSymmetryBreaker = true;
       ufSymmetryBreakerSetByUser = true;
@@ -993,21 +1038,62 @@ throw(OptionException) {
       }
       break;
 
-    case PIVOT_RULE:
+    case ARITHMETIC_UNATE_LEMMA_MODE:
+      if(!strcmp(optarg, "all")) {
+        arithUnateLemmaMode = ALL_PRESOLVE_LEMMAS;
+        break;
+      } else if(!strcmp(optarg, "none")) {
+        arithUnateLemmaMode = NO_PRESOLVE_LEMMAS;
+        break;
+      } else if(!strcmp(optarg, "ineqs")) {
+        arithUnateLemmaMode = INEQUALITY_PRESOLVE_LEMMAS;
+        break;
+      } else if(!strcmp(optarg, "eqs")) {
+        arithUnateLemmaMode = EQUALITY_PRESOLVE_LEMMAS;
+        break;
+      } else if(!strcmp(optarg, "help")) {
+        puts(arithPresolveLemmasHelp.c_str());
+        exit(1);
+      } else {
+        throw OptionException(string("unknown option for --arith-presolve-lemmas: `") +
+                              optarg + "'.  Try --arith-presolve-lemmas=help.");
+      }
+      break;
+
+    case ARITHMETIC_PROPAGATION_MODE:
+      if(!strcmp(optarg, "none")) {
+        arithPropagationMode = NO_PROP;
+        break;
+      } else if(!strcmp(optarg, "unate")) {
+        arithPropagationMode = UNATE_PROP;
+        break;
+      } else if(!strcmp(optarg, "bi")) {
+        arithPropagationMode = BOUND_INFERENCE_PROP;
+        break;
+      } else if(!strcmp(optarg, "both")) {
+        arithPropagationMode = BOTH_PROP;
+        break;
+      } else if(!strcmp(optarg, "help")) {
+        puts(propagationModeHelp.c_str());
+        exit(1);
+      } else {
+        throw OptionException(string("unknown option for --arith-prop: `") +
+                              optarg + "'.  Try --arith-prop help.");
+      }
+      break;
+
+    case ARITHMETIC_PIVOT_RULE:
       if(!strcmp(optarg, "min")) {
-        pivotRule = MINIMUM;
+        arithPivotRule = MINIMUM;
         break;
       } else if(!strcmp(optarg, "min-break-ties")) {
-        pivotRule = BREAK_TIES;
+        arithPivotRule = BREAK_TIES;
         break;
       } else if(!strcmp(optarg, "max")) {
-        pivotRule = MAXIMUM;
+        arithPivotRule = MAXIMUM;
         break;
       } else if(!strcmp(optarg, "help")) {
-        printf("Pivot rules available:\n");
-        printf("min\n");
-        printf("min-break-ties\n");
-        printf("max\n");
+        puts(pivotRulesHelp.c_str());
         exit(1);
       } else {
         throw OptionException(string("unknown option for --pivot-rule: `") +
@@ -1023,6 +1109,20 @@ throw(OptionException) {
       arithPropagateMaxLength = atoi(optarg);
       break;
 
+    case ARITHMETIC_DIO_SOLVER:
+      arithDioSolver = false;
+      break;
+
+    case ENABLE_ARITHMETIC_REWRITE_EQUALITIES:
+      arithRewriteEq = true;
+      arithRewriteEqSetByUser = true;
+      break;
+
+    case DISABLE_ARITHMETIC_REWRITE_EQUALITIES:
+      arithRewriteEq = false;
+      arithRewriteEqSetByUser = true;
+      break;
+
     case SHOW_DEBUG_TAGS:
       if(Configuration::isDebugBuild() && Configuration::isTracingBuild()) {
         printf("available tags:");
@@ -1121,7 +1221,8 @@ throw(OptionException) {
 
     case ':':
       // This can be a long or short option, and the way to get at the name of it is different.
-      if(optopt == 0) { // was a long option
+      if(optopt == 0 ||  // was a long option
+         (optopt >= OPTION_VALUE_BEGIN && optopt <= OPTION_VALUE_END)) { // OptionValue option
         throw OptionException(string("option `") + argv[optind - 1] + "' missing its required argument");
       } else { // was a short option
         throw OptionException(string("option `-") + char(optopt) + "' missing its required argument");
diff --git a/src/util/options.h b/src/util/options.h
index 896f77297..9c36a471d 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -203,9 +203,6 @@ struct CVC4_PUBLIC Options {
   /** Log to write replay instructions to; NULL if not logging. */
   std::ostream* replayLog;
 
-  /** Turn on and of arithmetic propagation. */
-  bool arithPropagation;
-
   /**
    * Frequency for the sat solver to make random decisions.
    * Should be between 0 and 1.
@@ -230,9 +227,17 @@ struct CVC4_PUBLIC Options {
   /** Restart interval increase factor for Minisat */
   double satRestartInc;
 
+  /** Determines the type of Arithmetic Presolve Lemmas are generated.*/
+  typedef enum { NO_PRESOLVE_LEMMAS, INEQUALITY_PRESOLVE_LEMMAS, EQUALITY_PRESOLVE_LEMMAS, ALL_PRESOLVE_LEMMAS} ArithUnateLemmaMode;
+  ArithUnateLemmaMode arithUnateLemmaMode;
+
+  /** Determines the mode of arithmetic propagation. */
+  typedef enum { NO_PROP, UNATE_PROP, BOUND_INFERENCE_PROP, BOTH_PROP} ArithPropagationMode;
+  ArithPropagationMode arithPropagationMode;
+
   /** The pivot rule for arithmetic */
   typedef enum { MINIMUM, BREAK_TIES, MAXIMUM } ArithPivotRule;
-  ArithPivotRule pivotRule;
+  ArithPivotRule arithPivotRule;
 
   /**
    * The number of pivots before Bland's pivot rule is used on a basic
@@ -246,22 +251,10 @@ struct CVC4_PUBLIC Options {
   uint16_t arithPropagateMaxLength;
 
   /**
-   * Whether to do the symmetry-breaking preprocessing in UF as
-   * described by Deharbe et al. in CADE 2011 (on by default).
-   */
-  bool ufSymmetryBreaker;
-
-  /**
-   * Whether the user explicitly requested that the symmetry
-   * breaker be enabled or disabled.
-   */
-  bool ufSymmetryBreakerSetByUser;
-
-  /**
    * Whether to do the linear diophantine equation solver
    * in Arith as described by Griggio JSAT 2012 (on by default).
    */
-  bool dioSolver;
+  bool arithDioSolver;
 
   /**
    * Whether to split (= x y) into (and (<= x y) (>= x y)) in
@@ -274,6 +267,19 @@ struct CVC4_PUBLIC Options {
    */
   bool arithRewriteEqSetByUser;
 
+  /**
+   * Whether to do the symmetry-breaking preprocessing in UF as
+   * described by Deharbe et al. in CADE 2011 (on by default).
+   */
+  bool ufSymmetryBreaker;
+
+  /**
+   * Whether the user explicitly requested that the symmetry
+   * breaker be enabled or disabled.
+   */
+  bool ufSymmetryBreakerSetByUser;
+
+
   /** The output channel to receive notfication events for new lemmas */
   LemmaOutputChannel* lemmaOutputChannel;
   LemmaInputChannel* lemmaInputChannel;