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.
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
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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 */
namespace CVC4 {
+class ProofNodeManager;
+
/** A node in a proof
*
* A ProofNode represents a single step in a proof. It contains:
*/
class ProofNode
{
+ friend class ProofNodeManager;
+
public:
ProofNode(PfRule id,
const std::vector<std::shared_ptr<ProofNode>>& children,
--- /dev/null
+/********************* */
+/*! \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
--- /dev/null
+/********************* */
+/*! \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 */
projects / cvc5.git / commitdiff