* 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

2 files changed, 81 insertions, 129 deletions

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 80bcb47dd..1dd74f060 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -23,17 +23,13 @@
 #include <map>
 #include "theory/rewriter.h"
 #include "expr/command.h"
-#include "theory/uf/equality_engine_impl.h"
-
 
 using namespace std;
 
-
 namespace CVC4 {
 namespace theory {
 namespace arrays {
 
-
 // These are the options that produce the best empirical results on QF_AX benchmarks.
 // eagerLemmas = true
 // eagerIndexSplitting = false
@@ -58,14 +54,12 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC
   d_numNonLinear("theory::arrays::number of calls to setNonLinear", 0),
   d_numSharedArrayVarSplits("theory::arrays::number of shared array var splits", 0),
   d_checkTimer("theory::arrays::checkTime"),
-  d_ppNotify(),
-  d_ppEqualityEngine(d_ppNotify, u, "theory::arrays::TheoryArraysPP"),
+  d_ppEqualityEngine(u, "theory::arrays::TheoryArraysPP"),
   d_ppFacts(u),
   //  d_ppCache(u),  
   d_literalsToPropagate(c),
   d_literalsToPropagateIndex(c, 0),
-  d_mayEqualNotify(),
-  d_mayEqualEqualityEngine(d_mayEqualNotify, c, "theory::arrays::TheoryArraysMayEqual"),
+  d_mayEqualEqualityEngine(c, "theory::arrays::TheoryArraysMayEqual"),
   d_notify(*this),
   d_equalityEngine(d_notify, c, "theory::arrays::TheoryArrays"),
   d_conflict(c, false),
@@ -91,14 +85,6 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC
   d_true = NodeManager::currentNM()->mkConst<bool>(true);
   d_false = NodeManager::currentNM()->mkConst<bool>(false);
 
-  d_ppEqualityEngine.addTerm(d_true);
-  d_ppEqualityEngine.addTerm(d_false);
-  d_ppEqualityEngine.addTriggerEquality(d_true, d_false, d_false);
-
-  d_equalityEngine.addTerm(d_true);
-  d_equalityEngine.addTerm(d_false);
-  d_equalityEngine.addTriggerEquality(d_true, d_false, d_false);
-
   // The kinds we are treating as function application in congruence
   d_equalityEngine.addFunctionKind(kind::SELECT);
   if (d_ccStore) {
@@ -281,7 +267,7 @@ Theory::PPAssertStatus TheoryArrays::ppAssert(TNode in, SubstitutionMap& outSubs
     case kind::EQUAL:
     {
       d_ppFacts.push_back(in);
-      d_ppEqualityEngine.addEquality(in[0], in[1], in);
+      d_ppEqualityEngine.assertEquality(in, true, in);
       if (in[0].getMetaKind() == kind::metakind::VARIABLE && !in[1].hasSubterm(in[0])) {
         outSubstitutions.addSubstitution(in[0], in[1]);
         return PP_ASSERT_STATUS_SOLVED;
@@ -299,7 +285,7 @@ Theory::PPAssertStatus TheoryArrays::ppAssert(TNode in, SubstitutionMap& outSubs
              in[0].getKind() == kind::IFF );
       Node a = in[0][0];
       Node b = in[0][1];
-      d_ppEqualityEngine.addDisequality(a, b, in);
+      d_ppEqualityEngine.assertEquality(in[0], false, in);
       break;
     }
     default:
@@ -335,10 +321,8 @@ bool TheoryArrays::propagate(TNode literal)
       Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate(" << literal << ", normalized = " << normalized << ") => conflict" << std::endl;
       std::vector<TNode> assumptions;
       Node negatedLiteral;
-      if (normalized != d_false) {
-        negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode();
-        assumptions.push_back(negatedLiteral);
-      }
+      negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode();
+      assumptions.push_back(negatedLiteral);
       explain(literal, assumptions);
       d_conflictNode = mkAnd(assumptions);
       d_conflict = true;
@@ -357,67 +341,40 @@ bool TheoryArrays::propagate(TNode literal)
 
 
 void TheoryArrays::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::SELECT:
-      lhs = literal;
-      rhs = d_true;
-      break;
-    case kind::NOT:
-      if (literal[0].getKind() == kind::EQUAL) {
-        // Disequalities
-        d_equalityEngine.explainDisequality(literal[0][0], literal[0][1], assumptions);
-        return;
-      } else {
-        // Predicates
-        lhs = literal[0];
-        rhs = d_false;
-        break;
-      }
-    case kind::CONST_BOOLEAN:
-      // we get to explain true = false, since we set false to be the trigger of this
-      lhs = d_true;
-      rhs = d_false;
-      break;
-    default:
-      Unreachable();
+  // Do the work
+  bool polarity = literal.getKind() != kind::NOT;
+  TNode atom = polarity ? literal : literal[0];
+  if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
+    d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
+  } else {
+    d_equalityEngine.explainPredicate(atom, polarity, assumptions);
   }
-  d_equalityEngine.explainEquality(lhs, rhs, assumptions);
 }
 
 
-  /**
-   * Stores in d_infoMap the following information for each term a of type array:
-   *
-   *    - all i, such that there exists a term a[i] or a = store(b i v)
-   *      (i.e. all indices it is being read atl; store(b i v) is implicitly read at
-   *      position i due to the implicit axiom store(b i v)[i] = v )
-   *
-   *    - all the stores a is congruent to (this information is context dependent)
-   *
-   *    - all store terms of the form store (a i v) (i.e. in which a appears
-   *      directly; this is invariant because no new store terms are created)
-   *
-   * Note: completeness depends on having pre-register called on all the input
-   *       terms before starting to instantiate lemmas.
-   */
+/**
+ * Stores in d_infoMap the following information for each term a of type array:
+ *
+ *    - all i, such that there exists a term a[i] or a = store(b i v)
+ *      (i.e. all indices it is being read atl; store(b i v) is implicitly read at
+ *      position i due to the implicit axiom store(b i v)[i] = v )
+ *
+ *    - all the stores a is congruent to (this information is context dependent)
+ *
+ *    - all store terms of the form store (a i v) (i.e. in which a appears
+ *      directly; this is invariant because no new store terms are created)
+ *
+ * Note: completeness depends on having pre-register called on all the input
+ *       terms before starting to instantiate lemmas.
+ */
 void TheoryArrays::preRegisterTerm(TNode node)
 {
   Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::preRegisterTerm(" << node << ")" << std::endl;
 
   switch (node.getKind()) {
   case kind::EQUAL:
-    // Add the terms
-    //    d_equalityEngine.addTerm(node[0]);
-    //    d_equalityEngine.addTerm(node[1]);
-    d_equalityEngine.addTerm(node);
     // Add the trigger for equality
-    d_equalityEngine.addTriggerEquality(node[0], node[1], node);
-    d_equalityEngine.addTriggerDisequality(node[0], node[1], node.notNode());
+    d_equalityEngine.addTriggerEquality(node);
     break;
   case kind::SELECT: {
     // Reads
@@ -438,7 +395,7 @@ void TheoryArrays::preRegisterTerm(TNode node)
           Assert(!d_equalityEngine.hasTerm(ni));
           preRegisterTerm(ni);
         }
-        d_equalityEngine.addEquality(ni, s[2], d_true);
+        d_equalityEngine.assertEquality(ni.eqNode(s[2]), true, d_true);
         Assert(++it == stores->end());
       }
     }
@@ -447,8 +404,7 @@ void TheoryArrays::preRegisterTerm(TNode node)
     // TODO: remove this or keep it if we allow Boolean elements in arrays.
     if (node.getType().isBoolean()) {
       // Get triggered for both equal and dis-equal
-      d_equalityEngine.addTriggerEquality(node, d_true, node);
-      d_equalityEngine.addTriggerEquality(node, d_false, node.notNode());
+      d_equalityEngine.addTriggerPredicate(node);
     }
 
     d_infoMap.addIndex(node[0], node[1]);
@@ -463,7 +419,7 @@ void TheoryArrays::preRegisterTerm(TNode node)
     //    TNode i = node[1];
     //    TNode v = node[2];
 
-    d_mayEqualEqualityEngine.addEquality(node, a, d_true);
+    d_mayEqualEqualityEngine.assertEquality(node.eqNode(a), true, d_true);
 
     // NodeManager* nm = NodeManager::currentNM();
     // Node ni = nm->mkNode(kind::SELECT, node, i);
@@ -508,10 +464,8 @@ void TheoryArrays::propagate(Effort e)
         Debug("arrays") << spaces(getSatContext()->getLevel()) << "TheoryArrays::propagate(): in conflict, normalized = " << normalized << std::endl;
         Node negatedLiteral;
         std::vector<TNode> assumptions;
-        if (normalized != d_false) {
-          negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode();
-          assumptions.push_back(negatedLiteral);
-        }
+        negatedLiteral = normalized.getKind() == kind::NOT ? (Node) normalized[0] : normalized.notNode();
+        assumptions.push_back(negatedLiteral);
         explain(literal, assumptions);
         d_conflictNode = mkAnd(assumptions);
         d_conflict = true;
@@ -727,17 +681,17 @@ void TheoryArrays::check(Effort e) {
     // Do the work
     switch (fact.getKind()) {
       case kind::EQUAL:
-        d_equalityEngine.addEquality(fact[0], fact[1], fact);
+        d_equalityEngine.assertEquality(fact, true, fact);
         break;
       case kind::SELECT:
-        d_equalityEngine.addPredicate(fact, true, fact);
+        d_equalityEngine.assertPredicate(fact, true, fact);
         break;
       case kind::NOT:
         if (fact[0].getKind() == kind::SELECT) {
-          d_equalityEngine.addPredicate(fact[0], false, fact);
+          d_equalityEngine.assertPredicate(fact[0], false, fact);
         } else if (!d_equalityEngine.areDisequal(fact[0][0], fact[0][1])) {
           // Assert the dis-equality
-          d_equalityEngine.addDisequality(fact[0][0], fact[0][1], fact);
+          d_equalityEngine.assertEquality(fact[0], false, fact);
 
           // Apply ArrDiseq Rule if diseq is between arrays
           if(fact[0][0].getType().isArray()) {
@@ -764,7 +718,7 @@ void TheoryArrays::check(Effort e) {
             if (!d_equalityEngine.hasTerm(bk)) {
               preRegisterTerm(bk);
             }
-            d_equalityEngine.addDisequality(ak, bk, fact);
+            d_equalityEngine.assertEquality(ak.eqNode(bk), false, fact);
             Trace("arrays-lem")<<"Arrays::addExtLemma "<< ak << " /= " << bk <<"\n";
             ++d_numExt;
           }
@@ -807,14 +761,11 @@ Node TheoryArrays::mkAnd(std::vector<TNode>& conjunctions)
   for (; i < conjunctions.size(); ++i) {
     t = conjunctions[i];
 
-    // Remove true node - represents axiomatically true assertion
-    if (t == d_true) continue;
-
     // Expand explanation resulting from propagating a ROW lemma
     if (t.getKind() == kind::OR) {
       if ((explained.find(t) == explained.end())) {
         Assert(t[1].getKind() == kind::EQUAL);
-        d_equalityEngine.explainDisequality(t[1][0], t[1][1], conjunctions);
+        d_equalityEngine.explainEquality(t[1][0], t[1][1], false, conjunctions);
         explained.insert(t);
       }
       continue;
@@ -949,7 +900,7 @@ void TheoryArrays::checkRIntro1(TNode a, TNode b)
     Node ni = nm->mkNode(kind::SELECT, s, s[1]);
     Assert(!d_equalityEngine.hasTerm(ni));
     preRegisterTerm(ni);
-    d_equalityEngine.addEquality(ni, s[2], d_true);
+    d_equalityEngine.assertEquality(ni.eqNode(s[2]), true, d_true);
   }
 }
 
@@ -1004,7 +955,7 @@ void TheoryArrays::mergeArrays(TNode a, TNode b)
       }
     }
 
-    d_mayEqualEqualityEngine.addEquality(a, b, d_true);
+    d_mayEqualEqualityEngine.assertEquality(a.eqNode(b), true, d_true);
 
     checkRowLemmas(a,b);
     checkRowLemmas(b,a);
@@ -1186,7 +1137,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
       if (!bjExists) {
         preRegisterTerm(bj);
       }
-      d_equalityEngine.addEquality(aj, bj, reason);
+      d_equalityEngine.assertEquality(aj.eqNode(bj), true, reason);
       ++d_numProp;
       return;
     }
@@ -1194,7 +1145,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
       Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::queueRowLemma: propagating i = j ("<<i<<", "<<j<<")\n";
       Node reason = nm->mkNode(kind::OR, i.eqNode(j), aj.eqNode(bj));
       d_permRef.push_back(reason);
-      d_equalityEngine.addEquality(i, j, reason);
+      d_equalityEngine.assertEquality(i.eqNode(j), true, reason);
       ++d_numProp;
       return;
     }
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index d18b3abde..88986ee7a 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -133,18 +133,8 @@ class TheoryArrays : public Theory {
 
   private:
 
-  // PPNotifyClass: dummy template class for d_ppEqualityEngine - notifications not used
-  class PPNotifyClass {
-  public:
-    bool notify(TNode propagation) { return true; }
-    void notify(TNode t1, TNode t2) { }
-  };
-
-  /** The notify class for d_ppEqualityEngine */
-  PPNotifyClass d_ppNotify;
-
   /** Equaltity engine */
-  uf::EqualityEngine<PPNotifyClass> d_ppEqualityEngine;
+  eq::EqualityEngine d_ppEqualityEngine;
 
   // List of facts learned by preprocessor - needed for permanent ref for benefit of d_ppEqualityEngine
   context::CDList<Node> d_ppFacts;
@@ -187,17 +177,8 @@ class TheoryArrays : public Theory {
 
   private:
 
-  class MayEqualNotifyClass {
-  public:
-    bool notify(TNode propagation) { return true; }
-    void notify(TNode t1, TNode t2) { }
-  };
-
-  /** The notify class for d_mayEqualEqualityEngine */
-  MayEqualNotifyClass d_mayEqualNotify;
-
   /** Equaltity engine for determining if two arrays might be equal */
-  uf::EqualityEngine<MayEqualNotifyClass> d_mayEqualEqualityEngine;
+  eq::EqualityEngine d_mayEqualEqualityEngine;
 
   public:
 
@@ -238,37 +219,57 @@ class TheoryArrays : public Theory {
   private:
 
   // NotifyClass: template helper class for d_equalityEngine - handles call-back from congruence closure module
-  class NotifyClass {
+  class NotifyClass : public eq::EqualityEngineNotify {
     TheoryArrays& d_arrays;
   public:
     NotifyClass(TheoryArrays& arrays): d_arrays(arrays) {}
 
-    bool notify(TNode propagation) {
-      Debug("arrays") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::notify(" << propagation << ")" << std::endl;
+    bool eqNotifyTriggerEquality(TNode equality, bool value) {
+      Debug("arrays") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false") << ")" << std::endl;
       // Just forward to arrays
-      return d_arrays.propagate(propagation);
+      if (value) {
+        return d_arrays.propagate(equality);
+      } else {
+        return d_arrays.propagate(equality.notNode());
+      }
+    }
+
+    bool eqNotifyTriggerPredicate(TNode predicate, bool value) {
+      Unreachable();
     }
 
-    void notify(TNode t1, TNode t2) {
-      Debug("arrays") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::notify(" << t1 << ", " << t2 << ")" << std::endl;
-      if (t1.getType().isArray()) {
-        d_arrays.mergeArrays(t1, t2);
-        if (!d_arrays.isShared(t1) || !d_arrays.isShared(t2)) {
-          return;
+    bool eqNotifyTriggerTermEquality(TNode t1, TNode t2, bool value) {
+      Debug("arrays") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyTriggerTermEquality(" << t1 << ", " << t2 << ")" << std::endl;
+      if (value) {
+        if (t1.getType().isArray()) {
+          d_arrays.mergeArrays(t1, t2);
+          if (!d_arrays.isShared(t1) || !d_arrays.isShared(t2)) {
+            return true;
+          }
         }
+        // Propagate equality between shared terms
+        Node equality = Rewriter::rewriteEquality(theory::THEORY_UF, t1.eqNode(t2));
+        d_arrays.propagate(equality);
       }
-      // Propagate equality between shared terms
-      Node equality = Rewriter::rewriteEquality(theory::THEORY_UF, t1.eqNode(t2));
-      d_arrays.propagate(equality);
+      // TODO: implement negation propagation
+      return true;
     }
-  };
 
+    bool eqNotifyConstantTermMerge(TNode t1, TNode t2) {
+      Debug("arrays") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
+      if (Theory::theoryOf(t1) == THEORY_BOOL) {
+        return d_arrays.propagate(t1.iffNode(t2));
+      } else {
+        return d_arrays.propagate(t1.eqNode(t2));
+      }
+    }
+  };
 
   /** The notify class for d_equalityEngine */
   NotifyClass d_notify;
 
   /** Equaltity engine */
-  uf::EqualityEngine<NotifyClass> d_equalityEngine;
+  eq::EqualityEngine d_equalityEngine;
 
   // Are we in conflict?
   context::CDO<bool> d_conflict;