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.
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
#include "expr/proof_node.h"
+#include "expr/proof_node_algorithm.h"
+#include "expr/proof_node_to_sexpr.h"
+
namespace CVC4 {
ProofNode::ProofNode(PfRule id,
Node ProofNode::getResult() const { return d_proven; }
-void ProofNode::getFreeAssumptions(std::vector<Node>& assump) const
+bool ProofNode::isClosed()
{
- // visited set false after preorder traversal, true after postorder traversal
- std::unordered_map<const ProofNode*, bool> visited;
- std::unordered_map<const ProofNode*, bool>::iterator it;
- std::vector<const ProofNode*> visit;
- // the current set of formulas bound by SCOPE
- std::unordered_set<Node, NodeHashFunction> 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<ProofNode>& 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<Node> assumps;
+ expr::getFreeAssumptions(this, assumps);
+ return assumps.empty();
}
-bool ProofNode::isClosed() const
+std::shared_ptr<ProofNode> ProofNode::clone() const
{
- std::vector<Node> assumps;
- getFreeAssumptions(assumps);
- return assumps.empty();
+ std::vector<std::shared_ptr<ProofNode>> cchildren;
+ for (const std::shared_ptr<ProofNode>& cp : d_children)
+ {
+ cchildren.push_back(cp->clone());
+ }
+ std::shared_ptr<ProofNode> thisc =
+ std::make_shared<ProofNode>(d_rule, cchildren, d_args);
+ thisc->d_proven = d_proven;
+ return thisc;
}
void ProofNode::setValue(
void ProofNode::printDebug(std::ostream& os) const
{
- os << "(" << d_rule;
- for (const std::shared_ptr<ProofNode>& 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
* 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
{
const std::vector<Node>& 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<Node>& 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<ProofNode> clone() const;
private:
/**
--- /dev/null
+/********************* */
+/*! \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<Node>& assump)
+{
+ std::map<Node, std::vector<ProofNode*>> amap;
+ getFreeAssumptionsMap(pn, amap);
+ for (const std::pair<const Node, std::vector<ProofNode*>>& p : amap)
+ {
+ assump.push_back(p.first);
+ }
+}
+
+void getFreeAssumptionsMap(ProofNode* pn,
+ std::map<Node, std::vector<ProofNode*>>& amap)
+{
+ // proof should not be cyclic
+ // visited set false after preorder traversal, true after postorder traversal
+ std::unordered_map<ProofNode*, bool> visited;
+ std::unordered_map<ProofNode*, bool>::iterator it;
+ std::vector<ProofNode*> 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<Node, uint32_t, NodeHashFunction> scopeDepth;
+ ProofNode* cur;
+ visit.push_back(pn);
+ do
+ {
+ cur = visit.back();
+ visit.pop_back();
+ it = visited.find(cur);
+ const std::vector<Node>& 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<std::shared_ptr<ProofNode>>& cs = cur->getChildren();
+ for (const std::shared_ptr<ProofNode>& 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
--- /dev/null
+/********************* */
+/*! \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 <vector>
+
+#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<Node>& 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<Node, std::vector<ProofNode*>>& amap);
+
+} // namespace expr
+} // namespace CVC4
+
+#endif /* CVC4__EXPR__PROOF_NODE_ALGORITHM_H */
projects / cvc5.git / commitdiff