From 77b7103d7796e11c3ebf1d80e09355ed0587ffdc Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 2 Jul 2020 05:48:09 -0500 Subject: [PATCH] (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. --- src/expr/CMakeLists.txt | 2 + src/expr/proof_node_updater.cpp | 82 +++++++++++++++++++++++++++++++++ src/expr/proof_node_updater.h | 79 +++++++++++++++++++++++++++++++ 3 files changed, 163 insertions(+) create mode 100644 src/expr/proof_node_updater.cpp create mode 100644 src/expr/proof_node_updater.h 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 pf) +{ + Trace("pf-process") << "ProofNodeUpdater::process" << std::endl; + std::unordered_set visited; + std::unordered_set::iterator it; + std::vector 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>& cc = cur->getChildren(); + std::vector ccn; + for (const std::shared_ptr& 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 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>& ccp = cur->getChildren(); + // now, process children + for (const std::shared_ptr& 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 +#include + +#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& children, + const std::vector& 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 pf); + + private: + /** The proof node manager */ + ProofNodeManager* d_pnm; + /** The callback */ + ProofNodeUpdaterCallback& d_cb; +}; + +} // namespace CVC4 + +#endif -- 2.30.2