diff options
Diffstat (limited to 'src/expr/proof_node_updater.h')
| -rw-r--r-- | src/expr/proof_node_updater.h | 164 |
1 files changed, 0 insertions, 164 deletions
diff --git a/src/expr/proof_node_updater.h b/src/expr/proof_node_updater.h deleted file mode 100644 index 215c61210..000000000 --- a/src/expr/proof_node_updater.h +++ /dev/null @@ -1,164 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andrew Reynolds, Haniel Barbosa, Gereon Kremer - * - * 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. - * **************************************************************************** - * - * A utility for updating proof nodes. - */ - -#include "cvc5_private.h" - -#ifndef CVC5__EXPR__PROOF_NODE_UPDATER_H -#define CVC5__EXPR__PROOF_NODE_UPDATER_H - -#include <map> -#include <memory> - -#include "expr/node.h" -#include "expr/proof_node.h" - -namespace cvc5 { - -class CDProof; -class ProofNode; -class ProofNodeManager; - -/** - * 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? - * - * @param pn the proof node that maybe should be updated - * @param fa the assumptions in scope - * @param continueUpdate whether we should continue recursively updating pn - * @return whether we should run the update method on pn - */ - virtual bool shouldUpdate(std::shared_ptr<ProofNode> pn, - const std::vector<Node>& fa, - bool& continueUpdate) = 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. - * - * If continueUpdate is set to false in this method, then the resulting - * proof (the proof of res in cdp) is *not* called back to update by the - * proof node updater, nor are its children recursed. Otherwise, by default, - * the proof node updater will continue updating the resulting proof and will - * recursively update its children. This is analogous to marking REWRITE_DONE - * in a rewrite response. - */ - virtual bool update(Node res, - PfRule id, - const std::vector<Node>& children, - const std::vector<Node>& args, - CDProof* cdp, - bool& continueUpdate); -}; - -/** - * 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. This update - * process is applied in a *pre-order* traversal. - */ -class ProofNodeUpdater -{ - public: - /** - * @param pnm The proof node manager we are using - * @param cb The callback to apply to each node - * @param mergeSubproofs Whether to automatically merge subproofs within - * the same SCOPE that prove the same fact. - * @param autoSym Whether intermediate CDProof objects passed to updater - * callbacks automatically introduce SYMM steps. - */ - ProofNodeUpdater(ProofNodeManager* pnm, - ProofNodeUpdaterCallback& cb, - bool mergeSubproofs = false, - bool autoSym = true); - /** - * Post-process, which performs the main post-processing technique described - * above. - */ - void process(std::shared_ptr<ProofNode> pf); - - /** - * Set free assumptions to freeAssumps. This indicates that we expect - * the proof we are processing to have free assumptions that are in - * freeAssumps. This enables checking when this is violated, which is - * expensive in general. It is not recommended that this method is called - * by default. - */ - void setDebugFreeAssumptions(const std::vector<Node>& freeAssumps); - - private: - /** The proof node manager */ - ProofNodeManager* d_pnm; - /** The callback */ - ProofNodeUpdaterCallback& d_cb; - /** - * Post-process, which performs the main post-processing technique described - * above. - * - * @param pf The proof to process - * @param fa The assumptions of the scope that fa is a subproof of with - * respect to the original proof. For example, if (SCOPE P :args (A B)), we - * may call this method on P with fa = { A, B }. - * @param traversing The list of proof nodes we are currently traversing - * beneath. This is used for checking for cycles in the overall proof. - */ - void processInternal(std::shared_ptr<ProofNode> pf, - const std::vector<Node>& fa, - std::vector<std::shared_ptr<ProofNode>>& traversing); - /** - * Update proof node cur based on the callback. This modifies curr using - * ProofNodeManager::updateNode based on the proof node constructed to - * replace it by the callback. Return true if cur was updated. If - * continueUpdate is updated to false, then cur is not updated further - * and its children are not traversed. - */ - bool runUpdate(std::shared_ptr<ProofNode> cur, - const std::vector<Node>& fa, - bool& continueUpdate); - /** - * Finalize the node cur. This is called at the moment that it is established - * that cur will appear in the final proof. We do any final debug checking - * and add it to the results cache resCache if we are merging subproofs. - */ - void runFinalize(std::shared_ptr<ProofNode> cur, - const std::vector<Node>& fa, - std::map<Node, std::shared_ptr<ProofNode>>& resCache); - /** Are we debugging free assumptions? */ - bool d_debugFreeAssumps; - /** The initial free assumptions */ - std::vector<Node> d_freeAssumps; - /** Whether we are merging subproofs */ - bool d_mergeSubproofs; - /** - * Whether intermediate CDProof objects passed to updater callbacks - * automatically introduce SYMM steps. - */ - bool d_autoSym; -}; - -} // namespace cvc5 - -#endif |