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
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
|
/******************************************************************************
* Top contributors (to current version):
* Andrew Reynolds, Gereon Kremer
*
* 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 proofs for preprocessing in an SMT engine.
*/
#include "cvc5_private.h"
#ifndef CVC5__SMT__PREPROCESS_PROOF_GENERATOR_H
#define CVC5__SMT__PREPROCESS_PROOF_GENERATOR_H
#include "context/cdhashmap.h"
#include "proof/lazy_proof.h"
#include "proof/proof.h"
#include "proof/proof_generator.h"
#include "proof/proof_set.h"
#include "proof/trust_node.h"
namespace cvc5 {
class LazyCDProof;
class ProofNodeManager;
namespace smt {
/**
* This is a proof generator that manages proofs for a set of formulas that
* may be replaced over time. This set of formulas is implicit; formulas that
* are not notified as assertions to this class are treated as assumptions.
*
* The main use case of this proof generator is for proofs of preprocessing,
* although it can be used in other scenarios where proofs for an evolving set
* of formulas is maintained. In the remainder of the description here, we
* describe its role as a proof generator for proofs of preprocessing.
*
* This class has two main interfaces during solving:
* (1) notifyNewAssert, for assertions that are not part of the input and are
* added to the assertion pipeline by preprocessing passes,
* (2) notifyPreprocessed, which is called when a preprocessing pass rewrites
* an assertion into another.
* Notice that input assertions do not need to be provided to this class.
*
* Its getProofFor method produces a proof for a preprocessed assertion
* whose free assumptions are intended to be input assertions, which are
* implictly all assertions that are not notified to this class.
*/
class PreprocessProofGenerator : public ProofGenerator
{
typedef context::CDHashMap<Node, TrustNode> NodeTrustNodeMap;
public:
/**
* @param pnm The proof node manager
* @param c The context this class depends on
* @param name The name of this generator (for debugging)
* @param ra The proof rule to use when no generator is provided for new
* assertions
* @param rpp The proof rule to use when no generator is provided for
* preprocessing steps.
*/
PreprocessProofGenerator(ProofNodeManager* pnm,
context::Context* c = nullptr,
std::string name = "PreprocessProofGenerator",
PfRule ra = PfRule::PREPROCESS_LEMMA,
PfRule rpp = PfRule::PREPROCESS);
~PreprocessProofGenerator() {}
/**
* Notify that n is an input (its proof is ASSUME).
*/
void notifyInput(Node n);
/**
* Notify that n is a new assertion, where pg can provide a proof of n.
*/
void notifyNewAssert(Node n, ProofGenerator* pg);
/** Notify a new assertion, trust node version. */
void notifyNewTrustedAssert(TrustNode tn);
/**
* Notify that n was replaced by np due to preprocessing, where pg can
* provide a proof of the equality n=np.
*/
void notifyPreprocessed(Node n, Node np, ProofGenerator* pg);
/** Notify preprocessed, trust node version */
void notifyTrustedPreprocessed(TrustNode tnp);
/**
* Get proof for f, which returns a proof based on proving an equality based
* on transitivity of preprocessing steps, and then using the original
* assertion with EQ_RESOLVE to obtain the proof of the ending assertion f.
*/
std::shared_ptr<ProofNode> getProofFor(Node f) override;
/** Identify */
std::string identify() const override;
/** Get the proof manager */
ProofNodeManager* getManager();
/**
* Allocate a helper proof. This returns a fresh lazy proof object that
* remains alive in the context. This feature is used to construct
* helper proofs for preprocessing, e.g. to support the skeleton of proofs
* that connect AssertionPipeline::conjoin steps.
*/
LazyCDProof* allocateHelperProof();
private:
/**
* Possibly check pedantic failure for null proof generator provided
* to this class.
*/
void checkEagerPedantic(PfRule r);
/** The proof node manager */
ProofNodeManager* d_pnm;
/** A dummy context used by this class if none is provided */
context::Context d_context;
/** The context used here */
context::Context* d_ctx;
/**
* The trust node that was the source of each node constructed during
* preprocessing. For each n, d_src[n] is a trust node whose node is n. This
* can either be:
* (1) A trust node REWRITE proving (n_src = n) for some n_src, or
* (2) A trust node LEMMA proving n.
*/
NodeTrustNodeMap d_src;
/** A context-dependent list of LazyCDProof, allocated for conjoin steps */
CDProofSet<LazyCDProof> d_helperProofs;
/**
* A cd proof for input assertions, this is an empty proof that intentionally
* returns (ASSUME f) for all f.
*/
CDProof d_inputPf;
/** Name for debugging */
std::string d_name;
/** The trust rule for new assertions with no provided proof generator */
PfRule d_ra;
/** The trust rule for rewrites with no provided proof generator */
PfRule d_rpp;
};
} // namespace smt
} // namespace cvc5
#endif
|
