diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-05-25 08:41:13 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-05-25 08:41:13 -0500 |
commit | 87a64143f02c919df14baeb3c1acdd1295df50e9 (patch) | |
tree | 8a60d9db3d7b37f5436caf456719d4fbc340ef98 /src/proof/proof_node_manager.h | |
parent | 23c30f6961f9b19d656a3fb513134ce6c50b82ac (diff) | |
parent | 8e1eac35d265eacfbeb5f16be61e5d4caf45d1af (diff) |
Merge branch 'master' into issue6453issue6453
Diffstat (limited to 'src/proof/proof_node_manager.h')
-rw-r--r-- | src/proof/proof_node_manager.h | 206 |
1 files changed, 206 insertions, 0 deletions
diff --git a/src/proof/proof_node_manager.h b/src/proof/proof_node_manager.h new file mode 100644 index 000000000..2fa7ed3e9 --- /dev/null +++ b/src/proof/proof_node_manager.h @@ -0,0 +1,206 @@ +/****************************************************************************** + * 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__PROOF__PROOF_NODE_MANAGER_H +#define CVC5__PROOF__PROOF_NODE_MANAGER_H + +#include <vector> + +#include "expr/node.h" +#include "proof/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__PROOF__PROOF_NODE_H */ |