Less aggressive caching in equality engine when proofs are enabled (#2964)

diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp
index 43a648da728359e0a1f5839d56c0a912ea0e3dea..10823693dabffce6d4a358f65bc29c2c92d82648 100644 (file)
--- a/src/proof/uf_proof.cpp
+++ b/src/proof/uf_proof.cpp
@@ -141,7 +141,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out,
 
     return Node();
   }
-
+  // TODO (#2965): improve this code, which is highly complicated.
   switch(pf.d_id) {
   case theory::eq::MERGED_THROUGH_CONGRUENCE: {
     Debug("pf::uf") << "\nok, looking at congruence:\n";

diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 148a5e427ac4d6726d8ec786e3bb3b95fc764241..3e321bf29965d44634d254ec522b332ec4ae6071 100644 (file)
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -1052,23 +1052,37 @@ void EqualityEngine::getExplanation(
   Trace("eq-exp") << d_name << "::eq::getExplanation(" << d_nodes[t1Id] << ","
                   << d_nodes[t2Id] << ") size = " << cache.size() << std::endl;
 
-  // We order the ids, since explaining t1 = t2 is the same as explaining
-  // t2 = t1.
-  std::pair<EqualityNodeId, EqualityNodeId> cacheKey = std::minmax(t1Id, t2Id);
-  std::map<std::pair<EqualityNodeId, EqualityNodeId>, EqProof*>::iterator it =
-      cache.find(cacheKey);
-  if (it != cache.end())
+  // determine if we have already computed the explanation.
+  std::pair<EqualityNodeId, EqualityNodeId> cacheKey;
+  std::map<std::pair<EqualityNodeId, EqualityNodeId>, EqProof*>::iterator it;
+  if (!eqp)
   {
-    // copy one level
-    if (eqp)
+    // If proofs are disabled, we order the ids, since explaining t1 = t2 is the
+    // same as explaining t2 = t1.
+    cacheKey = std::minmax(t1Id, t2Id);
+    it = cache.find(cacheKey);
+    if (it != cache.end())
+    {
+      return;
+    }
+  }
+  else
+  {
+    // If proofs are enabled, note that proofs are sensitive to the order of t1
+    // and t2, so we don't sort the ids in this case. TODO: Depending on how
+    // issue #2965 is resolved, we may be able to revisit this, if it is the
+    // case that proof/uf_proof.h,cpp is robust to equality ordering.
+    cacheKey = std::pair<EqualityNodeId, EqualityNodeId>(t1Id, t2Id);
+    it = cache.find(cacheKey);
+    if (it != cache.end())
     {
       if (it->second)
       {
-        eqp->d_node = it->second->d_node;
         eqp->d_id = it->second->d_id;
         eqp->d_children.insert(eqp->d_children.end(),
                                it->second->d_children.begin(),
                                it->second->d_children.end());
+        eqp->d_node = it->second->d_node;
       }
       else
       {
@@ -1077,8 +1091,8 @@ void EqualityEngine::getExplanation(
         Assert(eqp->d_id == MERGED_THROUGH_REFLEXIVITY);
         eqp->d_node = d_nodes[t1Id];
       }
+      return;
     }
-    return;
   }
   cache[cacheKey] = eqp;