* simplifying equality engine interface

* notifications are now through the interface subclass instead of a template
* notifications include constants being merged
* changed contextNotifyObj::notify to contextNotifyObj::contextNotifyPop so it's more descriptive and doesn't clutter methods when subclassed
* sat solver now has explicit methods to make true and false constants
* 0-level literals are removed from explanations of propagations

3 files changed, 42 insertions, 38 deletions

diff --git a/src/theory/arith/congruence_manager.cpp b/src/theory/arith/congruence_manager.cpp
index 201eb08e7..39468e928 100644
--- a/src/theory/arith/congruence_manager.cpp
+++ b/src/theory/arith/congruence_manager.cpp
@@ -1,5 +1,4 @@
 #include "theory/arith/congruence_manager.h"
-#include "theory/uf/equality_engine_impl.h"
 
 #include "theory/arith/constraint.h"
 #include "theory/arith/arith_utilities.h"
@@ -17,8 +16,7 @@ ArithCongruenceManager::ArithCongruenceManager(context::Context* c, ConstraintDa
     d_constraintDatabase(cd),
     d_setupLiteral(setup),
     d_av2Node(av2Node),
-    d_ee(d_notify, c, "theory::arith::ArithCongruenceManager"),
-    d_false(mkBoolNode(false))
+    d_ee(d_notify, c, "theory::arith::ArithCongruenceManager")
 {}
 
 ArithCongruenceManager::Statistics::Statistics():
@@ -113,7 +111,7 @@ bool ArithCongruenceManager::propagate(TNode x){
     }else{
       ++(d_statistics.d_conflicts);
 
-      Node conf = explainInternal(x);
+      Node conf = flattenAnd(explainInternal(x));
       d_conflict.set(conf);
       Debug("arith::congruenceManager") << "rewritten to false "<<x<<" with explanation "<< conf << std::endl;
       return false;
@@ -181,20 +179,11 @@ bool ArithCongruenceManager::propagate(TNode x){
 }
 
 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();
+  if (literal.getKind() != kind::NOT) {
+    d_ee.explainEquality(literal[0], literal[1], true, assumptions);
+  } else {
+    d_ee.explainEquality(literal[0][0], literal[0][1], false, assumptions);
   }
-  d_ee.explainEquality(lhs, rhs, assumptions);
 }
 
 void ArithCongruenceManager::enqueueIntoNB(const std::set<TNode> s, NodeBuilder<>& nb){
@@ -258,13 +247,10 @@ void ArithCongruenceManager::assertionToEqualityEngine(bool isEquality, ArithVar
   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);
+    d_ee.assertEquality(eq, true, reason);
   }else{
-    d_ee.addDisequality(x, y, reason);
+    d_ee.assertEquality(eq, false, reason);
   }
 }
 
@@ -286,7 +272,7 @@ void ArithCongruenceManager::equalsConstant(Constraint c){
   Node reason = c->explainForConflict();
   d_keepAlive.push_back(reason);
 
-  d_ee.addEquality(xAsNode, asRational, reason);
+  d_ee.assertEquality(eq, true, reason);
 }
 
 void ArithCongruenceManager::equalsConstant(Constraint lb, Constraint ub){
@@ -310,7 +296,7 @@ void ArithCongruenceManager::equalsConstant(Constraint lb, Constraint ub){
   d_keepAlive.push_back(reason);
 
 
-  d_ee.addEquality(xAsNode, asRational, reason);
+  d_ee.assertEquality(eq, true, reason);
 }
 
 void ArithCongruenceManager::addSharedTerm(Node x){
diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h
index a72989498..18ecbeb9d 100644
--- a/src/theory/arith/congruence_manager.h
+++ b/src/theory/arith/congruence_manager.h
@@ -37,24 +37,43 @@ private:
   ArithVarToNodeMap d_watchedEqualities;
 
 
-  class ArithCongruenceNotify {
+  class ArithCongruenceNotify : public eq::EqualityEngineNotify {
   private:
     ArithCongruenceManager& d_acm;
   public:
     ArithCongruenceNotify(ArithCongruenceManager& acm): d_acm(acm) {}
 
-    bool notify(TNode propagation) {
-      Debug("arith::congruences") << "ArithCongruenceNotify::notify(" << propagation << ")" << std::endl;
-      // Just forward to dm
-      return d_acm.propagate(propagation);
+    bool eqNotifyTriggerEquality(TNode equality, bool value) {
+      Debug("arith::congruences") << "ArithCongruenceNotify::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false") << ")" << std::endl;
+      if (value) {
+        return d_acm.propagate(equality);
+      } else {
+        return d_acm.propagate(equality.notNode());
+      }
     }
 
-    void notify(TNode t1, TNode t2) {
-      Debug("arith::congruences") << "ArithCongruenceNotify::notify(" << t1 << ", " << t2 << ")" << std::endl;
-      Node equality = t1.eqNode(t2);
-      d_acm.propagate(equality);
+    bool eqNotifyTriggerPredicate(TNode predicate, bool value) {
+      Unreachable();
     }
-  };
+
+    bool eqNotifyTriggerTermEquality(TNode t1, TNode t2, bool value) {
+      Debug("arith::congruences") << "ArithCongruenceNotify::eqNotifyTriggerTermEquality(" << t1 << ", " << t2 << ", " << (value ? "true" : "false") << ")" << std::endl;
+      if (value) {
+        return d_acm.propagate(t1.eqNode(t2));
+      } else {
+        return d_acm.propagate(t1.eqNode(t2).notNode());
+      }
+    }
+
+    bool eqNotifyConstantTermMerge(TNode t1, TNode t2) {
+      Debug("arith::congruences") << "ArithCongruenceNotify::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << std::endl;
+      if (t1.getKind() == kind::CONST_BOOLEAN) {
+        return d_acm.propagate(t1.iffNode(t2));
+      } else {
+        return d_acm.propagate(t1.eqNode(t2));
+      }
+    }
+   };
   ArithCongruenceNotify d_notify;
 
   context::CDList<Node> d_keepAlive;
@@ -75,8 +94,7 @@ private:
 
   const ArithVarNodeMap& d_av2Node;
 
-  theory::uf::EqualityEngine<ArithCongruenceNotify> d_ee;
-  Node d_false;
+  eq::EqualityEngine d_ee;
 
 public:
 
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index c7072de72..6bb3821da 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -1001,8 +1001,8 @@ 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;
+//      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;