1 

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

/*! \file proof_post_processor.h 
3 

** \verbatim 
4 

** Top contributors (to current version): 
5 

** 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 in the prop engine 
13 

**/ 
14 


15 

#include "cvc4_private.h" 
16 


17 

#ifndef CVC4__PROP__PROOF_POST_PROCESSOR_H 
18 

#define CVC4__PROP__PROOF_POST_PROCESSOR_H 
19 


20 

#include <map> 
21 

#include <unordered_set> 
22 


23 

#include "expr/proof_node_updater.h" 
24 

#include "prop/proof_cnf_stream.h" 
25 


26 

namespace CVC4 { 
27 


28 

namespace prop { 
29 


30 

/** 
31 

* A callback class used by PropEngine for postprocessing proof nodes by 
32 

* connecting proofs of resolution, whose leaves are clausified preprocessed 
33 

* assertions and lemmas, with the CNF transformation of these formulas, while 
34 

* expanding the generators of lemmas. 
35 

*/ 
36 

class ProofPostprocessCallback : public ProofNodeUpdaterCallback 
37 

{ 
38 

public: 
39 

ProofPostprocessCallback(ProofNodeManager* pnm, 
40 

ProofCnfStream* proofCnfStream); 
41 
966 
~ProofPostprocessCallback() {} 
42 

/** 
43 

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

* static information to be used by successive calls to update. For this 
45 

* callback it resets d_assumpToProof. 
46 

*/ 
47 

void initializeUpdate(); 
48 

/** Should proof pn be updated? 
49 

* 
50 

* For this callback a proof node is updatable if it's an assumption for which 
51 

* the proof cnf straem has a proof. However if the proof node is blocked 
52 

* (which is the case for proof nodes introduced into the proof cnf stream's 
53 

* proof via expansion of its generators) then traversal is the proof node is 
54 

* cancelled, i.e., continueUpdate is set to false. 
55 

*/ 
56 

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

bool& continueUpdate) override; 
58 

/** Update the proof rule application. 
59 

* 
60 

* Replaces assumptions by their proof in proof cnf stream. Note that in doing 
61 

* this the proof node is blocked, so that future postprocessing does not 
62 

* traverse it. 
63 

* 
64 

* This method uses the cache in d_assumpToProof to avoid recomputing proofs 
65 

* for the same assumption (in the same scope). 
66 

*/ 
67 

bool update(Node res, 
68 

PfRule id, 
69 

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

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

CDProof* cdp, 
72 

bool& continueUpdate) override; 
73 


74 

private: 
75 

/** The proof node manager */ 
76 

ProofNodeManager* d_pnm; 
77 

/** The cnf stream proof generator */ 
78 

ProofCnfStream* d_proofCnfStream; 
79 

//reset at the begining of each update 
80 

/** Mapping assumptions to their proof from cnf transformation */ 
81 

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

//end reset at the begining of each update 
83 

}; 
84 


85 

/** 
86 

* The proof postprocessor module. This postprocesses the refutation proof 
87 

* produced by the SAT solver. Its main task is to connect the refutation's 
88 

* assumptions to the CNF transformation proof in ProofCnfStream. 
89 

*/ 
90 

class ProofPostproccess 
91 

{ 
92 

public: 
93 

ProofPostproccess(ProofNodeManager* pnm, ProofCnfStream* proofCnfStream); 
94 

~ProofPostproccess(); 
95 

/** postprocess 
96 

* 
97 

* The postprocessing is done via a proof node updater run on pf with this 
98 

* class's callback d_cb. 
99 

*/ 
100 

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


102 

private: 
103 

/** The post process callback */ 
104 

ProofPostprocessCallback d_cb; 
105 

/** The proof node manager */ 
106 

ProofNodeManager* d_pnm; 
107 

}; 
108 


109 

} // namespace prop 
110 

} // namespace CVC4 
111 


112 

#endif 