GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/smt/proof_post_processor.h Lines: 1 1 100.0 %
Date: 2021-03-23 Branches: 0 0 0.0 %

Line Exec Source
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) 2009-2021 by the authors listed in the file AUTHORS
8
 ** in the top-level source directory and their institutional affiliations.
9
 ** All rights reserved.  See the file COPYING in the top-level 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 post-processing 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 post-processing 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
  /** post-process */
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