diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-05-24 13:51:09 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-05-24 15:51:09 -0300 |
commit | bd33d20609999f6f847aeb63a42350aeb3041406 (patch) | |
tree | 8b4a3ccb0ab48b65bd70222dbfd572de8743bcd9 /src/proof/proof_node.h | |
parent | 1516e3b5d9436be86841a52002fc728fcd52dd34 (diff) |
Move proof utilities to src/proof/ (#6611)
This moves all generic proof utilites from src/expr/ and src/theory/ to src/proof/.
It also changes the include for term conversion proof generator to conv_proof_generator in preparation to rename this utility on a followup PR (to avoid confusion with the use of "Term").
Diffstat (limited to 'src/proof/proof_node.h')
-rw-r--r-- | src/proof/proof_node.h | 145 |
1 files changed, 145 insertions, 0 deletions
diff --git a/src/proof/proof_node.h b/src/proof/proof_node.h new file mode 100644 index 000000000..db82cc63d --- /dev/null +++ b/src/proof/proof_node.h @@ -0,0 +1,145 @@ +/****************************************************************************** + * Top contributors (to current version): + * Andrew Reynolds, Haniel Barbosa, Alex Ozdemir + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Proof node utility. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__PROOF__PROOF_NODE_H +#define CVC5__PROOF__PROOF_NODE_H + +#include <vector> + +#include "expr/node.h" +#include "proof/proof_rule.h" + +namespace cvc5 { + +class ProofNodeManager; +class ProofNode; + +// Alias for shared pointer to a proof node +using Pf = std::shared_ptr<ProofNode>; + +struct ProofNodeHashFunction +{ + inline size_t operator()(std::shared_ptr<ProofNode> pfn) const; +}; /* struct ProofNodeHashFunction */ + +/** 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. + * + * 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 cvc5 sees only the *Skolem* form of arguments and + * conclusions in ProofNode, since this is what is used throughout cvc5. + */ +class ProofNode +{ + friend class ProofNodeManager; + + public: + ProofNode(PfRule id, + const std::vector<std::shared_ptr<ProofNode>>& children, + const std::vector<Node>& args); + ~ProofNode() {} + /** get the rule of this proof node */ + PfRule getRule() 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; + /** + * Returns true if this is a closed proof (i.e. it has no free assumptions). + */ + bool isClosed(); + /** 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 rule */ + PfRule d_rule; + /** 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; +}; + +inline size_t ProofNodeHashFunction::operator()( + std::shared_ptr<ProofNode> pfn) const +{ + return pfn->getResult().getId() + static_cast<unsigned>(pfn->getRule()); +} + +/** + * Serializes a given proof node to the given stream. + * + * @param out the output stream to use + * @param pn the proof node to output to the stream + * @return the stream + */ +std::ostream& operator<<(std::ostream& out, const ProofNode& pn); + +} // namespace cvc5 + +#endif /* CVC5__PROOF__PROOF_NODE_H */ |