From: Andrew Reynolds Date: Fri, 17 Apr 2020 16:57:07 +0000 (-0500) Subject: Add (context-dependent) Proof (#4323) X-Git-Tag: cvc5-1.0.0~3356 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c431160c5c9d706cd6424dc6c4b9b316ff8a5941;p=cvc5.git Add (context-dependent) Proof (#4323) A (context-dependent) collection of proof steps that are linked to together to form a ProofNode dag. Note that the name "Proof" is currently taken. I am calling this class "CDProof", although it is optionally context dependent. --- diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index f21241ef5..41df85455 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -33,6 +33,8 @@ libcvc4_add_sources( node_value.cpp node_value.h node_visitor.h + proof.cpp + proof.h proof_checker.cpp proof_checker.h proof_node.cpp diff --git a/src/expr/proof.cpp b/src/expr/proof.cpp new file mode 100644 index 000000000..6d2d70543 --- /dev/null +++ b/src/expr/proof.cpp @@ -0,0 +1,162 @@ +/********************* */ +/*! \file proof.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 + **/ + +#include "expr/proof.h" + +using namespace CVC4::kind; + +namespace CVC4 { + +CDProof::CDProof(ProofNodeManager* pnm, context::Context* c) + : d_manager(pnm), d_context(), d_nodes(c ? c : &d_context) +{ +} + +CDProof::~CDProof() {} + +std::shared_ptr CDProof::getProof(Node fact) const +{ + NodeProofNodeMap::iterator it = d_nodes.find(fact); + if (it != d_nodes.end()) + { + return (*it).second; + } + return nullptr; +} + +bool CDProof::addStep(Node expected, + PfRule id, + const std::vector& children, + const std::vector& args, + bool ensureChildren, + bool forceOverwrite) +{ + // we must provide expected + Assert(!expected.isNull()); + + NodeProofNodeMap::iterator it = d_nodes.find(expected); + if (it != d_nodes.end()) + { + if (!forceOverwrite + && ((*it).second->getId() != PfRule::ASSUME || id == PfRule::ASSUME)) + { + // we do not overwrite if forceOverwrite is false and the previously + // provided step was not an assumption, or if the currently provided step + // is a (duplicate) assumption + return true; + } + // we will overwrite the existing proof node by updating its contents below + } + + // collect the child proofs, for each premise + std::vector> pchildren; + for (const Node& c : children) + { + std::shared_ptr pc = getProof(c); + if (pc == nullptr) + { + if (ensureChildren) + { + // failed to get a proof for a child, fail + return false; + } + // otherwise, we initialize it as an assumption + std::vector pcargs = {c}; + std::vector> pcassume; + pc = d_manager->mkNode(PfRule::ASSUME, pcassume, pcargs, c); + // assumptions never fail to check + Assert(pc != nullptr); + d_nodes.insert(c, pc); + } + pchildren.push_back(pc); + } + + // create or update it + std::shared_ptr pthis; + if (it == d_nodes.end()) + { + pthis = d_manager->mkNode(id, pchildren, args, expected); + if (pthis == nullptr) + { + // failed to construct the node, perhaps due to a proof checking failure + return false; + } + d_nodes.insert(expected, pthis); + } + else + { + // update its value + pthis = (*it).second; + d_manager->updateNode(pthis.get(), id, pchildren, args); + } + // the result of the proof node should be expected + Assert(pthis->getResult() == expected); + return true; +} + +bool CDProof::addProof(ProofNode* pn, bool forceOverwrite) +{ + std::unordered_map visited; + std::unordered_map::iterator it; + std::vector visit; + ProofNode* cur; + Node curFact; + visit.push_back(pn); + bool retValue = true; + do + { + cur = visit.back(); + curFact = cur->getResult(); + visit.pop_back(); + it = visited.find(cur); + if (it == visited.end()) + { + // visit the children + visited[cur] = false; + visit.push_back(cur); + const std::vector>& cs = cur->getChildren(); + for (const std::shared_ptr& c : cs) + { + visit.push_back(c.get()); + } + } + else if (!it->second) + { + // we always call addStep, which may or may not overwrite the + // current step + std::vector pexp; + const std::vector>& cs = cur->getChildren(); + for (const std::shared_ptr& c : cs) + { + Assert(!c->getResult().isNull()); + pexp.push_back(c->getResult()); + } + // can ensure children at this point + bool res = addStep(curFact, + cur->getId(), + pexp, + cur->getArguments(), + true, + forceOverwrite); + // should always succeed + Assert(res); + retValue = retValue && res; + visited[cur] = true; + } + } while (!visit.empty()); + + return retValue; +} + +} // namespace CVC4 diff --git a/src/expr/proof.h b/src/expr/proof.h new file mode 100644 index 000000000..c3b9698ca --- /dev/null +++ b/src/expr/proof.h @@ -0,0 +1,196 @@ +/********************* */ +/*! \file proof.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 utility + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__EXPR__PROOF_H +#define CVC4__EXPR__PROOF_H + +#include +#include + +#include "context/cdhashmap.h" +#include "expr/node.h" +#include "expr/proof_node.h" +#include "expr/proof_node_manager.h" + +namespace CVC4 { + +/** + * A (context-dependent) proof. + * + * This maintains a context-dependent map from formulas to ProofNode shared + * pointers. When a step is added, it internally uses mutable ProofNode pointers + * to link the steps in the proof together. + * + * It is important to note that the premises of proof steps given to this class + * are *Node* not *ProofNode*. In other words, the user of this class does + * not have to manage ProofNode pointers while using this class. Instead, + * ProofNode is the final product of this class, via the getProof interface, + * which returns a ProofNode object that has linked together the proof steps + * added to this object. + * + * Its main interface is the function addStep, which registers a single + * step in the proof. Its interface is: + * addStep( , , , , ...... ) + * where conclusion is what to be proven, rule is an identifier, premises + * are the formulas that imply conclusion, and args are additional arguments to + * the proof rule application. The options include whether we ensure children + * proofs already exist for the premises and our policty for overwriting + * existing steps. + * + * As an example, let A, B, C, D be formulas represented by Nodes. If we + * call: + * - addStep( A, ID_A, { B, C }, {} ) + * - addStep( B, ID_B, { D }, {} ) + * - addStep( E, ID_E, {}, {} ) + * with default options, then getProof( A ) returns the ProofNode of the form: + * ID_A( ID_B( ASSUME( D ) ), ASSUME( C ) ) + * Notice that the above calls to addStep can be made in either order. The + * proof step for E was not involved in the proof of A. + * + * If the user wants to combine proofs, then a addProof interface is + * available. The method addProof can be seen as syntax sugar for making + * multiple calls to addStep. Continuing the above example, if we call: + * - addProof( F, ID_F( ASSUME( A ), ASSUME( E ) ) ) + * is the same as calling steps corresponding the steps in the provided proof + * bottom-up, starting from the leaves. + * --- addStep( A, ASSUME, {}, {}, true ) + * --- addStep( E, ASSUME, {}, {}, true ) + * --- addStep( F, ID_F, { A, E }, {}, true ) + * The fifth argument provided indicates that we want to ensure child proofs + * are already available for the step (see ensureChildren in addStep below). + * This will result in getProof( F ) returning: + * ID_F( ID_A( ID_B( ASSUME( D ) ), ASSUME( C ) ), ID_E() ) + * Notice that the proof of A by ID_A was not overwritten by ASSUME in the + * addStep call above. + * + * The policy for overwriting proof steps gives ASSUME a special status. An + * ASSUME step can be seen as a step whose justification has not yet been + * provided. Thus, it is always overwritten. Other proof rules are never + * overwritten, unless the argument forceOverwrite is true. + * + * As an another example, say that we call: + * - addStep( B, ID_B1 {}, {} ) + * - addStep( A, ID_A1, {B, C}, {} ) + * At this point, getProof( A ) returns: + * ID_A1( ID_B1(), ASSUME(C) ) + * Now, assume an additional call is made to addProof, where notice + * forceOverwrite is false by default: + * - addProof( D, ID_D( ID_A2( ID_B2(), ID_C() ) ) ) + * where assume ID_B2() and ID_C() prove B and C respectively. This call is + * equivalent to calling: + * --- addStep( B, ID_B2, {}, {}, true ) + * --- addStep( C, ID_C, {}, {}, true ) + * --- addStep( A, ID_A2, {B, C}, {}, true ) + * --- addStep( D, ID_D, {A}, {}, true ) + * Afterwards, getProof( D ) returns: + * ID_D( ID_A1( ID_B1(), ID_C() ) ) + * Notice that the steps with ID_A1 and ID_B1 were not overwritten by this call, + * whereas the assumption of C was overwritten by the proof ID_C(). Notice that + * the proof of D was completely traversed in addProof, despite encountering + * formulas, A and B, that were already given proof steps. + * + * This class requires a ProofNodeManager object, which is a trusted way of + * allocating ProofNode pointers. This manager may have an underlying checker, + * although this is not required. It also (optionally) takes a context c. + * If no context is provided, then this proof is context-independent. This + * is implemented internally by using a dummy context that is never pushed + * or popped. The map from Nodes to ProofNodes is context-dependent and is + * backtracked when its context backtracks. + * + * An important invariant of this object is that there exists (at most) one + * proof step for each Node. Thus, the ProofNode objects returned by this + * class share proofs for common subformulas, as guaranteed by the fact that + * Node objects have perfect sharing. + */ +class CDProof +{ + typedef context::CDHashMap, NodeHashFunction> + NodeProofNodeMap; + + public: + CDProof(ProofNodeManager* pnm, context::Context* c = nullptr); + ~CDProof(); + /** + * Get proof for fact, or nullptr if it does not exist. Notice that this call + * does *not* clone the ProofNode object. Hence, the returned proof may + * be updated by further calls to this class. The caller should call + * ProofNode::clone if they want to own it. + */ + std::shared_ptr getProof(Node fact) const; + /** Add step + * + * @param expected The intended conclusion of this proof step. This must be + * non-null. + * @param id The identifier for the proof step. + * @param children The antecendants of the proof step. Each children[i] should + * be a fact previously added as a conclusion of an addStep call when + * ensureChildren is true. + * @param args The arguments of the proof step. + * @param ensureChildren Whether we wish to ensure steps have been added + * for all nodes in children + * @param forceOverwrite Whether we wish to overwrite if a step for expected + * was already provided (via a previous call to addStep) + * @return The true if indeed the proof step proves expected, or + * false otherwise. The latter can happen if the proof has a different (or + * invalid) conclusion, or if one of the children does not have a proof and + * ensureChildren is true. + * + * This method may create proofs justified by ASSUME of the facts in + * children that have not already been proven when ensureChildren is false. + * Notice that ensureChildren should be true if the proof is being + * constructed is a strictly eager fashion (bottom up from its leaves), while + * ensureChildren should be false if the steps are added lazily or out + * of order. + * + * This method only overwrites proofs for facts that were added as + * steps with id ASSUME when forceOverwrite is false, and otherwise always + * overwrites an existing step if one was provided when forceOverwrite is + * true. + */ + bool addStep(Node expected, + PfRule id, + const std::vector& children, + const std::vector& args, + bool ensureChildren = false, + bool forceOverwrite = false); + /** Add proof + * + * @param pn The proof of the given fact. + * @param forceOverwrite Whether we wish to force overwriting if a step was + * already provided, for each node in the proof. + * @return true if all steps were successfully added to this class. If it + * returns true, it registers a copy of all of the subnodes of pn to this + * proof class. + * + * This method is implemented by calling addStep above for all subnodes + * of pn, traversed as a dag. This means that fresh ProofNode objects may be + * generated by this call, and further modifications to pn does not impact the + * internal data of this class. + */ + bool addProof(ProofNode* pn, bool forceOverwrite = false); + + protected: + /** The proof manager, used for allocating new ProofNode objects */ + ProofNodeManager* d_manager; + /** A dummy context used by this class if none is provided */ + context::Context d_context; + /** The nodes of the proof */ + NodeProofNodeMap d_nodes; +}; + +} // namespace CVC4 + +#endif /* CVC4__EXPR__PROOF_MANAGER_H */