GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/proof/sat_proof.h Lines: 9 10 90.0 %
Date: 2021-03-23 Branches: 4 6 66.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sat_proof.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Liana Hadarean, Tim King, Andres Noetzli
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 Resolution proof
13
 **
14
 ** Resolution proof
15
 **/
16
17
#include "cvc4_private.h"
18
19
#ifndef CVC4__SAT__PROOF_H
20
#define CVC4__SAT__PROOF_H
21
22
#include <iosfwd>
23
#include <set>
24
#include <sstream>
25
#include <unordered_map>
26
#include <vector>
27
28
#include "context/cdhashmap.h"
29
#include "context/cdmaybe.h"
30
#include "expr/node.h"
31
#include "proof/clause_id.h"
32
#include "proof/proof_manager.h"
33
#include "util/statistics_registry.h"
34
#include "util/stats_histogram.h"
35
36
// Forward declarations.
37
namespace CVC4 {
38
class CnfProof;
39
} /* namespace CVC4 */
40
41
namespace CVC4 {
42
/**
43
 * Helper debugging functions
44
 */
45
template <class Solver>
46
void printDebug(typename Solver::TLit l);
47
template <class Solver>
48
void printDebug(typename Solver::TClause& c);
49
50
enum ClauseKind {
51
  INPUT,
52
  THEORY_LEMMA,  // we need to distinguish because we must reprove deleted
53
                 // theory lemmas
54
  LEARNT
55
}; /* enum ClauseKind */
56
57
template <class Solver>
58
struct ResStep {
59
  typename Solver::TLit lit;
60
  ClauseId id;
61
  bool sign;
62
3674379
  ResStep(typename Solver::TLit l, ClauseId i, bool s)
63
3674379
      : lit(l), id(i), sign(s) {}
64
}; /* struct ResStep */
65
66
template <class Solver>
67
class ResChain {
68
 public:
69
  typedef std::vector<ResStep<Solver> > ResSteps;
70
  typedef std::set<typename Solver::TLit> LitSet;
71
72
  ResChain(ClauseId start);
73
  ~ResChain();
74
75
  void addStep(typename Solver::TLit, ClauseId, bool);
76
93782
  bool redundantRemoved() {
77
93782
    return (d_redundantLits == NULL || d_redundantLits->empty());
78
  }
79
  void addRedundantLit(typename Solver::TLit lit);
80
81
  // accessor methods
82
39672
  ClauseId getStart() const { return d_start; }
83
39672
  const ResSteps& getSteps() const { return d_steps; }
84
93782
  LitSet* getRedundant() const { return d_redundantLits; }
85
86
 private:
87
  ClauseId d_start;
88
  ResSteps d_steps;
89
  LitSet* d_redundantLits;
90
}; /* class ResChain */
91
92
template <class Solver>
93
class TSatProof {
94
 protected:
95
  typedef ResChain<Solver> ResolutionChain;
96
97
  typedef std::set<typename Solver::TLit> LitSet;
98
  typedef std::set<typename Solver::TVar> VarSet;
99
  typedef std::unordered_map<ClauseId, typename Solver::TCRef> IdCRefMap;
100
  typedef std::unordered_map<typename Solver::TCRef, ClauseId> ClauseIdMap;
101
  typedef context::CDHashMap<ClauseId, typename Solver::TLit> IdUnitMap;
102
  typedef context::CDHashMap<int, ClauseId> UnitIdMap;
103
  typedef context::CDHashMap<ClauseId, ResolutionChain*> IdResMap;
104
  typedef std::unordered_map<ClauseId, uint64_t> IdProofRuleMap;
105
  typedef std::vector<ResolutionChain*> ResStack;
106
  typedef std::set<ClauseId> IdSet;
107
  typedef std::vector<typename Solver::TLit> LitVector;
108
  typedef std::unordered_map<ClauseId, typename Solver::TClause&>
109
      IdToMinisatClause;
110
  typedef std::unordered_map<ClauseId, LitVector*> IdToConflicts;
111
112
 public:
113
  TSatProof(Solver* solver, context::Context* context,
114
            const std::string& name, bool checkRes = false);
115
  ~TSatProof();
116
117
  void startResChain(typename Solver::TLit start);
118
  void startResChain(typename Solver::TCRef start);
119
  void addResolutionStep(typename Solver::TLit lit,
120
                         typename Solver::TCRef clause, bool sign);
121
  /**
122
   * Pops the current resolution of the stack and stores it
123
   * in the resolution map. Also registers the 'clause' parameter
124
   * @param clause the clause the resolution is proving
125
   */
126
  // void endResChain(typename Solver::TCRef clause);
127
  void endResChain(typename Solver::TLit lit);
128
  void endResChain(ClauseId id);
129
130
  /**
131
   * Pops the current resolution of the stack *without* storing it.
132
   */
133
  void cancelResChain();
134
135
  /**
136
   * Stores in the current derivation the redundant literals that were
137
   * eliminated from the conflict clause during conflict clause minimization.
138
   * @param lit the eliminated literal
139
   */
140
  void storeLitRedundant(typename Solver::TLit lit);
141
142
  /// update the CRef Id maps when Minisat does memory reallocation x
143
  void updateCRef(typename Solver::TCRef old_ref,
144
                  typename Solver::TCRef new_ref);
145
  void finishUpdateCRef();
146
147
  /**
148
   * Constructs the empty clause resolution from the final conflict
149
   *
150
   * @param conflict
151
   */
152
  void finalizeProof(typename Solver::TCRef conflict);
153
154
  /// clause registration methods
155
156
  ClauseId registerClause(const typename Solver::TCRef clause, ClauseKind kind);
157
  ClauseId registerUnitClause(const typename Solver::TLit lit, ClauseKind kind);
158
  void registerTrueLit(const typename Solver::TLit lit);
159
  void registerFalseLit(const typename Solver::TLit lit);
160
161
  ClauseId getTrueUnit() const;
162
  ClauseId getFalseUnit() const;
163
164
  void registerAssumption(const typename Solver::TVar var);
165
  ClauseId registerAssumptionConflict(const typename Solver::TLitVec& confl);
166
167
  ClauseId storeUnitConflict(typename Solver::TLit lit, ClauseKind kind);
168
169
  /**
170
   * Marks the deleted clauses as deleted. Note we may still use them in the
171
   * final
172
   * resolution.
173
   * @param clause
174
   */
175
  void markDeleted(typename Solver::TCRef clause);
176
283146
  bool isDeleted(ClauseId id) { return d_deleted.find(id) != d_deleted.end(); }
177
  /**
178
   * Constructs the resolution of ~q and resolves it with the current
179
   * resolution thus eliminating q from the current clause
180
   * @param q the literal to be resolved out
181
   */
182
  void resolveOutUnit(typename Solver::TLit q);
183
  /**
184
   * Constructs the resolution of the literal lit. Called when a clause
185
   * containing lit becomes satisfied and is removed.
186
   * @param lit
187
   */
188
  void storeUnitResolution(typename Solver::TLit lit);
189
190
  /**
191
   * Constructs the SAT proof for the given clause,
192
   * by collecting the needed clauses in the d_seen
193
   * data-structures, also notifying the proofmanager.
194
   */
195
  void constructProof(ClauseId id);
196
  void constructProof() { constructProof(d_emptyClauseId); }
197
  void refreshProof(ClauseId id);
198
908
  void refreshProof() { refreshProof(d_emptyClauseId); }
199
  bool proofConstructed() const;
200
  void collectClauses(ClauseId id);
201
  bool derivedEmptyClause() const;
202
  prop::SatClause* buildClause(ClauseId id);
203
204
  void collectClausesUsed(IdToSatClause& inputs, IdToSatClause& lemmas);
205
206
  void storeClauseGlue(ClauseId clause, int glue);
207
208
  bool isInputClause(ClauseId id) const;
209
  bool isLemmaClause(ClauseId id) const;
210
  bool isAssumptionConflict(ClauseId id) const;
211
212
  bool hasResolutionChain(ClauseId id) const;
213
214
  /** Returns the resolution chain associated with id. Assert fails if
215
   * hasResolution(id) does not hold. */
216
  const ResolutionChain& getResolutionChain(ClauseId id) const;
217
218
  const std::string& getName() const { return d_name; }
219
  const ClauseId& getEmptyClauseId() const { return d_emptyClauseId; }
220
  const IdSet& getSeenLearnt() const { return d_seenLearnt; }
221
  const IdToConflicts& getAssumptionConflicts() const
222
  {
223
    return d_assumptionConflictsDebug;
224
  }
225
226
 private:
227
  bool isUnit(ClauseId id) const;
228
  typename Solver::TLit getUnit(ClauseId id) const;
229
230
  bool isUnit(typename Solver::TLit lit) const;
231
  ClauseId getUnitId(typename Solver::TLit lit) const;
232
233
  void createLitSet(ClauseId id, LitSet& set);
234
235
  /**
236
   * Registers a ClauseId with a resolution chain res.
237
   * Takes ownership of the memory associated with res.
238
   */
239
  void registerResolution(ClauseId id, ResolutionChain* res);
240
241
242
  bool hasClauseIdForCRef(typename Solver::TCRef clause) const;
243
  ClauseId getClauseIdForCRef(typename Solver::TCRef clause) const;
244
245
  bool hasClauseIdForLiteral(typename Solver::TLit lit) const;
246
  ClauseId getClauseIdForLiteral(typename Solver::TLit lit) const;
247
248
  bool hasClauseRef(ClauseId id) const;
249
  typename Solver::TCRef getClauseRef(ClauseId id) const;
250
251
252
  const typename Solver::TClause& getClause(typename Solver::TCRef ref) const;
253
254
  void getLitVec(ClauseId id, LitVector& vec);
255
256
  bool checkResolution(ClauseId id);
257
258
  /**
259
   * Constructs a resolution tree that proves lit
260
   * and returns the ClauseId for the unit clause lit
261
   * @param lit the literal we are proving
262
   *
263
   * @return
264
   */
265
  ClauseId resolveUnit(typename Solver::TLit lit);
266
267
  /**
268
   * Does a depth first search on removed literals and adds the literals
269
   * to be removed in the proper order to the stack.
270
   *
271
   * @param lit the literal we are recursing on
272
   * @param removedSet the previously computed set of redundant literals
273
   * @param removeStack the stack of literals in reverse order of resolution
274
   */
275
  void removedDfs(typename Solver::TLit lit, LitSet* removedSet,
276
                  LitVector& removeStack, LitSet& inClause, LitSet& seen);
277
  void removeRedundantFromRes(ResChain<Solver>* res, ClauseId id);
278
279
  void print(ClauseId id) const;
280
  void printRes(ClauseId id) const;
281
  void printRes(const ResolutionChain& res) const;
282
283
  std::unordered_map<ClauseId, int> d_glueMap;
284
  struct Statistics {
285
    IntStat d_numLearnedClauses;
286
    IntStat d_numLearnedInProof;
287
    IntStat d_numLemmasInProof;
288
    AverageStat d_avgChainLength;
289
    IntegralHistogramStat<uint64_t> d_resChainLengths;
290
    IntegralHistogramStat<uint64_t> d_usedResChainLengths;
291
    IntegralHistogramStat<uint64_t> d_clauseGlue;
292
    IntegralHistogramStat<uint64_t> d_usedClauseGlue;
293
    Statistics(const std::string& name);
294
    ~Statistics();
295
  };
296
297
  std::string d_name;
298
299
  const ClauseId d_emptyClauseId;
300
  IdSet d_seenLearnt;
301
  IdToConflicts d_assumptionConflictsDebug;
302
303
  // Internal data.
304
  Solver* d_solver;
305
  context::Context* d_context;
306
307
  // clauses
308
  IdCRefMap d_idClause;
309
  ClauseIdMap d_clauseId;
310
  IdUnitMap d_idUnit;
311
  UnitIdMap d_unitId;
312
  IdHashSet d_deleted;
313
  IdToSatClause d_deletedTheoryLemmas;
314
315
  IdHashSet d_inputClauses;
316
  IdHashSet d_lemmaClauses;
317
  VarSet d_assumptions;             // assumption literals for bv solver
318
  IdHashSet d_assumptionConflicts;  // assumption conflicts not actually added
319
                                    // to SAT solver
320
321
  // Resolutions.
322
323
  /**
324
   * Map from ClauseId to resolution chain corresponding proving the
325
   * clause corresponding to the ClauseId. d_resolutionChains owns the
326
   * memory of the ResChain* it contains.
327
   */
328
  IdResMap d_resolutionChains;
329
330
   /*
331
   * Stack containting current ResChain* we are working on. d_resStack
332
   * owns the memory for the ResChain* it contains. Invariant: no
333
   * ResChain* pointer can be both in d_resStack and
334
   * d_resolutionChains. Memory ownership is transfered from
335
   * d_resStack to d_resolutionChains via registerResolution.
336
   */
337
  ResStack d_resStack;
338
  bool d_checkRes;
339
340
  const ClauseId d_nullId;
341
342
  // temporary map for updating CRefs
343
  ClauseIdMap d_temp_clauseId;
344
  IdCRefMap d_temp_idClause;
345
346
  // unit conflict
347
  context::CDMaybe<ClauseId> d_unitConflictId;
348
349
  ClauseId d_trueLit;
350
  ClauseId d_falseLit;
351
352
  IdToSatClause d_seenInputs;
353
  IdToSatClause d_seenLemmas;
354
355
  bool d_satProofConstructed;
356
  Statistics d_statistics;
357
}; /* class TSatProof */
358
359
template <class Solver>
360
prop::SatLiteral toSatLiteral(typename Solver::TLit lit);
361
362
/**
363
 * Convert from minisat clause to SatClause
364
 *
365
 * @param minisat_cl
366
 * @param sat_cl
367
 */
368
template <class Solver>
369
void toSatClause(const typename Solver::TClause& minisat_cl,
370
                 prop::SatClause& sat_cl);
371
372
} /* CVC4 namespace */
373
374
#endif /* CVC4__SAT__PROOF_H */