This commit merges in the branch branches/arithmetic/congruence into trunk. Here are a summary of the changes:

- Adds CDMaybe and CDRaised in cdmaybe.h
- Add test for congruence over arithmetic terms and constants
- Renames DifferenceManager to CongruenceManager
- Changes a number of internal details for CongruenceManager

12 files changed, 536 insertions, 373 deletions

diff --git a/src/context/Makefile.am b/src/context/Makefile.am
index d0c2b9783..13a151ffc 100644
--- a/src/context/Makefile.am
+++ b/src/context/Makefile.am
@@ -23,5 +23,6 @@ libcontext_la_SOURCES = \
 	cdcirclist.h \
 	cdcirclist_forward.h \
 	cdvector.h \
+	cdmaybe.h \
 	stacking_map.h \
 	stacking_vector.h
diff --git a/src/context/cdmaybe.h b/src/context/cdmaybe.h
new file mode 100644
index 000000000..3c95ab126
--- /dev/null
+++ b/src/context/cdmaybe.h
@@ -0,0 +1,65 @@
+/**
+ * This implements a CDMaybe.
+ * This has either been set in the context or it has not.
+ * T must have a default constructor and support assignment.
+ */
+
+#include "cvc4_private.h"
+
+#pragma once
+
+#include "context/cdo.h"
+#include "context/context.h"
+
+namespace CVC4 {
+namespace context {
+
+class CDRaised {
+private:
+  context::CDO<bool> d_flag;
+
+public:
+ CDRaised(context::Context* c)
+ : d_flag(c, false)
+ {}
+
+
+  bool isRaised() const {
+    return d_flag.get();
+  }
+
+  void raise(){
+    Assert(!isRaised());
+    d_flag.set(true);
+  }
+
+}; /* class CDRaised */
+
+template <class T>
+class CDMaybe {
+private:
+  typedef std::pair<bool, T> BoolTPair;
+  context::CDO<BoolTPair> d_data;
+
+public:
+  CDMaybe(context::Context* c) : d_data(c, std::make_pair(false, T()))
+  {}
+
+  bool isSet() const {
+    return d_data.get().first;
+  }
+
+  void set(const T& d){
+    Assert(!isSet());
+    d_data.set(std::make_pair(true, d));
+  }
+
+  const T& get() const{
+    Assert(isSet());
+    return d_data.get().second;
+  }
+}; /* class CDMaybe<T> */
+
+}/* CVC4::context namespace */
+}/* CVC4 namespace */
+
diff --git a/src/theory/arith/Makefile.am b/src/theory/arith/Makefile.am
index b97a6f384..f9c423ef7 100644
--- a/src/theory/arith/Makefile.am
+++ b/src/theory/arith/Makefile.am
@@ -16,8 +16,8 @@ libarith_la_SOURCES = \
 	constraint_forward.h \
 	constraint.h \
 	constraint.cpp \
-	difference_manager.h \
-	difference_manager.cpp \
+	congruence_manager.h \
+	congruence_manager.cpp \
 	normal_form.h\
 	normal_form.cpp \
 	arith_utilities.h \
diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
new file mode 100644
index 000000000..201eb08e7
--- /dev/null
+++ b/src/theory/arith/congruence_manager.cpp
@@ -0,0 +1,322 @@
+#include "theory/arith/congruence_manager.h"
+#include "theory/uf/equality_engine_impl.h"
+
+#include "theory/arith/constraint.h"
+#include "theory/arith/arith_utilities.h"
+
+namespace CVC4 {
+namespace theory {
+namespace arith {
+
+ArithCongruenceManager::ArithCongruenceManager(context::Context* c, ConstraintDatabase& cd, TNodeCallBack& setup, const ArithVarNodeMap& av2Node)
+  : d_conflict(c),
+    d_notify(*this),
+    d_keepAlive(c),
+    d_propagatations(c),
+    d_explanationMap(c),
+    d_constraintDatabase(cd),
+    d_setupLiteral(setup),
+    d_av2Node(av2Node),
+    d_ee(d_notify, c, "theory::arith::ArithCongruenceManager"),
+    d_false(mkBoolNode(false))
+{}
+
+ArithCongruenceManager::Statistics::Statistics():
+  d_watchedVariables("theory::arith::congruence::watchedVariables", 0),
+  d_watchedVariableIsZero("theory::arith::congruence::watchedVariableIsZero", 0),
+  d_watchedVariableIsNotZero("theory::arith::congruence::watchedVariableIsNotZero", 0),
+  d_equalsConstantCalls("theory::arith::congruence::equalsConstantCalls", 0),
+  d_propagations("theory::arith::congruence::propagations", 0),
+  d_propagateConstraints("theory::arith::congruence::propagateConstraints", 0),
+  d_conflicts("theory::arith::congruence::conflicts", 0)
+{
+  StatisticsRegistry::registerStat(&d_watchedVariables);
+  StatisticsRegistry::registerStat(&d_watchedVariableIsZero);
+  StatisticsRegistry::registerStat(&d_watchedVariableIsNotZero);
+  StatisticsRegistry::registerStat(&d_equalsConstantCalls);
+  StatisticsRegistry::registerStat(&d_propagations);
+  StatisticsRegistry::registerStat(&d_propagateConstraints);
+  StatisticsRegistry::registerStat(&d_conflicts);
+}
+
+ArithCongruenceManager::Statistics::~Statistics(){
+  StatisticsRegistry::unregisterStat(&d_watchedVariables);
+  StatisticsRegistry::unregisterStat(&d_watchedVariableIsZero);
+  StatisticsRegistry::unregisterStat(&d_watchedVariableIsNotZero);
+  StatisticsRegistry::unregisterStat(&d_equalsConstantCalls);
+  StatisticsRegistry::unregisterStat(&d_propagations);
+  StatisticsRegistry::unregisterStat(&d_propagateConstraints);
+  StatisticsRegistry::unregisterStat(&d_conflicts);
+}
+
+void ArithCongruenceManager::watchedVariableIsZero(Constraint lb, Constraint ub){
+  Assert(lb->isLowerBound());
+  Assert(ub->isUpperBound());
+  Assert(lb->getVariable() == ub->getVariable());
+  Assert(lb->getValue().sgn() == 0);
+  Assert(ub->getValue().sgn() == 0);
+
+  ++(d_statistics.d_watchedVariableIsZero);
+
+  ArithVar s = lb->getVariable();
+  Node reason = ConstraintValue::explainConflict(lb,ub);
+
+  d_keepAlive.push_back(reason);
+  assertionToEqualityEngine(true, s, reason);
+}
+
+void ArithCongruenceManager::watchedVariableIsZero(Constraint eq){
+  Assert(eq->isEquality());
+  Assert(eq->getValue().sgn() == 0);
+
+  ++(d_statistics.d_watchedVariableIsZero);
+
+  ArithVar s = eq->getVariable();
+
+  //Explain for conflict is correct as these proofs are generated
+  //and stored eagerly
+  //These will be safe for propagation later as well
+  Node reason = eq->explainForConflict();
+
+  d_keepAlive.push_back(reason);
+  assertionToEqualityEngine(true, s, reason);
+}
+
+void ArithCongruenceManager::watchedVariableCannotBeZero(Constraint c){
+  ++(d_statistics.d_watchedVariableIsNotZero);
+
+  ArithVar s = c->getVariable();
+
+  //Explain for conflict is correct as these proofs are generated and stored eagerly
+  //These will be safe for propagation later as well
+  Node reason = c->explainForConflict();
+
+  d_keepAlive.push_back(reason);
+  assertionToEqualityEngine(false, s, reason);
+}
+
+
+bool ArithCongruenceManager::propagate(TNode x){
+  Debug("arith::congruenceManager")<< "ArithCongruenceManager::propagate("<<x<<")"<<std::endl;
+  if(inConflict()){
+    return true;
+  }
+
+  Node rewritten = Rewriter::rewrite(x);
+
+  //Need to still propagate this!
+  if(rewritten.getKind() == kind::CONST_BOOLEAN){
+    pushBack(x);
+
+    if(rewritten.getConst<bool>()){
+      return true;
+    }else{
+      ++(d_statistics.d_conflicts);
+
+      Node conf = explainInternal(x);
+      d_conflict.set(conf);
+      Debug("arith::congruenceManager") << "rewritten to false "<<x<<" with explanation "<< conf << std::endl;
+      return false;
+    }
+  }
+
+  Assert(rewritten.getKind() != kind::CONST_BOOLEAN);
+
+  Constraint c = d_constraintDatabase.lookup(rewritten);
+  if(c == NullConstraint){
+    //using setup as there may not be a corresponding congruence literal yet
+    d_setupLiteral(rewritten);
+    c = d_constraintDatabase.lookup(rewritten);
+    Assert(c != NullConstraint);
+  }
+
+  Debug("arith::congruenceManager")<< "x is "
+                                   <<  c->hasProof() << " "
+                                   << (x == rewritten) << " "
+                                   << c->canBePropagated() << " "
+                                   << c->negationHasProof() << std::endl;
+
+  if(c->negationHasProof()){
+    Node expC = explainInternal(x);
+    Node neg = c->getNegation()->explainForConflict();
+    Node conf = expC.andNode(neg);
+    Node final = flattenAnd(conf);
+
+    ++(d_statistics.d_conflicts);
+    d_conflict.set(final);
+    Debug("arith::congruenceManager") << "congruenceManager found a conflict " << final << std::endl;
+    return false;
+  }
+
+  // Cases for propagation
+  // C : c has a proof
+  // S : x == rewritten
+  // P : c can be propagated
+  //
+  // CSP
+  // 000 : propagate x, and mark C it as being explained
+  // 001 : propagate x, and propagate c after marking it as being explained
+  // 01* : propagate x, mark c but do not propagate c
+  // 10* : propagate x, do not mark c and do not propagate c
+  // 11* : drop the constraint, do not propagate x or c
+
+  if(!c->hasProof() && x != rewritten){
+    pushBack(x, rewritten);
+
+    c->setEqualityEngineProof();
+    if(c->canBePropagated() && !c->assertedToTheTheory()){
+
+      ++(d_statistics.d_propagateConstraints);
+      c->propagate();
+    }
+  }else if(!c->hasProof() && x == rewritten){
+    pushBack(x, rewritten);
+    c->setEqualityEngineProof();
+  }else if(c->hasProof() && x != rewritten){
+    pushBack(x, rewritten);
+  }else{
+    Assert(c->hasProof() && x == rewritten);
+  }
+  return true;
+}
+
+void ArithCongruenceManager::explain(TNode literal, std::vector<TNode>& assumptions) {
+  TNode lhs, rhs;
+  switch (literal.getKind()) {
+  case kind::EQUAL:
+    lhs = literal[0];
+    rhs = literal[1];
+    break;
+  case kind::NOT:
+    lhs = literal[0];
+    rhs = d_false;
+    break;
+  default:
+    Unreachable();
+  }
+  d_ee.explainEquality(lhs, rhs, assumptions);
+}
+
+void ArithCongruenceManager::enqueueIntoNB(const std::set<TNode> s, NodeBuilder<>& nb){
+  std::set<TNode>::const_iterator it = s.begin();
+  std::set<TNode>::const_iterator it_end = s.end();
+  for(; it != it_end; ++it) {
+    nb << *it;
+  }
+}
+
+Node ArithCongruenceManager::explainInternal(TNode internal){
+  std::vector<TNode> assumptions;
+  explain(internal, assumptions);
+
+  std::set<TNode> assumptionSet;
+  assumptionSet.insert(assumptions.begin(), assumptions.end());
+
+  if (assumptionSet.size() == 1) {
+    // All the same, or just one
+    return assumptions[0];
+  }else{
+    NodeBuilder<> conjunction(kind::AND);
+    enqueueIntoNB(assumptionSet, conjunction);
+    return conjunction;
+  }
+}
+Node ArithCongruenceManager::explain(TNode external){
+  Node internal = externalToInternal(external);
+  return explainInternal(internal);
+}
+
+void ArithCongruenceManager::explain(TNode external, NodeBuilder<>& out){
+  Node internal = externalToInternal(external);
+
+  std::vector<TNode> assumptions;
+  explain(internal, assumptions);
+  std::set<TNode> assumptionSet;
+  assumptionSet.insert(assumptions.begin(), assumptions.end());
+
+  enqueueIntoNB(assumptionSet, out);
+}
+
+void ArithCongruenceManager::addWatchedPair(ArithVar s, TNode x, TNode y){
+  Assert(!isWatchedVariable(s));
+
+  Debug("arith::congruenceManager")
+    << "addWatchedPair(" << s << ", " << x << ", " << y << ")" << std::endl;
+
+
+  ++(d_statistics.d_watchedVariables);
+
+  d_watchedVariables.add(s);
+
+  Node eq = x.eqNode(y);
+  d_watchedEqualities[s] = eq;
+}
+
+void ArithCongruenceManager::assertionToEqualityEngine(bool isEquality, ArithVar s, TNode reason){
+  Assert(isWatchedVariable(s));
+
+  TNode eq = d_watchedEqualities[s];
+  Assert(eq.getKind() == kind::EQUAL);
+
+  TNode x = eq[0];
+  TNode y = eq[1];
+
+  if(isEquality){
+    d_ee.addEquality(x, y, reason);
+  }else{
+    d_ee.addDisequality(x, y, reason);
+  }
+}
+
+void ArithCongruenceManager::equalsConstant(Constraint c){
+  Assert(c->isEquality());
+
+  ++(d_statistics.d_equalsConstantCalls);
+  Debug("equalsConstant") << "equals constant " << c << std::endl;
+
+  ArithVar x = c->getVariable();
+  Node xAsNode = d_av2Node.asNode(x);
+  Node asRational = mkRationalNode(c->getValue().getNoninfinitesimalPart());
+
+
+  //No guarentee this is in normal form!
+  Node eq = xAsNode.eqNode(asRational);
+  d_keepAlive.push_back(eq);
+
+  Node reason = c->explainForConflict();
+  d_keepAlive.push_back(reason);
+
+  d_ee.addEquality(xAsNode, asRational, reason);
+}
+
+void ArithCongruenceManager::equalsConstant(Constraint lb, Constraint ub){
+  Assert(lb->isLowerBound());
+  Assert(ub->isUpperBound());
+  Assert(lb->getVariable() == ub->getVariable());
+
+  ++(d_statistics.d_equalsConstantCalls);
+  Debug("equalsConstant") << "equals constant " << lb << std::endl
+                          << ub << std::endl;
+
+  ArithVar x = lb->getVariable();
+  Node reason = ConstraintValue::explainConflict(lb,ub);
+
+  Node xAsNode = d_av2Node.asNode(x);
+  Node asRational = mkRationalNode(lb->getValue().getNoninfinitesimalPart());
+
+  //No guarentee this is in normal form!
+  Node eq = xAsNode.eqNode(asRational);
+  d_keepAlive.push_back(eq);
+  d_keepAlive.push_back(reason);
+
+
+  d_ee.addEquality(xAsNode, asRational, reason);
+}
+
+void ArithCongruenceManager::addSharedTerm(Node x){
+  d_ee.addTriggerTerm(x);
+}
+
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
diff --git a/src/theory/arith/difference_manager.h b/src/theory/arith/congruence_manager.h
index 7862a6b31..e70773030 100644
--- a/src/theory/arith/difference_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -2,106 +2,70 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY__ARITH__DIFFERENCE_MANAGER_H
-#define __CVC4__THEORY__ARITH__DIFFERENCE_MANAGER_H
+#pragma once
 
 #include "theory/arith/arithvar.h"
+#include "theory/arith/arithvar_set.h"
+#include "theory/arith/arithvar_node_map.h"
 #include "theory/arith/constraint_forward.h"
+
 #include "theory/uf/equality_engine.h"
+
 #include "context/cdo.h"
 #include "context/cdlist.h"
 #include "context/context.h"
 #include "context/cdtrail_queue.h"
+#include "context/cdmaybe.h"
+
 #include "util/stats.h"
 
 namespace CVC4 {
 namespace theory {
 namespace arith {
 
-/**
- * This implements a CDMaybe.
- * This has either been set in the context or it has not.
- * T must have a default constructor and support assignment.
- */
-template <class T>
-class CDMaybe {
+class ArithCongruenceManager {
 private:
-  typedef std::pair<bool, T> BoolTPair;
-  context::CDO<BoolTPair> d_data;
-
-public:
-  CDMaybe(context::Context* c) : d_data(c, std::make_pair(false, T()))
-  {}
-
-  bool isSet() const {
-    return d_data.get().first;
-  }
-
-  void set(const T& d){
-    Assert(!isSet());
-    d_data.set(std::make_pair(true, d));
-  }
-
-  const T& get() const{
-    Assert(isSet());
-    return d_data.get().second;
-  }
-};
+  context::CDMaybe<Node> d_conflict;
 
-class DifferenceManager {
-private:
-  CDMaybe<Node> d_conflict;
-
-  struct Difference {
-    bool isSlack;
-    TNode x;
-    TNode y;
-    Difference() : isSlack(false), x(TNode::null()),  y(TNode::null()){}
-    Difference(TNode a, TNode b) : isSlack(true), x(a), y(b) {
-      Assert(x < y);
-    }
-  };
+  /**
+   * The set of ArithVars equivalent to a pair of terms.
+   * If this is 0 or cannot be 0, this can be signalled.
+   * The pair of terms for the congruence is stored in watched equalities.
+   */
+  PermissiveBackArithVarSet d_watchedVariables;
+  /** d_watchedVariables |-> (= x y) */
+  ArithVarToNodeMap d_watchedEqualities;
 
 
-  class DifferenceNotifyClass {
+  class ArithCongruenceNotify {
   private:
-    DifferenceManager& d_dm;
+    ArithCongruenceManager& d_acm;
   public:
-    DifferenceNotifyClass(DifferenceManager& dm): d_dm(dm) {}
+    ArithCongruenceNotify(ArithCongruenceManager& acm): d_acm(acm) {}
 
     bool notify(TNode propagation) {
-      Debug("arith::differences") << "DifferenceNotifyClass::notify(" << propagation << ")" << std::endl;
+      Debug("arith::congruences") << "ArithCongruenceNotify::notify(" << propagation << ")" << std::endl;
       // Just forward to dm
-      return d_dm.propagate(propagation);
+      return d_acm.propagate(propagation);
     }
 
     void notify(TNode t1, TNode t2) {
-      Debug("arith::differences") << "DifferenceNotifyClass::notify(" << t1 << ", " << t2 << ")" << std::endl;
+      Debug("arith::congruences") << "ArithCongruenceNotify::notify(" << t1 << ", " << t2 << ")" << std::endl;
       Node equality = t1.eqNode(t2);
-      d_dm.propagate(equality);
+      d_acm.propagate(equality);
     }
   };
+  ArithCongruenceNotify d_notify;
 
-  std::vector< Difference > d_differences;
-
-  struct LiteralsQueueElem {
-    bool d_eq;
-    ArithVar d_var;
-    Node d_reason;
-    LiteralsQueueElem() : d_eq(false), d_var(ARITHVAR_SENTINEL), d_reason() {}
-    LiteralsQueueElem(bool eq, ArithVar v, Node n) : d_eq(eq), d_var(v), d_reason(n) {}
-  };
-
-  /** Stores the queue of assertions. This keeps the Node backing the reasons */
-  context::CDTrailQueue<LiteralsQueueElem> d_literalsQueue;
-  //PropManager& d_queue;
+  context::CDList<Node> d_keepAlive;
 
   /** Store the propagations. */
   context::CDTrailQueue<Node> d_propagatations;
 
   /* This maps the node a theory engine will request on an explain call to
    * to its corresponding PropUnit.
-   * This is node is potentially both the propagation or Rewriter::rewrite(propagation).
+   * This is node is potentially both the propagation or
+   * Rewriter::rewrite(propagation).
    */
   typedef context::CDHashMap<Node, size_t, NodeHashFunction> ExplainMap;
   ExplainMap d_explanationMap;
@@ -109,6 +73,11 @@ private:
   ConstraintDatabase& d_constraintDatabase;
   TNodeCallBack& d_setupLiteral;
 
+  const ArithVarNodeMap& d_av2Node;
+
+  theory::uf::EqualityEngine<ArithCongruenceNotify> d_ee;
+  Node d_false;
+
 public:
 
   bool inConflict() const{
@@ -138,35 +107,35 @@ public:
 private:
   Node externalToInternal(TNode n) const{
     Assert(canExplain(n));
-    size_t pos = (*(d_explanationMap.find(n))).second;
+    ExplainMap::const_iterator iter = d_explanationMap.find(n);
+    size_t pos = (*iter).second;
     return d_propagatations[pos];
   }
 
   void pushBack(TNode n){
     d_explanationMap.insert(n, d_propagatations.size());
     d_propagatations.enqueue(n);
+
+    ++(d_statistics.d_propagations);
   }
 
   void pushBack(TNode n, TNode r){
     d_explanationMap.insert(r, d_propagatations.size());
     d_explanationMap.insert(n, d_propagatations.size());
     d_propagatations.enqueue(n);
-  }
 
-  DifferenceNotifyClass d_notify;
-  theory::uf::EqualityEngine<DifferenceNotifyClass> d_ee;
+    ++(d_statistics.d_propagations);
+  }
 
   bool propagate(TNode x);
   void explain(TNode literal, std::vector<TNode>& assumptions);
 
-  Node d_false;
-
   /**
    * This is set to true when the first shared term is added.
    * When this is set to true in the context, d_queue is emptied
    * and not used again in the context.
    */
-  context::CDO<bool> d_hasSharedTerms;
+  //context::CDO<bool> d_hasSharedTerms;
 
 
   /**
@@ -174,10 +143,11 @@ private:
    * If there are shared equalities, this is added to the equality engine.
    * Otherwise, this is put on a queue until there is a shared term.
    */
-  void assertLiteral(bool eq, ArithVar s, TNode reason);
+  //void assertLiteral(bool eq, ArithVar s, TNode reason);
 
   /** This sends a shared term to the uninterpretted equality engine. */
-  void addAssertionToEqualityEngine(bool eq, ArithVar s, TNode reason);
+  //void addAssertionToEqualityEngine(bool eq, ArithVar s, TNode reason);
+  void assertionToEqualityEngine(bool eq, ArithVar s, TNode reason);
 
   /** Dequeues the delay queue and asserts these equalities.*/
   void enableSharedTerms();
@@ -189,36 +159,58 @@ private:
 
 public:
 
-  DifferenceManager(context::Context* satContext, ConstraintDatabase&, TNodeCallBack&);
+  ArithCongruenceManager(context::Context* satContext, ConstraintDatabase&, TNodeCallBack&, const ArithVarNodeMap&);
 
   Node explain(TNode literal);
   void explain(TNode lit, NodeBuilder<>& out);
 
-  void addDifference(ArithVar s, Node x, Node y);
+  void addWatchedPair(ArithVar s, TNode x, TNode y);
 
-  inline bool isDifferenceSlack(ArithVar s) const{
-    if(s < d_differences.size()){
-      return d_differences[s].isSlack;
-    }else{
-      return false;
-    }
+  inline bool isWatchedVariable(ArithVar s) const {
+    return d_watchedVariables.isMember(s);
   }
 
   /** Assert an equality. */
-  void differenceIsZero(Constraint eq);
+  void watchedVariableIsZero(Constraint eq);
 
   /** Assert a conjunction from lb and ub. */
-  void differenceIsZero(Constraint lb, Constraint ub);
+  void watchedVariableIsZero(Constraint lb, Constraint ub);
+
+  /** Assert that the value cannot be zero. */
+  void watchedVariableCannotBeZero(Constraint c);
 
   /** Assert that the value cannot be zero. */
-  void differenceCannotBeZero(Constraint c);
+  void watchedVariableCannotBeZero(Constraint c, Constraint d);
+
+
+  /** Assert that the value is congruent to a constant. */
+  void equalsConstant(Constraint eq);
+  void equalsConstant(Constraint lb, Constraint ub);
+
 
   void addSharedTerm(Node x);
-};/* class DifferenceManager */
+
+private:
+  class Statistics {
+  public:
+    IntStat d_watchedVariables;
+    IntStat d_watchedVariableIsZero;
+    IntStat d_watchedVariableIsNotZero;
+
+    IntStat d_equalsConstantCalls;
+
+    IntStat d_propagations;
+    IntStat d_propagateConstraints;
+    IntStat d_conflicts;
+
+    Statistics();
+    ~Statistics();
+  } d_statistics;
+
+};/* class CongruenceManager */
 
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
 
-#endif /* __CVC4__THEORY__ARITH__DIFFERENCE_MANAGER_H */
 
diff --git a/src/theory/arith/constraint.cpp b/src/theory/arith/constraint.cpp
index f78ecdddf..460877a23 100644
--- a/src/theory/arith/constraint.cpp
+++ b/src/theory/arith/constraint.cpp
@@ -444,14 +444,13 @@ Constraint ConstraintValue::makeNegation(ArithVar v, ConstraintType t, const Del
   }
 }
 
-ConstraintDatabase::ConstraintDatabase(context::Context* satContext, context::Context* userContext, const ArithVarNodeMap& av2nodeMap,
-                                       DifferenceManager& dm)
+ConstraintDatabase::ConstraintDatabase(context::Context* satContext, context::Context* userContext, const ArithVarNodeMap& av2nodeMap, ArithCongruenceManager& cm)
   : d_varDatabases(),
     d_toPropagate(satContext),
     d_proofs(satContext, false),
     d_watches(new Watches(satContext, userContext)),
     d_av2nodeMap(av2nodeMap),
-    d_differenceManager(dm),
+    d_congruenceManager(cm),
     d_satContext(satContext),
     d_satAllocationLevel(d_satContext->getLevel())
 {
@@ -997,12 +996,12 @@ Constraint ConstraintDatabase::getBestImpliedBound(ArithVar v, ConstraintType t,
 }
 Node ConstraintDatabase::eeExplain(const ConstraintValue* const c) const{
   Assert(c->hasLiteral());
-  return d_differenceManager.explain(c->getLiteral());
+  return d_congruenceManager.explain(c->getLiteral());
 }
 
 void ConstraintDatabase::eeExplain(const ConstraintValue* const c, NodeBuilder<>& nb) const{
   Assert(c->hasLiteral());
-  d_differenceManager.explain(c->getLiteral(), nb);
+  d_congruenceManager.explain(c->getLiteral(), nb);
 }
 
 bool ConstraintDatabase::variableDatabaseIsSetup(ArithVar v) const {
diff --git a/src/theory/arith/constraint.h b/src/theory/arith/constraint.h
index e1939159b..2e0a9d067 100644
--- a/src/theory/arith/constraint.h
+++ b/src/theory/arith/constraint.h
@@ -77,7 +77,7 @@
 #include "theory/arith/arithvar_node_map.h"
 #include "theory/arith/delta_rational.h"
 
-#include "theory/arith/difference_manager.h"
+#include "theory/arith/congruence_manager.h"
 
 #include "theory/arith/constraint_forward.h"
 
@@ -746,7 +746,7 @@ private:
     return d_av2nodeMap;
   }
 
-  DifferenceManager& d_differenceManager;
+  ArithCongruenceManager& d_congruenceManager;
 
   //Constraint allocateConstraintForLiteral(ArithVar v, Node literal);
 
@@ -760,7 +760,7 @@ public:
   ConstraintDatabase( context::Context* satContext,
                       context::Context* userContext,
                       const ArithVarNodeMap& av2nodeMap,
-                      DifferenceManager& dm);
+                      ArithCongruenceManager& dm);
 
   ~ConstraintDatabase();
 
diff --git a/src/theory/arith/difference_manager.cpp b/src/theory/arith/difference_manager.cpp
deleted file mode 100644
index 70588bc16..000000000
--- a/src/theory/arith/difference_manager.cpp
+++ /dev/null
@@ -1,242 +0,0 @@
-#include "theory/arith/difference_manager.h"
-#include "theory/uf/equality_engine_impl.h"
-
-#include "theory/arith/constraint.h"
-#include "theory/arith/arith_utilities.h"
-
-namespace CVC4 {
-namespace theory {
-namespace arith {
-
-DifferenceManager::DifferenceManager(context::Context* c, ConstraintDatabase& cd, TNodeCallBack& setup)
-  : d_conflict(c),
-    d_literalsQueue(c),
-    d_propagatations(c),
-    d_explanationMap(c),
-    d_constraintDatabase(cd),
-    d_setupLiteral(setup),
-    d_notify(*this),
-    d_ee(d_notify, c, "theory::arith::DifferenceManager"),
-    d_false(NodeManager::currentNM()->mkConst<bool>(false)),
-    d_hasSharedTerms(c, false)
-{}
-
-void DifferenceManager::differenceIsZero(Constraint lb, Constraint ub){
-  Assert(lb->isLowerBound());
-  Assert(ub->isUpperBound());
-  Assert(lb->getVariable() == ub->getVariable());
-  Assert(lb->getValue().sgn() == 0);
-  Assert(ub->getValue().sgn() == 0);
-
-  ArithVar s = lb->getVariable();
-  Node reason = ConstraintValue::explainConflict(lb,ub);
-
-  assertLiteral(true, s, reason);
-}
-
-void DifferenceManager::differenceIsZero(Constraint eq){
-  Assert(eq->isEquality());
-  Assert(eq->getValue().sgn() == 0);
-
-  ArithVar s = eq->getVariable();
-
-  //Explain for conflict is correct as these proofs are generated and stored eagerly
-  //These will be safe for propagation later as well
-  Node reason = eq->explainForConflict();
-
-  assertLiteral(true, s, reason);
-}
-
-void DifferenceManager::differenceCannotBeZero(Constraint c){
-  ArithVar s = c->getVariable();
-
-  //Explain for conflict is correct as these proofs are generated and stored eagerly
-  //These will be safe for propagation later as well
-  Node reason = c->explainForConflict();
-  assertLiteral(false, s, reason);
-}
-
-
-bool DifferenceManager::propagate(TNode x){
-  Debug("arith::differenceManager")<< "DifferenceManager::propagate("<<x<<")"<<std::endl;
-  if(inConflict()){
-    return true;
-  }
-
-  Node rewritten = Rewriter::rewrite(x);
-
-  //Need to still propagate this!
-  if(rewritten.getKind() == kind::CONST_BOOLEAN){
-    pushBack(x);
-  }
-
-  Assert(rewritten.getKind() != kind::CONST_BOOLEAN);
-
-  Constraint c = d_constraintDatabase.lookup(rewritten);
-  if(c == NullConstraint){
-    //using setup as there may not be a corresponding difference literal yet
-    d_setupLiteral(rewritten);
-    c = d_constraintDatabase.lookup(rewritten);
-    Assert(c != NullConstraint);
-    //c = d_constraintDatabase.addLiteral(rewritten);
-  }
-
-  Debug("arith::differenceManager")<< "x is "
-                                   <<  c->hasProof() << " "
-                                   << (x == rewritten) << " "
-                                   << c->canBePropagated() << " "
-                                   << c->negationHasProof() << std::endl;
-
-  if(c->negationHasProof()){
-    Node expC = explainInternal(x);
-    Node neg = c->getNegation()->explainForConflict();
-    Node conf = expC.andNode(neg);
-    Node final = flattenAnd(conf);
-
-    d_conflict.set(final);
-    Debug("arith::differenceManager") << "differenceManager found a conflict " << final << std::endl;
-    return false;
-  }
-
-  // Cases for propagation
-  // C : c has a proof
-  // S : x == rewritten
-  // P : c can be propagated
-  //
-  // CSP
-  // 000 : propagate x, and mark C it as being explained
-  // 001 : propagate x, and propagate c after marking it as being explained
-  // 01* : propagate x, mark c but do not propagate c
-  // 10* : propagate x, do not mark c and do not propagate c
-  // 11* : drop the constraint, do not propagate x or c
-
-  if(!c->hasProof() && x != rewritten){
-    pushBack(x, rewritten);
-
-    c->setEqualityEngineProof();
-    if(c->canBePropagated() && !c->assertedToTheTheory()){
-      c->propagate();
-    }
-  }else if(!c->hasProof() && x == rewritten){
-    pushBack(x, rewritten);
-    c->setEqualityEngineProof();
-  }else if(c->hasProof() && x != rewritten){
-    pushBack(x, rewritten);
-  }else{
-    Assert(c->hasProof() && x == rewritten);
-  }
-  return true;
-}
-
-void DifferenceManager::explain(TNode literal, std::vector<TNode>& assumptions) {
-  TNode lhs, rhs;
-  switch (literal.getKind()) {
-    case kind::EQUAL:
-      lhs = literal[0];
-      rhs = literal[1];
-      break;
-    case kind::NOT:
-      lhs = literal[0];
-      rhs = d_false;
-      break;
-    default:
-      Unreachable();
-  }
-  d_ee.explainEquality(lhs, rhs, assumptions);
-}
-
-void DifferenceManager::enqueueIntoNB(const std::set<TNode> s, NodeBuilder<>& nb){
-  std::set<TNode>::const_iterator it = s.begin();
-  std::set<TNode>::const_iterator it_end = s.end();
-  for(; it != it_end; ++it) {
-    nb << *it;
-  }
-}
-
-Node DifferenceManager::explainInternal(TNode internal){
-  std::vector<TNode> assumptions;
-  explain(internal, assumptions);
-
-  std::set<TNode> assumptionSet;
-  assumptionSet.insert(assumptions.begin(), assumptions.end());
-
-  if (assumptionSet.size() == 1) {
-    // All the same, or just one
-    return assumptions[0];
-  }else{
-    NodeBuilder<> conjunction(kind::AND);
-    enqueueIntoNB(assumptionSet, conjunction);
-    return conjunction;
-  }
-}
-Node DifferenceManager::explain(TNode external){
-  Node internal = externalToInternal(external);
-  return explainInternal(internal);
-}
-
-void DifferenceManager::explain(TNode external, NodeBuilder<>& out){
-  Node internal = externalToInternal(external);
-
-  std::vector<TNode> assumptions;
-  explain(internal, assumptions);
-  std::set<TNode> assumptionSet;
-  assumptionSet.insert(assumptions.begin(), assumptions.end());
-
-  enqueueIntoNB(assumptionSet, out);
-}
-
-void DifferenceManager::addDifference(ArithVar s, Node x, Node y){
-  Assert(s >= d_differences.size() || !isDifferenceSlack(s));
-
-  Debug("arith::differenceManager") << s << x << y << std::endl;
-
-  d_differences.resize(s+1);
-  d_differences[s] = Difference(x,y);
-}
-
-void DifferenceManager::addAssertionToEqualityEngine(bool eq, ArithVar s, TNode reason){
-  Assert(isDifferenceSlack(s));
-
-  TNode x = d_differences[s].x;
-  TNode y = d_differences[s].y;
-
-  if(eq){
-    d_ee.addEquality(x, y, reason);
-  }else{
-    d_ee.addDisequality(x, y, reason);
-  }
-}
-
-void DifferenceManager::dequeueLiterals(){
-  Assert(d_hasSharedTerms);
-  while(!d_literalsQueue.empty() && !inConflict()){
-    const LiteralsQueueElem& front = d_literalsQueue.front();
-    d_literalsQueue.dequeue();
-
-    addAssertionToEqualityEngine(front.d_eq, front.d_var, front.d_reason);
-  }
-}
-
-void DifferenceManager::enableSharedTerms(){
-  Assert(!d_hasSharedTerms);
-  d_hasSharedTerms = true;
-  dequeueLiterals();
-}
-
-void DifferenceManager::assertLiteral(bool eq, ArithVar s, TNode reason){
-  d_literalsQueue.enqueue(LiteralsQueueElem(eq, s, reason));
-  if(d_hasSharedTerms){
-    dequeueLiterals();
-  }
-}
-
-void DifferenceManager::addSharedTerm(Node x){
-  if(!d_hasSharedTerms){
-    enableSharedTerms();
-  }
-  d_ee.addTriggerTerm(x);
-}
-
-}/* CVC4::theory::arith namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 502a92962..bc8861996 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -72,9 +72,9 @@ TheoryArith::TheoryArith(context::Context* c, context::UserContext* u, OutputCha
   d_tableauResetPeriod(10),
   d_conflicts(c),
   d_conflictCallBack(d_conflicts),
-  d_differenceManager(c, d_constraintDatabase, d_setupLiteralCallback),
+  d_congruenceManager(c, d_constraintDatabase, d_setupLiteralCallback, d_arithvarNodeMap),
   d_simplex(d_linEq, d_conflictCallBack),
-  d_constraintDatabase(c, u, d_arithvarNodeMap, d_differenceManager),
+  d_constraintDatabase(c, u, d_arithvarNodeMap, d_congruenceManager),
   d_basicVarModelUpdateCallBack(d_simplex),
   d_DELTA_ZERO(0),
   d_statistics()
@@ -151,7 +151,7 @@ TheoryArith::Statistics::~Statistics(){
 }
 
 void TheoryArith::zeroDifferenceDetected(ArithVar x){
-  Assert(d_differenceManager.isDifferenceSlack(x));
+  Assert(d_congruenceManager.isWatchedVariable(x));
   Assert(d_partialModel.upperBoundIsZero(x));
   Assert(d_partialModel.lowerBoundIsZero(x));
 
@@ -159,11 +159,11 @@ void TheoryArith::zeroDifferenceDetected(ArithVar x){
   Constraint ub = d_partialModel.getUpperBoundConstraint(x);
 
   if(lb->isEquality()){
-    d_differenceManager.differenceIsZero(lb);
+    d_congruenceManager.watchedVariableIsZero(lb);
   }else if(ub->isEquality()){
-    d_differenceManager.differenceIsZero(ub);
+    d_congruenceManager.watchedVariableIsZero(ub);
   }else{
-    d_differenceManager.differenceIsZero(lb, ub);
+    d_congruenceManager.watchedVariableIsZero(lb, ub);
   }
 }
 
@@ -195,6 +195,14 @@ Node TheoryArith::AssertLower(Constraint constraint){
     if(isInteger(x_i)){
       d_constantIntegerVariables.push_back(x_i);
     }
+    Constraint ub = d_partialModel.getUpperBoundConstraint(x_i);
+
+    if(!d_congruenceManager.isWatchedVariable(x_i) || c_i.sgn() != 0){
+      // if it is not a watched variable report it
+      // if it is is a watched variable and c_i == 0,
+      // let zeroDifferenceDetected(x_i) catch this
+      d_congruenceManager.equalsConstant(constraint, ub);
+    }
 
     const ValueCollection& vc = constraint->getValueCollection();
     if(vc.hasDisequality()){
@@ -202,7 +210,7 @@ Node TheoryArith::AssertLower(Constraint constraint){
       const Constraint eq = vc.getEquality();
       const Constraint diseq = vc.getDisequality();
       if(diseq->isTrue()){
-        const Constraint ub = vc.getUpperBound();
+        //const Constraint ub = vc.getUpperBound();
         Node conflict = ConstraintValue::explainConflict(diseq, ub, constraint);
 
         ++(d_statistics.d_statDisequalityConflicts);
@@ -217,10 +225,10 @@ Node TheoryArith::AssertLower(Constraint constraint){
 
   d_partialModel.setLowerBoundConstraint(constraint);
 
-  if(d_differenceManager.isDifferenceSlack(x_i)){
+  if(d_congruenceManager.isWatchedVariable(x_i)){
     int sgn = c_i.sgn();
     if(sgn > 0){
-      d_differenceManager.differenceCannotBeZero(constraint);
+      d_congruenceManager.watchedVariableCannotBeZero(constraint);
     }else if(sgn == 0 && d_partialModel.upperBoundIsZero(x_i)){
       zeroDifferenceDetected(x_i);
     }
@@ -273,6 +281,13 @@ Node TheoryArith::AssertUpper(Constraint constraint){
     if(isInteger(x_i)){
       d_constantIntegerVariables.push_back(x_i);
     }
+    Constraint lb = d_partialModel.getLowerBoundConstraint(x_i);
+    if(!d_congruenceManager.isWatchedVariable(x_i) || c_i.sgn() != 0){
+      // if it is not a watched variable report it
+      // if it is is a watched variable and c_i == 0,
+      // let zeroDifferenceDetected(x_i) catch this
+      d_congruenceManager.equalsConstant(lb, constraint);
+    }
 
     const ValueCollection& vc = constraint->getValueCollection();
     if(vc.hasDisequality()){
@@ -280,7 +295,6 @@ Node TheoryArith::AssertUpper(Constraint constraint){
       const Constraint diseq = vc.getDisequality();
       const Constraint eq = vc.getEquality();
       if(diseq->isTrue()){
-        const Constraint lb = vc.getLowerBound();
         Node conflict = ConstraintValue::explainConflict(diseq, lb, constraint);
         Debug("eq") << " assert upper conflict " << conflict << endl;
         return conflict;
@@ -294,10 +308,10 @@ Node TheoryArith::AssertUpper(Constraint constraint){
 
   d_partialModel.setUpperBoundConstraint(constraint);
 
-  if(d_differenceManager.isDifferenceSlack(x_i)){
+  if(d_congruenceManager.isWatchedVariable(x_i)){
     int sgn = c_i.sgn();
      if(sgn < 0){
-       d_differenceManager.differenceCannotBeZero(constraint);
+       d_congruenceManager.watchedVariableCannotBeZero(constraint);
      }else if(sgn == 0 && d_partialModel.lowerBoundIsZero(x_i)){
        zeroDifferenceDetected(x_i);
      }
@@ -370,16 +384,18 @@ Node TheoryArith::AssertEquality(Constraint constraint){
   d_partialModel.setUpperBoundConstraint(constraint);
   d_partialModel.setLowerBoundConstraint(constraint);
 
-  if(d_differenceManager.isDifferenceSlack(x_i)){
+  if(d_congruenceManager.isWatchedVariable(x_i)){
     int sgn = c_i.sgn();
     if(sgn == 0){
       zeroDifferenceDetected(x_i);
     }else{
-      d_differenceManager.differenceCannotBeZero(constraint);
+      d_congruenceManager.watchedVariableCannotBeZero(constraint);
+      d_congruenceManager.equalsConstant(constraint);
     }
+  }else{
+    d_congruenceManager.equalsConstant(constraint);
   }
 
-
   d_updatedBounds.softAdd(x_i);
 
   if(!d_tableau.isBasic(x_i)){
@@ -406,10 +422,10 @@ Node TheoryArith::AssertDisequality(Constraint constraint){
   //Should be fine in integers
   Assert(!isInteger(x_i) || c_i.isIntegral());
 
-  if(d_differenceManager.isDifferenceSlack(x_i)){
+  if(d_congruenceManager.isWatchedVariable(x_i)){
     int sgn = c_i.sgn();
     if(sgn == 0){
-      d_differenceManager.differenceCannotBeZero(constraint);
+      d_congruenceManager.watchedVariableCannotBeZero(constraint);
     }
   }
 
@@ -444,7 +460,7 @@ Node TheoryArith::AssertDisequality(Constraint constraint){
 
 
   if(c_i == d_partialModel.getAssignment(x_i)){
-    Debug("eq") << "lemma now!" << endl;
+    Debug("eq") << "lemma now! " << constraint << endl;
     d_out->lemma(constraint->split());
     return Node::null();
   }else if(d_partialModel.strictlyLessThanLowerBound(x_i, c_i)){
@@ -460,7 +476,7 @@ Node TheoryArith::AssertDisequality(Constraint constraint){
 }
 
 void TheoryArith::addSharedTerm(TNode n){
-  d_differenceManager.addSharedTerm(n);
+  d_congruenceManager.addSharedTerm(n);
   if(!n.isConst() && !isSetup(n)){
     Polynomial poly = Polynomial::parsePolynomial(n);
     Polynomial::iterator it = poly.begin();
@@ -713,7 +729,7 @@ void TheoryArith::setupPolynomial(const Polynomial& poly) {
             VarList vl0 = first.getVarList();
             VarList vl1 = second.getVarList();
             if(vl0.singleton() && vl1.singleton()){
-              d_differenceManager.addDifference(varSlack, vl0.getNode(), vl1.getNode());
+              d_congruenceManager.addWatchedPair(varSlack, vl0.getNode(), vl1.getNode());
             }
           }
         }
@@ -1137,8 +1153,8 @@ void TheoryArith::check(Effort effortLevel){
       d_out->conflict(possibleConflict);
       return;
     }
-    if(d_differenceManager.inConflict()){
-      Node c = d_differenceManager.conflict();
+    if(d_congruenceManager.inConflict()){
+      Node c = d_congruenceManager.conflict();
       d_partialModel.revertAssignmentChanges();
       Debug("arith::conflict") << "difference manager conflict   " << c << endl;
       clearUpdates();
@@ -1344,9 +1360,9 @@ Node TheoryArith::explain(TNode n) {
     Debug("arith::explain") << "constraint explanation" << n << ":" << exp << endl;
     return exp;
   }else{
-    Assert(d_differenceManager.canExplain(n));
+    Assert(d_congruenceManager.canExplain(n));
     Debug("arith::explain") << "dm explanation" << n << endl;
-    return d_differenceManager.explain(n);
+    return d_congruenceManager.explain(n);
   }
 }
 
@@ -1379,8 +1395,8 @@ void TheoryArith::propagate(Effort e) {
     }
   }
 
-  while(d_differenceManager.hasMorePropagations()){
-    TNode toProp = d_differenceManager.getNextPropagation();
+  while(d_congruenceManager.hasMorePropagations()){
+    TNode toProp = d_congruenceManager.getNextPropagation();
 
     //Currently if the flag is set this came from an equality detected by the
     //equality engine in the the difference manager.
@@ -1391,7 +1407,7 @@ void TheoryArith::propagate(Effort e) {
       Debug("arith::prop") << "propagating on non-constraint? "  << toProp << endl;
       d_out->propagate(toProp);
     }else if(constraint->negationHasProof()){
-      Node exp = d_differenceManager.explain(toProp);
+      Node exp = d_congruenceManager.explain(toProp);
       Node notNormalized = normalized.getKind() == NOT ?
         normalized[0] : normalized.notNode();
       Node lp = flattenAnd(exp.andNode(notNormalized));
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index 4a5c398bd..3ed1d1941 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -38,7 +38,7 @@
 #include "theory/arith/arith_static_learner.h"
 #include "theory/arith/arithvar_node_map.h"
 #include "theory/arith/dio_solver.h"
-#include "theory/arith/difference_manager.h"
+#include "theory/arith/congruence_manager.h"
 
 #include "theory/arith/constraint.h"
 
@@ -241,14 +241,8 @@ private:
    */
   Tableau d_smallTableauCopy;
 
-  /**
-   * The atom database keeps track of the atoms that have been preregistered.
-   * Used to add unate propagations.
-   */
-  //ArithAtomDatabase d_atomDatabase;
-
   /** This keeps track of difference equalities. Mostly for sharing. */
-  DifferenceManager d_differenceManager;
+  ArithCongruenceManager d_congruenceManager;
 
   /** This implements the Simplex decision procedure. */
   SimplexDecisionProcedure d_simplex;
diff --git a/test/regress/regress0/uflra/Makefile.am b/test/regress/regress0/uflra/Makefile.am
index 4817582c0..0418fc3e9 100644
--- a/test/regress/regress0/uflra/Makefile.am
+++ b/test/regress/regress0/uflra/Makefile.am
@@ -13,6 +13,7 @@ MAKEFLAGS = -k
 
 # Regression tests for SMT inputs
 SMT_TESTS = \
+	constants0.smt \
 	simple.01.cvc \
 	simple.02.cvc \
 	simple.03.cvc \
diff --git a/test/regress/regress0/uflra/constants0.smt b/test/regress/regress0/uflra/constants0.smt
new file mode 100644
index 000000000..b07a6bc4e
--- /dev/null
+++ b/test/regress/regress0/uflra/constants0.smt
@@ -0,0 +1,15 @@
+(benchmark mathsat
+:logic QF_UFLRA
+:status unsat 
+:category { crafted } 
+:extrafuns ((f Real Real))
+:extrafuns ((x Real))
+:extrafuns ((y Real))
+:formula
+(and (or (= x 3) (= x 5))
+     (or (= y 3) (= y 5))
+     (not (= (f x) (f y)))
+     (implies (= (f 3) (f x)) (= (f 5) (f x)))
+     (implies (= (f 3) (f y)) (= (f 5) (f y)))
+)
+)
\ No newline at end of file