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

Line Exec Source
1
/*********************                                                        */
2
/*! \file sat_proof_manager.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Haniel Barbosa, Gereon Kremer
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 proof manager for Minisat
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__SAT_PROOF_MANAGER_H
18
#define CVC4__SAT_PROOF_MANAGER_H
19
20
#include "context/cdhashset.h"
21
#include "expr/buffered_proof_generator.h"
22
#include "expr/lazy_proof_chain.h"
23
#include "expr/node.h"
24
#include "prop/minisat/core/SolverTypes.h"
25
#include "prop/sat_solver_types.h"
26
27
namespace Minisat {
28
class Solver;
29
}
30
31
namespace CVC4 {
32
33
class ProofNodeManager;
34
35
namespace prop {
36
37
class CnfStream;
38
39
/**
40
 * This class is responsible for managing the proof production of the SAT
41
 * solver. It tracks resolutions produced during solving and stores them,
42
 * independently, with the connection of the resolutions only made when the
43
 * empty clause is produced and the refutation is complete. The expected
44
 * assumptions of the refutation are the clausified preprocessed assertions and
45
 * lemmas.
46
 *
47
 * These resolutions are stored in a LazyCDProofChain, a user-context-dependent
48
 * proof that takes lazy steps and can connect them when generating a proof for
49
 * a given fact. Its use in this proof manager is so that, assuming the
50
 * following lazy steps are saved in the LazyCDProofChain:
51
 *
52
 * --- S0: (l4,          PG0)
53
 * --- S1: ((or l3 l4),  PG1)
54
 * --- S2: ((or l1 ~l3), PG2)
55
 * --- S3: (false,       PG3)
56
 * --- S4: (~l2,         PG4)
57
 * --- S5: (~l3,         PG5)
58
 * --- S6: (~l5,         PG6)
59
 *
60
 * when requesting the proof of false, assuming that the proof generators have
61
 * the following expansions:
62
 *
63
 * --- PG0 -> (CHAIN_RES ((or l4 l1) ~l1))
64
 * --- PG1 -> (CHAIN_RES ((or l3 l5 l6 l7) ~l5 (or ~l6 l7) (or l4 ~l7)))
65
 * --- PG2 -> (CHAIN_RES ((or l1 ~l3 l5) ~l5))
66
 * --- PG3 -> (CHAIN_RES ((or l1 l2) ~l1 ~l2))
67
 * --- PG4 -> (CHAIN_RES ((or l3 ~l2) ~l3))
68
 * --- PG5 -> (CHAIN_RES ((or l1 ~l3) ~l1))
69
 * --- PG6 -> (CHAIN_RES ((or l1 ~l5) ~l1))
70
 *
71
 * will connect the independent resolutions and yield the following refutation
72
 *
73
 *                                             (or l1 ~l5)  ~l1
74
 *                                             ---------------- CHAIN_RES
75
 *                            (or l1 ~l3 l5)   ~l5
76
 *                            ---------------------- CHAIN_RES
77
 *                                      (or l1 ~l3)              ~l1
78
 *                                      ----------------------------- CHAIN_RES
79
 *                       (or l3 ~l2)     ~l3
80
 *                       -------------------- CHAIN_RES
81
 *   (or l1 l2)   ~l1    ~l2
82
 *  --------------------------- CHAIN_RES
83
 *              false
84
 *
85
 * where note that the steps S0 and S1, for l4 and (or l3 l4), respectively,
86
 * were ignored, since they were not part of the chain starting with
87
 * false. Moreover there is no requirement that the steps are registered
88
 * chronologically in the LazyCDProofChain. The chain started on step S3 and
89
 * proceeded to steps S4, S5, S2, and finally S6.
90
 *
91
 * To track the reasoning of the SAT solver and produce the steps above this
92
 * class does three main things:
93
 *  (1) Register the resolutions for learned clauses as they are learned.
94
 *  (2) Register the resolutions for propagated literals when necessary.
95
 *  (3) Register the *full* resolution proof for the empty clause.
96
 *
97
 * Case (1) covers the learned clauses during backjumping. The only information
98
 * saved is that, from clauses C1 to Cn, a given learned clause C is derived via
99
 * chain resolution (and possibly factoring, reordering and double negation
100
 * elimination in its literals), i.e., we do not recursively prove C1 to Cn at
101
 * this moment.
102
 *
103
 * Not explaining C1 to Cn eagerly is beneficial because:
104
 * - we might be wasting resources in fully explanaining it now, since C may not
105
 *   be necessary for the derivation of the empty clause, and
106
 * - in explaining clauses lazily we might have shorter explanations, which has
107
 *   been observed empirically to be often the case.
108
 *
109
 * The latter case is a result of the SAT solver possibly changing the
110
 * explanation of each of C, C1 to Cn, or the components of their
111
 * explanations. This is because the set of propagated literals that may be used
112
 * in these explanations can change in different SAT contexts, with the same
113
 * clause being derived several times, each from a different set of clauses.
114
 *
115
 * Therefore we only fully explain a clause when absolutely necessary, i.e.,
116
 * when we are done (see case (3)) or when we'd not be able to do it afterwards
117
 * (see case (2)). In the example above, step S2 is generated from case (1),
118
 * with the shallow proof
119
 *
120
 *        (or l1 ~l3 l5)       ~l5
121
 *        ------------------------- CHAIN_RES
122
 *                 (or l1 ~l3)
123
 *
124
 * explaining the learned clause (or l1 ~l3). Its full proof would only be
125
 * produced if it were part of the final refutation, as it indeed is. Note that
126
 * in the example above the refutation proof contains the resolution proof of
127
 * ~l5.
128
 *
129
 * Case (2) covers:
130
 *  (2.1) propagated literals explained by clauses being deleted
131
 *  (2.2) propagated literals whose negation occurs in a learned clause, which
132
 *  are then deleted for being redundant.
133
 *
134
 * Case (2.1) only happens for the so-called "locked clauses", which are clauses
135
 * C = l1 v ... v ln that propagate their first literal, l1. When a locked
136
 * clause C is deleted we save a chain resolution proof of l1 because we'd not
137
 * be able to retrieve C afterwards, since it is deleted. The proof is a chain
138
 * resolution step between C and ~l2, ..., ~ln, concluding l1. In the example
139
 * above, step S0 is generated from case (2.1), with the locked clause (or l4
140
 * l1) being deleted and requiring the registration in the LazyCDPRoofChain of a
141
 * lazy step for
142
 *
143
 *         (or l4 l1)       ~l1
144
 *      ------------------------- CHAIN_RES
145
 *               l4
146
 *
147
 * Case (2.2) requires that, when a redundant literal (i.e., a literal whose
148
 * negation is propagated) is deleted from a learned clause, we add the
149
 * explanation of its negation to the chain resolution proof of the learned
150
 * clause. This justifies the deletion of the redundant literal. However, the
151
 * explanation for the propagated literal (the SAT solver maintains a map from
152
 * propagated literals to the clauses that propagate them in the current
153
 * context, i.e., their explanations, clauses in which all literals but the
154
 * propagated one have their negation propagated) may also contain literals that
155
 * were in the learned clause and were deleted for being redundant. Therefore
156
 * eliminating a redundant literal requires recursively explaining the
157
 * propagated literals in its explanation as long as they are, themselves,
158
 * redundant literals in the learned clause.
159
 *
160
 * In the above example step S1, concluding (or l3 l4), is generated from the
161
 * resolutions
162
 *
163
 *   (or l3 l5 l6 l7)    ~l5
164
 *  -------------------------- CHAIN_RES
165
 *     (or l3 l6 l7)                        (or ~l6 l7)   (or l4 ~l7)
166
 *    ---------------------------------------------------------------- CHAIN_RES
167
 *                           (or l3 l4)
168
 *
169
 * as l6 and l7 are redundant, which leads to (or l3 l6 l7) being resolved with
170
 * l6's explanation, (or ~l6 l7). The literals in the explanation of l7 are
171
 * recursively explained if they are also redundant, which is the case for l7,
172
 * so its explanation is also added as premise for the resolution. Since l4 is
173
 * not redundant, it is not recursively explained.
174
 *
175
 * Note that the actual proof generated does not have the intermediary step
176
 * before removing redundant literals. It's all done in one fell swoop:
177
 *
178
 *   (or l3 l5 l6 l7)   ~l5   (or ~l6 l7)   (or l4 ~l7)
179
 *   --------------------------------------------------- CHAIN_RES
180
 *                           (or l3 l4)
181
 *
182
 * Finally, case (3) happens when the SAT solver derives the empty clause and
183
 * it's not possible to backjump. The empty clause is learned from a conflict
184
 * clause: a clause whose every literal has its negation propagated in the
185
 * current context. Thus the proof of the empty clause is generated, at first,
186
 * in the same way as case (1): a resolution chain betweeen the conflict clause
187
 * and its negated literals. However, since we are now done, we recursively
188
 * explain the propagated literals, starting from the negated literals from the
189
 * conflict clause and progressing to all propagated literals ocurring in a
190
 * given explanation.
191
 *
192
 * In the above example this happens as: step S3
193
 *
194
 *    (or l1 l2)   ~l1    ~l2
195
 *  --------------------------- CHAIN_RES
196
 *             false
197
 *
198
 * is added for a conflict clause (or l1 l2). Then we attempt to explain ~l1 and
199
 * ~l2. The former has no explanation (i.e., it's an input), while the latter
200
 * has explanation (or l3 ~l2). This leads to step S4
201
 *
202
 *  (or l3 ~l2)     ~l3
203
 *  -------------------- CHAIN_RES
204
 *        ~l2
205
 *
206
 * being added to the LazyCDProofChain. In explaining ~l3 the step S5
207
 *
208
 *  (or l1 ~l3)      ~l1
209
 *  --------------------- CHAIN_RES
210
 *         ~l3
211
 *
212
 * is added. Since ~l1 has no explanation, the process halts. Note that at this
213
 * point the step S6 has not been added to the LazyCDProofChain. This is because
214
 * to explain ~l5 we need to look at the literal premises in the proofs of
215
 * learned clauses.
216
 *
217
 * The last thing done then in case (3), after the resolution on the conflict
218
 * clause and an initial recursive explanation of propagated literals, is to
219
 * connect the refutation proof and then recursively its propagated literal
220
 * leaves, repeating until a fix point.
221
 *
222
 * In the above example the first connection yields
223
 *
224
 *                           (or l1 ~l3 l5)   ~l5
225
 *                           ---------------------- CHAIN_RES
226
 *                                     (or l1 ~l3)              ~l1
227
 *                                     ----------------------------- CHAIN_RES
228
 *                      (or l3 ~l2)     ~l3
229
 *                      -------------------- CHAIN_RES
230
 *  (or l1 l2)   ~l1    ~l2
231
 * --------------------------- CHAIN_RES
232
 *                     false
233
 *
234
 * whose literal leaves are ~l1 and ~l5. The former has no explanation, but the
235
 * latter is explained by (or l1 ~l5), thus leading to step S6
236
 *
237
 *  (or l1 ~l5)      ~l1
238
 *  --------------------- CHAIN_RES
239
 *         ~l5
240
 *
241
 * then the final connection
242
 *
243
 *                                             (or l1 ~l5)  ~l1
244
 *                                             ---------------- CHAIN_RES
245
 *                            (or l1 ~l3 l5)   ~l5
246
 *                            ---------------------- CHAIN_RES
247
 *                                      (or l1 ~l3)              ~l1
248
 *                                      ----------------------------- CHAIN_RES
249
 *                       (or l3 ~l2)     ~l3
250
 *                       -------------------- CHAIN_RES
251
 *   (or l1 l2)   ~l1    ~l2
252
 *  --------------------------- CHAIN_RES
253
 *                      false
254
 *
255
 * which has no more explainable literals as leaves.
256
 *
257
 * The interfaces below provide ways for the SAT solver to register its
258
 * assumptions (clausified assertions and lemmas) for the SAT proof
259
 * (registerSatAssumption), register resolution steps (startResChain /
260
 * addResolutionStep / endResChain), build the final refutation proof
261
 * (finalizeProof) and retrieve the refutation proof (getProof). So in a given
262
 * run of the SAT solver these interfaces are expected to be used in the
263
 * following order:
264
 *
265
 * (registerSatAssumptions | (startResChain (addResolutionStep)+ endResChain)*)*
266
 * finalizeProof
267
 * getProof
268
 *
269
 */
270
966
class SatProofManager
271
{
272
 public:
273
  SatProofManager(Minisat::Solver* solver,
274
                  CnfStream* cnfStream,
275
                  context::UserContext* userContext,
276
                  ProofNodeManager* pnm);
277
278
  /** Marks the start of a resolution chain.
279
   *
280
   * This call is followed by *at least one* call to addResolution step and one
281
   * call to endResChain.
282
   *
283
   * The given clause, at the node level, is registered in d_resLinks with a
284
   * null pivot, since this is the first link in the chain.
285
   *
286
   * @param start a SAT solver clause (list of literals) that will be the first
287
   * clause in a resolution chain.
288
   */
289
  void startResChain(const Minisat::Clause& start);
290
  /** Adds a resolution step with a clause
291
   *
292
   * There must have been a call to startResChain before any call to
293
   * addResolution step. After following calls to addResolution step there is
294
   * one call to endResChain.
295
   *
296
   * The resolution step is added to d_resLinks with the clause, at the node
297
   * level, and the literal, at the node level, as the pivot.
298
   *
299
   * @param clause the clause being resolved against
300
   * @param lit the literal occurring in clause to be the pivot of the
301
   * resolution step
302
   */
303
  void addResolutionStep(const Minisat::Clause& clause, Minisat::Lit lit);
304
  /** Adds a resolution step with a unit clause
305
   *
306
   * The resolution step is added to d_resLinks such that lit, at the node
307
   * level, is the pivot and and the unit clause is ~lit, at the node level.
308
   *
309
   * If the literal is marked as redundant, then a step is *not* is added to
310
   * d_resLinks. It is rather saved to d_redundandLits, whose components we will
311
   * be handled in a special manner when the resolution chain is finished. This
312
   * is because the steps corresponding to the removal of redundant literals
313
   * have to be done in a specific order. See proccessRedundantLits below.
314
   *
315
   * @param lit the literal being resolved against
316
   * @param redundant whether lit is redundant
317
   */
318
  void addResolutionStep(Minisat::Lit lit, bool redundant = false);
319
  /** Ends resolution chain concluding a unit clause
320
   *
321
   * This call must have been preceded by one call to startResChain and at least
322
   * one call to addResolutionStep.
323
   *
324
   * This and the version below both call the node version of this method,
325
   * described further below, which actually does the necessary processing.
326
   */
327
  void endResChain(Minisat::Lit lit);
328
  /** Ends resolution chain concluding a clause */
329
  void endResChain(const Minisat::Clause& clause);
330
  /** Build refutation proof starting from conflict clause
331
   *
332
   * This method (or its variations) is only called when the SAT solver has
333
   * reached an unsatisfiable state.
334
   *
335
   * This and the versions below call the node version of this method, described
336
   * further below, which actually does the necessary processing.
337
   *
338
   * @param adding whether the conflict is coming from a freshly added clause
339
   */
340
  void finalizeProof(const Minisat::Clause& inConflict, bool adding = false);
341
  /** Build refutation proof starting from conflict unit clause
342
   *
343
   * @param adding whether the conflict is coming from a freshly added clause
344
   */
345
  void finalizeProof(Minisat::Lit inConflict, bool adding = false);
346
  /** As above, but uses the unit conflict clause saved in d_conflictLit. */
347
  void finalizeProof();
348
  /** Set the unit conflict clause d_conflictLit. */
349
  void storeUnitConflict(Minisat::Lit inConflict);
350
351
  /** Retrive the refutation proof
352
   *
353
   * If there is no chain for false in d_resChains, meaning that this call was
354
   * made before finalizeProof, an assumption proof node is produced.
355
   */
356
  std::shared_ptr<ProofNode> getProof();
357
358
  /** Register a unit clause input, converted to its node representation.  */
359
  void registerSatLitAssumption(Minisat::Lit lit);
360
  /** Register a set clause inputs. */
361
  void registerSatAssumptions(const std::vector<Node>& assumps);
362
363
 private:
364
  /** Ends resolution chain concluding clause
365
   *
366
   * This method builds the proof of conclusion from the resolution chain
367
   * currently saved in d_resLinks.
368
   *
369
   * First each saved redundant literals in d_redundantLits is processed via
370
   * processRedundantLit. The literals in the resolution chain's conclusion are
371
   * used to verifynig which literals in the computed explanations are
372
   * redundant, i.e., don't occur in conclusionLits. The nessary resolution
373
   * steps will be added to d_resLinks.
374
   *
375
   * The proof to be built will be a CHAIN_RESOLUTION step, whose children and
376
   * arguments will be retrieved from traversing d_resLinks. Consider the
377
   * following d_resLinks (where each [~]li is its node equivalent):
378
   *
379
   * - <(or l3 l5 l6 l7), null>
380
   * - <~l5, l5>
381
   * - <(or ~l6 l7), l6>
382
   * - <(or l4 ~l7), l7>
383
   *
384
   * The resulting children and arguments for the CHAIN_RESOLUTION proof step would be:
385
   * - [(or l3 l5 l6 l7), ~l5, (or ~l6 l7), (or l4 ~l7)]
386
   * - [l5, l6, l7]
387
   * and the proof step
388
   *
389
   *   (or l3 l5 l6 l7)   ~l5   (or ~l6 l7)   (or l4 ~l7)
390
   *   --------------------------------------------------- CHAIN_RES_{l5,l6,l7}
391
   *                           (or l3 l4)
392
   *
393
   * The conclusion of the CHAIN_RES proof step is *not* the given conclusion of
394
   * this method. This is because conclusion is the node equivalent of the
395
   * clause in the SAT solver, which is kept modulo duplicates, reordering, and
396
   * double negation elimination. Therefore we generate the above step in the
397
   * correct way for the semantics of CHAIN_RES, based on its children and
398
   * arguments, via the d_pnm's proof checker. The resulting node n is fed into
399
   * the clause normalization in TheoryProofStepBuffer, which reduces n to
400
   * conclusion.
401
   *
402
   * All the proof steps generated to conclude conclusion from the premises in
403
   * d_resLinks are saved into d_resChainPg, which is saved as the proof
404
   * generator for lazy step added to d_resChains for the conclusion.
405
   *
406
   * @param conclusion the node-level conclusion of the resolution chain
407
   * @param conclusionLits the set of literals in the conclusion
408
   */
409
  void endResChain(Node conclusion, const std::set<SatLiteral>& conclusionLits);
410
411
  /** Explain redundant literal and generate corresponding resolution steps
412
   *
413
   * If the redundant literal has a reason, we add a resolution step with that
414
   * clause, otherwise with the negation of the redundant literal as the unit
415
   * clause. The redundant literal is the resolvent in both cases.  The steps
416
   * are always added as the *first* link after last resolution step added
417
   * *before* processing redundant literals began, i.e., at d_resLinks.begin() +
418
   * pos. This is to guarantee that the links are in the correct order for the
419
   * chain resolution, see below.
420
   *
421
   * If the reason contains literals that do not occur in conclusionLits, they
422
   * are redundant and recursively processed by this method. This recursive
423
   * processing happens *before* the resolution step for lit is added. Since
424
   * steps are always added in position pos, pushing steps after that 1
425
   * position, this guarantees that a step with a clause will occur before the
426
   * steps that eliminate its redundant literals.
427
   *
428
   * Consider d_resLinks with 3 links before the first processRedundantLit call,
429
   * i.e., pos = 3, and d_redundantLits = {l1}, with reason(l1) = (or l1 ~l2),
430
   * with ~l2 redundant. Assume ~l2 has no explanation. By processing ~l2 first,
431
   * the link <~l2, l2> will be added at position 3. Then by coming back to the
432
   * processing of l1 the link <(or l1 ~l2), l1> will also be added position 3,
433
   * with <~l2, l2> pushed to position 4. If this these links had the reverse
434
   * order the literal ~l2 would, erroneously, occur in the chain resolution
435
   * conclusion, as it is introduced by (or l1 ~l2).
436
   *
437
   * After a resolution step for a redundant literal is added, it is marked as
438
   * visited, thus avoiding adding redundunt resolution steps to the chain if
439
   * that literal occurs again in another redundant literal's reason.
440
   *
441
   * @param lit the redundant literal
442
   * @param conclusionLits the literals in the clause from which redundant
443
   * literals have been removed
444
   * @param visited cache of literals already processed
445
   * @param pos position, in d_resLinks, of last resolution step added *before*
446
   * processing redundant literals
447
   */
448
  void processRedundantLit(SatLiteral lit,
449
                           const std::set<SatLiteral>& conclusionLits,
450
                           std::set<SatLiteral>& visited,
451
                           unsigned pos);
452
  /** Explain literal if it is propagated in the SAT solver
453
   *
454
   * If a literal is propagated, i.e., it has a reason in the SAT solver, that
455
   * clause is retrieved. This method is then called recursively on the negation
456
   * of each of reason's literals (that is not lit). Afterwards a
457
   * CHAIN_RESOLUTION proof step is created to conclude lit from the reason and
458
   * its literals, other than lit, negations.
459
   *
460
   * This method also tracks all the literals and clauses, at the node level,
461
   * that have been used as premises of resolutions steps in the recursive
462
   * explanations. A resolution step is only created if the conclusion does not
463
   * occur in these premises, as this would configure a cyclic proof.
464
   *
465
   * These cyclic proofs, at the node level, are naturally generated by the SAT
466
   * solver because they are so that a literal is derived from a clause (so they
467
   * are different) but both correspond to the *same node*. For example,
468
   * consider the following derivation at the SAT solver level
469
   *
470
   *                       [l1, l2, l3]    ~l2   ~l3
471
   *                       -------------------------- CHAIN_RES
472
   *           [l0, ~l1]       l1
473
   *           ---------------------- CHAIN_RES
474
   *                    l0
475
   *
476
   * which has no issues. However, its node equivalent is
477
   *
478
   *                  (or a b c)    (not b)   (not c)
479
   *                  ------------------------------- CHAIN_RES
480
   *      (or (or a b c) (not a))       a
481
   *      --------------------------------- CHAIN_RES
482
   *               (or a b c)
483
   *
484
   * which is cyclic. The issue is that l0 = (or a b c). Only at the SAT level
485
   * are l0 and [l1, l2, l3] different.
486
   *
487
   * If a cyclic proof is identified, the respective node is kept as an
488
   * assumption.
489
   *
490
   * @param lit the literal to explained
491
   * @param premises set of literals and clauses, at the node level, that
492
   * have been used as premises of resolution steps while explaining
493
   * propagations
494
   */
495
  void explainLit(prop::SatLiteral lit,
496
                  std::unordered_set<TNode, TNodeHashFunction>& premises);
497
498
  /** Build refutation proof starting from conflict clause
499
   *
500
   * Given a conflict clause, this method handles case (3) described in the
501
   * preamble. Each of the literals in the conflict clause is either
502
   * explainable, the result of a previously saved resolution chain, or an
503
   * input.
504
   *
505
   * First, explainLit is called recursively on the negated literals from
506
   * the conflict clause.
507
   *
508
   * Second, a CHAIN_RESOLUTION proof step is added between
509
   * the conflict clause and its negated literals, concluding false.
510
   *
511
   * Third, until a fix point, the refutation proof is connected, by calling
512
   * d_resChain.getProofFor(d_false), its free assumptions are determined and,
513
   * in case any as a literal that might be explained, we call explainLit.
514
   *
515
   * The latter is called to a fix point because adding an explanation to a
516
   * propagated literal may connect it with a previously saved resolution chain,
517
   * which may have free assumptions that are literals that can be explained and
518
   * so on.
519
   *
520
   * @param inConflictNode node corresponding to conflict clause
521
   * @param inConflict literals in the conflict clause
522
   */
523
  void finalizeProof(Node inConflictNode,
524
                     const std::vector<SatLiteral>& inConflict);
525
526
  /** The SAT solver to which we are managing proofs */
527
  Minisat::Solver* d_solver;
528
  /** Pointer to the underlying cnf stream. */
529
  CnfStream* d_cnfStream;
530
  /** The proof node manager */
531
  ProofNodeManager* d_pnm;
532
  /** Resolution steps (links) accumulator for chain resolution.
533
   *
534
   * Each tuple has a clause and the pivot for the resolution step it is
535
   * involved on, as well as whether the pivot occurs positively/negatively or
536
   * negatively/positively in the clauses being resolved. If the third argument
537
   * is true (resp. false), the pivot occurs positively (negatively) in the
538
   * clause yielded by the resolution up to the previous link and negatively
539
   * (positively) in this link. The first link has a null pivot. Links are kept
540
   * at the node level.
541
   *
542
   * This accumulator is reset after each chain resolution. */
543
  std::vector<std::tuple<Node, Node, bool>> d_resLinks;
544
545
  /** Redundant literals removed from the resolution chain's conclusion.
546
   *
547
   * This accumulator is reset after each chain resolution. */
548
  std::vector<SatLiteral> d_redundantLits;
549
550
  /**
551
   * Associates clauses to their local proofs. These proofs are local and
552
   * possibly updated during solving. When the final conclusion is reached, a
553
   * final proof is built based on the proofs saved here.
554
   *
555
   * This chain is initialized so that its getProofFor method, which connects
556
   * the chain, accounts for cyclic proofs. This is so that we avoid the issue
557
   * described in explainLit.
558
   */
559
  LazyCDProofChain d_resChains;
560
561
  /** The proof generator for resolution chains */
562
  BufferedProofGenerator d_resChainPg;
563
564
  /** The false node */
565
  Node d_false;
566
567
  /** All clauses added to the SAT solver, kept in a context-dependent manner.
568
   */
569
  context::CDHashSet<Node, NodeHashFunction> d_assumptions;
570
571
  /**
572
   * A placeholder that may be used to store the literal with the final
573
   * conflict.
574
   */
575
  SatLiteral d_conflictLit;
576
  /** Gets node equivalent to literal */
577
  Node getClauseNode(SatLiteral satLit);
578
  /** Gets node equivalent to clause.
579
   *
580
   * To avoid generating different nodes for the same clause, modulo ordering,
581
   * an invariant assumed throughout this class, the OR node generated by this
582
   * method always has its children ordered.
583
   */
584
  Node getClauseNode(const Minisat::Clause& clause);
585
  /** Prints clause, as a sequence of literals, in the "sat-proof" trace. */
586
  void printClause(const Minisat::Clause& clause);
587
}; /* class SatProofManager */
588
589
}  // namespace prop
590
}  // namespace CVC4
591
592
#endif /* CVC4__SAT_PROOF_MANAGER_H */