From: Andrew Reynolds Date: Wed, 4 Aug 2021 18:58:14 +0000 (-0500) Subject: Add containsAssumption proof utility (#6953) X-Git-Tag: cvc5-1.0.0~1409 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6db55eeefaf15f8aa1c08a73ad2a589da443cdc0;p=cvc5.git Add containsAssumption proof utility (#6953) Work towards making our policy for subproof merging safer. --- diff --git a/src/proof/proof_node_algorithm.cpp b/src/proof/proof_node_algorithm.cpp index 82ccc034f..5f56d785e 100644 --- a/src/proof/proof_node_algorithm.cpp +++ b/src/proof/proof_node_algorithm.cpp @@ -136,6 +136,71 @@ void getFreeAssumptionsMap( } while (!visit.empty()); } +bool containsAssumption(const ProofNode* pn, + std::unordered_map& caMap) +{ + std::unordered_map visited; + std::unordered_map::iterator it; + std::vector visit; + visit.push_back(pn); + bool foundAssumption = false; + const ProofNode* cur; + while (!visit.empty()) + { + cur = visit.back(); + visit.pop_back(); + // have we already computed? + it = caMap.find(cur); + if (it != caMap.end()) + { + // if cached, we set found assumption to true if applicable and continue + if (it->second) + { + foundAssumption = true; + } + continue; + } + it = visited.find(cur); + if (it == visited.end()) + { + PfRule r = cur->getRule(); + if (r == PfRule::ASSUME) + { + visited[cur] = true; + caMap[cur] = true; + foundAssumption = true; + } + else if (!foundAssumption) + { + // if we haven't found an assumption yet, recurse. Otherwise, we will + // not bother computing whether this subproof contains an assumption + // since we know its parent already contains one by another child. + visited[cur] = false; + visit.push_back(cur); + const std::vector>& children = + cur->getChildren(); + for (const std::shared_ptr& cp : children) + { + visit.push_back(cp.get()); + } + } + } + else if (!it->second) + { + visited[cur] = true; + // we contain an assumption if we've found an assumption in a child + caMap[cur] = foundAssumption; + } + } + return caMap[cur]; +} + +bool containsAssumption(const ProofNode* pn) +{ + std::unordered_map caMap; + return containsAssumption(pn, caMap); +} + bool containsSubproof(ProofNode* pn, ProofNode* pnc) { std::unordered_set visited; diff --git a/src/proof/proof_node_algorithm.h b/src/proof/proof_node_algorithm.h index 1ccefb0a2..f35a84c87 100644 --- a/src/proof/proof_node_algorithm.h +++ b/src/proof/proof_node_algorithm.h @@ -56,6 +56,27 @@ void getFreeAssumptionsMap( std::shared_ptr pn, std::map>>& amap); +/** + * Return true if pn contains a subproof whose rule is ASSUME. Notice that we + * do *not* distinguish between free vs. non-free assumptions in this call. + * This call involves at most a single dag traversal over the proof node. + * + * This call will partially populate caMap. In particular, it will only fill + * caMap for the proof nodes that were traversed up to where the first + * assumption in pn was found. + * + * @param pn The proof node. + * @param caMap Cache of results, mapping proof nodes to whether they contain + * assumptions. + * @return true if pn contains assumptions + */ +bool containsAssumption(const ProofNode* pn, + std::unordered_map& caMap); +/** + * Same as above, with an empty cache as the initial value of caMap. + */ +bool containsAssumption(const ProofNode* pn); + /** * @return true if pn contains pnc. */