1 

/********************* */ 
2 

/*! \file proof_node_manager.h 
3 

** \verbatim 
4 

** Top contributors (to current version): 
5 

** Andrew Reynolds, Haniel Barbosa, Gereon Kremer 
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 manager utility 
13 

**/ 
14 


15 

#include "cvc4_private.h" 
16 


17 

#ifndef CVC4__EXPR__PROOF_NODE_MANAGER_H 
18 

#define CVC4__EXPR__PROOF_NODE_MANAGER_H 
19 


20 

#include <vector> 
21 


22 

#include "expr/node.h" 
23 

#include "expr/proof_rule.h" 
24 


25 

namespace CVC4 { 
26 


27 

class ProofChecker; 
28 

class ProofNode; 
29 


30 

/** 
31 

* A manager for proof node objects. This is a trusted interface for creating 
32 

* and updating ProofNode objects. 
33 

* 
34 

* In more detail, we say a ProofNode is "wellformed (with respect to checker 
35 

* X)" if its d_proven field is nonnull, and corresponds to the formula that 
36 

* the ProofNode proves according to X. The ProofNodeManager class constructs 
37 

* and update nodes that are wellformed with respect to its underlying checker. 
38 

* 
39 

* If no checker is provided, then the ProofNodeManager assigns the d_proven 
40 

* field of ProofNode based on the provided "expected" argument in mkNode below, 
41 

* which must be provided in this case. 
42 

* 
43 

* The ProofNodeManager is used as a trusted way of updating ProofNode objects 
44 

* via updateNode below. In particular, this method leaves the d_proven field 
45 

* unchanged and updates (if possible) the remaining content of a given proof 
46 

* node. 
47 

* 
48 

* Notice that ProofNode objects are mutable, and hence this class does not 
49 

* cache the results of mkNode. A version of this class that caches 
50 

* immutable version of ProofNode objects could be built as an extension 
51 

* or layer on top of this class. 
52 

*/ 
53 

class ProofNodeManager 
54 

{ 
55 

public: 
56 

ProofNodeManager(ProofChecker* pc = nullptr); 
57 
962 
~ProofNodeManager() {} 
58 

/** 
59 

* This constructs a ProofNode with the given arguments. The expected 
60 

* argument, when provided, indicates the formula that the returned node 
61 

* is expected to prove. If we find that it does not, based on the underlying 
62 

* checker, this method returns nullptr. 
63 

* 
64 

* @param id The id of the proof node. 
65 

* @param children The children of the proof node. 
66 

* @param args The arguments of the proof node. 
67 

* @param expected (Optional) the expected conclusion of the proof node. 
68 

* @return the proof node, or nullptr if the given arguments do not 
69 

* consistute a proof of the expected conclusion according to the underlying 
70 

* checker, if both are provided. It also returns nullptr if neither the 
71 

* checker nor the expected field is provided, since in this case the 
72 

* conclusion is unknown. 
73 

*/ 
74 

std::shared_ptr<ProofNode> mkNode( 
75 

PfRule id, 
76 

const std::vector<std::shared_ptr<ProofNode>>& children, 
77 

const std::vector<Node>& args, 
78 

Node expected = Node::null()); 
79 

/** 
80 

* Make the proof node corresponding to the assumption of fact. 
81 

* 
82 

* @param fact The fact to assume. 
83 

* @return The ASSUME proof of fact. 
84 

*/ 
85 

std::shared_ptr<ProofNode> mkAssume(Node fact); 
86 

/** 
87 

* Make transitivity proof, where children contains one or more proofs of 
88 

* equalities that form an ordered chain. In other words, the vector children 
89 

* is a legal set of children for an application of TRANS. 
90 

*/ 
91 

std::shared_ptr<ProofNode> mkTrans( 
92 

const std::vector<std::shared_ptr<ProofNode>>& children, 
93 

Node expected = Node::null()); 
94 


95 

/** 
96 

* Make scope having body pf and arguments (assumptionstoclose) assumps. 
97 

* If ensureClosed is true, then this method throws an assertion failure if 
98 

* the returned proof is not closed. This is the case if a free assumption 
99 

* of pf is missing from the vector assumps. 
100 

* 
101 

* For conveinence, the proof pf may be modified to ensure that the overall 
102 

* result is closed. For instance, given input: 
103 

* pf = TRANS( ASSUME( x=y ), ASSUME( y=z ) ) 
104 

* assumps = { y=x, y=z } 
105 

* This method will modify pf to be: 
106 

* pf = TRANS( SYMM( ASSUME( y=x ) ), ASSUME( y=z ) ) 
107 

* so that y=x matches the free assumption. The returned proof is: 
108 

* SCOPE(TRANS( SYMM( ASSUME( y=x ) ), ASSUME( y=z ) ) :args { y=x, y=z }) 
109 

* 
110 

* When ensureClosed is true, duplicates are eliminated from assumps. The 
111 

* reason for this is due to performance, since in this method, assumps is 
112 

* converted to an unordered_set to do the above check and hence it is a 
113 

* convienient time to eliminate duplicate literals. 
114 

* 
115 

* Additionally, if both ensureClosed and doMinimize are true, assumps is 
116 

* updated to contain exactly the free asumptions of pf. This also includes 
117 

* having no duplicates. Furthermore, if assumps is empty after minimization, 
118 

* this method is a noop. 
119 

* 
120 

* In each case, the update vector assumps is passed as arguments to SCOPE. 
121 

* 
122 

* @param pf The body of the proof, 
123 

* @param assumps The assumptionstoclose of the scope, 
124 

* @param ensureClosed Whether to ensure that the proof is closed, 
125 

* @param doMinimize Whether to minimize assumptions. 
126 

* @param expected the node that the scope should prove. 
127 

* @return The scoped proof. 
128 

*/ 
129 

std::shared_ptr<ProofNode> mkScope(std::shared_ptr<ProofNode> pf, 
130 

std::vector<Node>& assumps, 
131 

bool ensureClosed = true, 
132 

bool doMinimize = false, 
133 

Node expected = Node::null()); 
134 

/** 
135 

* This method updates pn to be a proof of the form <id>( children, args ), 
136 

* while maintaining its d_proven field. This method returns false if this 
137 

* proof manager is using a checker, and we compute that the above proof 
138 

* is not a proof of the fact that pn previously proved. 
139 

* 
140 

* @param pn The proof node to update. 
141 

* @param id The updated id of the proof node. 
142 

* @param children The updated children of the proof node. 
143 

* @param args The updated arguments of the proof node. 
144 

* @return true if the update was successful. 
145 

* 
146 

* Notice that updateNode always returns true if there is no underlying 
147 

* checker. 
148 

*/ 
149 

bool updateNode(ProofNode* pn, 
150 

PfRule id, 
151 

const std::vector<std::shared_ptr<ProofNode>>& children, 
152 

const std::vector<Node>& args); 
153 

/** 
154 

* Update node pn to have the contents of pnr. It should be the case that 
155 

* pn and pnr prove the same fact, otherwise false is returned and pn is 
156 

* unchanged. 
157 

*/ 
158 

bool updateNode(ProofNode* pn, ProofNode* pnr); 
159 

/** Get the underlying proof checker */ 
160 

ProofChecker* getChecker() const; 
161 


162 

private: 
163 

/** The (optional) proof checker */ 
164 

ProofChecker* d_checker; 
165 

/** the true node */ 
166 

Node d_true; 
167 

/** Check internal 
168 

* 
169 

* This returns the result of proof checking a ProofNode with the provided 
170 

* arguments with an expected conclusion, which may not null if there is 
171 

* no expected conclusion. 
172 

* 
173 

* This throws an assertion error if we fail to check such a proof node, or 
174 

* if expected is provided (nonnull) and is different what is proven by the 
175 

* other arguments. 
176 

*/ 
177 

Node checkInternal(PfRule id, 
178 

const std::vector<std::shared_ptr<ProofNode>>& children, 
179 

const std::vector<Node>& args, 
180 

Node expected); 
181 

/** 
182 

* Update node internal, return true if successful. This is called by 
183 

* the update node methods above. The argument needsCheck is whether we 
184 

* need to check the correctness of the rule application. This is false 
185 

* for the updateNode routine where pnr is an (already checked) proof node. 
186 

*/ 
187 

bool updateNodeInternal( 
188 

ProofNode* pn, 
189 

PfRule id, 
190 

const std::vector<std::shared_ptr<ProofNode>>& children, 
191 

const std::vector<Node>& args, 
192 

bool needsCheck); 
193 

}; 
194 


195 

} // namespace CVC4 
196 


197 

#endif /* CVC4__EXPR__PROOF_NODE_H */ 