* 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

1 files changed, 38 insertions, 18 deletions

diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index 6956390f5..9017928b7 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -39,21 +39,46 @@ namespace uf {
 class TheoryUF : public Theory {
 public:
 
-  class NotifyClass {
+  class NotifyClass : public eq::EqualityEngineNotify {
     TheoryUF& d_uf;
   public:
     NotifyClass(TheoryUF& uf): d_uf(uf) {}
 
-    bool notify(TNode propagation) {
-      Debug("uf") << "NotifyClass::notify(" << propagation << ")" << std::endl;
-      // Just forward to uf
-      return d_uf.propagate(propagation);
+    bool eqNotifyTriggerEquality(TNode equality, bool value) {
+      Debug("uf") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl;
+      if (value) {
+        return d_uf.propagate(equality);
+      } else {
+        // We use only literal triggers so taking not is safe
+        return d_uf.propagate(equality.notNode());
+      }
     }
-    
-    void notify(TNode t1, TNode t2) {
-      Debug("uf") << "NotifyClass::notify(" << t1 << ", " << t2 << ")" << std::endl;
-      Node equality = Rewriter::rewriteEquality(theory::THEORY_UF, t1.eqNode(t2));
-      d_uf.propagate(equality);
+
+    bool eqNotifyTriggerPredicate(TNode predicate, bool value) {
+      Debug("uf") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false" )<< ")" << std::endl;
+      if (value) {
+        return d_uf.propagate(predicate);
+      } else {
+       return d_uf.propagate(predicate.notNode());
+      }
+    }
+
+    bool eqNotifyTriggerTermEquality(TNode t1, TNode t2, bool value) {
+      Debug("uf") << "NotifyClass::eqNotifyTriggerTermMerge(" << t1 << ", " << t2 << std::endl;
+      if (value) {
+        return d_uf.propagate(t1.eqNode(t2));
+      } else {
+        return d_uf.propagate(t1.eqNode(t2).notNode());
+      }
+    }
+
+    bool eqNotifyConstantTermMerge(TNode t1, TNode t2) {
+      Debug("uf") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << std::endl;
+      if (Theory::theoryOf(t1) == THEORY_BOOL) {
+        return d_uf.propagate(t1.iffNode(t2));
+      } else {
+        return d_uf.propagate(t1.eqNode(t2));
+      }
     }
   };
 
@@ -63,7 +88,7 @@ private:
   NotifyClass d_notify;
 
   /** Equaltity engine */
-  EqualityEngine<NotifyClass> d_equalityEngine;
+  eq::EqualityEngine d_equalityEngine;
 
   /** Are we in conflict */
   context::CDO<bool> d_conflict;
@@ -72,7 +97,8 @@ private:
   Node d_conflictNode;
 
   /**
-   * Should be called to propagate the literal. 
+   * Should be called to propagate the literal. We use a node here 
+   * since some of the propagated literals are not kept anywhere. 
    */
   bool propagate(TNode literal);
 
@@ -90,12 +116,6 @@ private:
   /** All the function terms that the theory has seen */
   context::CDList<TNode> d_functionsTerms;
 
-  /** True node for predicates = true */
-  Node d_true;
-
-  /** True node for predicates = false */
-  Node d_false;
-
   /** Symmetry analyzer */
   SymmetryBreaker d_symb;