diff options
Diffstat (limited to 'src/proof/proof_node_algorithm.cpp')
| -rw-r--r-- | src/proof/proof_node_algorithm.cpp | 176 |
1 files changed, 176 insertions, 0 deletions
diff --git a/src/proof/proof_node_algorithm.cpp b/src/proof/proof_node_algorithm.cpp new file mode 100644 index 000000000..82ccc034f --- /dev/null +++ b/src/proof/proof_node_algorithm.cpp @@ -0,0 +1,176 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Haniel Barbosa + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Implementation of proof node algorithm utilities. + */ + +#include "proof/proof_node_algorithm.h" + +#include "proof/proof_node.h" + +namespace cvc5 { +namespace expr { + +void getFreeAssumptions(ProofNode* pn, std::vector<Node>& assump) +{ + std::map<Node, std::vector<std::shared_ptr<ProofNode>>> amap; + std::shared_ptr<ProofNode> spn = std::make_shared<ProofNode>( + pn->getRule(), pn->getChildren(), pn->getArguments()); + getFreeAssumptionsMap(spn, amap); + for (const std::pair<const Node, std::vector<std::shared_ptr<ProofNode>>>& p : + amap) + { + assump.push_back(p.first); + } +} + +void getFreeAssumptionsMap( + std::shared_ptr<ProofNode> pn, + std::map<Node, std::vector<std::shared_ptr<ProofNode>>>& amap) +{ + // proof should not be cyclic + // visited set false after preorder traversal, true after postorder traversal + 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. + // + // This map is used to track which nodes are in scope while traversing the + // DAG. The in-scope assumptions are keys in the map. They're removed when + // their binding count drops to zero. Let's annotate the above example to + // serve as an illustration: + // + // (SCOPE0 (SCOPE1 (ASSUME x) (x y)) (y)) + // + // This is how the map changes during the traversal: + // after previsiting SCOPE0: { y: 1 } + // after previsiting SCOPE1: { y: 2, x: 1 } + // at ASSUME: { y: 2, x: 1 } (so x is in scope!) + // after postvisiting SCOPE1: { y: 1 } + // after postvisiting SCOPE2: {} + // + std::unordered_map<Node, uint32_t> scopeDepth; + std::shared_ptr<ProofNode> cur; + visit.push_back(pn); + do + { + cur = visit.back(); + visit.pop_back(); + it = visited.find(cur.get()); + const std::vector<Node>& cargs = cur->getArguments(); + if (it == visited.end()) + { + PfRule id = cur->getRule(); + if (id == PfRule::ASSUME) + { + visited[cur.get()] = true; + Assert(cargs.size() == 1); + Node f = cargs[0]; + if (!scopeDepth.count(f)) + { + amap[f].push_back(cur); + } + } + else + { + if (id == PfRule::SCOPE) + { + // mark that its arguments are bound in the current scope + for (const Node& a : cargs) + { + scopeDepth[a] += 1; + } + // will need to unbind the variables below + } + // 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-eager-checking)" + << std::endl; + } + visit.push_back(cp); + } + } + } + else if (!it->second) + { + Assert(!traversing.empty()); + traversing.pop_back(); + visited[cur.get()] = true; + if (cur->getRule() == PfRule::SCOPE) + { + // unbind its assumptions + for (const Node& a : cargs) + { + 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 cvc5 |