1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
|
/******************************************************************************
* Top contributors (to current version):
* Haniel Barbosa
*
* This file is part of the cvc5 project.
*
* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
* in the top-level source directory and their institutional affiliations.
* All rights reserved. See the file COPYING in the top-level source
* directory for licensing information.
* ****************************************************************************
*
* The module for processing proof nodes in the prop engine.
*/
#include "cvc5_private.h"
#ifndef CVC5__PROP__PROOF_POST_PROCESSOR_H
#define CVC5__PROP__PROOF_POST_PROCESSOR_H
#include <map>
#include <unordered_set>
#include "proof/proof_node_updater.h"
#include "prop/proof_cnf_stream.h"
namespace cvc5 {
namespace prop {
/**
* A callback class used by PropEngine for post-processing proof nodes by
* connecting proofs of resolution, whose leaves are clausified preprocessed
* assertions and lemmas, with the CNF transformation of these formulas, while
* expanding the generators of lemmas.
*/
class ProofPostprocessCallback : public ProofNodeUpdaterCallback
{
public:
ProofPostprocessCallback(ProofNodeManager* pnm,
ProofCnfStream* proofCnfStream);
~ProofPostprocessCallback() {}
/**
* Initialize, called once for each new ProofNode to process. This initializes
* static information to be used by successive calls to update. For this
* callback it resets d_assumpToProof.
*/
void initializeUpdate();
/** Should proof pn be updated?
*
* For this callback a proof node is updatable if it's an assumption for which
* the proof cnf straem has a proof. However if the proof node is blocked
* (which is the case for proof nodes introduced into the proof cnf stream's
* proof via expansion of its generators) then traversal is the proof node is
* cancelled, i.e., continueUpdate is set to false.
*/
bool shouldUpdate(std::shared_ptr<ProofNode> pn,
const std::vector<Node>& fa,
bool& continueUpdate) override;
/** Update the proof rule application.
*
* Replaces assumptions by their proof in proof cnf stream. Note that in doing
* this the proof node is blocked, so that future post-processing does not
* traverse it.
*
* This method uses the cache in d_assumpToProof to avoid recomputing proofs
* for the same assumption (in the same scope).
*/
bool update(Node res,
PfRule id,
const std::vector<Node>& children,
const std::vector<Node>& args,
CDProof* cdp,
bool& continueUpdate) override;
private:
/** The proof node manager */
ProofNodeManager* d_pnm;
/** The cnf stream proof generator */
ProofCnfStream* d_proofCnfStream;
//---------------------------------reset at the begining of each update
/** Mapping assumptions to their proof from cnf transformation */
std::map<Node, std::shared_ptr<ProofNode> > d_assumpToProof;
//---------------------------------end reset at the begining of each update
};
/**
* The proof postprocessor module. This postprocesses the refutation proof
* produced by the SAT solver. Its main task is to connect the refutation's
* assumptions to the CNF transformation proof in ProofCnfStream.
*/
class ProofPostproccess
{
public:
ProofPostproccess(ProofNodeManager* pnm, ProofCnfStream* proofCnfStream);
~ProofPostproccess();
/** post-process
*
* The post-processing is done via a proof node updater run on pf with this
* class's callback d_cb.
*/
void process(std::shared_ptr<ProofNode> pf);
private:
/** The post process callback */
ProofPostprocessCallback d_cb;
/** The proof node manager */
ProofNodeManager* d_pnm;
};
} // namespace prop
} // namespace cvc5
#endif
|
