From e5f51e82aceda35642acd92b417bfeb74edfdcdd Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 15 Jun 2020 18:23:24 -0500 Subject: [PATCH] (proof-new) Update proof node, add proof node algorithm utility file. (#4600) Moves get free assumptions to a proof_node_algorithm.h/cpp file, analogous to node_algorithm.h/cpp. Adds a more general form of it, getFreeAssumptionsMap, which is required for future method ProofNodeManager::mkScope. --- src/expr/CMakeLists.txt | 2 + src/expr/proof_node.cpp | 93 ++++++----------------- src/expr/proof_node.h | 42 ++++++++--- src/expr/proof_node_algorithm.cpp | 118 ++++++++++++++++++++++++++++++ src/expr/proof_node_algorithm.h | 58 +++++++++++++++ 5 files changed, 229 insertions(+), 84 deletions(-) create mode 100644 src/expr/proof_node_algorithm.cpp create mode 100644 src/expr/proof_node_algorithm.h diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index 00eeaecea..5173c076d 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -47,6 +47,8 @@ libcvc4_add_sources( proof_generator.h proof_node.cpp proof_node.h + proof_node_algorithm.cpp + proof_node_algorithm.h proof_node_to_sexpr.cpp proof_node_to_sexpr.h proof_node_manager.cpp diff --git a/src/expr/proof_node.cpp b/src/expr/proof_node.cpp index b5e391049..6ef31b903 100644 --- a/src/expr/proof_node.cpp +++ b/src/expr/proof_node.cpp @@ -14,6 +14,9 @@ #include "expr/proof_node.h" +#include "expr/proof_node_algorithm.h" +#include "expr/proof_node_to_sexpr.h" + namespace CVC4 { ProofNode::ProofNode(PfRule id, @@ -34,71 +37,24 @@ const std::vector& ProofNode::getArguments() const { return d_args; } Node ProofNode::getResult() const { return d_proven; } -void ProofNode::getFreeAssumptions(std::vector& assump) const +bool ProofNode::isClosed() { - // visited set false after preorder traversal, true after postorder traversal - std::unordered_map visited; - std::unordered_map::iterator it; - std::vector visit; - // the current set of formulas bound by SCOPE - std::unordered_set currentScope; - const ProofNode* cur; - visit.push_back(this); - do - { - cur = visit.back(); - visit.pop_back(); - it = visited.find(cur); - if (it == visited.end()) - { - visited[cur] = true; - PfRule id = cur->getRule(); - if (id == PfRule::ASSUME) - { - Assert(cur->d_args.size() == 1); - Node f = cur->d_args[0]; - if (currentScope.find(f) == currentScope.end()) - { - assump.push_back(f); - } - } - else - { - if (id == PfRule::SCOPE) - { - // mark that its arguments are bound in the current scope - for (const Node& a : cur->d_args) - { - // should not have assumption shadowing - Assert(currentScope.find(a) != currentScope.end()); - currentScope.insert(a); - } - // will need to unbind the variables below - visited[cur] = false; - } - for (const std::shared_ptr& cp : cur->d_children) - { - visit.push_back(cp.get()); - } - } - } - else if (!it->second) - { - Assert(cur->getRule() == PfRule::SCOPE); - // unbind its assumptions - for (const Node& a : cur->d_args) - { - currentScope.erase(a); - } - } - } while (!visit.empty()); + std::vector assumps; + expr::getFreeAssumptions(this, assumps); + return assumps.empty(); } -bool ProofNode::isClosed() const +std::shared_ptr ProofNode::clone() const { - std::vector assumps; - getFreeAssumptions(assumps); - return assumps.empty(); + std::vector> cchildren; + for (const std::shared_ptr& cp : d_children) + { + cchildren.push_back(cp->clone()); + } + std::shared_ptr thisc = + std::make_shared(d_rule, cchildren, d_args); + thisc->d_proven = d_proven; + return thisc; } void ProofNode::setValue( @@ -113,17 +69,10 @@ void ProofNode::setValue( void ProofNode::printDebug(std::ostream& os) const { - os << "(" << d_rule; - for (const std::shared_ptr& c : d_children) - { - os << " "; - c->printDebug(os); - } - if (!d_args.empty()) - { - os << " :args " << d_args; - } - os << ")"; + // convert to sexpr and print + ProofNodeToSExpr pnts; + Node ps = pnts.convertToSExpr(this); + os << ps; } } // namespace CVC4 diff --git a/src/expr/proof_node.h b/src/expr/proof_node.h index c3f1719e7..41575200f 100644 --- a/src/expr/proof_node.h +++ b/src/expr/proof_node.h @@ -45,6 +45,33 @@ class ProofNodeManager; * ProofNode objects in trusted ways that ensure that the node maintains * the invariant above. Furthermore, notice that this class is not responsible * for setting d_proven; this is done externally by a ProofNodeManager class. + * + * Notice that all fields of ProofNode are stored in ***Skolem form***. Their + * correctness is checked in ***witness form*** (for details on this + * terminology, see expr/skolem_manager.h). As a simple example, say a + * theory solver has a term t, and wants to introduce a unit lemma (= k t) + * where k is a fresh Skolem variable. It creates this variable via: + * k = SkolemManager::mkPurifySkolem(t,"k"); + * A checked ProofNode for the fact (= k t) then may have fields: + * d_rule := MACRO_SR_PRED_INTRO, + * d_children := {}, + * d_args := {(= k t)} + * d_proven := (= k t). + * Its justification via the rule MACRO_SR_PRED_INTRO (see documentation + * in theory/builtin/proof_kinds) is in terms of the witness form of the + * argument: + * (= (witness ((z T)) (= z t)) t) + * which, by that rule's side condition, is such that: + * Rewriter::rewrite((= (witness ((z T)) (= z t)) t)) = true. + * Notice that the correctness of the rule is justified here by rewriting + * the witness form of (= k t). The conversion to/from witness form is + * managed by ProofRuleChecker::check. + * + * An external proof checker is expected to formalize the ProofNode only in + * terms of *witness* forms. + * + * However, the rest of CVC4 sees only the *Skolem* form of arguments and + * conclusions in ProofNode, since this is what is used throughout CVC4. */ class ProofNode { @@ -63,23 +90,14 @@ class ProofNode const std::vector& getArguments() const; /** get what this node proves, or the null node if this is an invalid proof */ Node getResult() const; - /** - * This adds to the vector assump all formulas that are "free assumptions" of - * the proof whose root is this ProofNode. A free assumption is a formula F - * that is an argument (in d_args) of a ProofNode whose kind is ASSUME, and - * that proof node is not beneath an application of SCOPE containing F as an - * argument. - * - * This traverses the structure of the dag represented by this ProofNode. - * Its implementation is analogous to expr::getFreeVariables. - */ - void getFreeAssumptions(std::vector& assump) const; /** * Returns true if this is a closed proof (i.e. it has no free assumptions). */ - bool isClosed() const; + bool isClosed(); /** Print debug on output strem os */ void printDebug(std::ostream& os) const; + /** Clone, create a deep copy of this */ + std::shared_ptr clone() const; private: /** diff --git a/src/expr/proof_node_algorithm.cpp b/src/expr/proof_node_algorithm.cpp new file mode 100644 index 000000000..1929088dc --- /dev/null +++ b/src/expr/proof_node_algorithm.cpp @@ -0,0 +1,118 @@ +/********************* */ +/*! \file proof_node_algorithm.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 algorithm utilities + **/ + +#include "expr/proof_node_algorithm.h" + +namespace CVC4 { +namespace expr { + +void getFreeAssumptions(ProofNode* pn, std::vector& assump) +{ + std::map> amap; + getFreeAssumptionsMap(pn, amap); + for (const std::pair>& p : amap) + { + assump.push_back(p.first); + } +} + +void getFreeAssumptionsMap(ProofNode* pn, + std::map>& amap) +{ + // proof should not be cyclic + // visited set false after preorder traversal, true after postorder traversal + std::unordered_map visited; + std::unordered_map::iterator it; + std::vector visit; + // Maps a bound assumption to the number of bindings it is under + // e.g. in (SCOPE (SCOPE (ASSUME x) (x y)) (y)), y would be mapped to 2 at + // (ASSUME x), and x would be mapped to 1. + // + // This map is used to track which nodes are in scope while traversing the + // DAG. The in-scope assumptions are keys in the map. They're removed when + // their binding count drops to zero. Let's annotate the above example to + // serve as an illustration: + // + // (SCOPE0 (SCOPE1 (ASSUME x) (x y)) (y)) + // + // This is how the map changes during the traversal: + // after previsiting SCOPE0: { y: 1 } + // after previsiting SCOPE1: { y: 2, x: 1 } + // at ASSUME: { y: 2, x: 1 } (so x is in scope!) + // after postvisiting SCOPE1: { y: 1 } + // after postvisiting SCOPE2: {} + // + std::unordered_map scopeDepth; + ProofNode* cur; + visit.push_back(pn); + do + { + cur = visit.back(); + visit.pop_back(); + it = visited.find(cur); + const std::vector& cargs = cur->getArguments(); + if (it == visited.end()) + { + visited[cur] = true; + PfRule id = cur->getRule(); + if (id == PfRule::ASSUME) + { + Assert(cargs.size() == 1); + Node f = cargs[0]; + if (!scopeDepth.count(f)) + { + amap[f].push_back(cur); + } + } + else + { + if (id == PfRule::SCOPE) + { + // mark that its arguments are bound in the current scope + for (const Node& a : cargs) + { + scopeDepth[a] += 1; + } + // will need to unbind the variables below + visited[cur] = false; + } + // The following loop cannot be merged with the loop above because the + // same subproof + const std::vector>& cs = cur->getChildren(); + for (const std::shared_ptr& cp : cs) + { + visit.push_back(cp.get()); + } + } + } + else if (!it->second) + { + Assert(cur->getRule() == PfRule::SCOPE); + // unbind its assumptions + for (const Node& a : cargs) + { + auto scopeCt = scopeDepth.find(a); + Assert(scopeCt != scopeDepth.end()); + scopeCt->second -= 1; + if (scopeCt->second == 0) + { + scopeDepth.erase(scopeCt); + } + } + } + } while (!visit.empty()); +} + +} // namespace expr +} // namespace CVC4 diff --git a/src/expr/proof_node_algorithm.h b/src/expr/proof_node_algorithm.h new file mode 100644 index 000000000..a82f52539 --- /dev/null +++ b/src/expr/proof_node_algorithm.h @@ -0,0 +1,58 @@ +/********************* */ +/*! \file proof_node_algorithm.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 algorithm utilities. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__EXPR__PROOF_NODE_ALGORITHM_H +#define CVC4__EXPR__PROOF_NODE_ALGORITHM_H + +#include + +#include "expr/node.h" +#include "expr/proof_node.h" + +namespace CVC4 { +namespace expr { + +/** + * This adds to the vector assump all formulas that are "free assumptions" of + * the proof whose root is ProofNode pn. A free assumption is a formula F + * that is an argument (in d_args) of a ProofNode whose kind is ASSUME, and + * that proof node is not beneath an application of SCOPE containing F as an + * argument. + * + * This traverses the structure of the dag represented by this ProofNode. + * Its implementation is analogous to expr::getFreeVariables. + * + * @param pn The proof node. + * @param assump The vector to add the free asumptions of pn to. + */ +void getFreeAssumptions(ProofNode* pn, std::vector& assump); +/** + * Same as above, but maps assumptions to the proof pointer(s) for that + * assumption. Notice that depending on how pn is constructed, there may be + * multiple ProofNode that are ASSUME proofs of the same assumption, which + * are each added to the range of the assumption. + * + * @param pn The proof node. + * @param amap The mapping to add the free asumptions of pn and their + * corresponding proof nodes to. + */ +void getFreeAssumptionsMap(ProofNode* pn, + std::map>& amap); + +} // namespace expr +} // namespace CVC4 + +#endif /* CVC4__EXPR__PROOF_NODE_ALGORITHM_H */ -- 2.30.2