From: Andrew Reynolds Date: Mon, 19 Oct 2020 00:58:50 +0000 (-0500) Subject: (proof-new) Refactoring cyclic checks (#5291) X-Git-Tag: cvc5-1.0.0~2697 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=94e3d9a;p=cvc5.git (proof-new) Refactoring cyclic checks (#5291) This PR makes it so that cyclic checks are only performed eager when proofNewEagerChecking is true. It refactors the existing cyclic check in ProofNodeToSExpr to have a more consistent style, and adds a cyclic check to getFreeAssumptions. --- diff --git a/src/expr/proof_node_algorithm.cpp b/src/expr/proof_node_algorithm.cpp index 8f8813f41..b21bdec23 100644 --- a/src/expr/proof_node_algorithm.cpp +++ b/src/expr/proof_node_algorithm.cpp @@ -39,6 +39,7 @@ void getFreeAssumptionsMap( std::unordered_map visited; std::unordered_map::iterator it; std::vector> visit; + std::vector> traversing; // Maps a bound assumption to the number of bindings it is under // e.g. in (SCOPE (SCOPE (ASSUME x) (x y)) (y)), y would be mapped to 2 at // (ASSUME x), and x would be mapped to 1. @@ -68,10 +69,10 @@ void getFreeAssumptionsMap( const std::vector& cargs = cur->getArguments(); if (it == visited.end()) { - visited[cur.get()] = true; PfRule id = cur->getRule(); if (id == PfRule::ASSUME) { + visited[cur.get()] = true; Assert(cargs.size() == 1); Node f = cargs[0]; if (!scopeDepth.count(f)) @@ -89,36 +90,84 @@ void getFreeAssumptionsMap( scopeDepth[a] += 1; } // will need to unbind the variables below - visited[cur.get()] = false; - visit.push_back(cur); } // The following loop cannot be merged with the loop above because the // same subproof + visited[cur.get()] = false; + visit.push_back(cur); + traversing.push_back(cur); const std::vector>& cs = cur->getChildren(); for (const std::shared_ptr& cp : cs) { + if (std::find(traversing.begin(), traversing.end(), cp) + != traversing.end()) + { + Unhandled() << "getFreeAssumptionsMap: cyclic proof! (use " + "--proof-new-eager-checking)" + << std::endl; + } visit.push_back(cp); } } } else if (!it->second) { + Assert(!traversing.empty()); + traversing.pop_back(); visited[cur.get()] = true; - Assert(cur->getRule() == PfRule::SCOPE); - // unbind its assumptions - for (const Node& a : cargs) + if (cur->getRule() == PfRule::SCOPE) { - auto scopeCt = scopeDepth.find(a); - Assert(scopeCt != scopeDepth.end()); - scopeCt->second -= 1; - if (scopeCt->second == 0) + // unbind its assumptions + for (const Node& a : cargs) { - scopeDepth.erase(scopeCt); + auto scopeCt = scopeDepth.find(a); + Assert(scopeCt != scopeDepth.end()); + scopeCt->second -= 1; + if (scopeCt->second == 0) + { + scopeDepth.erase(scopeCt); + } } } } } while (!visit.empty()); } +bool containsSubproof(ProofNode* pn, ProofNode* pnc) +{ + std::unordered_set visited; + return containsSubproof(pn, pnc, visited); +} + +bool containsSubproof(ProofNode* pn, + ProofNode* pnc, + std::unordered_set& visited) +{ + std::unordered_map::iterator it; + std::vector visit; + visit.push_back(pn); + const ProofNode* cur; + while (!visit.empty()) + { + cur = visit.back(); + visit.pop_back(); + if (visited.find(cur) == visited.end()) + { + visited.insert(cur); + if (cur == pnc) + { + return true; + } + const std::vector>& children = + cur->getChildren(); + for (const std::shared_ptr& cp : children) + { + visit.push_back(cp.get()); + } + } + } + return false; +} + } // namespace expr } // namespace CVC4 diff --git a/src/expr/proof_node_algorithm.h b/src/expr/proof_node_algorithm.h index 71d29532f..d6bd1963c 100644 --- a/src/expr/proof_node_algorithm.h +++ b/src/expr/proof_node_algorithm.h @@ -53,6 +53,20 @@ void getFreeAssumptionsMap( std::shared_ptr pn, std::map>>& amap); +/** + * @return true if pn contains pnc. + */ +bool containsSubproof(ProofNode* pn, ProofNode* pnc); + +/** + * Same as above, with a visited cache. + * + * @return true if pn contains pnc. + */ +bool containsSubproof(ProofNode* pn, + ProofNode* pnc, + std::unordered_set& visited); + } // namespace expr } // namespace CVC4 diff --git a/src/expr/proof_node_manager.cpp b/src/expr/proof_node_manager.cpp index 8ed9779d3..c238f9e35 100644 --- a/src/expr/proof_node_manager.cpp +++ b/src/expr/proof_node_manager.cpp @@ -16,6 +16,7 @@ #include "expr/proof.h" #include "expr/proof_node_algorithm.h" +#include "options/smt_options.h" #include "theory/rewriter.h" using namespace CVC4::kind; @@ -300,23 +301,12 @@ bool ProofNodeManager::updateNodeInternal( { Assert(pn != nullptr); // ---------------- check for cyclic - std::unordered_map visited; - std::unordered_map::iterator it; - std::vector visit; - for (const std::shared_ptr& cp : children) + if (options::proofNewEagerChecking()) { - visit.push_back(cp.get()); - } - const ProofNode* cur; - while (!visit.empty()) - { - cur = visit.back(); - visit.pop_back(); - it = visited.find(cur); - if (it == visited.end()) + std::unordered_set visited; + for (const std::shared_ptr& cpc : children) { - visited[cur] = true; - if (cur == pn) + if (expr::containsSubproof(cpc.get(), pn, visited)) { std::stringstream ss; ss << "ProofNodeManager::updateNode: attempting to make cyclic proof! " @@ -334,10 +324,6 @@ bool ProofNodeManager::updateNodeInternal( } Unreachable() << ss.str(); } - for (const std::shared_ptr& cp : cur->d_children) - { - visit.push_back(cp.get()); - } } } // ---------------- end check for cyclic diff --git a/src/expr/proof_node_to_sexpr.cpp b/src/expr/proof_node_to_sexpr.cpp index db7fb1a6f..2dbb2a873 100644 --- a/src/expr/proof_node_to_sexpr.cpp +++ b/src/expr/proof_node_to_sexpr.cpp @@ -32,7 +32,7 @@ Node ProofNodeToSExpr::convertToSExpr(const ProofNode* pn) NodeManager* nm = NodeManager::currentNM(); std::map::iterator it; std::vector visit; - std::vector constructing; + std::vector traversing; const ProofNode* cur; visit.push_back(pn); do @@ -44,16 +44,17 @@ Node ProofNodeToSExpr::convertToSExpr(const ProofNode* pn) if (it == d_pnMap.end()) { d_pnMap[cur] = Node::null(); - constructing.push_back(cur); + traversing.push_back(cur); visit.push_back(cur); const std::vector>& pc = cur->getChildren(); for (const std::shared_ptr& cp : pc) { - if (std::find(constructing.begin(), constructing.end(), cp.get()) - != constructing.end()) + if (std::find(traversing.begin(), traversing.end(), cp.get()) + != traversing.end()) { - AlwaysAssert(false) - << "ProofNodeToSExpr::convertToSExpr: cyclic proof!" << std::endl; + Unhandled() << "ProofNodeToSExpr::convertToSExpr: cyclic proof! (use " + "--proof-new-eager-checking)" + << std::endl; return Node::null(); } visit.push_back(cp.get()); @@ -61,8 +62,8 @@ Node ProofNodeToSExpr::convertToSExpr(const ProofNode* pn) } else if (it->second.isNull()) { - Assert(!constructing.empty()); - constructing.pop_back(); + Assert(!traversing.empty()); + traversing.pop_back(); std::vector children; // add proof rule children.push_back(getOrMkPfRuleVariable(cur->getRule()));