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 /src/expr/proof_node_manager.cpp | |
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.
Diffstat (limited to 'src/expr/proof_node_manager.cpp')
-rw-r--r-- | src/expr/proof_node_manager.cpp | 89 |
1 files changed, 89 insertions, 0 deletions
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 |