diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-04-18 14:07:49 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-04-18 14:07:49 -0500 |
commit | 83e65b595123b2113ba81ebb942d2b320619f7a5 (patch) | |
tree | e958b60bcc49fb9699d877a0ef5915b9ee1caad4 /src/theory/uf | |
parent | d9a103f371cd800615b37fa378ad9d8b7681ee1c (diff) |
Less aggressive caching in equality engine when proofs are enabled (#2964)
Diffstat (limited to 'src/theory/uf')
-rw-r--r-- | src/theory/uf/equality_engine.cpp | 34 |
1 files changed, 24 insertions, 10 deletions
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; |