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.h | |
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.h')
-rw-r--r-- | src/expr/proof_node_updater.h | 79 |
1 files changed, 79 insertions, 0 deletions
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 |