diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-10-18 19:58:50 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-10-18 19:58:50 -0500 |
commit | 94e3d9a0c2a51fbfd44516113527f34ed2c13e44 (patch) | |
tree | fc3b5fbac632c53b83f3d103f2a653cbf41d48ea | |
parent | 912ada0fb5368f3420b455b8bc76e88db164c37c (diff) |
(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.
-rw-r--r-- | src/expr/proof_node_algorithm.cpp | 71 | ||||
-rw-r--r-- | src/expr/proof_node_algorithm.h | 14 | ||||
-rw-r--r-- | src/expr/proof_node_manager.cpp | 24 | ||||
-rw-r--r-- | src/expr/proof_node_to_sexpr.cpp | 17 |
4 files changed, 88 insertions, 38 deletions
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<ProofNode*, bool> visited; std::unordered_map<ProofNode*, bool>::iterator it; std::vector<std::shared_ptr<ProofNode>> visit; + std::vector<std::shared_ptr<ProofNode>> 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<Node>& 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<std::shared_ptr<ProofNode>>& cs = cur->getChildren(); for (const std::shared_ptr<ProofNode>& 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<const ProofNode*> visited; + return containsSubproof(pn, pnc, visited); +} + +bool containsSubproof(ProofNode* pn, + ProofNode* pnc, + std::unordered_set<const ProofNode*>& visited) +{ + std::unordered_map<const ProofNode*, bool>::iterator it; + std::vector<const ProofNode*> 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<std::shared_ptr<ProofNode>>& children = + cur->getChildren(); + for (const std::shared_ptr<ProofNode>& 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<ProofNode> pn, std::map<Node, std::vector<std::shared_ptr<ProofNode>>>& 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<const ProofNode*>& 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<const ProofNode*, bool> visited; - std::unordered_map<const ProofNode*, bool>::iterator it; - std::vector<const ProofNode*> visit; - for (const std::shared_ptr<ProofNode>& 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<const ProofNode*> visited; + for (const std::shared_ptr<ProofNode>& 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<ProofNode>& 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<const ProofNode*, Node>::iterator it; std::vector<const ProofNode*> visit; - std::vector<const ProofNode*> constructing; + std::vector<const ProofNode*> 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<std::shared_ptr<ProofNode>>& pc = cur->getChildren(); for (const std::shared_ptr<ProofNode>& 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<Node> children; // add proof rule children.push_back(getOrMkPfRuleVariable(cur->getRule())); |