diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-04-16 16:00:25 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-04-16 16:00:25 -0500 |
commit | 51a6be99deb292161b0469b70b4d8410bd7a975f (patch) | |
tree | 3675d28a6a7f44016f14679e274381f97780e517 | |
parent | f0e6c103304fc5c00c9bdfb699ad878ead5c66ed (diff) |
Add ProofNodeManager and ProofChecker (#4317)
Further work on adding core utilities for ProofNode objects, in support of the new proof infrastructure.
ProofNodeManager is analogous to NodeManager. It is a trusted way of generating only "well-formed" ProofNode pointers (according to a checker).
ProofChecker is analogous to TypeChecker. It is intended to be infrastructure for our internal proof checker.
This PR (and 1 more) is required to get to a place where Haniel and I can collaborate on further development for proofs.
-rw-r--r-- | src/expr/CMakeLists.txt | 4 | ||||
-rw-r--r-- | src/expr/proof_checker.cpp | 82 | ||||
-rw-r--r-- | src/expr/proof_checker.h | 94 | ||||
-rw-r--r-- | src/expr/proof_node.h | 4 | ||||
-rw-r--r-- | src/expr/proof_node_manager.cpp | 89 | ||||
-rw-r--r-- | src/expr/proof_node_manager.h | 117 |
6 files changed, 390 insertions, 0 deletions
diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index aa928fdb7..f21241ef5 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -33,8 +33,12 @@ libcvc4_add_sources( node_value.cpp node_value.h node_visitor.h + proof_checker.cpp + proof_checker.h proof_node.cpp proof_node.h + proof_node_manager.cpp + proof_node_manager.h proof_rule.cpp proof_rule.h symbol_table.cpp diff --git a/src/expr/proof_checker.cpp b/src/expr/proof_checker.cpp new file mode 100644 index 000000000..f4c275c47 --- /dev/null +++ b/src/expr/proof_checker.cpp @@ -0,0 +1,82 @@ +/********************* */ +/*! \file proof_checker.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 proof checker + **/ + +#include "expr/proof_checker.h" + +namespace CVC4 { + +Node ProofChecker::check(ProofNode* pn, Node expected) +{ + return check(pn->getId(), pn->getChildren(), pn->getArguments(), expected); +} + +Node ProofChecker::check( + PfRule id, + const std::vector<std::shared_ptr<ProofNode>>& children, + const std::vector<Node>& args, + Node expected) +{ + std::map<PfRule, ProofRuleChecker*>::iterator it = d_checker.find(id); + if (it == d_checker.end()) + { + // no checker for the rule + Trace("pfcheck") << "ProofChecker::check: no checker for rule " << id + << std::endl; + return Node::null(); + } + // check it with the corresponding checker + std::vector<Node> cchildren; + for (const std::shared_ptr<ProofNode>& pc : children) + { + Assert(pc != nullptr); + Node cres = pc->getResult(); + if (cres.isNull()) + { + Trace("pfcheck") + << "ProofChecker::check: child proof was invalid (null conclusion)" + << std::endl; + // should not have been able to create such a proof node + Assert(false); + return Node::null(); + } + cchildren.push_back(cres); + } + Node res = it->second->check(id, cchildren, args); + if (!expected.isNull() && res != expected) + { + Trace("pfcheck") + << "ProofChecker::check: result does not match expected value." + << std::endl; + Trace("pfcheck") << " result: " << res << std::endl; + Trace("pfcheck") << " expected: " << expected << std::endl; + // it did not match the given expectation, fail + return Node::null(); + } + return res; +} + +void ProofChecker::registerChecker(PfRule id, ProofRuleChecker* psc) +{ + std::map<PfRule, ProofRuleChecker*>::iterator it = d_checker.find(id); + if (it != d_checker.end()) + { + // checker is already provided + Notice() << "ProofChecker::registerChecker: checker already exists for " + << id << std::endl; + return; + } + d_checker[id] = psc; +} + +} // namespace CVC4 diff --git a/src/expr/proof_checker.h b/src/expr/proof_checker.h new file mode 100644 index 000000000..48b41453f --- /dev/null +++ b/src/expr/proof_checker.h @@ -0,0 +1,94 @@ +/********************* */ +/*! \file proof_checker.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 Proof checker utility + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__EXPR__PROOF_CHECKER_H +#define CVC4__EXPR__PROOF_CHECKER_H + +#include <map> + +#include "expr/node.h" +#include "expr/proof_node.h" + +namespace CVC4 { + +/** A virtual base class for checking a proof rule */ +class ProofRuleChecker +{ + public: + ProofRuleChecker() {} + virtual ~ProofRuleChecker() {} + /** + * This checks a single step in a proof. + * + * Return the formula that is proven by a proof node with the given id, + * premises and arguments, or null if such a proof node is not well-formed. + * + * @param id The id of the proof node to check + * @param children The premises of the proof node to check. These are nodes + * corresponding to the conclusion (ProofNode::getResult) of the children + * of the proof node we are checking. + * @param args The arguments of the proof node to check + * @return The conclusion of the proof node if successful or null if such a + * proof node is malformed. + */ + virtual Node check(PfRule id, + const std::vector<Node>& children, + const std::vector<Node>& args) = 0; +}; + +/** A class for checking proofs */ +class ProofChecker +{ + public: + ProofChecker() {} + ~ProofChecker() {} + /** + * Return the formula that is proven by proof node pn, or null if pn is not + * well-formed. If expected is non-null, then we return null if pn does not + * prove expected. + * + * @param pn The proof node to check + * @param expected The (optional) formula that is the expected conclusion of + * the proof node. + * @return The conclusion of the proof node if successful or null if the + * proof is malformed, or if no checker is available for id. + */ + Node check(ProofNode* pn, Node expected = Node::null()); + /** Same as above, with explicit arguments + * + * @param id The id of the proof node to check + * @param children The children of the proof node to check + * @param args The arguments of the proof node to check + * @param expected The (optional) formula that is the expected conclusion of + * the proof node. + * @return The conclusion of the proof node if successful or null if the + * proof is malformed, or if no checker is available for id. + */ + Node check(PfRule id, + const std::vector<std::shared_ptr<ProofNode>>& children, + const std::vector<Node>& args, + Node expected = Node::null()); + /** Indicate that psc is the checker for proof rule id */ + void registerChecker(PfRule id, ProofRuleChecker* psc); + + private: + /** Maps proof steps to their checker */ + std::map<PfRule, ProofRuleChecker*> d_checker; +}; + +} // namespace CVC4 + +#endif /* CVC4__EXPR__PROOF_CHECKER_H */ diff --git a/src/expr/proof_node.h b/src/expr/proof_node.h index 7bf7cb0b4..9a460c59b 100644 --- a/src/expr/proof_node.h +++ b/src/expr/proof_node.h @@ -24,6 +24,8 @@ namespace CVC4 { +class ProofNodeManager; + /** A node in a proof * * A ProofNode represents a single step in a proof. It contains: @@ -46,6 +48,8 @@ namespace CVC4 { */ class ProofNode { + friend class ProofNodeManager; + public: ProofNode(PfRule id, const std::vector<std::shared_ptr<ProofNode>>& children, diff --git a/src/expr/proof_node_manager.cpp b/src/expr/proof_node_manager.cpp new file mode 100644 index 000000000..e2f5ca2dc --- /dev/null +++ b/src/expr/proof_node_manager.cpp @@ -0,0 +1,89 @@ +/********************* */ +/*! \file proof_node_manager.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 proof node manager + **/ + +#include "expr/proof_node_manager.h" + +using namespace CVC4::kind; + +namespace CVC4 { + +ProofNodeManager::ProofNodeManager(ProofChecker* pc) : d_checker(pc) {} + +std::shared_ptr<ProofNode> ProofNodeManager::mkNode( + PfRule id, + const std::vector<std::shared_ptr<ProofNode>>& children, + const std::vector<Node>& args, + Node expected) +{ + Node res = checkInternal(id, children, args, expected); + if (res.isNull()) + { + // if it was invalid, then we return the null node + return nullptr; + } + // otherwise construct the proof node and set its proven field + std::shared_ptr<ProofNode> pn = + std::make_shared<ProofNode>(id, children, args); + pn->d_proven = res; + return pn; +} + +bool ProofNodeManager::updateNode( + ProofNode* pn, + PfRule id, + const std::vector<std::shared_ptr<ProofNode>>& children, + const std::vector<Node>& args) +{ + // should have already computed what is proven + Assert(!pn->d_proven.isNull()) + << "ProofNodeManager::updateProofNode: invalid proof provided"; + // We expect to prove the same thing as before + Node res = checkInternal(id, children, args, pn->d_proven); + if (res.isNull()) + { + // if it was invalid, then we do not update + return false; + } + // we update its value + pn->setValue(id, children, args); + // proven field should already be the same as the result + Assert(res == pn->d_proven); + return true; +} + +Node ProofNodeManager::checkInternal( + PfRule id, + const std::vector<std::shared_ptr<ProofNode>>& children, + const std::vector<Node>& args, + Node expected) +{ + Node res; + if (d_checker) + { + // check with the checker, which takes expected as argument + res = d_checker->check(id, children, args, expected); + Assert(!res.isNull()) + << "ProofNodeManager::checkInternal: failed to check proof"; + } + else + { + // otherwise we trust the expected value, if it exists + Assert(!expected.isNull()) << "ProofNodeManager::checkInternal: no checker " + "or expected value provided"; + res = expected; + } + return res; +} + +} // namespace CVC4 diff --git a/src/expr/proof_node_manager.h b/src/expr/proof_node_manager.h new file mode 100644 index 000000000..17c5580bf --- /dev/null +++ b/src/expr/proof_node_manager.h @@ -0,0 +1,117 @@ +/********************* */ +/*! \file proof_node_manager.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 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 Proof node manager utility + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__EXPR__PROOF_NODE_MANAGER_H +#define CVC4__EXPR__PROOF_NODE_MANAGER_H + +#include <vector> + +#include "expr/proof_checker.h" +#include "expr/proof_node.h" + +namespace CVC4 { + +/** + * 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()); + /** + * 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); + + private: + /** The (optional) proof checker */ + ProofChecker* d_checker; + /** 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); +}; + +} // namespace CVC4 + +#endif /* CVC4__EXPR__PROOF_NODE_H */ |