src/expr/proof_node.h

   1 /*********************                                                        */
   2 /*! \file proof_node.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Proof node utility
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__EXPR__PROOF_NODE_H
  18 #define CVC4__EXPR__PROOF_NODE_H
  19
  20 #include <vector>
  21
  22 #include "expr/node.h"
  23 #include "expr/proof_rule.h"
  24
  25 namespace CVC4 {
  26
  27 class ProofNodeManager;
  28
  29 /** A node in a proof
  30  *
  31  * A ProofNode represents a single step in a proof. It contains:
  32  * (1) d_id, an identifier indicating the kind of inference,
  33  * (2) d_children, the child ProofNode objects indicating its premises,
  34  * (3) d_args, additional arguments used to determine the conclusion,
  35  * (4) d_proven, cache of the formula that this ProofNode proves.
  36  *
  37  * Overall, a ProofNode and its children form a directed acyclic graph.
  38  *
  39  * A ProofNode is partially mutable in that (1), (2) and (3) can be
  40  * modified. A motivating example of when this is useful is when a ProofNode
  41  * is established to be a "hole" for something to be proven later. On the other
  42  * hand, (4) is intended to be immutable.
  43  *
  44  * The method setValue is private and can be called by objects that manage
  45  * ProofNode objects in trusted ways that ensure that the node maintains
  46  * the invariant above. Furthermore, notice that this class is not responsible
  47  * for setting d_proven; this is done externally by a ProofNodeManager class.
  48  *
  49  * Notice that all fields of ProofNode are stored in ***Skolem form***. Their
  50  * correctness is checked in ***witness form*** (for details on this
  51  * terminology, see expr/skolem_manager.h). As a simple example, say a
  52  * theory solver has a term t, and wants to introduce a unit lemma (= k t)
  53  * where k is a fresh Skolem variable. It creates this variable via:
  54  *   k = SkolemManager::mkPurifySkolem(t,"k");
  55  * A checked ProofNode for the fact (= k t) then may have fields:
  56  *   d_rule := MACRO_SR_PRED_INTRO,
  57  *   d_children := {},
  58  *   d_args := {(= k t)}
  59  *   d_proven := (= k t).
  60  * Its justification via the rule MACRO_SR_PRED_INTRO (see documentation
  61  * in theory/builtin/proof_kinds) is in terms of the witness form of the
  62  * argument:
  63  *   (= (witness ((z T)) (= z t)) t)
  64  * which, by that rule's side condition, is such that:
  65  *   Rewriter::rewrite((= (witness ((z T)) (= z t)) t)) = true.
  66  * Notice that the correctness of the rule is justified here by rewriting
  67  * the witness form of (= k t). The conversion to/from witness form is
  68  * managed by ProofRuleChecker::check.
  69  *
  70  * An external proof checker is expected to formalize the ProofNode only in
  71  * terms of *witness* forms.
  72  *
  73  * However, the rest of CVC4 sees only the *Skolem* form of arguments and
  74  * conclusions in ProofNode, since this is what is used throughout CVC4.
  75  */
  76 class ProofNode
  77 {
  78   friend class ProofNodeManager;
  79
  80  public:
  81   ProofNode(PfRule id,
  82             const std::vector<std::shared_ptr<ProofNode>>& children,
  83             const std::vector<Node>& args);
  84   ~ProofNode() {}
  85   /** get the rule of this proof node */
  86   PfRule getRule() const;
  87   /** Get children */
  88   const std::vector<std::shared_ptr<ProofNode>>& getChildren() const;
  89   /** Get arguments */
  90   const std::vector<Node>& getArguments() const;
  91   /** get what this node proves, or the null node if this is an invalid proof */
  92   Node getResult() const;
  93   /**
  94    * Returns true if this is a closed proof (i.e. it has no free assumptions).
  95    */
  96   bool isClosed();
  97   /** Print debug on output strem os */
  98   void printDebug(std::ostream& os) const;
  99   /** Clone, create a deep copy of this */
 100   std::shared_ptr<ProofNode> clone() const;
 101
 102  private:
 103   /**
 104    * Set value, called to overwrite the contents of this ProofNode with the
 105    * given arguments.
 106    */
 107   void setValue(PfRule id,
 108                 const std::vector<std::shared_ptr<ProofNode>>& children,
 109                 const std::vector<Node>& args);
 110   /** The proof rule */
 111   PfRule d_rule;
 112   /** The children of this proof node */
 113   std::vector<std::shared_ptr<ProofNode>> d_children;
 114   /** arguments of this node */
 115   std::vector<Node> d_args;
 116   /** The cache of the fact that has been proven, modifiable by ProofChecker */
 117   Node d_proven;
 118 };
 119
 120 }  // namespace CVC4
 121
 122 #endif /* CVC4__EXPR__PROOF_NODE_H */