diff options
-rw-r--r-- | src/proof/uf_proof.cpp | 2 | ||||
-rw-r--r-- | src/theory/uf/equality_engine.cpp | 34 |
2 files changed, 25 insertions, 11 deletions
diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp index 43a648da7..10823693d 100644 --- 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 148a5e427..3e321bf29 100644 --- 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; |