diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-02 05:48:09 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-07-02 05:48:09 -0500 |
commit | 77b7103d7796e11c3ebf1d80e09355ed0587ffdc (patch) | |
tree | c5a889a1e172ae77b04509e2aac2e8ae78997875 /src/expr/proof_node_updater.cpp | |
parent | e968ea45fd46ce6837d50b2893568872378171f1 (diff) |
(proof-new) Proof node updater (#4647)
Adds utility for updating proof nodes. The module for post-processing proof nodes in the SmtEngine for the sake of proof conversion to external formats will build on this utility.
Requires #4617.
Diffstat (limited to 'src/expr/proof_node_updater.cpp')
-rw-r--r-- | src/expr/proof_node_updater.cpp | 82 |
1 files changed, 82 insertions, 0 deletions
diff --git a/src/expr/proof_node_updater.cpp b/src/expr/proof_node_updater.cpp new file mode 100644 index 000000000..227be2122 --- /dev/null +++ b/src/expr/proof_node_updater.cpp @@ -0,0 +1,82 @@ +/********************* */ +/*! \file proof_node_updater.cpp + ** \verbatim + ** Top contributors (to current version): + ** Morgan Deters, Andrew Reynolds, Tim King + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 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.\endverbatim + ** + ** \brief Implementation of a utility for updating proof nodes + **/ + +#include "expr/proof_node_updater.h" + +#include "expr/lazy_proof.h" + + +namespace CVC4 { + +ProofNodeUpdaterCallback::ProofNodeUpdaterCallback() {} +ProofNodeUpdaterCallback::~ProofNodeUpdaterCallback() {} + +ProofNodeUpdater::ProofNodeUpdater(ProofNodeManager* pnm, + ProofNodeUpdaterCallback& cb) + : d_pnm(pnm), d_cb(cb) +{ +} + +void ProofNodeUpdater::process(std::shared_ptr<ProofNode> pf) +{ + Trace("pf-process") << "ProofNodeUpdater::process" << std::endl; + std::unordered_set<ProofNode*> visited; + std::unordered_set<ProofNode*>::iterator it; + std::vector<ProofNode*> visit; + ProofNode* cur; + visit.push_back(pf.get()); + do + { + cur = visit.back(); + it = visited.find(cur); + if (it == visited.end()) + { + visited.insert(cur); + // should it be updated? + if (d_cb.shouldUpdate(cur)) + { + PfRule id = cur->getRule(); + // use CDProof to open a scope for which the callback updates + CDProof cpf(d_pnm); + const std::vector<std::shared_ptr<ProofNode>>& cc = cur->getChildren(); + std::vector<Node> ccn; + for (const std::shared_ptr<ProofNode>& cp : cc) + { + Node cpres = cp->getResult(); + ccn.push_back(cpres); + // store in the proof + cpf.addProof(cp); + } + // only if the callback updated the node + if (d_cb.update(id, ccn, cur->getArguments(), &cpf)) + { + // build the proof, which should be closed + std::shared_ptr<ProofNode> npn = cpf.getProofFor(cur->getResult()); + Assert(npn->isClosed()); + // then, update the original proof node based on this one + d_pnm->updateNode(cur, npn.get()); + } + const std::vector<std::shared_ptr<ProofNode>>& ccp = cur->getChildren(); + // now, process children + for (const std::shared_ptr<ProofNode>& cp : ccp) + { + visit.push_back(cp.get()); + } + } + } + } while (!visit.empty()); + Trace("pf-process") << "ProofNodeUpdater::process: finished" << std::endl; +} + +} // namespace CVC4 |