1 

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

/*! \file proof_post_processor.h 
3 

** \verbatim 
4 

** Top contributors (to current version): 
5 

** Andrew Reynolds, Haniel Barbosa 
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 The module for processing proof nodes 
13 

**/ 
14 


15 

#include "cvc4_private.h" 
16 


17 

#ifndef CVC4__SMT__PROOF_POST_PROCESSOR_H 
18 

#define CVC4__SMT__PROOF_POST_PROCESSOR_H 
19 


20 

#include <map> 
21 

#include <unordered_set> 
22 


23 

#include "expr/proof_node_updater.h" 
24 

#include "smt/witness_form.h" 
25 

#include "util/statistics_registry.h" 
26 

#include "util/stats_histogram.h" 
27 


28 

namespace CVC4 { 
29 


30 

class SmtEngine; 
31 


32 

namespace smt { 
33 


34 

/** 
35 

* A callback class used by SmtEngine for postprocessing proof nodes by 
36 

* connecting proofs of preprocessing, and expanding macro PfRule applications. 
37 

*/ 
38 

class ProofPostprocessCallback : public ProofNodeUpdaterCallback 
39 

{ 
40 

public: 
41 

ProofPostprocessCallback(ProofNodeManager* pnm, 
42 

SmtEngine* smte, 
43 

ProofGenerator* pppg); 
44 
962 
~ProofPostprocessCallback() {} 
45 

/** 
46 

* Initialize, called once for each new ProofNode to process. This initializes 
47 

* static information to be used by successive calls to update. 
48 

*/ 
49 

void initializeUpdate(); 
50 

/** 
51 

* Set eliminate rule, which adds rule to the list of rules we will eliminate 
52 

* during update. This adds rule to d_elimRules. Supported rules for 
53 

* elimination include MACRO_*, SUBS and REWRITE. Otherwise, this method 
54 

* has no effect. 
55 

*/ 
56 

void setEliminateRule(PfRule rule); 
57 

/** Should proof pn be updated? */ 
58 

bool shouldUpdate(std::shared_ptr<ProofNode> pn, 
59 

bool& continueUpdate) override; 
60 

/** Update the proof rule application. */ 
61 

bool update(Node res, 
62 

PfRule id, 
63 

const std::vector<Node>& children, 
64 

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

CDProof* cdp, 
66 

bool& continueUpdate) override; 
67 


68 

private: 
69 

/** Common constants */ 
70 

Node d_true; 
71 

/** The proof node manager */ 
72 

ProofNodeManager* d_pnm; 
73 

/** Pointer to the SmtEngine, which should have proofs enabled */ 
74 

SmtEngine* d_smte; 
75 

/** The preprocessing proof generator */ 
76 

ProofGenerator* d_pppg; 
77 

/** The witness form proof generator */ 
78 

WitnessFormGenerator d_wfpm; 
79 

/** The witness form assumptions used in the proof */ 
80 

std::vector<Node> d_wfAssumptions; 
81 

/** Kinds of proof rules we are eliminating */ 
82 

std::unordered_set<PfRule, PfRuleHashFunction> d_elimRules; 
83 

//reset at the begining of each update 
84 

/** Mapping assumptions to their proof from preprocessing */ 
85 

std::map<Node, std::shared_ptr<ProofNode> > d_assumpToProof; 
86 

//end reset at the begining of each update 
87 

/** 
88 

* Expand rules in the given application, add the expanded proof to cdp. 
89 

* The set of rules we expand is configured by calls to setEliminateRule 
90 

* above. This method calls update to perform possible postprocessing in the 
91 

* rules it introduces as a result of the expansion. 
92 

* 
93 

* @param id The rule of the application 
94 

* @param children The children of the application 
95 

* @param args The arguments of the application 
96 

* @param cdp The proof to add to 
97 

* @return The conclusion of the rule, or null if this rule is not eliminated. 
98 

*/ 
99 

Node expandMacros(PfRule id, 
100 

const std::vector<Node>& children, 
101 

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

CDProof* cdp); 
103 

/** 
104 

* Update the proof rule application, called during expand macros when 
105 

* we wish to apply the update method. This method has the same behavior 
106 

* as update apart from ignoring the continueUpdate flag. 
107 

*/ 
108 

bool updateInternal(Node res, 
109 

PfRule id, 
110 

const std::vector<Node>& children, 
111 

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

CDProof* cdp); 
113 

/** 
114 

* Add proof for witness form. This returns the equality t = toWitness(t) 
115 

* and ensures that the proof of this equality has been added to cdp. 
116 

* Notice the proof of this fact may have open assumptions of the form: 
117 

* k = toWitness(k) 
118 

* where k is a skolem. Furthermore, note that all open assumptions of this 
119 

* form are available via d_wfpm.getWitnessFormEqs() in the remainder of 
120 

* the lifetime of this class. 
121 

*/ 
122 

Node addProofForWitnessForm(Node t, CDProof* cdp); 
123 

/** 
124 

* Apply transivity if necessary for the arguments. The nodes in 
125 

* tchildren have been ordered such that they are legal arguments to TRANS. 
126 

* 
127 

* Returns the conclusion of the transitivity step, which is null if 
128 

* tchildren is empty. Also note if tchildren contains a single element, 
129 

* then no TRANS step is necessary to add to cdp. 
130 

* 
131 

* @param tchildren The children of a TRANS step 
132 

* @param cdp The proof to add the TRANS step to 
133 

* @return The conclusion of the TRANS step. 
134 

*/ 
135 

Node addProofForTrans(const std::vector<Node>& tchildren, CDProof* cdp); 
136 

/** 
137 

* Add proof for substitution step. Some substitutions are derived based 
138 

* on viewing a formula as a Boolean assignment (see MethodId::SB_LITERAL for 
139 

* example). This method ensures that the proof of var == subs exists 
140 

* in cdp, where var, subs were derived from BuiltinProofRuleChecker's 
141 

* getSubstitution method. 
142 

* 
143 

* @param var The variable of the substitution 
144 

* @param subs The substituted term 
145 

* @param assump The formula the substitution was derived from 
146 

* @param cdp The proof to add to 
147 

* @return var == subs, the conclusion of the substitution step. 
148 

*/ 
149 

Node addProofForSubsStep(Node var, Node subs, Node assump, CDProof* cdp); 
150 

/** Add eq (or its symmetry) to transivity children, if not reflexive */ 
151 

bool addToTransChildren(Node eq, 
152 

std::vector<Node>& tchildren, 
153 

bool isSymm = false); 
154 


155 

/** 
156 

* When given children and args lead to different sets of literals in a 
157 

* conclusion depending on whether macro resolution or chain resolution is 
158 

* applied, the literals that appear in the chain resolution result, but not 
159 

* in the macro resolution result, from now on "crowding literals", are 
160 

* literals removed implicitly by macro resolution. For example 
161 

* 
162 

* l0 v l0 v l0 v l1 v l2 ~l0 v l1 ~l1 
163 

* (1)  MACRO_RES 
164 

* l2 
165 

* 
166 

* but 
167 

* 
168 

* l0 v l0 v l0 v l1 v l2 ~l0 v l1 ~l1 
169 

* (2)  CHAIN_RES 
170 

* l0 v l0 v l1 v l2 
171 

* 
172 

* where l0 and l1 are crowding literals in the second proof. 
173 

* 
174 

* There are two views for how MACRO_RES implicitly removes the crowding 
175 

* literal, i.e., how MACRO_RES can be expanded into CHAIN_RES so that 
176 

* crowding literals are removed. The first is that (1) becomes 
177 

* 
178 

* l0 v l0 v l0 v l1 v l2 ~l0 v l1 ~l0 v l1 ~l0 v l1 ~l1 ~l1 ~l1 ~l1 
179 

*  CHAIN_RES 
180 

* l2 
181 

* 
182 

* via the repetition of the premise responsible for removing more than one 
183 

* occurrence of the crowding literal. The issue however is that this 
184 

* expansion is exponential. Note that (2) has two occurrences of l0 and one 
185 

* of l1 as crowding literals. However, by repeating ~l0 v l1 two times to 
186 

* remove l0, the clause ~l1, which would originally need to be repeated only 
187 

* one time, now has to be repeated two extra times on top of that one. With 
188 

* multiple crowding literals and their elimination depending on premises that 
189 

* themselves add crowding literals one can easily end up with resolution 
190 

* chains going from dozens to thousands of premises. Such examples do occur 
191 

* in practice, even in our regressions. 
192 

* 
193 

* The second way of expanding MACRO_RES, which avoids this exponential 
194 

* behavior, is so that (1) becomes 
195 

* 
196 

* l0 v l0 v l0 v l1 v l2 
197 

* (4)  FACTORING 
198 

* l0 v l1 v l2 ~l0 v l1 
199 

*  CHAIN_RES 
200 

* l1 v l1 v l2 
201 

*  FACTORING 
202 

* l1 v l2 ~l1 
203 

*  CHAIN_RES 
204 

* l2 
205 

* 
206 

* This method first determines what are the crowding literals by checking 
207 

* what literals occur in clauseLits that do not occur in targetClauseLits 
208 

* (the latter contains the literals from the original MACRO_RES conclusion 
209 

* while the former the literals from a direct application of CHAIN_RES). Then 
210 

* it builds a proof such as (4) and adds the steps to cdp. The final 
211 

* conclusion is returned. 
212 

* 
213 

* Note that in the example the CHAIN_RES steps introduced had only two 
214 

* premises, and could thus be replaced by a RESOLUTION step, but since we 
215 

* general there can be more than two premises we always use CHAIN_RES. 
216 

* 
217 

* @param clauseLits literals in the conclusion of a CHAIN_RESOLUTION step 
218 

* with children and args[1:] 
219 

* @param clauseLits literals in the conclusion of a MACRO_RESOLUTION step 
220 

* with children and args 
221 

* @param children a list of clauses 
222 

* @param args a list of arguments to a MACRO_RESOLUTION step 
223 

* @param cdp a CDProof 
224 

* @return The resulting node of transforming MACRO_RESOLUTION into 
225 

* CHAIN_RESOLUTION according to the above idea. 
226 

*/ 
227 

Node eliminateCrowdingLits(const std::vector<Node>& clauseLits, 
228 

const std::vector<Node>& targetClauseLits, 
229 

const std::vector<Node>& children, 
230 

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

CDProof* cdp); 
232 

}; 
233 


234 

/** Final callback class, for stats and pedantic checking */ 
235 

class ProofPostprocessFinalCallback : public ProofNodeUpdaterCallback 
236 

{ 
237 

public: 
238 

ProofPostprocessFinalCallback(ProofNodeManager* pnm); 
239 

~ProofPostprocessFinalCallback(); 
240 

/** 
241 

* Initialize, called once for each new ProofNode to process. This initializes 
242 

* static information to be used by successive calls to update. 
243 

*/ 
244 

void initializeUpdate(); 
245 

/** Should proof pn be updated? Returns false, adds to stats. */ 
246 

bool shouldUpdate(std::shared_ptr<ProofNode> pn, 
247 

bool& continueUpdate) override; 
248 

/** was pedantic failure */ 
249 

bool wasPedanticFailure(std::ostream& out) const; 
250 


251 

private: 
252 

/** Counts number of postprocessed proof nodes for each kind of proof rule */ 
253 

IntegralHistogramStat<PfRule> d_ruleCount; 
254 

/** Total number of postprocessed rule applications */ 
255 

IntStat d_totalRuleCount; 
256 

/** The minimum pedantic level of any rule encountered */ 
257 

IntStat d_minPedanticLevel; 
258 

/** The total number of final proofs */ 
259 

IntStat d_numFinalProofs; 
260 

/** Proof node manager (used for pedantic checking) */ 
261 

ProofNodeManager* d_pnm; 
262 

/** Was there a pedantic failure? */ 
263 

bool d_pedanticFailure; 
264 

/** The pedantic failure string for debugging */ 
265 

std::stringstream d_pedanticFailureOut; 
266 

}; 
267 


268 

/** 
269 

* The proof postprocessor module. This postprocesses the final proof 
270 

* produced by an SmtEngine. Its main two tasks are to: 
271 

* (1) Connect proofs of preprocessing, 
272 

* (2) Expand macro PfRule applications. 
273 

*/ 
274 

class ProofPostproccess 
275 

{ 
276 

public: 
277 

ProofPostproccess(ProofNodeManager* pnm, 
278 

SmtEngine* smte, 
279 

ProofGenerator* pppg); 
280 

~ProofPostproccess(); 
281 

/** postprocess */ 
282 

void process(std::shared_ptr<ProofNode> pf); 
283 

/** set eliminate rule */ 
284 

void setEliminateRule(PfRule rule); 
285 


286 

private: 
287 

/** The proof node manager */ 
288 

ProofNodeManager* d_pnm; 
289 

/** The post process callback */ 
290 

ProofPostprocessCallback d_cb; 
291 

/** 
292 

* The updater, which is responsible for expanding macros in the final proof 
293 

* and connecting preprocessed assumptions to input assumptions. 
294 

*/ 
295 

ProofNodeUpdater d_updater; 
296 

/** The post process callback for finalization */ 
297 

ProofPostprocessFinalCallback d_finalCb; 
298 

/** 
299 

* The finalizer, which is responsible for taking stats and checking for 
300 

* (lazy) pedantic failures. 
301 

*/ 
302 

ProofNodeUpdater d_finalizer; 
303 

}; 
304 


305 

} // namespace smt 
306 

} // namespace CVC4 
307 


308 

#endif 