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 | |
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')
-rw-r--r-- | src/expr/CMakeLists.txt | 2 | ||||
-rw-r--r-- | src/expr/proof_node_updater.cpp | 82 | ||||
-rw-r--r-- | src/expr/proof_node_updater.h | 79 |
3 files changed, 163 insertions, 0 deletions
diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index 5173c076d..b042b9352 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -53,6 +53,8 @@ libcvc4_add_sources( proof_node_to_sexpr.h proof_node_manager.cpp proof_node_manager.h + proof_node_updater.cpp + proof_node_updater.h proof_rule.cpp proof_rule.h proof_step_buffer.cpp 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 diff --git a/src/expr/proof_node_updater.h b/src/expr/proof_node_updater.h new file mode 100644 index 000000000..be7a120ee --- /dev/null +++ b/src/expr/proof_node_updater.h @@ -0,0 +1,79 @@ +/********************* */ +/*! \file proof_node_updater.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** 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 A utility for updating proof nodes + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__EXPR__PROOF_NODE_UPDATER_H +#define CVC4__EXPR__PROOF_NODE_UPDATER_H + +#include <map> +#include <unordered_set> + +#include "expr/proof.h" +#include "expr/proof_node.h" +#include "expr/proof_node_manager.h" + +namespace CVC4 { + +/** + * A virtual callback class for updating ProofNode. An example use case of this + * class is to eliminate a proof rule by expansion. + */ +class ProofNodeUpdaterCallback +{ + public: + ProofNodeUpdaterCallback(); + virtual ~ProofNodeUpdaterCallback(); + /** Should proof pn be updated? */ + virtual bool shouldUpdate(ProofNode* pn) = 0; + /** + * Update the proof rule application, store steps in cdp. Return true if + * the proof changed. It can be assumed that cdp contains proofs of each + * fact in children. + */ + virtual bool update(PfRule id, + const std::vector<Node>& children, + const std::vector<Node>& args, + CDProof* cdp) = 0; +}; + +/** + * A generic class for updating ProofNode. It is parameterized by a callback + * class. Its process method runs this callback on all subproofs of a provided + * ProofNode application that meet some criteria + * (ProofNodeUpdaterCallback::shouldUpdate) + * and overwrites them based on the update procedure of the callback + * (ProofNodeUpdaterCallback::update), which uses local CDProof objects that + * should be filled in the callback for each ProofNode to update. + */ +class ProofNodeUpdater +{ + public: + ProofNodeUpdater(ProofNodeManager* pnm, ProofNodeUpdaterCallback& cb); + /** + * Post-process, which performs the main post-processing technique described + * above. + */ + void process(std::shared_ptr<ProofNode> pf); + + private: + /** The proof node manager */ + ProofNodeManager* d_pnm; + /** The callback */ + ProofNodeUpdaterCallback& d_cb; +}; + +} // namespace CVC4 + +#endif |