some changes to the uf engine

* dramatically less terms to manage by doing reflexivity semantically
* fixes the problem clark had with not detecting inconsistencies with shared terms
i'm not sure what's the performance impact, but this is so much better and we'll deal with performance later

2 files changed, 36 insertions, 11 deletions

diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 96c8e8b59..2ffb72d91 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -147,9 +147,9 @@ EqualityNodeId EqualityEngine::newApplicationNode(TNode original, EqualityNodeId
     Debug("equality") << d_name << "::eq::newApplicationNode(" << original << ", " << t1 << ", " << t2 << "): no lookup, setting up" << std::endl;
     // Mark the normalization to the lookup
     storeApplicationLookup(funNormalized, funId);
-    // If an equality, we do some extra reasoning 
-    if (isEquality && d_isConstant[t1ClassId] && d_isConstant[t2ClassId]) {
-      if (t1ClassId != t2ClassId) {
+    // If an equality over constants we merge to false 
+    if (isEquality) {
+      if (d_isConstant[t1ClassId] && d_isConstant[t2ClassId] && t1ClassId != t2ClassId) {
         Debug("equality") << d_name << "::eq::newApplicationNode(" << original << ", " << t1 << ", " << t2 << "): got constants" << std::endl;
         Assert(d_nodes[funId].getKind() == kind::EQUAL);
         enqueue(MergeCandidate(funId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null()));
@@ -161,6 +161,9 @@ EqualityNodeId EqualityEngine::newApplicationNode(TNode original, EqualityNodeId
           enqueue(MergeCandidate(symmFunId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null()));              
         }
       }
+      if (t1ClassId == t2ClassId) {
+        enqueue(MergeCandidate(funId, d_trueId, MERGED_THROUGH_REFLEXIVITY, TNode::null()));
+      }
     }
   } else {
     // If it's there, we need to merge these two
@@ -343,9 +346,6 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason) {
     // Add equality between terms
     assertEqualityInternal(eq[0], eq[1], reason);
     propagate();
-    // Add eq = true for dis-equality propagation
-    assertEqualityInternal(eq, d_true, reason);
-    propagate();    
   } else {
     // If two terms are already dis-equal, don't assert anything
     if (hasTerm(eq[0]) && hasTerm(eq[1]) && areDisequal(eq[0], eq[1], false)) {
@@ -361,8 +361,6 @@ void EqualityEngine::assertEquality(TNode eq, bool polarity, TNode reason) {
 
     assertEqualityInternal(eq, d_false, reason);
     propagate();    
-    assertEqualityInternal(eq[1].eqNode(eq[0]), d_false, reason);
-    propagate();    
   
     if (d_done) {
       return;
@@ -557,8 +555,11 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
         } else {
           // There is no representative, so we can add one, we remove this when backtracking
           storeApplicationLookup(funNormalized, funId);
+          // Note: both checks below we don't need to do in the above case as the normalized lookup
+          //       has already been checked for this
           // Now, if we're constant and it's an equality, check if the other guy is also a constant
-          if (funNormalized.isEquality) {
+          if (fun.isEquality) {
+            // If the equation normalizes to two constants, it's disequal
             if (d_isConstant[aNormalized] && d_isConstant[bNormalized] && aNormalized != bNormalized) {
               Assert(d_nodes[funId].getKind() == kind::EQUAL);
               enqueue(MergeCandidate(funId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null()));
@@ -570,9 +571,14 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect
                 enqueue(MergeCandidate(symmFunId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null()));              
               }
             }
-          }          
+            // If the function normalizes to a = a, we merge it with true, we check that its not
+            // already there so as not to enqueue multiple times when several things get merged
+            if (aNormalized == bNormalized && getEqualityNode(funId).getFind() != d_trueId) {
+              enqueue(MergeCandidate(funId, d_trueId, MERGED_THROUGH_REFLEXIVITY, TNode::null()));                            
+            } 
+          }
         }
-   
+                  
         // Go to the next one in the use list
         currentUseId = useNode.getNext();
       }
@@ -953,6 +959,20 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
               Debug("equality") << d_name << "::eq::getExplanation(): adding: " << d_equalityEdges[currentEdge].getReason() << std::endl;
               equalities.push_back(d_equalityEdges[currentEdge].getReason());
               break;
+            case MERGED_THROUGH_REFLEXIVITY: {
+              // f(x1, x2) == f(y1, y2) because x1 = y1 and x2 = y2
+              Debug("equality") << d_name << "::eq::getExplanation(): due to reflexivity, going deeper" << std::endl;
+              EqualityNodeId eqId = currentNode == d_trueId ? edgeNode : currentNode;
+              const FunctionApplication& eq = d_applications[eqId].original;
+              Assert(eq.isEquality, "Must be an equality");
+              
+              // Explain why a = b constant
+              Debug("equality") << push;
+              getExplanation(eq.a, eq.b, equalities);
+              Debug("equality") << pop;
+              
+              break;              
+            }
             case MERGED_THROUGH_CONSTANTS: {
               // (a = b) == false because a and b are different constants
               Debug("equality") << d_name << "::eq::getExplanation(): due to constants, going deeper" << std::endl;
diff --git a/src/theory/uf/equality_engine_types.h b/src/theory/uf/equality_engine_types.h
index 056ee0b84..591b15bf4 100644
--- a/src/theory/uf/equality_engine_types.h
+++ b/src/theory/uf/equality_engine_types.h
@@ -65,6 +65,8 @@ enum MergeReasonType {
   MERGED_THROUGH_CONGRUENCE,
   /** Terms were merged due to application of pure equality */
   MERGED_THROUGH_EQUALITY,
+  /** Equality was merged to true, due to both sides of equality being in the same class */
+  MERGED_THROUGH_REFLEXIVITY,
   /** Equality was merged to false, due to both sides of equality being a constant */
   MERGED_THROUGH_CONSTANTS,
 };
@@ -77,6 +79,9 @@ inline std::ostream& operator << (std::ostream& out, MergeReasonType reason) {
   case MERGED_THROUGH_EQUALITY:
     out << "pure equality";
     break;
+  case MERGED_THROUGH_REFLEXIVITY:
+    out << "reflexivity";
+    break;
   case MERGED_THROUGH_CONSTANTS:
     out << "constants disequal";
     break;