diff options
Diffstat (limited to 'src/expr/proof_node_manager.h')
| -rw-r--r-- | src/expr/proof_node_manager.h | 206 |
1 files changed, 0 insertions, 206 deletions
diff --git a/src/expr/proof_node_manager.h b/src/expr/proof_node_manager.h deleted file mode 100644 index 853d22de7..000000000 --- a/src/expr/proof_node_manager.h +++ /dev/null @@ -1,206 +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. - * **************************************************************************** - * - * Proof node manager utility. - */ - -#include "cvc5_private.h" - -#ifndef CVC5__EXPR__PROOF_NODE_MANAGER_H -#define CVC5__EXPR__PROOF_NODE_MANAGER_H - -#include <vector> - -#include "expr/node.h" -#include "expr/proof_rule.h" - -namespace cvc5 { - -class ProofChecker; -class ProofNode; - -/** - * A manager for proof node objects. This is a trusted interface for creating - * and updating ProofNode objects. - * - * In more detail, we say a ProofNode is "well-formed (with respect to checker - * X)" if its d_proven field is non-null, and corresponds to the formula that - * the ProofNode proves according to X. The ProofNodeManager class constructs - * and update nodes that are well-formed with respect to its underlying checker. - * - * If no checker is provided, then the ProofNodeManager assigns the d_proven - * field of ProofNode based on the provided "expected" argument in mkNode below, - * which must be provided in this case. - * - * The ProofNodeManager is used as a trusted way of updating ProofNode objects - * via updateNode below. In particular, this method leaves the d_proven field - * unchanged and updates (if possible) the remaining content of a given proof - * node. - * - * Notice that ProofNode objects are mutable, and hence this class does not - * cache the results of mkNode. A version of this class that caches - * immutable version of ProofNode objects could be built as an extension - * or layer on top of this class. - */ -class ProofNodeManager -{ - public: - ProofNodeManager(ProofChecker* pc = nullptr); - ~ProofNodeManager() {} - /** - * This constructs a ProofNode with the given arguments. The expected - * argument, when provided, indicates the formula that the returned node - * is expected to prove. If we find that it does not, based on the underlying - * checker, this method returns nullptr. - * - * @param id The id of the proof node. - * @param children The children of the proof node. - * @param args The arguments of the proof node. - * @param expected (Optional) the expected conclusion of the proof node. - * @return the proof node, or nullptr if the given arguments do not - * consistute a proof of the expected conclusion according to the underlying - * checker, if both are provided. It also returns nullptr if neither the - * checker nor the expected field is provided, since in this case the - * conclusion is unknown. - */ - std::shared_ptr<ProofNode> mkNode( - PfRule id, - const std::vector<std::shared_ptr<ProofNode>>& children, - const std::vector<Node>& args, - Node expected = Node::null()); - /** - * Make the proof node corresponding to the assumption of fact. - * - * @param fact The fact to assume. - * @return The ASSUME proof of fact. - */ - std::shared_ptr<ProofNode> mkAssume(Node fact); - /** - * Make transitivity proof, where children contains one or more proofs of - * equalities that form an ordered chain. In other words, the vector children - * is a legal set of children for an application of TRANS. - */ - std::shared_ptr<ProofNode> mkTrans( - const std::vector<std::shared_ptr<ProofNode>>& children, - Node expected = Node::null()); - - /** - * Make scope having body pf and arguments (assumptions-to-close) assumps. - * If ensureClosed is true, then this method throws an assertion failure if - * the returned proof is not closed. This is the case if a free assumption - * of pf is missing from the vector assumps. - * - * For conveinence, the proof pf may be modified to ensure that the overall - * result is closed. For instance, given input: - * pf = TRANS( ASSUME( x=y ), ASSUME( y=z ) ) - * assumps = { y=x, y=z } - * This method will modify pf to be: - * pf = TRANS( SYMM( ASSUME( y=x ) ), ASSUME( y=z ) ) - * so that y=x matches the free assumption. The returned proof is: - * SCOPE(TRANS( SYMM( ASSUME( y=x ) ), ASSUME( y=z ) ) :args { y=x, y=z }) - * - * When ensureClosed is true, duplicates are eliminated from assumps. The - * reason for this is due to performance, since in this method, assumps is - * converted to an unordered_set to do the above check and hence it is a - * convienient time to eliminate duplicate literals. - * - * Additionally, if both ensureClosed and doMinimize are true, assumps is - * updated to contain exactly the free asumptions of pf. This also includes - * having no duplicates. Furthermore, if assumps is empty after minimization, - * this method is a no-op. - * - * In each case, the update vector assumps is passed as arguments to SCOPE. - * - * @param pf The body of the proof, - * @param assumps The assumptions-to-close of the scope, - * @param ensureClosed Whether to ensure that the proof is closed, - * @param doMinimize Whether to minimize assumptions. - * @param expected the node that the scope should prove. - * @return The scoped proof. - */ - std::shared_ptr<ProofNode> mkScope(std::shared_ptr<ProofNode> pf, - std::vector<Node>& assumps, - bool ensureClosed = true, - bool doMinimize = false, - Node expected = Node::null()); - /** - * This method updates pn to be a proof of the form <id>( children, args ), - * while maintaining its d_proven field. This method returns false if this - * proof manager is using a checker, and we compute that the above proof - * is not a proof of the fact that pn previously proved. - * - * @param pn The proof node to update. - * @param id The updated id of the proof node. - * @param children The updated children of the proof node. - * @param args The updated arguments of the proof node. - * @return true if the update was successful. - * - * Notice that updateNode always returns true if there is no underlying - * checker. - */ - bool updateNode(ProofNode* pn, - PfRule id, - const std::vector<std::shared_ptr<ProofNode>>& children, - const std::vector<Node>& args); - /** - * Update node pn to have the contents of pnr. It should be the case that - * pn and pnr prove the same fact, otherwise false is returned and pn is - * unchanged. - */ - bool updateNode(ProofNode* pn, ProofNode* pnr); - /** Get the underlying proof checker */ - ProofChecker* getChecker() const; - /** - * Clone a proof node, which creates a deep copy of pn and returns it. The - * dag structure of pn is the same as that in the returned proof node. - * - * @param pn The proof node to clone - * @return the cloned proof node. - */ - std::shared_ptr<ProofNode> clone(std::shared_ptr<ProofNode> pn); - - private: - /** The (optional) proof checker */ - ProofChecker* d_checker; - /** the true node */ - Node d_true; - /** Check internal - * - * This returns the result of proof checking a ProofNode with the provided - * arguments with an expected conclusion, which may not null if there is - * no expected conclusion. - * - * This throws an assertion error if we fail to check such a proof node, or - * if expected is provided (non-null) and is different what is proven by the - * other arguments. - */ - Node checkInternal(PfRule id, - const std::vector<std::shared_ptr<ProofNode>>& children, - const std::vector<Node>& args, - Node expected); - /** - * Update node internal, return true if successful. This is called by - * the update node methods above. The argument needsCheck is whether we - * need to check the correctness of the rule application. This is false - * for the updateNode routine where pnr is an (already checked) proof node. - */ - bool updateNodeInternal( - ProofNode* pn, - PfRule id, - const std::vector<std::shared_ptr<ProofNode>>& children, - const std::vector<Node>& args, - bool needsCheck); -}; - -} // namespace cvc5 - -#endif /* CVC5__EXPR__PROOF_NODE_H */ |