From: Andrew Reynolds Date: Wed, 15 Apr 2020 22:09:40 +0000 (-0500) Subject: Add ProofNode data structure (#4311) X-Git-Tag: cvc5-1.0.0~3361 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=912b65006615fe4074cde54b080f48e3d6c12042;p=cvc5.git Add ProofNode data structure (#4311) 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). --- diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index a308e536c..aa928fdb7 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -33,6 +33,10 @@ libcvc4_add_sources( 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 diff --git a/src/expr/proof_node.cpp b/src/expr/proof_node.cpp new file mode 100644 index 000000000..94c175025 --- /dev/null +++ b/src/expr/proof_node.cpp @@ -0,0 +1,92 @@ +/********************* */ +/*! \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>& children, + const std::vector& args) +{ + setValue(id, children, args); +} + +PfRule ProofNode::getId() const { return d_id; } + +const std::vector>& ProofNode::getChildren() const +{ + return d_children; +} + +const std::vector& ProofNode::getArguments() const { return d_args; } + +Node ProofNode::getResult() const { return d_proven; } + +void ProofNode::getAssumptions(std::vector& assump) const +{ + std::unordered_set visited; + std::unordered_set::iterator it; + std::vector 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& cp : cur->d_children) + { + visit.push_back(cp.get()); + } + } + } + } while (!visit.empty()); +} + +void ProofNode::setValue( + PfRule id, + const std::vector>& children, + const std::vector& 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& c : d_children) + { + os << " "; + c->printDebug(os); + } + if (!d_args.empty()) + { + os << " :args " << d_args; + } + os << ")"; +} + +} // namespace CVC4 diff --git a/src/expr/proof_node.h b/src/expr/proof_node.h new file mode 100644 index 000000000..7bf7cb0b4 --- /dev/null +++ b/src/expr/proof_node.h @@ -0,0 +1,93 @@ +/********************* */ +/*! \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 + +#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>& children, + const std::vector& args); + ~ProofNode() {} + /** get the id of this proof node */ + PfRule getId() const; + /** Get children */ + const std::vector>& getChildren() const; + /** Get arguments */ + const std::vector& 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& 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>& children, + const std::vector& args); + /** The proof step */ + PfRule d_id; + /** The children of this proof node */ + std::vector> d_children; + /** arguments of this node */ + std::vector 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 */ diff --git a/src/expr/proof_rule.cpp b/src/expr/proof_rule.cpp new file mode 100644 index 000000000..2c10e09e6 --- /dev/null +++ b/src/expr/proof_rule.cpp @@ -0,0 +1,39 @@ +/********************* */ +/*! \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 + +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 diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h new file mode 100644 index 000000000..16f4ca971 --- /dev/null +++ b/src/expr/proof_rule.h @@ -0,0 +1,78 @@ +/********************* */ +/*! \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 + +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 "" 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 */