This is the core data structure for proofs in the new proofs infrastructure. PfRule is a global enumeration of ids of proof nodes (analogous to Kind for Nodes).
node_value.cpp
node_value.h
node_visitor.h
+ proof_node.cpp
+ proof_node.h
+ proof_rule.cpp
+ proof_rule.h
symbol_table.cpp
symbol_table.h
term_canonize.cpp
--- /dev/null
+/********************* */
+/*! \file proof_node.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 utility
+ **/
+
+#include "expr/proof_node.h"
+
+namespace CVC4 {
+
+ProofNode::ProofNode(PfRule id,
+ const std::vector<std::shared_ptr<ProofNode>>& children,
+ const std::vector<Node>& args)
+{
+ setValue(id, children, args);
+}
+
+PfRule ProofNode::getId() const { return d_id; }
+
+const std::vector<std::shared_ptr<ProofNode>>& ProofNode::getChildren() const
+{
+ return d_children;
+}
+
+const std::vector<Node>& ProofNode::getArguments() const { return d_args; }
+
+Node ProofNode::getResult() const { return d_proven; }
+
+void ProofNode::getAssumptions(std::vector<Node>& assump) const
+{
+ std::unordered_set<const ProofNode*> visited;
+ std::unordered_set<const ProofNode*>::iterator it;
+ std::vector<const ProofNode*> visit;
+ const ProofNode* cur;
+ visit.push_back(this);
+ do
+ {
+ cur = visit.back();
+ visit.pop_back();
+ it = visited.find(cur);
+ if (it == visited.end())
+ {
+ visited.insert(cur);
+ if (cur->getId() == PfRule::ASSUME)
+ {
+ assump.push_back(cur->d_proven);
+ }
+ else
+ {
+ for (const std::shared_ptr<ProofNode>& cp : cur->d_children)
+ {
+ visit.push_back(cp.get());
+ }
+ }
+ }
+ } while (!visit.empty());
+}
+
+void ProofNode::setValue(
+ PfRule id,
+ const std::vector<std::shared_ptr<ProofNode>>& children,
+ const std::vector<Node>& args)
+{
+ d_id = id;
+ d_children = children;
+ d_args = args;
+}
+
+void ProofNode::printDebug(std::ostream& os) const
+{
+ os << "(" << d_id;
+ for (const std::shared_ptr<ProofNode>& c : d_children)
+ {
+ os << " ";
+ c->printDebug(os);
+ }
+ if (!d_args.empty())
+ {
+ os << " :args " << d_args;
+ }
+ os << ")";
+}
+
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file proof_node.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 utility
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__EXPR__PROOF_NODE_H
+#define CVC4__EXPR__PROOF_NODE_H
+
+#include <vector>
+
+#include "expr/node.h"
+#include "expr/proof_rule.h"
+
+namespace CVC4 {
+
+/** A node in a proof
+ *
+ * A ProofNode represents a single step in a proof. It contains:
+ * (1) d_id, an identifier indicating the kind of inference,
+ * (2) d_children, the child ProofNode objects indicating its premises,
+ * (3) d_args, additional arguments used to determine the conclusion,
+ * (4) d_proven, cache of the formula that this ProofNode proves.
+ *
+ * Overall, a ProofNode and its children form a directed acyclic graph.
+ *
+ * A ProofNode is partially mutable in that (1), (2) and (3) can be
+ * modified. A motivating example of when this is useful is when a ProofNode
+ * is established to be a "hole" for something to be proven later. On the other
+ * hand, (4) is intended to be immutable.
+ *
+ * The method setValue is private and can be called by objects that manage
+ * 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.
+ */
+class ProofNode
+{
+ public:
+ ProofNode(PfRule id,
+ const std::vector<std::shared_ptr<ProofNode>>& children,
+ const std::vector<Node>& args);
+ ~ProofNode() {}
+ /** get the id of this proof node */
+ PfRule getId() const;
+ /** Get children */
+ const std::vector<std::shared_ptr<ProofNode>>& getChildren() const;
+ /** Get arguments */
+ const std::vector<Node>& getArguments() const;
+ /** get what this node proves, or the null node if this is an invalid proof */
+ Node getResult() const;
+ /** Get assumptions
+ *
+ * This adds to the vector assump all formulas that are "assumptions" of the
+ * proof whose root is this ProofNode. An assumption is a formula that is an
+ * argument (in d_args) of a ProofNode whose kind is ASSUME. This traverses
+ * the structure of the dag represented by this ProofNode.
+ */
+ void getAssumptions(std::vector<Node>& assump) const;
+ /** Print debug on output strem os */
+ void printDebug(std::ostream& os) const;
+
+ private:
+ /**
+ * Set value, called to overwrite the contents of this ProofNode with the
+ * given arguments.
+ */
+ void setValue(PfRule id,
+ const std::vector<std::shared_ptr<ProofNode>>& children,
+ const std::vector<Node>& args);
+ /** The proof step */
+ PfRule d_id;
+ /** The children of this proof node */
+ std::vector<std::shared_ptr<ProofNode>> d_children;
+ /** arguments of this node */
+ std::vector<Node> d_args;
+ /** The cache of the fact that has been proven, modifiable by ProofChecker */
+ Node d_proven;
+};
+
+} // namespace CVC4
+
+#endif /* CVC4__EXPR__PROOF_NODE_H */
--- /dev/null
+/********************* */
+/*! \file proof_rule.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 rule
+ **/
+
+#include "expr/proof_rule.h"
+
+#include <iostream>
+
+namespace CVC4 {
+
+const char* toString(PfRule id)
+{
+ switch (id)
+ {
+ //================================================= Core rules
+ case PfRule::ASSUME: return "ASSUME";
+ //================================================= Unknown rule
+ case PfRule::UNKNOWN: return "UNKNOWN";
+ default: return "?";
+ }
+}
+
+std::ostream& operator<<(std::ostream& out, PfRule id)
+{
+ out << toString(id);
+ return out;
+}
+
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \file proof_rule.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 rule enumeration
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__EXPR__PROOF_RULE_H
+#define CVC4__EXPR__PROOF_RULE_H
+
+#include <iosfwd>
+
+namespace CVC4 {
+
+/**
+ * An enumeration for proof rules. This enumeration is analogous to Kind for
+ * Node objects. In the documentation below, P:F denotes a ProofNode that
+ * proves formula F.
+ *
+ * Conceptually, the following proof rules form a calculus whose target
+ * user is the Node-level theory solvers. This means that the rules below
+ * are designed to reason about, among other things, common operations on Node
+ * objects like Rewriter::rewrite or Node::substitute. It is intended to be
+ * translated or printed in other formats.
+ *
+ * The following PfRule values include core rules and those categorized by
+ * theory, including the theory of equality.
+ *
+ * The "core rules" include ASSUME, which represents an open leaf in a proof.
+ * The core rules additionally correspond to generic operations that are done
+ * internally on nodes, e.g. calling Rewriter::rewrite.
+ */
+enum class PfRule : uint32_t
+{
+ //================================================= Core rules
+ // ======== Assumption (a leaf)
+ // Children: none
+ // Arguments: (F)
+ // --------------
+ // Conclusion F
+ ASSUME,
+
+ //================================================= Unknown rule
+ UNKNOWN,
+};
+
+/**
+ * Converts a proof rule to a string. Note: This function is also used in
+ * `safe_print()`. Changing this function name or signature will result in
+ * `safe_print()` printing "<unsupported>" instead of the proper strings for
+ * the enum values.
+ *
+ * @param id The proof rule
+ * @return The name of the proof rule
+ */
+const char* toString(PfRule id);
+
+/**
+ * Writes a proof rule name to a stream.
+ *
+ * @param out The stream to write to
+ * @param id The proof rule to write to the stream
+ * @return The stream
+ */
+std::ostream& operator<<(std::ostream& out, PfRule id);
+
+} // namespace CVC4
+
+#endif /* CVC4__EXPR__PROOF_RULE_H */
projects / cvc5.git / commitdiff