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) 20092021 by the authors listed in the file AUTHORS 
8 

** in the toplevel source directory and their institutional affiliations. 
9 

** All rights reserved. See the file COPYING in the toplevel 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 */ 