- Added a loop to internally assert constraints that are marked as true.

- Changes how CongruenceManager reports conflicts.
- ConstraintDatabase can now detect and raise conflicts when doing unate propagation.

6 files changed, 408 insertions, 154 deletions

diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index 649e34134..14d2370ab 100644
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -7,8 +7,9 @@ namespace CVC4 {
 namespace theory {
 namespace arith {
 
-ArithCongruenceManager::ArithCongruenceManager(context::Context* c, ConstraintDatabase& cd, TNodeCallBack& setup, const ArithVarNodeMap& av2Node)
-  : d_conflict(c),
+ArithCongruenceManager::ArithCongruenceManager(context::Context* c, ConstraintDatabase& cd, TNodeCallBack& setup, const ArithVarNodeMap& av2Node, NodeCallBack& raiseConflict)
+  : d_inConflict(c),
+    d_raiseConflict(raiseConflict),
     d_notify(*this),
     d_keepAlive(c),
     d_propagatations(c),
@@ -112,7 +113,7 @@ bool ArithCongruenceManager::propagate(TNode x){
       ++(d_statistics.d_conflicts);
 
       Node conf = flattenAnd(explainInternal(x));
-      d_conflict.set(conf);
+      raiseConflict(conf);
       Debug("arith::congruenceManager") << "rewritten to false "<<x<<" with explanation "<< conf << std::endl;
       return false;
     }
@@ -141,7 +142,7 @@ bool ArithCongruenceManager::propagate(TNode x){
     Node final = flattenAnd(conf);
 
     ++(d_statistics.d_conflicts);
-    d_conflict.set(final);
+    raiseConflict(final);
     Debug("arith::congruenceManager") << "congruenceManager found a conflict " << final << std::endl;
     return false;
   }
diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index 63a370f9a..1864bc89e 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -25,7 +25,8 @@ namespace arith {
 
 class ArithCongruenceManager {
 private:
-  context::CDMaybe<Node> d_conflict;
+  context::CDRaised d_inConflict;
+  NodeCallBack& d_raiseConflict;
 
   /**
    * The set of ArithVars equivalent to a pair of terms.
@@ -101,17 +102,18 @@ private:
 
   eq::EqualityEngine d_ee;
 
+  void raiseConflict(Node conflict){
+    Assert(!inConflict());
+    Debug("arith::conflict") << "difference manager conflict   " << conflict << std::endl;
+    d_inConflict.raise();
+    d_raiseConflict(conflict);
+  }
 public:
 
   bool inConflict() const{
-    return d_conflict.isSet();
+    return d_inConflict.isRaised();
   };
 
-  Node conflict() const{
-    Assert(inConflict());
-    return d_conflict.get();
-  }
-
   bool hasMorePropagations() const {
     return !d_propagatations.empty();
   }
@@ -182,7 +184,7 @@ private:
 
 public:
 
-  ArithCongruenceManager(context::Context* satContext, ConstraintDatabase&, TNodeCallBack&, const ArithVarNodeMap&);
+  ArithCongruenceManager(context::Context* satContext, ConstraintDatabase&, TNodeCallBack& setLiteral, const ArithVarNodeMap&, NodeCallBack& raiseConflict);
 
   Node explain(TNode literal);
   void explain(TNode lit, NodeBuilder<>& out);
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index d451e9597..bedb91756 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -448,7 +448,7 @@ Constraint ConstraintValue::makeNegation(ArithVar v, ConstraintType t, const Del
   }
 }
 
-ConstraintDatabase::ConstraintDatabase(context::Context* satContext, context::Context* userContext, const ArithVarNodeMap& av2nodeMap, ArithCongruenceManager& cm)
+ConstraintDatabase::ConstraintDatabase(context::Context* satContext, context::Context* userContext, const ArithVarNodeMap& av2nodeMap, ArithCongruenceManager& cm, NodeCallBack& raiseConflict)
   : d_varDatabases(),
     d_toPropagate(satContext),
     d_proofs(satContext, false),
@@ -456,7 +456,8 @@ ConstraintDatabase::ConstraintDatabase(context::Context* satContext, context::Co
     d_av2nodeMap(av2nodeMap),
     d_congruenceManager(cm),
     d_satContext(satContext),
-    d_satAllocationLevel(d_satContext->getLevel())
+    d_satAllocationLevel(d_satContext->getLevel()),
+    d_raiseConflict(raiseConflict)
 {
   d_selfExplainingProof = d_proofs.size();
   d_proofs.push_back(NullConstraint);
@@ -1153,6 +1154,20 @@ void ConstraintDatabase::outputUnateInequalityLemmas(std::vector<Node>& lemmas)
   }
 }
 
+void ConstraintDatabase::raiseUnateConflict(Constraint ant, Constraint cons){
+  Assert(ant->hasProof());
+  Constraint negCons = cons->getNegation();
+  Assert(negCons->hasProof());
+
+  Debug("arith::unate::conf") << ant << "implies " << cons << endl;
+  Debug("arith::unate::conf") << negCons << " is true." << endl;
+
+
+  Node conf = ConstraintValue::explainConflict(ant, negCons);
+  Debug("arith::unate::conf") << conf << std::endl;
+  d_raiseConflict(conf);
+}
+
 void ConstraintDatabase::unatePropLowerBound(Constraint curr, Constraint prev){
   Debug("arith::unate") << "unatePropLowerBound " << curr << " " << prev << endl;
   Assert(curr != prev);
@@ -1186,17 +1201,25 @@ void ConstraintDatabase::unatePropLowerBound(Constraint curr, Constraint prev){
     //These should all be handled by propagating the LowerBounds!
     if(vc.hasLowerBound()){
       Constraint lb = vc.getLowerBound();
-      if(!lb->isTrue()){
+      if(lb->negationHasProof()){
+        raiseUnateConflict(curr, lb);
+        return;
+      }else 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()){
+      if(dis->negationHasProof()){
+        raiseUnateConflict(curr, dis);
+        return;
+      }else if(!dis->isTrue()){
         ++d_statistics.d_unatePropagateImplications;
         Debug("arith::unate") << "unatePropLowerBound " << curr << " implies " << dis << endl;
+
         dis->impliedBy(curr);
       }
     }
@@ -1229,7 +1252,10 @@ void ConstraintDatabase::unatePropUpperBound(Constraint curr, Constraint prev){
     //These should all be handled by propagating the UpperBounds!
     if(vc.hasUpperBound()){
       Constraint ub = vc.getUpperBound();
-      if(!ub->isTrue()){
+      if(ub->negationHasProof()){
+        raiseUnateConflict(curr, ub);
+        return;
+      }else if(!ub->isTrue()){
         ++d_statistics.d_unatePropagateImplications;
         Debug("arith::unate") << "unatePropUpperBound " << curr << " implies " << ub << endl;
         ub->impliedBy(curr);
@@ -1237,9 +1263,13 @@ void ConstraintDatabase::unatePropUpperBound(Constraint curr, Constraint prev){
     }
     if(vc.hasDisequality()){
       Constraint dis = vc.getDisequality();
-      if(!dis->isTrue()){
+      if(dis->negationHasProof()){
+        raiseUnateConflict(curr, dis);
+        return;
+      }else if(!dis->isTrue()){
         Debug("arith::unate") << "unatePropUpperBound " << curr << " implies " << dis << endl;
         ++d_statistics.d_unatePropagateImplications;
+
         dis->impliedBy(curr);
       }
     }
@@ -1279,7 +1309,10 @@ void ConstraintDatabase::unatePropEquality(Constraint curr, Constraint prevLB, C
     //These should all be handled by propagating the LowerBounds!
     if(vc.hasLowerBound()){
       Constraint lb = vc.getLowerBound();
-      if(!lb->isTrue()){
+      if(lb->negationHasProof()){
+        raiseUnateConflict(curr, lb);
+        return;
+      }else if(!lb->isTrue()){
         ++d_statistics.d_unatePropagateImplications;
         Debug("arith::unate") << "unatePropUpperBound " << curr << " implies " << lb << endl;
         lb->impliedBy(curr);
@@ -1287,9 +1320,13 @@ void ConstraintDatabase::unatePropEquality(Constraint curr, Constraint prevLB, C
     }
     if(vc.hasDisequality()){
       Constraint dis = vc.getDisequality();
-      if(!dis->isTrue()){
+      if(dis->negationHasProof()){
+        raiseUnateConflict(curr, dis);
+        return;
+      }else if(!dis->isTrue()){
         ++d_statistics.d_unatePropagateImplications;
         Debug("arith::unate") << "unatePropUpperBound " << curr << " implies " << dis << endl;
+
         dis->impliedBy(curr);
       }
     }
@@ -1307,15 +1344,22 @@ void ConstraintDatabase::unatePropEquality(Constraint curr, Constraint prevLB, C
     //These should all be handled by propagating the UpperBounds!
     if(vc.hasUpperBound()){
       Constraint ub = vc.getUpperBound();
-      if(!ub->isTrue()){
+      if(ub->negationHasProof()){
+        raiseUnateConflict(curr, ub);
+        return;
+      }else 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()){
+      if(dis->negationHasProof()){
+        raiseUnateConflict(curr, dis);
+        return;
+      }else if(!dis->isTrue()){
         ++d_statistics.d_unatePropagateImplications;
         Debug("arith::unate") << "unateProp " << curr << " implies " << dis << endl;
         dis->impliedBy(curr);
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index 5b49dd54d..dcc3bf8bb 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -762,6 +762,8 @@ private:
   const context::Context * const d_satContext;
   const int d_satAllocationLevel;
 
+  NodeCallBack& d_raiseConflict;
+
   friend class ConstraintValue;
 
 public:
@@ -769,12 +771,13 @@ public:
   ConstraintDatabase( context::Context* satContext,
                       context::Context* userContext,
                       const ArithVarNodeMap& av2nodeMap,
-                      ArithCongruenceManager& dm);
+                      ArithCongruenceManager& dm,
+                      NodeCallBack& conflictCallBack);
 
   ~ConstraintDatabase();
 
+  /** Adds a literal to the database. */
   Constraint addLiteral(TNode lit);
-  //Constraint addAtom(TNode atom);
 
   /**
    * If hasLiteral() is true, returns the constraint.
@@ -852,6 +855,8 @@ public:
   void unatePropEquality(Constraint curr, Constraint prevLB, Constraint prevUB);
 
 private:
+  void raiseUnateConflict(Constraint ant, Constraint cons);
+
   class Statistics {
   public:
     IntStat d_unatePropagateCalls;
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index be24e43ba..faf0e3563 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -61,6 +61,8 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputCha
   d_nextIntegerCheckVar(0),
   d_constantIntegerVariables(c),
   d_diseqQueue(c, false),
+  d_currentPropagationList(),
+  d_learnedBounds(c),
   d_partialModel(c),
   d_tableau(),
   d_linEq(d_partialModel, d_tableau, d_basicVarModelUpdateCallBack),
@@ -71,10 +73,10 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputCha
   d_tableauResetDensity(1.6),
   d_tableauResetPeriod(10),
   d_conflicts(c),
-  d_conflictCallBack(d_conflicts),
-  d_congruenceManager(c, d_constraintDatabase, d_setupLiteralCallback, d_arithvarNodeMap),
-  d_simplex(d_linEq, d_conflictCallBack),
-  d_constraintDatabase(c, u, d_arithvarNodeMap, d_congruenceManager),
+  d_raiseConflict(d_conflicts),
+  d_congruenceManager(c, d_constraintDatabase, d_setupLiteralCallback, d_arithvarNodeMap, d_raiseConflict),
+  d_simplex(d_linEq, d_raiseConflict),
+  d_constraintDatabase(c, u, d_arithvarNodeMap, d_congruenceManager, d_raiseConflict),
   d_basicVarModelUpdateCallBack(d_simplex),
   d_DELTA_ZERO(0),
   d_statistics()
@@ -181,7 +183,7 @@ void TheoryArith::zeroDifferenceDetected(ArithVar x){
 }
 
 /* procedure AssertLower( x_i >= c_i ) */
-Node TheoryArith::AssertLower(Constraint constraint){
+bool TheoryArith::AssertLower(Constraint constraint){
   Assert(constraint != NullConstraint);
   Assert(constraint->isLowerBound());
 
@@ -194,7 +196,7 @@ Node TheoryArith::AssertLower(Constraint constraint){
 
   //TODO Relax to less than?
   if(d_partialModel.lessThanLowerBound(x_i, c_i)){
-    return Node::null();
+    return false; //sat
   }
 
   int cmpToUB = d_partialModel.cmpToUpperBound(x_i, c_i);
@@ -203,7 +205,8 @@ Node TheoryArith::AssertLower(Constraint constraint){
     Node conflict = ConstraintValue::explainConflict(ubc, constraint);
     Debug("arith") << "AssertLower conflict " << conflict << endl;
     ++(d_statistics.d_statAssertLowerConflicts);
-    return conflict;
+    d_raiseConflict(conflict);
+    return true;
   }else if(cmpToUB == 0){
     if(isInteger(x_i)){
       d_constantIntegerVariables.push_back(x_i);
@@ -229,10 +232,33 @@ Node TheoryArith::AssertLower(Constraint constraint){
 
         ++(d_statistics.d_statDisequalityConflicts);
         Debug("eq") << " assert lower conflict " << conflict << endl;
-        return conflict;
+        d_raiseConflict(conflict);
+        return true;
       }else if(!eq->isTrue()){
         Debug("eq") << "lb == ub, propagate eq" << eq << endl;
         eq->impliedBy(constraint, d_partialModel.getUpperBoundConstraint(x_i));
+        // do not need to add to d_learnedBounds
+      }
+    }
+  }else{
+    Assert(cmpToUB < 0);
+    const ValueCollection& vc = constraint->getValueCollection();
+    if(vc.hasDisequality() && vc.hasUpperBound()){
+      const Constraint diseq = vc.getDisequality();
+      if(diseq->isTrue()){
+        const Constraint ub = vc.getUpperBound();
+        if(ub->hasProof()){
+          Node conflict = ConstraintValue::explainConflict(diseq, ub, constraint);
+          Debug("eq") << " assert upper conflict " << conflict << endl;
+          d_raiseConflict(conflict);
+          return true;
+        }else if(!ub->negationHasProof()){
+          Constraint negUb = ub->getNegation();
+          negUb->impliedBy(constraint, diseq);
+          //if(!negUb->canBePropagated()){
+          d_learnedBounds.push_back(negUb);
+            //}//otherwise let this be propagated/asserted later
+        }
       }
     }
   }
@@ -263,11 +289,11 @@ Node TheoryArith::AssertLower(Constraint constraint){
 
   if(Debug.isOn("model")) { d_partialModel.printModel(x_i); }
 
-  return Node::null();
+  return false; //sat
 }
 
 /* procedure AssertUpper( x_i <= c_i) */
-Node TheoryArith::AssertUpper(Constraint constraint){
+bool TheoryArith::AssertUpper(Constraint constraint){
   ArithVar x_i = constraint->getVariable();
   const DeltaRational& c_i = constraint->getValue();
 
@@ -283,7 +309,7 @@ Node TheoryArith::AssertUpper(Constraint constraint){
   Debug("arith") << "AssertUpper(" << x_i << " " << c_i << ")"<< std::endl;
 
   if(d_partialModel.greaterThanUpperBound(x_i, c_i) ){ // \upperbound(x_i) <= c_i
-    return Node::null(); //sat
+    return false; //sat
   }
 
   // cmpToLb =  \lowerbound(x_i).cmp(c_i)
@@ -293,7 +319,8 @@ Node TheoryArith::AssertUpper(Constraint constraint){
     Node conflict =  ConstraintValue::explainConflict(lbc, constraint);
     Debug("arith") << "AssertUpper conflict " << conflict << endl;
     ++(d_statistics.d_statAssertUpperConflicts);
-    return conflict;
+    d_raiseConflict(conflict);
+    return true;
   }else if(cmpToLB == 0){ // \lowerBound(x_i) == \upperbound(x_i)
     if(isInteger(x_i)){
       d_constantIntegerVariables.push_back(x_i);
@@ -315,13 +342,34 @@ Node TheoryArith::AssertUpper(Constraint constraint){
       if(diseq->isTrue()){
         Node conflict = ConstraintValue::explainConflict(diseq, lb, constraint);
         Debug("eq") << " assert upper conflict " << conflict << endl;
-        return conflict;
+        d_raiseConflict(conflict);
+        return true;
       }else if(!eq->isTrue()){
         Debug("eq") << "lb == ub, propagate eq" << eq << endl;
         eq->impliedBy(constraint, d_partialModel.getLowerBoundConstraint(x_i));
+        //do not bother to add to d_learnedBounds
+      }
+    }
+  }else if(cmpToLB > 0){
+    const ValueCollection& vc = constraint->getValueCollection();
+    if(vc.hasDisequality() && vc.hasLowerBound()){
+      const Constraint diseq = vc.getDisequality();
+      if(diseq->isTrue()){
+        const Constraint lb = vc.getLowerBound();
+        if(lb->hasProof()){
+          Node conflict = ConstraintValue::explainConflict(diseq, lb, constraint);
+          Debug("eq") << " assert upper conflict " << conflict << endl;
+          d_raiseConflict(conflict);
+          return true;
+        }else if(!lb->negationHasProof()){
+          Constraint negLb = lb->getNegation();
+          negLb->impliedBy(constraint, diseq);
+          //if(!negLb->canBePropagated()){
+          d_learnedBounds.push_back(negLb);
+          //}//otherwise let this be propagated/asserted later
+        }
       }
     }
-
   }
 
   d_currentPropagationList.push_back(constraint);
@@ -351,12 +399,12 @@ Node TheoryArith::AssertUpper(Constraint constraint){
 
   if(Debug.isOn("model")) { d_partialModel.printModel(x_i); }
 
-  return Node::null();
+  return false; //sat
 }
 
 
 /* procedure AssertEquality( x_i == c_i ) */
-Node TheoryArith::AssertEquality(Constraint constraint){
+bool TheoryArith::AssertEquality(Constraint constraint){
   AssertArgument(constraint != NullConstraint,
                  "AssertUpper() called on a NullConstraint.");
 
@@ -374,21 +422,23 @@ Node TheoryArith::AssertEquality(Constraint constraint){
   // u_i <= c_i <= l_i
   // This can happen if both c_i <= x_i and x_i <= c_i are in the system.
   if(cmpToUB >= 0 && cmpToLB <= 0){
-    return Node::null(); //sat
+    return false; //sat
   }
 
   if(cmpToUB > 0){
     Constraint ubc = d_partialModel.getUpperBoundConstraint(x_i);
     Node conflict = ConstraintValue::explainConflict(ubc, constraint);
     Debug("arith") << "AssertEquality conflicts with upper bound " << conflict << endl;
-    return conflict;
+    d_raiseConflict(conflict);
+    return true;
   }
 
   if(cmpToLB < 0){
     Constraint lbc = d_partialModel.getLowerBoundConstraint(x_i);
     Node conflict = ConstraintValue::explainConflict(lbc, constraint);
     Debug("arith") << "AssertEquality conflicts with lower bound" << conflict << endl;
-    return conflict;
+    d_raiseConflict(conflict);
+    return true;
   }
 
   Assert(cmpToUB <= 0);
@@ -431,12 +481,12 @@ Node TheoryArith::AssertEquality(Constraint constraint){
   }else{
     d_simplex.updateBasic(x_i);
   }
-  return Node::null();
+  return false;
 }
 
 
 /* procedure AssertDisequality( x_i != c_i ) */
-Node TheoryArith::AssertDisequality(Constraint constraint){
+bool TheoryArith::AssertDisequality(Constraint constraint){
 
   AssertArgument(constraint != NullConstraint,
                  "AssertUpper() called on a NullConstraint.");
@@ -457,7 +507,7 @@ Node TheoryArith::AssertDisequality(Constraint constraint){
 
   if(constraint->isSplit()){
     Debug("eq") << "skipping already split " << constraint << endl;
-    return Node::null();
+    return false;
   }
 
   const ValueCollection& vc = constraint->getValueCollection();
@@ -468,18 +518,25 @@ Node TheoryArith::AssertDisequality(Constraint constraint){
       //in conflict
       Debug("eq") << "explaining" << endl;
       ++(d_statistics.d_statDisequalityConflicts);
-      return ConstraintValue::explainConflict(constraint, lb, ub);
+      Node conflict = ConstraintValue::explainConflict(constraint, lb, ub);
+      d_raiseConflict(conflict);
+      return true;
+
     }else if(lb->isTrue()){
       Debug("eq") << "propagate UpperBound " << constraint << lb << ub << endl;
       const Constraint negUb = ub->getNegation();
       if(!negUb->isTrue()){
         negUb->impliedBy(constraint, lb);
+        d_learnedBounds.push_back(negUb);
       }
     }else if(ub->isTrue()){
       Debug("eq") << "propagate LowerBound " << constraint << lb << ub << endl;
       const Constraint negLb = lb->getNegation();
       if(!negLb->isTrue()){
         negLb->impliedBy(constraint, ub);
+        //if(!negLb->canBePropagated()){
+        d_learnedBounds.push_back(negLb);
+        //}
       }
     }
   }
@@ -488,7 +545,7 @@ Node TheoryArith::AssertDisequality(Constraint constraint){
   if(c_i == d_partialModel.getAssignment(x_i)){
     Debug("eq") << "lemma now! " << constraint << endl;
     d_out->lemma(constraint->split());
-    return Node::null();
+    return false;
   }else if(d_partialModel.strictlyLessThanLowerBound(x_i, c_i)){
     Debug("eq") << "can drop as less than lb" << constraint << endl;
   }else if(d_partialModel.strictlyGreaterThanUpperBound(x_i, c_i)){
@@ -497,7 +554,7 @@ Node TheoryArith::AssertDisequality(Constraint constraint){
     Debug("eq") << "push back" << constraint << endl;
     d_diseqQueue.push(constraint);
   }
-  return Node::null();
+  return false;
 
 }
 
@@ -1006,23 +1063,48 @@ Node TheoryArith::callDioSolver(){
   return d_diosolver.processEquationsForConflict();
 }
 
-Node TheoryArith::assertionCases(TNode assertion){
-  Constraint constraint = d_constraintDatabase.lookup(assertion);
+Constraint TheoryArith::constraintFromFactQueue(){
+  Assert(!done());
+  TNode assertion = get();
 
   Kind simpleKind = Comparison::comparisonKind(assertion);
-  Assert(simpleKind != UNDEFINED_KIND);
-  Assert(constraint != NullConstraint ||
-         simpleKind == EQUAL ||
-         simpleKind == DISTINCT );
-  if(simpleKind == EQUAL || simpleKind == DISTINCT){
+  Constraint constraint = d_constraintDatabase.lookup(assertion);
+  if(constraint == NullConstraint){
+    Assert(simpleKind == EQUAL || simpleKind == DISTINCT );
+    bool isDistinct = simpleKind == DISTINCT;
     Node eq = (simpleKind == DISTINCT) ? assertion[0] : assertion;
-
-    if(!isSetup(eq)){
-      //The previous code was equivalent to:
-      setupAtom(eq);
-      constraint = d_constraintDatabase.lookup(assertion);
+    Assert(!isSetup(eq));
+    Node reEq = Rewriter::rewrite(eq);
+    if(reEq.getKind() == CONST_BOOLEAN){
+      if(reEq.getConst<bool>() != isDistinct){
+        Assert((reEq.getConst<bool>() && isDistinct) ||
+               (!reEq.getConst<bool>() && !isDistinct));
+        d_raiseConflict(assertion);
+      }
+      return NullConstraint;
     }
-  }
+    Assert(reEq.getKind() != CONST_BOOLEAN);
+    if(!isSetup(reEq)){
+      setupAtom(reEq);
+    }
+    Node reAssertion = isDistinct ? reEq.notNode() : reEq;
+    constraint = d_constraintDatabase.lookup(reAssertion);
+  }
+
+  // Kind simpleKind = Comparison::comparisonKind(assertion);
+  // Assert(simpleKind != UNDEFINED_KIND);
+  // Assert(constraint != NullConstraint ||
+  //        simpleKind == EQUAL ||
+  //        simpleKind == DISTINCT );
+  // if(simpleKind == EQUAL || simpleKind == DISTINCT){
+  //   Node eq = (simpleKind == DISTINCT) ? assertion[0] : assertion;
+
+  //   if(!isSetup(eq)){
+  //     //The previous code was equivalent to:
+  //     setupAtom(eq);
+  //     constraint = d_constraintDatabase.lookup(assertion);
+  //   }
+  // }
   Assert(constraint != NullConstraint);
 
   if(constraint->negationHasProof()){
@@ -1031,8 +1113,6 @@ Node TheoryArith::assertionCases(TNode assertion){
       if(Debug.isOn("whytheoryenginewhy")){
         debugPrintFacts();
       }
-//      Warning() << "arith: Theory engine is sending me both a literal and its negation?"
-//                << "BOOOOOOOOOOOOOOOOOOOOOO!!!!"<< endl;
     }
     Debug("arith::eq") << constraint << endl;
     Debug("arith::eq") << negation << endl;
@@ -1042,94 +1122,202 @@ Node TheoryArith::assertionCases(TNode assertion){
     negation->explainForConflict(nb);
     Node conflict = nb;
     Debug("arith::eq") << "conflict" << conflict << endl;
-    return conflict;
+    d_raiseConflict(conflict);
+    return NullConstraint;
   }
   Assert(!constraint->negationHasProof());
 
   if(constraint->assertedToTheTheory()){
     //Do nothing
-    return Node::null();
-  }
-  Assert(!constraint->assertedToTheTheory());
-  constraint->setAssertedToTheTheory();
-
-  ArithVar x_i = constraint->getVariable();
-  //DeltaRational c_i = determineRightConstant(assertion, simpleKind);
-
-  //Assert(constraint->getVariable() == determineLeftVariable(assertion, simpleKind));
-  //Assert(constraint->getValue() == determineRightConstant(assertion, simpleKind));
-  Assert(!constraint->hasLiteral() || constraint->getLiteral() == assertion);
-
-  Debug("arith::assertions")  << "arith assertion @" << getSatContext()->getLevel()
-                              <<"(" << assertion
-                              << " \\-> "
-    //<< determineLeftVariable(assertion, simpleKind)
-                              <<" "<< simpleKind <<" "
-    //<< determineRightConstant(assertion, simpleKind)
-                              << ")" << std::endl;
-
+    return NullConstraint;
+  }else{
+    Debug("arith::constraint") << "arith constraint " << constraint << std::endl;
+    constraint->setAssertedToTheTheory();
 
-  Debug("arith::constraint") << "arith constraint " << constraint << std::endl;
+    if(!constraint->hasProof()){
+      Debug("arith::constraint") << "marking as constraint as self explaining " << endl;
+      constraint->selfExplaining();
+    }else{
+      Debug("arith::constraint") << "already has proof: " << constraint->explainForConflict() << endl;
+    }
 
-  if(!constraint->hasProof()){
-    Debug("arith::constraint") << "marking as constraint as self explaining " << endl;
-    constraint->selfExplaining();
-  }else{
-    Debug("arith::constraint") << "already has proof: " << constraint->explainForConflict() << endl;
+    return constraint;
   }
+}
+
+bool TheoryArith::assertionCases(Constraint constraint){
+  Assert(constraint->hasProof());
+  Assert(!constraint->negationHasProof());
 
-  Assert(!isInteger(x_i) ||
-         simpleKind == EQUAL ||
-         simpleKind == DISTINCT ||
-         simpleKind == GEQ ||
-         simpleKind == LT);
+  ArithVar x_i = constraint->getVariable();
 
   switch(constraint->getType()){
   case UpperBound:
-    if(simpleKind == LT && isInteger(x_i)){
+    if(isInteger(x_i) && constraint->isStrictUpperBound()){
       Constraint floorConstraint = constraint->getFloor();
       if(!floorConstraint->isTrue()){
         if(floorConstraint->negationHasProof()){
-          return ConstraintValue::explainConflict(constraint, floorConstraint->getNegation());
+          Node conf = ConstraintValue::explainConflict(constraint, floorConstraint->getNegation());
+          d_raiseConflict(conf);
+          return true;
         }else{
           floorConstraint->impliedBy(constraint);
+          // Do not need to add to d_learnedBounds
         }
       }
-      //c_i = DeltaRational(c_i.floor());
-      //return AssertUpper(x_i, c_i, assertion, floorConstraint);
       return AssertUpper(floorConstraint);
     }else{
       return AssertUpper(constraint);
     }
-    //return AssertUpper(x_i, c_i, assertion, constraint);
   case LowerBound:
-    if(simpleKind == LT && isInteger(x_i)){
+    if(isInteger(x_i) && constraint->isStrictLowerBound()){
       Constraint ceilingConstraint = constraint->getCeiling();
       if(!ceilingConstraint->isTrue()){
         if(ceilingConstraint->negationHasProof()){
-
-          return ConstraintValue::explainConflict(constraint, ceilingConstraint->getNegation());
+          Node conf = ConstraintValue::explainConflict(constraint, ceilingConstraint->getNegation());
+          d_raiseConflict(conf);
+          return true;
         }
         ceilingConstraint->impliedBy(constraint);
+        // Do not need to add to learnedBounds
       }
-      //c_i = DeltaRational(c_i.ceiling());
-      //return AssertLower(x_i, c_i, assertion, ceilingConstraint);
       return AssertLower(ceilingConstraint);
     }else{
       return AssertLower(constraint);
     }
-    //return AssertLower(x_i, c_i, assertion, constraint);
   case Equality:
     return AssertEquality(constraint);
-    //return AssertEquality(x_i, c_i, assertion, constraint);
   case Disequality:
     return AssertDisequality(constraint);
-    //return AssertDisequality(x_i, c_i, assertion, constraint);
   default:
     Unreachable();
-    return Node::null();
+    return false;
   }
 }
+// Node TheoryArith::assertionCases(TNode assertion){
+//   Constraint constraint = d_constraintDatabase.lookup(assertion);
+
+//   Kind simpleKind = Comparison::comparisonKind(assertion);
+//   Assert(simpleKind != UNDEFINED_KIND);
+//   Assert(constraint != NullConstraint ||
+//          simpleKind == EQUAL ||
+//          simpleKind == DISTINCT );
+//   if(simpleKind == EQUAL || simpleKind == DISTINCT){
+//     Node eq = (simpleKind == DISTINCT) ? assertion[0] : assertion;
+
+//     if(!isSetup(eq)){
+//       //The previous code was equivalent to:
+//       setupAtom(eq);
+//       constraint = d_constraintDatabase.lookup(assertion);
+//     }
+//   }
+//   Assert(constraint != NullConstraint);
+
+//   if(constraint->negationHasProof()){
+//     Constraint negation = constraint->getNegation();
+//     if(negation->isSelfExplaining()){
+//       if(Debug.isOn("whytheoryenginewhy")){
+//         debugPrintFacts();
+//       }
+// //      Warning() << "arith: Theory engine is sending me both a literal and its negation?"
+// //                << "BOOOOOOOOOOOOOOOOOOOOOO!!!!"<< endl;
+//     }
+//     Debug("arith::eq") << constraint << endl;
+//     Debug("arith::eq") << negation << endl;
+
+//     NodeBuilder<> nb(kind::AND);
+//     nb << assertion;
+//     negation->explainForConflict(nb);
+//     Node conflict = nb;
+//     Debug("arith::eq") << "conflict" << conflict << endl;
+//     return conflict;
+//   }
+//   Assert(!constraint->negationHasProof());
+
+//   if(constraint->assertedToTheTheory()){
+//     //Do nothing
+//     return Node::null();
+//   }
+//   Assert(!constraint->assertedToTheTheory());
+//   constraint->setAssertedToTheTheory();
+
+//   ArithVar x_i = constraint->getVariable();
+//   //DeltaRational c_i = determineRightConstant(assertion, simpleKind);
+
+//   //Assert(constraint->getVariable() == determineLeftVariable(assertion, simpleKind));
+//   //Assert(constraint->getValue() == determineRightConstant(assertion, simpleKind));
+//   Assert(!constraint->hasLiteral() || constraint->getLiteral() == assertion);
+
+//   Debug("arith::assertions")  << "arith assertion @" << getSatContext()->getLevel()
+//                               <<"(" << assertion
+//                               << " \\-> "
+//     //<< determineLeftVariable(assertion, simpleKind)
+//                               <<" "<< simpleKind <<" "
+//     //<< determineRightConstant(assertion, simpleKind)
+//                               << ")" << std::endl;
+
+
+//   Debug("arith::constraint") << "arith constraint " << constraint << std::endl;
+
+//   if(!constraint->hasProof()){
+//     Debug("arith::constraint") << "marking as constraint as self explaining " << endl;
+//     constraint->selfExplaining();
+//   }else{
+//     Debug("arith::constraint") << "already has proof: " << constraint->explainForConflict() << endl;
+//   }
+
+//   Assert(!isInteger(x_i) ||
+//          simpleKind == EQUAL ||
+//          simpleKind == DISTINCT ||
+//          simpleKind == GEQ ||
+//          simpleKind == LT);
+
+//   switch(constraint->getType()){
+//   case UpperBound:
+//     if(simpleKind == LT && isInteger(x_i)){
+//       Constraint floorConstraint = constraint->getFloor();
+//       if(!floorConstraint->isTrue()){
+//         if(floorConstraint->negationHasProof()){
+//           return ConstraintValue::explainConflict(constraint, floorConstraint->getNegation());
+//         }else{
+//           floorConstraint->impliedBy(constraint);
+//         }
+//       }
+//       //c_i = DeltaRational(c_i.floor());
+//       //return AssertUpper(x_i, c_i, assertion, floorConstraint);
+//       return AssertUpper(floorConstraint);
+//     }else{
+//       return AssertUpper(constraint);
+//     }
+//     //return AssertUpper(x_i, c_i, assertion, constraint);
+//   case LowerBound:
+//     if(simpleKind == LT && isInteger(x_i)){
+//       Constraint ceilingConstraint = constraint->getCeiling();
+//       if(!ceilingConstraint->isTrue()){
+//         if(ceilingConstraint->negationHasProof()){
+
+//           return ConstraintValue::explainConflict(constraint, ceilingConstraint->getNegation());
+//         }
+//         ceilingConstraint->impliedBy(constraint);
+//       }
+//       //c_i = DeltaRational(c_i.ceiling());
+//       //return AssertLower(x_i, c_i, assertion, ceilingConstraint);
+//       return AssertLower(ceilingConstraint);
+//     }else{
+//       return AssertLower(constraint);
+//     }
+//     //return AssertLower(x_i, c_i, assertion, constraint);
+//   case Equality:
+//     return AssertEquality(constraint);
+//     //return AssertEquality(x_i, c_i, assertion, constraint);
+//   case Disequality:
+//     return AssertDisequality(constraint);
+//     //return AssertDisequality(x_i, c_i, assertion, constraint);
+//   default:
+//     Unreachable();
+//     return Node::null();
+//   }
+// }
 
 /**
  * Looks for the next integer variable without an integer assignment in a round robin fashion.
@@ -1154,6 +1342,15 @@ bool TheoryArith::hasIntegerModel(){
   return true;
 }
 
+/** Outputs conflicts to the output channel. */
+void TheoryArith::outputConflicts(){
+  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);
+  }
+}
 
 void TheoryArith::check(Effort effortLevel){
   Assert(d_currentPropagationList.empty());
@@ -1161,22 +1358,29 @@ void TheoryArith::check(Effort effortLevel){
 
   d_hasDoneWorkSinceCut = d_hasDoneWorkSinceCut || !done();
   while(!done()){
-
-    Node assertion = get();
-    Node possibleConflict = assertionCases(assertion);
-
-    if(!possibleConflict.isNull()){
+    Constraint curr = constraintFromFactQueue();
+    if(curr != NullConstraint){
+      bool res = assertionCases(curr);
+      Assert(!res || inConflict());
+    }
+    if(inConflict()){
       revertOutOfConflict();
-
-      Debug("arith::conflict") << "conflict   " << possibleConflict << endl;
-      d_out->conflict(possibleConflict);
+      outputConflicts();
       return;
     }
-    if(d_congruenceManager.inConflict()){
-      Node c = d_congruenceManager.conflict();
+  }
+  while(!d_learnedBounds.empty()){
+    // we may attempt some constraints twice.  this is okay!
+    Constraint curr = d_learnedBounds.front();
+    d_learnedBounds.pop();
+    Debug("arith::learned") << curr << endl;
+
+    bool res = assertionCases(curr);
+    Assert(!res || inConflict());
+
+    if(inConflict()){
       revertOutOfConflict();
-      Debug("arith::conflict") << "difference manager conflict   " << c << endl;
-      d_out->conflict(c);
+      outputConflicts();
       return;
     }
   }
@@ -1191,13 +1395,7 @@ void TheoryArith::check(Effort effortLevel){
   bool foundConflict = d_simplex.findModel();
   if(foundConflict){
     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);
-    }
+    outputConflicts();
     emmittedConflictOrSplit = true;
   }else{
     d_partialModel.commitAssignmentChanges();
@@ -1208,7 +1406,7 @@ void TheoryArith::check(Effort effortLevel){
       Options::current()->arithPropagationMode == Options::BOTH_PROP)){
     TimerStat::CodeTimer codeTimer(d_statistics.d_newPropTime);
 
-    while(!d_currentPropagationList.empty()){
+    while(!d_currentPropagationList.empty()  && !inConflict()){
       Constraint curr = d_currentPropagationList.front();
       d_currentPropagationList.pop_front();
 
@@ -1244,6 +1442,13 @@ void TheoryArith::check(Effort effortLevel){
         Unhandled(curr->getType());
       }
     }
+
+    if(inConflict()){
+      Debug("arith::unate") << "unate conflict" << endl;
+      revertOutOfConflict();
+      outputConflicts();
+      return;
+    }
   }else{
     TimerStat::CodeTimer codeTimer(d_statistics.d_newPropTime);
     d_currentPropagationList.clear();
@@ -1800,25 +2005,10 @@ bool TheoryArith::propagateCandidateBound(ArithVar basic, bool upperBound){
           Assert(bestImplied != d_partialModel.getLowerBoundConstraint(basic));
           d_linEq.propagateNonbasicsLowerBound(basic, bestImplied);
         }
+        // I think this can be skipped if canBePropagated is true
+        //d_learnedBounds.push(bestImplied);
         return true;
       }
-
-      // bool asserted = valuationIsAsserted(bestImplied);
-      // bool propagated = d_theRealPropManager.isPropagated(bestImplied);
-      // if( !asserted && !propagated){
-
-      //   NodeBuilder<> nb(kind::AND);
-      //   if(upperBound){
-      //     d_linEq.explainNonbasicsUpperBound(basic, nb);
-      //   }else{
-      //     d_linEq.explainNonbasicsLowerBound(basic, nb);
-      //   }
-      //   Node explanation = nb;
-      //   d_theRealPropManager.propagate(bestImplied, explanation, false);
-      //   return true;
-      // }else{
-      //   Debug("arith::prop") << basic << " " << asserted << " " << propagated << endl;
-      // }
     }
   }
   return false;
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 1f0120387..e23a9a943 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -184,6 +184,8 @@ private:
    */
   std::deque<Constraint> d_currentPropagationList;
 
+  context::CDQueue<Constraint> d_learnedBounds;
+
   /**
    * Manages information about the assignment and upper and lower bounds on
    * variables.
@@ -245,8 +247,17 @@ private:
     void operator()(Node n){
       d_list.push_back(n);
     }
-  };
-  PushCallBack d_conflictCallBack;
+  } d_raiseConflict;
+
+  /** Returns true iff a conflict has been raised. */
+  inline bool inConflict() const {
+    return !d_conflicts.empty();
+  }
+  /**
+   * Outputs the contents of d_conflicts onto d_out.
+   * Must be inConflict().
+   */
+  void outputConflicts();
 
 
   /**
@@ -386,10 +397,10 @@ private:
    * a node describing this conflict is returned.
    * If this new bound is not in conflict, Node::null() is returned.
    */
-  Node AssertLower(Constraint constraint);
-  Node AssertUpper(Constraint constraint);
-  Node AssertEquality(Constraint constraint);
-  Node AssertDisequality(Constraint constraint);
+  bool AssertLower(Constraint constraint);
+  bool AssertUpper(Constraint constraint);
+  bool AssertEquality(Constraint constraint);
+  bool AssertDisequality(Constraint constraint);
 
   /** Tracks the bounds that were updated in the current round. */
   DenseSet d_updatedBounds;
@@ -423,7 +434,8 @@ private:
    * Returns a conflict if one was found.
    * Returns Node::null if no conflict was found.
    */
-  Node assertionCases(TNode assertion);
+  Constraint constraintFromFactQueue();
+  bool assertionCases(Constraint c);
 
   /**
    * Returns the basic variable with the shorted row containg a non-basic variable.