GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/proof_node.h Lines: 3 3 100.0 %
Date: 2021-03-23 Branches: 2 4 50.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file proof_node.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Haniel Barbosa, Alex Ozdemir
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 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
class ProofNode;
29
30
// Alias for shared pointer to a proof node
31
using Pf = std::shared_ptr<ProofNode>;
32
33
struct ProofNodeHashFunction
34
{
35
  inline size_t operator()(std::shared_ptr<ProofNode> pfn) const;
36
}; /* struct ProofNodeHashFunction */
37
38
/** A node in a proof
39
 *
40
 * A ProofNode represents a single step in a proof. It contains:
41
 * (1) d_id, an identifier indicating the kind of inference,
42
 * (2) d_children, the child ProofNode objects indicating its premises,
43
 * (3) d_args, additional arguments used to determine the conclusion,
44
 * (4) d_proven, cache of the formula that this ProofNode proves.
45
 *
46
 * Overall, a ProofNode and its children form a directed acyclic graph.
47
 *
48
 * A ProofNode is partially mutable in that (1), (2) and (3) can be
49
 * modified. A motivating example of when this is useful is when a ProofNode
50
 * is established to be a "hole" for something to be proven later. On the other
51
 * hand, (4) is intended to be immutable.
52
 *
53
 * The method setValue is private and can be called by objects that manage
54
 * ProofNode objects in trusted ways that ensure that the node maintains
55
 * the invariant above. Furthermore, notice that this class is not responsible
56
 * for setting d_proven; this is done externally by a ProofNodeManager class.
57
 *
58
 * Notice that all fields of ProofNode are stored in ***Skolem form***. Their
59
 * correctness is checked in ***witness form*** (for details on this
60
 * terminology, see expr/skolem_manager.h). As a simple example, say a
61
 * theory solver has a term t, and wants to introduce a unit lemma (= k t)
62
 * where k is a fresh Skolem variable. It creates this variable via:
63
 *   k = SkolemManager::mkPurifySkolem(t,"k");
64
 * A checked ProofNode for the fact (= k t) then may have fields:
65
 *   d_rule := MACRO_SR_PRED_INTRO,
66
 *   d_children := {},
67
 *   d_args := {(= k t)}
68
 *   d_proven := (= k t).
69
 * Its justification via the rule MACRO_SR_PRED_INTRO (see documentation
70
 * in theory/builtin/proof_kinds) is in terms of the witness form of the
71
 * argument:
72
 *   (= (witness ((z T)) (= z t)) t)
73
 * which, by that rule's side condition, is such that:
74
 *   Rewriter::rewrite((= (witness ((z T)) (= z t)) t)) = true.
75
 * Notice that the correctness of the rule is justified here by rewriting
76
 * the witness form of (= k t). The conversion to/from witness form is
77
 * managed by ProofRuleChecker::check.
78
 *
79
 * An external proof checker is expected to formalize the ProofNode only in
80
 * terms of *witness* forms.
81
 *
82
 * However, the rest of CVC4 sees only the *Skolem* form of arguments and
83
 * conclusions in ProofNode, since this is what is used throughout CVC4.
84
 */
85
class ProofNode
86
{
87
  friend class ProofNodeManager;
88
89
 public:
90
  ProofNode(PfRule id,
91
            const std::vector<std::shared_ptr<ProofNode>>& children,
92
            const std::vector<Node>& args);
93
16262766
  ~ProofNode() {}
94
  /** get the rule of this proof node */
95
  PfRule getRule() const;
96
  /** Get children */
97
  const std::vector<std::shared_ptr<ProofNode>>& getChildren() const;
98
  /** Get arguments */
99
  const std::vector<Node>& getArguments() const;
100
  /** get what this node proves, or the null node if this is an invalid proof */
101
  Node getResult() const;
102
  /**
103
   * Returns true if this is a closed proof (i.e. it has no free assumptions).
104
   */
105
  bool isClosed();
106
  /** Print debug on output strem os */
107
  void printDebug(std::ostream& os) const;
108
  /** Clone, create a deep copy of this */
109
  std::shared_ptr<ProofNode> clone() const;
110
111
 private:
112
  /**
113
   * Set value, called to overwrite the contents of this ProofNode with the
114
   * given arguments.
115
   */
116
  void setValue(PfRule id,
117
                const std::vector<std::shared_ptr<ProofNode>>& children,
118
                const std::vector<Node>& args);
119
  /** The proof rule */
120
  PfRule d_rule;
121
  /** The children of this proof node */
122
  std::vector<std::shared_ptr<ProofNode>> d_children;
123
  /** arguments of this node */
124
  std::vector<Node> d_args;
125
  /** The cache of the fact that has been proven, modifiable by ProofChecker */
126
  Node d_proven;
127
};
128
129
1026969
inline size_t ProofNodeHashFunction::operator()(
130
    std::shared_ptr<ProofNode> pfn) const
131
{
132
1026969
  return pfn->getResult().getId() + static_cast<unsigned>(pfn->getRule());
133
}
134
135
/**
136
 * Serializes a given proof node to the given stream.
137
 *
138
 * @param out the output stream to use
139
 * @param pn the proof node to output to the stream
140
 * @return the stream
141
 */
142
std::ostream& operator<<(std::ostream& out, const ProofNode& pn);
143
144
}  // namespace CVC4
145
146
#endif /* CVC4__EXPR__PROOF_NODE_H */