Committing the work on equality engine, I need to see how it does on the regressions. New additions:

* areDisequal(x, y) -> areDisequal(x, y, needProof): when asking for a disequality you must say needProof if you will ask for an explanation later.
* propagation of shared dis-equalities (not yet complete, once case missing)
* changes to the theories that use it, authors should check up on the changes

2 files changed, 28 insertions, 15 deletions

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 44e362f90..15636fc72 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -86,12 +86,19 @@ TheoryArrays::TheoryArrays(context::Context* c, context::UserContext* u, OutputC
   d_true = NodeManager::currentNM()->mkConst<bool>(true);
   d_false = NodeManager::currentNM()->mkConst<bool>(false);
 
+  // The preprocessing congruence kinds
+  d_ppEqualityEngine.addFunctionKind(kind::SELECT);
+  d_ppEqualityEngine.addFunctionKind(kind::STORE);
+
+  // The mayequal congruence kinds
+  d_mayEqualEqualityEngine.addFunctionKind(kind::SELECT);
+  d_mayEqualEqualityEngine.addFunctionKind(kind::STORE);
+
   // The kinds we are treating as function application in congruence
   d_equalityEngine.addFunctionKind(kind::SELECT);
   if (d_ccStore) {
     d_equalityEngine.addFunctionKind(kind::STORE);
   }
-  d_equalityEngine.addFunctionKind(kind::EQUAL);
   if (d_useArrTable) {
     d_equalityEngine.addFunctionKind(kind::ARR_TABLE_FUN);
   }
@@ -118,12 +125,13 @@ TheoryArrays::~TheoryArrays() {
 
 Node TheoryArrays::ppRewrite(TNode term) {
   if (!d_preprocess) return term;
+  d_ppEqualityEngine.addTerm(term);
   switch (term.getKind()) {
     case kind::SELECT: {
       // select(store(a,i,v),j) = select(a,j)
       //    IF i != j
       if (term[0].getKind() == kind::STORE &&
-          (d_ppEqualityEngine.areDisequal(term[0][1], term[1]) ||
+          (d_ppEqualityEngine.areDisequal(term[0][1], term[1], false) ||
            (term[0][1].isConst() && term[1].isConst() && term[0][1] != term[1]))) {
         return NodeBuilder<2>(kind::SELECT) << term[0][0] << term[1];
       }
@@ -134,7 +142,7 @@ Node TheoryArrays::ppRewrite(TNode term) {
       //    IF i != j and j comes before i in the ordering
       if (term[0].getKind() == kind::STORE &&
           (term[1] < term[0][1]) &&
-          (d_ppEqualityEngine.areDisequal(term[1], term[0][1]) ||
+          (d_ppEqualityEngine.areDisequal(term[1], term[0][1], false) ||
            (term[0][1].isConst() && term[1].isConst() && term[0][1] != term[1]))) {
         Node inner = NodeBuilder<3>(kind::STORE) << term[0][0] << term[1] << term[2];
         Node outer = NodeBuilder<3>(kind::STORE) << inner << term[0][1] << term[0][2];
@@ -198,7 +206,7 @@ Node TheoryArrays::ppRewrite(TNode term) {
                 NodeBuilder<> hyp(kind::AND);
                 for (j = leftWrites - 1; j > i; --j) {
                   index_j = write_j[1];
-                  if (d_ppEqualityEngine.areDisequal(index_i, index_j) ||
+                  if (d_ppEqualityEngine.areDisequal(index_i, index_j, false) ||
                       (index_i.isConst() && index_j.isConst() && index_i != index_j)) {
                     continue;
                   }
@@ -374,6 +382,7 @@ void TheoryArrays::preRegisterTerm(TNode node)
   switch (node.getKind()) {
   case kind::EQUAL:
     // Add the trigger for equality
+    // NOTE: note that if the equality is true or false already, it might not be added
     d_equalityEngine.addTriggerEquality(node);
     break;
   case kind::SELECT: {
@@ -385,6 +394,9 @@ void TheoryArrays::preRegisterTerm(TNode node)
     // Reads
     TNode store = d_equalityEngine.getRepresentative(node[0]);
 
+    // The may equal needs the store
+    d_mayEqualEqualityEngine.addTerm(store);
+
     // Apply RIntro1 rule to any stores equal to store if not done already
     const CTNodeList* stores = d_infoMap.getStores(store);
     CTNodeList::const_iterator it = stores->begin();
@@ -460,7 +472,8 @@ void TheoryArrays::preRegisterTerm(TNode node)
     break;
   }
   // Invariant: preregistered terms are exactly the terms in the equality engine
-  Assert(d_equalityEngine.hasTerm(node));
+  // Disabled, see comment above for kind::EQUAL
+  // Assert(d_equalityEngine.hasTerm(node) || !d_equalityEngine.consistent());
 }
 
 
@@ -525,7 +538,7 @@ EqualityStatus TheoryArrays::getEqualityStatus(TNode a, TNode b) {
     // The terms are implied to be equal
     return EQUALITY_TRUE;
   }
-  if (d_equalityEngine.areDisequal(a, b)) {
+  if (d_equalityEngine.areDisequal(a, b, false)) {
     // The terms are implied to be dis-equal
     return EQUALITY_FALSE;
   }
@@ -576,10 +589,10 @@ void TheoryArrays::computeCareGraph()
 
         if (r1[0] != r2[0]) {
           // If arrays are known to be disequal, or cannot become equal, we can continue
-          Assert(d_equalityEngine.hasTerm(r1[0]) && d_equalityEngine.hasTerm(r2[0]));
+          Assert(d_mayEqualEqualityEngine.hasTerm(r1[0]) && d_mayEqualEqualityEngine.hasTerm(r2[0]));
           if (r1[0].getType() != r2[0].getType() ||
               (!d_mayEqualEqualityEngine.areEqual(r1[0], r2[0])) ||
-              d_equalityEngine.areDisequal(r1[0], r2[0])) {
+              d_equalityEngine.areDisequal(r1[0], r2[0], false)) {
             Debug("arrays::sharing") << "TheoryArrays::computeCareGraph(): arrays can't be equal, skipping" << std::endl;
             continue;
           }
@@ -704,7 +717,7 @@ void TheoryArrays::check(Effort e) {
       case kind::NOT:
         if (fact[0].getKind() == kind::SELECT) {
           d_equalityEngine.assertPredicate(fact[0], false, fact);
-        } else if (!d_equalityEngine.areDisequal(fact[0][0], fact[0][1])) {
+        } else if (!d_equalityEngine.areDisequal(fact[0][0], fact[0][1], false)) {
           // Assert the dis-equality
           d_equalityEngine.assertEquality(fact[0], false, fact);
 
@@ -1141,7 +1154,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
 
   // If propagating, check propagations
   if (d_propagateLemmas) {
-    if (d_equalityEngine.areDisequal(i,j)) {
+    if (d_equalityEngine.areDisequal(i,j,true)) {
       Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::queueRowLemma: propagating aj = bj ("<<aj<<", "<<bj<<")\n";
       Node aj_eq_bj = aj.eqNode(bj);
       Node i_eq_j = i.eqNode(j);
@@ -1157,7 +1170,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
       ++d_numProp;
       return;
     }
-    if (bothExist && d_equalityEngine.areDisequal(aj,bj)) {
+    if (bothExist && d_equalityEngine.areDisequal(aj,bj,true)) {
       Trace("arrays-lem") << spaces(getSatContext()->getLevel()) <<"Arrays::queueRowLemma: propagating i = j ("<<i<<", "<<j<<")\n";
       Node aj_eq_bj = aj.eqNode(bj);
       Node i_eq_j = i.eqNode(j);
@@ -1178,7 +1191,7 @@ void TheoryArrays::queueRowLemma(RowLemmaType lem)
   }
 
   // Prefer equality between indexes so as not to introduce new read terms
-  if (d_eagerIndexSplitting && !bothExist && !d_equalityEngine.areDisequal(i,j)) {
+  if (d_eagerIndexSplitting && !bothExist && !d_equalityEngine.areDisequal(i,j, false)) {
     Node split = d_valuation.ensureLiteral(i.eqNode(j));
     d_out->propagateAsDecision(split);
   }
diff --git a/src/theory/arrays/theory_arrays.h b/src/theory/arrays/theory_arrays.h
index 639b03df8..03d7e7d8d 100644
--- a/src/theory/arrays/theory_arrays.h
+++ b/src/theory/arrays/theory_arrays.h
@@ -228,7 +228,7 @@ class TheoryArrays : public Theory {
     NotifyClass(TheoryArrays& arrays): d_arrays(arrays) {}
 
     bool eqNotifyTriggerEquality(TNode equality, bool value) {
-      Debug("arrays") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false") << ")" << std::endl;
+      Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false") << ")" << std::endl;
       // Just forward to arrays
       if (value) {
         return d_arrays.propagate(equality);
@@ -242,7 +242,7 @@ class TheoryArrays : public Theory {
     }
 
     bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
-      Debug("arrays") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyTriggerTermEquality(" << t1 << ", " << t2 << ")" << std::endl;
+      Debug("arrays::propagate") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyTriggerTermEquality(" << t1 << ", " << t2 << ")" << std::endl;
       if (value) {
         if (t1.getType().isArray()) {
           d_arrays.mergeArrays(t1, t2);
@@ -259,7 +259,7 @@ class TheoryArrays : public Theory {
     }
 
     bool eqNotifyConstantTermMerge(TNode t1, TNode t2) {
-      Debug("arrays") << spaces(d_arrays.getSatContext()->getLevel()) << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
+      Debug("arrays::propagate") << 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 {