GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/proof/sat_proof_implementation.h Lines: 383 559 68.5 %
Date: 2021-03-22 Branches: 424 1652 25.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sat_proof_implementation.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Liana Hadarean, Tim King, Guy Katz
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_IMPLEMENTATION_H
20
#define CVC4__SAT__PROOF_IMPLEMENTATION_H
21
22
#include "proof/clause_id.h"
23
#include "proof/sat_proof.h"
24
#include "prop/minisat/core/Solver.h"
25
#include "prop/minisat/minisat.h"
26
#include "prop/sat_solver_types.h"
27
#include "smt/smt_statistics_registry.h"
28
29
namespace CVC4 {
30
31
template <class Solver>
32
void printLit(typename Solver::TLit l) {
33
  Debug("proof:sat") << (sign(l) ? "-" : "") << var(l) + 1;
34
}
35
36
template <class Solver>
37
void printClause(const typename Solver::TClause& c) {
38
  for (int i = 0; i < c.size(); i++) {
39
    Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " ";
40
  }
41
}
42
43
template <class Solver>
44
void printClause(const std::vector<typename Solver::TLit>& c) {
45
  for (unsigned i = 0; i < c.size(); i++) {
46
    Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " ";
47
  }
48
}
49
50
template <class Solver>
51
void printLitSet(const std::set<typename Solver::TLit>& s) {
52
  typename std::set<typename Solver::TLit>::const_iterator it = s.begin();
53
  for (; it != s.end(); ++it) {
54
    printLit<Solver>(*it);
55
    Debug("proof:sat") << " ";
56
  }
57
  Debug("proof:sat") << std::endl;
58
}
59
60
// purely debugging functions
61
template <class Solver>
62
void printDebug(typename Solver::TLit l) {
63
  Debug("proof:sat") << (sign(l) ? "-" : "") << var(l) + 1 << std::endl;
64
}
65
template <class Solver>
66
void printDebug(typename Solver::TClause& c) {
67
  for (int i = 0; i < c.size(); i++) {
68
    Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " ";
69
  }
70
  Debug("proof:sat") << std::endl;
71
}
72
73
/**
74
 * Converts the clause associated to id to a set of literals
75
 *
76
 * @param id the clause id
77
 * @param set the clause converted to a set of literals
78
 */
79
template <class Solver>
80
48867
void TSatProof<Solver>::createLitSet(ClauseId id, LitSet& set) {
81
48867
  Assert(set.empty());
82
48867
  if (isUnit(id)) {
83
4
    set.insert(getUnit(id));
84
4
    return;
85
  }
86
48863
  if (id == d_emptyClauseId) {
87
    return;
88
  }
89
  // if it's an assumption
90
48863
  if (d_assumptionConflictsDebug.find(id) != d_assumptionConflictsDebug.end()) {
91
    LitVector* clause = d_assumptionConflictsDebug[id];
92
    for (unsigned i = 0; i < clause->size(); ++i) {
93
      set.insert(clause->operator[](i));
94
    }
95
    return;
96
  }
97
98
48863
  typename Solver::TCRef ref = getClauseRef(id);
99
48863
  const typename Solver::TClause& c = getClause(ref);
100
885330
  for (int i = 0; i < c.size(); i++) {
101
836467
    set.insert(c[i]);
102
  }
103
}
104
105
/**
106
 * Resolves clause1 and clause2 on variable var and stores the
107
 * result in clause1
108
 * @param v
109
 * @param clause1
110
 * @param clause2
111
 */
112
template <class Solver>
113
bool resolve(const typename Solver::TLit v,
114
             std::set<typename Solver::TLit>& clause1,
115
             std::set<typename Solver::TLit>& clause2, bool s) {
116
  Assert(!clause1.empty());
117
  Assert(!clause2.empty());
118
  typename Solver::TLit var = sign(v) ? ~v : v;
119
  if (s) {
120
    // literal appears positive in the first clause
121
    if (!clause2.count(~var)) {
122
      if (Debug.isOn("proof:sat")) {
123
        Debug("proof:sat") << "proof:resolve: Missing literal ";
124
        printLit<Solver>(var);
125
        Debug("proof:sat") << std::endl;
126
      }
127
      return false;
128
    }
129
    clause1.erase(var);
130
    clause2.erase(~var);
131
    typename std::set<typename Solver::TLit>::iterator it = clause2.begin();
132
    for (; it != clause2.end(); ++it) {
133
      clause1.insert(*it);
134
    }
135
  } else {
136
    // literal appears negative in the first clause
137
    if (!clause1.count(~var) || !clause2.count(var)) {
138
      if (Debug.isOn("proof:sat")) {
139
        Debug("proof:sat") << "proof:resolve: Missing literal ";
140
        printLit<Solver>(var);
141
        Debug("proof:sat") << std::endl;
142
      }
143
      return false;
144
    }
145
    clause1.erase(~var);
146
    clause2.erase(var);
147
    typename std::set<typename Solver::TLit>::iterator it = clause2.begin();
148
    for (; it != clause2.end(); ++it) {
149
      clause1.insert(*it);
150
    }
151
  }
152
  return true;
153
}
154
155
/// ResChain
156
template <class Solver>
157
93776
ResChain<Solver>::ResChain(ClauseId start)
158
93776
    : d_start(start), d_steps(), d_redundantLits(NULL) {}
159
160
template <class Solver>
161
ResChain<Solver>::~ResChain() {
162
  if (d_redundantLits != NULL) {
163
    delete d_redundantLits;
164
  }
165
}
166
167
template <class Solver>
168
3674363
void ResChain<Solver>::addStep(typename Solver::TLit lit, ClauseId id,
169
                               bool sign) {
170
3674363
  ResStep<Solver> step(lit, id, sign);
171
3674363
  d_steps.push_back(step);
172
3674363
}
173
174
template <class Solver>
175
529680
void ResChain<Solver>::addRedundantLit(typename Solver::TLit lit) {
176
529680
  if (d_redundantLits) {
177
480813
    d_redundantLits->insert(lit);
178
  } else {
179
48867
    d_redundantLits = new LitSet();
180
48867
    d_redundantLits->insert(lit);
181
  }
182
529680
}
183
184
/// SatProof
185
template <class Solver>
186
1826
TSatProof<Solver>::TSatProof(Solver* solver, context::Context* context,
187
                             const std::string& name, bool checkRes)
188
    : d_name(name),
189
      d_emptyClauseId(ClauseIdEmpty),
190
      d_seenLearnt(),
191
      d_assumptionConflictsDebug(),
192
      d_solver(solver),
193
      d_context(context),
194
      d_idClause(),
195
      d_clauseId(),
196
      d_idUnit(context),
197
      d_unitId(context),
198
      d_deleted(),
199
      d_inputClauses(),
200
      d_lemmaClauses(),
201
      d_assumptions(),
202
      d_assumptionConflicts(),
203
      d_resolutionChains(d_context),
204
      d_resStack(),
205
      d_checkRes(checkRes),
206
      d_nullId(-2),
207
      d_temp_clauseId(),
208
      d_temp_idClause(),
209
      d_unitConflictId(context),
210
      d_trueLit(ClauseIdUndef),
211
      d_falseLit(ClauseIdUndef),
212
      d_seenInputs(),
213
      d_seenLemmas(),
214
      d_satProofConstructed(false),
215
1826
      d_statistics(name) {
216
1826
}
217
218
template <class Solver>
219
1826
TSatProof<Solver>::~TSatProof() {
220
  // FIXME: double free if deleted clause also appears in d_seenLemmas?
221
1826
  IdToSatClause::const_iterator it = d_deletedTheoryLemmas.begin();
222
1826
  IdToSatClause::const_iterator end = d_deletedTheoryLemmas.end();
223
224
109526
  for (; it != end; ++it) {
225
53850
    ClauseId id = it->first;
226
    // otherwise deleted in next loop
227
53850
    if (d_seenLemmas.find(id) == d_seenLemmas.end()) {
228
39459
      delete it->second;
229
    }
230
  }
231
232
1826
  IdToSatClause::const_iterator seen_lemma_it = d_seenLemmas.begin();
233
1826
  IdToSatClause::const_iterator seen_lemma_end = d_seenLemmas.end();
234
235
65402
  for (; seen_lemma_it != seen_lemma_end; ++seen_lemma_it) {
236
31788
    delete seen_lemma_it->second;
237
  }
238
239
1826
  IdToSatClause::const_iterator seen_input_it = d_seenInputs.begin();
240
1826
  IdToSatClause::const_iterator seen_input_end = d_seenInputs.end();
241
242
55472
  for (; seen_input_it != seen_input_end; ++seen_input_it) {
243
26823
    delete seen_input_it->second;
244
  }
245
246
  typedef typename IdResMap::const_iterator ResolutionChainIterator;
247
1826
  ResolutionChainIterator resolution_it = d_resolutionChains.begin();
248
1826
  ResolutionChainIterator resolution_it_end = d_resolutionChains.end();
249
1826
  for (; resolution_it != resolution_it_end; ++resolution_it) {
250
    ResChain<Solver>* current = (*resolution_it).second;
251
    delete current;
252
  }
253
254
  // It could be the case that d_resStack is not empty at destruction time
255
  // (for example in the SAT case).
256
1826
  typename ResStack::const_iterator resolution_stack_it = d_resStack.begin();
257
1826
  typename ResStack::const_iterator resolution_stack_it_end = d_resStack.end();
258
1826
  for (; resolution_stack_it != resolution_stack_it_end;
259
       ++resolution_stack_it) {
260
    ResChain<Solver>* current = *resolution_stack_it;
261
    delete current;
262
  }
263
1826
}
264
265
/**
266
 * Returns true if the resolution chain corresponding to id
267
 * does resolve to the clause associated to id
268
 * @param id
269
 *
270
 * @return
271
 */
272
template <class Solver>
273
bool TSatProof<Solver>::checkResolution(ClauseId id) {
274
  if (d_checkRes) {
275
    bool validRes = true;
276
    Assert(hasResolutionChain(id));
277
    const ResolutionChain& res = getResolutionChain(id);
278
    LitSet clause1;
279
    createLitSet(res.getStart(), clause1);
280
    const typename ResolutionChain::ResSteps& steps = res.getSteps();
281
    for (unsigned i = 0; i < steps.size(); i++) {
282
      typename Solver::TLit var = steps[i].lit;
283
      LitSet clause2;
284
      createLitSet(steps[i].id, clause2);
285
      if (!resolve<Solver>(var, clause1, clause2, steps[i].sign))
286
      {
287
        validRes = false;
288
        break;
289
      }
290
    }
291
    // compare clause we claimed to prove with the resolution result
292
    if (isUnit(id)) {
293
      // special case if it was a unit clause
294
      typename Solver::TLit unit = getUnit(id);
295
      validRes = clause1.size() == clause1.count(unit) && !clause1.empty();
296
      return validRes;
297
    }
298
    if (id == d_emptyClauseId) {
299
      return clause1.empty();
300
    }
301
302
    LitVector c;
303
    getLitVec(id, c);
304
305
    for (unsigned i = 0; i < c.size(); ++i) {
306
      int count = clause1.erase(c[i]);
307
      if (count == 0) {
308
        if (Debug.isOn("proof:sat")) {
309
          Debug("proof:sat")
310
              << "proof:checkResolution::literal not in computed result ";
311
          printLit<Solver>(c[i]);
312
          Debug("proof:sat") << "\n";
313
        }
314
        validRes = false;
315
      }
316
    }
317
    validRes = clause1.empty();
318
    if (!validRes) {
319
      if (Debug.isOn("proof:sat")) {
320
        Debug("proof:sat") << "proof:checkResolution::Invalid Resolution, "
321
                              "unremoved literals: \n";
322
        printLitSet<Solver>(clause1);
323
        Debug("proof:sat") << "proof:checkResolution:: result should be: \n";
324
        printClause<Solver>(c);
325
      }
326
    }
327
    return validRes;
328
329
  } else {
330
    return true;
331
  }
332
}
333
334
/// helper methods
335
template <class Solver>
336
412354
bool TSatProof<Solver>::hasClauseIdForCRef(typename Solver::TCRef ref) const {
337
412354
  return d_clauseId.find(ref) != d_clauseId.end();
338
}
339
340
template <class Solver>
341
333169
ClauseId TSatProof<Solver>::getClauseIdForCRef(
342
    typename Solver::TCRef ref) const {
343
333169
  if (d_clauseId.find(ref) == d_clauseId.end()) {
344
    Debug("proof:sat") << "Missing clause \n";
345
  }
346
333169
  Assert(hasClauseIdForCRef(ref));
347
333169
  return d_clauseId.find(ref)->second;
348
}
349
350
template <class Solver>
351
394046
bool TSatProof<Solver>::hasClauseIdForLiteral(typename Solver::TLit lit) const {
352
394046
  return d_unitId.find(toInt(lit)) != d_unitId.end();
353
}
354
355
template <class Solver>
356
394046
ClauseId TSatProof<Solver>::getClauseIdForLiteral(
357
    typename Solver::TLit lit) const {
358
394046
  Assert(hasClauseIdForLiteral(lit));
359
394046
  return (*d_unitId.find(toInt(lit))).second;
360
}
361
362
template <class Solver>
363
635212
bool TSatProof<Solver>::hasClauseRef(ClauseId id) const {
364
635212
  return d_idClause.find(id) != d_idClause.end();
365
}
366
367
template <class Solver>
368
317606
typename Solver::TCRef TSatProof<Solver>::getClauseRef(ClauseId id) const {
369
317606
  if (!hasClauseRef(id)) {
370
    Debug("proof:sat") << "proof:getClauseRef cannot find clause " << id << " "
371
                       << ((d_deleted.find(id) != d_deleted.end()) ? "deleted"
372
                                                                   : "")
373
                       << (isUnit(id) ? "Unit" : "") << std::endl;
374
  }
375
317606
  Assert(hasClauseRef(id));
376
317606
  return d_idClause.find(id)->second;
377
}
378
379
template <class Solver>
380
4060526
const typename Solver::TClause& TSatProof<Solver>::getClause(
381
    typename Solver::TCRef ref) const {
382
4060526
  Assert(ref != Solver::TCRef_Undef);
383
4060526
  Assert(ref >= 0 && ref < d_solver->ca.size());
384
4060526
  return d_solver->ca[ref];
385
}
386
387
template <class Solver>
388
void TSatProof<Solver>::getLitVec(ClauseId id, LitVector& vec) {
389
  if (isUnit(id)) {
390
    typename Solver::TLit lit = getUnit(id);
391
    vec.push_back(lit);
392
    return;
393
  }
394
  if (isAssumptionConflict(id)) {
395
    vec = *(d_assumptionConflictsDebug[id]);
396
    return;
397
  }
398
  typename Solver::TCRef cref = getClauseRef(id);
399
  const typename Solver::TClause& cl = getClause(cref);
400
  for (int i = 0; i < cl.size(); ++i) {
401
    vec.push_back(cl[i]);
402
  }
403
}
404
405
template <class Solver>
406
341003
bool TSatProof<Solver>::isUnit(ClauseId id) const {
407
341003
  return d_idUnit.find(id) != d_idUnit.end();
408
}
409
410
template <class Solver>
411
4508
typename Solver::TLit TSatProof<Solver>::getUnit(ClauseId id) const {
412
4508
  Assert(isUnit(id));
413
4508
  return (*d_idUnit.find(id)).second;
414
}
415
416
template <class Solver>
417
721585
bool TSatProof<Solver>::isUnit(typename Solver::TLit lit) const {
418
721585
  return d_unitId.find(toInt(lit)) != d_unitId.end();
419
}
420
421
template <class Solver>
422
151694
ClauseId TSatProof<Solver>::getUnitId(typename Solver::TLit lit) const {
423
151694
  Assert(isUnit(lit));
424
151694
  return (*d_unitId.find(toInt(lit))).second;
425
}
426
427
template <class Solver>
428
527494
bool TSatProof<Solver>::hasResolutionChain(ClauseId id) const {
429
527494
  return d_resolutionChains.find(id) != d_resolutionChains.end();
430
}
431
432
template <class Solver>
433
const typename TSatProof<Solver>::ResolutionChain&
434
39672
TSatProof<Solver>::getResolutionChain(ClauseId id) const {
435
39672
  Assert(hasResolutionChain(id));
436
39672
  const ResolutionChain* chain = (*d_resolutionChains.find(id)).second;
437
39672
  return *chain;
438
}
439
440
template <class Solver>
441
324456
bool TSatProof<Solver>::isInputClause(ClauseId id) const {
442
324456
  return d_inputClauses.find(id) != d_inputClauses.end();
443
}
444
445
template <class Solver>
446
162149
bool TSatProof<Solver>::isLemmaClause(ClauseId id) const {
447
162149
  return d_lemmaClauses.find(id) != d_lemmaClauses.end();
448
}
449
450
template <class Solver>
451
39672
bool TSatProof<Solver>::isAssumptionConflict(ClauseId id) const {
452
39672
  return d_assumptionConflicts.find(id) != d_assumptionConflicts.end();
453
}
454
455
template <class Solver>
456
void TSatProof<Solver>::print(ClauseId id) const {
457
  if (d_deleted.find(id) != d_deleted.end()) {
458
    Debug("proof:sat") << "del" << id;
459
  } else if (isUnit(id)) {
460
    printLit<Solver>(getUnit(id));
461
  } else if (id == d_emptyClauseId) {
462
    Debug("proof:sat") << "empty " << std::endl;
463
  } else {
464
    typename Solver::TCRef ref = getClauseRef(id);
465
    printClause<Solver>(getClause(ref));
466
  }
467
}
468
469
template <class Solver>
470
void TSatProof<Solver>::printRes(ClauseId id) const {
471
  Assert(hasResolutionChain(id));
472
  Debug("proof:sat") << "id " << id << ": ";
473
  printRes(getResolutionChain(id));
474
}
475
476
template <class Solver>
477
void TSatProof<Solver>::printRes(const ResolutionChain& res) const {
478
  ClauseId start_id = res.getStart();
479
480
  if (Debug.isOn("proof:sat")) {
481
    Debug("proof:sat") << "(";
482
    print(start_id);
483
  }
484
485
  const typename ResolutionChain::ResSteps& steps = res.getSteps();
486
  for (unsigned i = 0; i < steps.size(); i++) {
487
    typename Solver::TLit v = steps[i].lit;
488
    ClauseId id = steps[i].id;
489
490
    if (Debug.isOn("proof:sat")) {
491
      Debug("proof:sat") << "[";
492
      printLit<Solver>(v);
493
      Debug("proof:sat") << "] ";
494
      print(id);
495
    }
496
  }
497
  Debug("proof:sat") << ") \n";
498
}
499
500
/// registration methods
501
template <class Solver>
502
3615261
ClauseId TSatProof<Solver>::registerClause(typename Solver::TCRef clause,
503
                                           ClauseKind kind) {
504
3615261
  Assert(clause != Solver::TCRef_Undef);
505
3615261
  typename ClauseIdMap::iterator it = d_clauseId.find(clause);
506
3615261
  if (it == d_clauseId.end()) {
507
483001
    ClauseId newId = ProofManager::currentPM()->nextId();
508
509
483001
    d_clauseId.insert(std::make_pair(clause, newId));
510
483001
    d_idClause.insert(std::make_pair(newId, clause));
511
483001
    if (kind == INPUT) {
512
189783
      Assert(d_inputClauses.find(newId) == d_inputClauses.end());
513
189783
      d_inputClauses.insert(newId);
514
    }
515
483001
    if (kind == THEORY_LEMMA) {
516
227604
      Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end());
517
227604
      d_lemmaClauses.insert(newId);
518
455208
      Debug("pf::sat") << "TSatProof::registerClause registering a new lemma clause: "
519
227604
                       << newId << " = " << *buildClause(newId)
520
                       << std::endl;
521
    }
522
  }
523
524
3615261
  ClauseId id = d_clauseId[clause];
525
3615261
  Assert(kind != INPUT || d_inputClauses.count(id));
526
3615261
  Assert(kind != THEORY_LEMMA || d_lemmaClauses.count(id));
527
528
7230522
  Debug("proof:sat:detailed") << "registerClause CRef: " << clause
529
3615261
                              << " id: " << d_clauseId[clause]
530
3615261
                              << "                kind: " << kind << "\n";
531
  // ProofManager::currentPM()->setRegisteredClauseId( d_clauseId[clause] );
532
3615261
  return id;
533
}
534
535
template <class Solver>
536
81280
ClauseId TSatProof<Solver>::registerUnitClause(typename Solver::TLit lit,
537
                                               ClauseKind kind) {
538
81280
  Debug("cores") << "registerUnitClause " << kind << std::endl;
539
81280
  typename UnitIdMap::iterator it = d_unitId.find(toInt(lit));
540
81280
  if (it == d_unitId.end()) {
541
81206
    ClauseId newId = ProofManager::currentPM()->nextId();
542
543
81206
    if (d_unitId.find(toInt(lit)) == d_unitId.end())
544
81206
      d_unitId[toInt(lit)] = newId;
545
81206
    if (d_idUnit.find(newId) == d_idUnit.end())
546
81206
      d_idUnit[newId] = lit;
547
548
81206
    if (kind == INPUT) {
549
45138
      Assert(d_inputClauses.find(newId) == d_inputClauses.end());
550
90276
      Debug("pf::sat") << "TSatProof::registerUnitClause: registering a new "
551
                          "input (UNIT CLAUSE): "
552
45138
                       << lit << std::endl;
553
45138
      d_inputClauses.insert(newId);
554
    }
555
81206
    if (kind == THEORY_LEMMA) {
556
9674
      Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end());
557
19348
      Debug("pf::sat") << "TSatProof::registerUnitClause: registering a new lemma (UNIT CLAUSE): "
558
9674
                       << lit
559
                       << std::endl;
560
9674
      d_lemmaClauses.insert(newId);
561
    }
562
  }
563
81280
  ClauseId id = d_unitId[toInt(lit)];
564
81280
  Assert(kind != INPUT || d_inputClauses.count(id));
565
81280
  Assert(kind != THEORY_LEMMA || d_lemmaClauses.count(id));
566
162560
  Debug("proof:sat:detailed") << "registerUnitClause id: " << id
567
81280
                              << " kind: " << kind << "\n";
568
  // ProofManager::currentPM()->setRegisteredClauseId( d_unitId[toInt(lit)] );
569
81280
  return id;
570
}
571
template <class Solver>
572
1826
void TSatProof<Solver>::registerTrueLit(const typename Solver::TLit lit) {
573
1826
  Assert(d_trueLit == ClauseIdUndef);
574
1826
  d_trueLit = registerUnitClause(lit, INPUT);
575
1826
}
576
577
template <class Solver>
578
1826
void TSatProof<Solver>::registerFalseLit(const typename Solver::TLit lit) {
579
1826
  Assert(d_falseLit == ClauseIdUndef);
580
1826
  d_falseLit = registerUnitClause(lit, INPUT);
581
1826
}
582
583
template <class Solver>
584
1826
ClauseId TSatProof<Solver>::getTrueUnit() const {
585
1826
  Assert(d_trueLit != ClauseIdUndef);
586
1826
  return d_trueLit;
587
}
588
589
template <class Solver>
590
1826
ClauseId TSatProof<Solver>::getFalseUnit() const {
591
1826
  Assert(d_falseLit != ClauseIdUndef);
592
1826
  return d_falseLit;
593
}
594
595
template <class Solver>
596
void TSatProof<Solver>::registerAssumption(const typename Solver::TVar var) {
597
  Assert(d_assumptions.find(var) == d_assumptions.end());
598
  d_assumptions.insert(var);
599
}
600
601
template <class Solver>
602
ClauseId TSatProof<Solver>::registerAssumptionConflict(
603
    const typename Solver::TLitVec& confl) {
604
  Debug("proof:sat:detailed") << "registerAssumptionConflict " << std::endl;
605
  // Uniqueness is checked in the bit-vector proof
606
  // should be vars
607
  for (int i = 0; i < confl.size(); ++i) {
608
    Assert(d_assumptions.find(var(confl[i])) != d_assumptions.end());
609
  }
610
  ClauseId new_id = ProofManager::currentPM()->nextId();
611
  d_assumptionConflicts.insert(new_id);
612
  LitVector* vec_confl = new LitVector(confl.size());
613
  for (int i = 0; i < confl.size(); ++i) {
614
    vec_confl->operator[](i) = confl[i];
615
  }
616
  if (Debug.isOn("proof:sat:detailed")) {
617
    printClause<Solver>(*vec_confl);
618
    Debug("proof:sat:detailed") << "\n";
619
  }
620
621
  d_assumptionConflictsDebug[new_id] = vec_confl;
622
  return new_id;
623
}
624
625
template <class Solver>
626
1526161
void TSatProof<Solver>::removedDfs(typename Solver::TLit lit,
627
                                   LitSet* removedSet, LitVector& removeStack,
628
                                   LitSet& inClause, LitSet& seen) {
629
  // if we already added the literal return
630
1526161
  if (seen.count(lit)) {
631
90155
    return;
632
  }
633
634
1436006
  typename Solver::TCRef reason_ref = d_solver->reason(var(lit));
635
1436006
  if (reason_ref == Solver::TCRef_Undef) {
636
151694
    seen.insert(lit);
637
151694
    removeStack.push_back(lit);
638
151694
    return;
639
  }
640
641
1284312
  int size = getClause(reason_ref).size();
642
3582481
  for (int i = 1; i < size; i++) {
643
2298169
    typename Solver::TLit v = getClause(reason_ref)[i];
644
2298169
    if (inClause.count(v) == 0 && seen.count(v) == 0) {
645
996481
      removedDfs(v, removedSet, removeStack, inClause, seen);
646
    }
647
  }
648
1284312
  if (seen.count(lit) == 0) {
649
1284312
    seen.insert(lit);
650
1284312
    removeStack.push_back(lit);
651
  }
652
}
653
654
template <class Solver>
655
93776
void TSatProof<Solver>::removeRedundantFromRes(ResChain<Solver>* res,
656
                                               ClauseId id) {
657
93776
  LitSet* removed = res->getRedundant();
658
93776
  if (removed == NULL) {
659
44909
    return;
660
  }
661
662
97734
  LitSet inClause;
663
48867
  createLitSet(id, inClause);
664
665
97734
  LitVector removeStack;
666
97734
  LitSet seen;
667
578547
  for (typename LitSet::iterator it = removed->begin(); it != removed->end();
668
       ++it) {
669
529680
    removedDfs(*it, removed, removeStack, inClause, seen);
670
  }
671
672
1484873
  for (int i = removeStack.size() - 1; i >= 0; --i) {
673
1436006
    typename Solver::TLit lit = removeStack[i];
674
1436006
    typename Solver::TCRef reason_ref = d_solver->reason(var(lit));
675
    ClauseId reason_id;
676
677
1436006
    if (reason_ref == Solver::TCRef_Undef) {
678
151694
      Assert(isUnit(~lit));
679
151694
      reason_id = getUnitId(~lit);
680
    } else {
681
1284312
      reason_id = registerClause(reason_ref, LEARNT);
682
    }
683
1436006
    res->addStep(lit, reason_id, !sign(lit));
684
  }
685
48867
  removed->clear();
686
}
687
688
template <class Solver>
689
93776
void TSatProof<Solver>::registerResolution(ClauseId id, ResChain<Solver>* res) {
690
93776
  Assert(res != NULL);
691
692
93776
  removeRedundantFromRes(res, id);
693
93776
  Assert(res->redundantRemoved());
694
695
  // Because the SAT solver can add the same clause multiple times, it
696
  // could be the case that a resolution chain for this clause already
697
  // exists (e.g. when removing units in addClause).
698
93776
  if (hasResolutionChain(id)) {
699
    ResChain<Solver>* current = (*d_resolutionChains.find(id)).second;
700
    delete current;
701
  }
702
703
93776
  d_resolutionChains.insert(id, res);
704
705
93776
  if (Debug.isOn("proof:sat")) {
706
    printRes(id);
707
  }
708
93776
  if (d_checkRes) {
709
    Assert(checkResolution(id));
710
  }
711
712
93776
}
713
714
/// recording resolutions
715
template <class Solver>
716
67857
void TSatProof<Solver>::startResChain(typename Solver::TCRef start) {
717
67857
  ClauseId id = getClauseIdForCRef(start);
718
67857
  ResolutionChain* res = new ResolutionChain(id);
719
67857
  d_resStack.push_back(res);
720
67857
}
721
722
template <class Solver>
723
void TSatProof<Solver>::startResChain(typename Solver::TLit start) {
724
  ClauseId id = getUnitId(start);
725
  ResolutionChain* res = new ResolutionChain(id);
726
  d_resStack.push_back(res);
727
}
728
729
template <class Solver>
730
1822420
void TSatProof<Solver>::addResolutionStep(typename Solver::TLit lit,
731
                                          typename Solver::TCRef clause,
732
                                          bool sign) {
733
1822420
  ClauseId id = registerClause(clause, LEARNT);
734
1822420
  ResChain<Solver>* res = d_resStack.back();
735
1822420
  res->addStep(lit, id, sign);
736
1822420
}
737
738
template <class Solver>
739
65614
void TSatProof<Solver>::endResChain(ClauseId id) {
740
65614
  Debug("proof:sat:detailed") << "endResChain " << id << "\n";
741
65614
  Assert(d_resStack.size() > 0);
742
65614
  ResChain<Solver>* res = d_resStack.back();
743
65614
  registerResolution(id, res);
744
65614
  d_resStack.pop_back();
745
65614
}
746
747
template <class Solver>
748
2243
void TSatProof<Solver>::endResChain(typename Solver::TLit lit) {
749
2243
  Assert(d_resStack.size() > 0);
750
2243
  ClauseId id = registerUnitClause(lit, LEARNT);
751
2243
  Debug("proof:sat:detailed") << "endResChain unit " << id << "\n";
752
2243
  ResolutionChain* res = d_resStack.back();
753
2243
  d_glueMap[id] = 1;
754
2243
  registerResolution(id, res);
755
2243
  d_resStack.pop_back();
756
2243
}
757
758
template <class Solver>
759
void TSatProof<Solver>::cancelResChain() {
760
  Assert(d_resStack.size() > 0);
761
  ResolutionChain* back = d_resStack.back();
762
  delete back;
763
  d_resStack.pop_back();
764
}
765
766
template <class Solver>
767
529680
void TSatProof<Solver>::storeLitRedundant(typename Solver::TLit lit) {
768
529680
  Assert(d_resStack.size() > 0);
769
529680
  ResolutionChain* res = d_resStack.back();
770
529680
  res->addRedundantLit(lit);
771
529680
}
772
773
/// constructing resolutions
774
template <class Solver>
775
365352
void TSatProof<Solver>::resolveOutUnit(typename Solver::TLit lit) {
776
365352
  ClauseId id = resolveUnit(~lit);
777
365352
  ResChain<Solver>* res = d_resStack.back();
778
365352
  res->addStep(lit, id, !sign(lit));
779
365352
}
780
template <class Solver>
781
2260
void TSatProof<Solver>::storeUnitResolution(typename Solver::TLit lit) {
782
2260
  Debug("cores") << "STORE UNIT RESOLUTION" << std::endl;
783
2260
  resolveUnit(lit);
784
2260
}
785
template <class Solver>
786
418197
ClauseId TSatProof<Solver>::resolveUnit(typename Solver::TLit lit) {
787
  // first check if we already have a resolution for lit
788
789
418197
  if (isUnit(lit)) {
790
394046
    ClauseId id = getClauseIdForLiteral(lit);
791
394046
    Assert(hasResolutionChain(id) || isInputClause(id) || isLemmaClause(id));
792
394046
    return id;
793
  }
794
24151
  typename Solver::TCRef reason_ref = d_solver->reason(var(lit));
795
24151
  Assert(reason_ref != Solver::TCRef_Undef);
796
797
24151
  ClauseId reason_id = registerClause(reason_ref, LEARNT);
798
799
24151
  ResChain<Solver>* res = new ResChain<Solver>(reason_id);
800
  // Here, the call to resolveUnit() can reallocate memory in the
801
  // clause allocator.  So reload reason ptr each time.
802
24151
  const typename Solver::TClause& initial_reason = getClause(reason_ref);
803
24151
  size_t current_reason_size = initial_reason.size();
804
91780
  for (size_t i = 0; i < current_reason_size; i++) {
805
67629
    const typename Solver::TClause& current_reason = getClause(reason_ref);
806
67629
    current_reason_size = current_reason.size();
807
67629
    typename Solver::TLit l = current_reason[i];
808
67629
    if (lit != l) {
809
43478
      ClauseId res_id = resolveUnit(~l);
810
43478
      res->addStep(l, res_id, !sign(l));
811
    }
812
  }
813
24151
  ClauseId unit_id = registerUnitClause(lit, LEARNT);
814
24151
  registerResolution(unit_id, res);
815
24151
  return unit_id;
816
}
817
818
template <class Solver>
819
391
ClauseId TSatProof<Solver>::storeUnitConflict(
820
    typename Solver::TLit conflict_lit, ClauseKind kind) {
821
391
  Debug("cores") << "STORE UNIT CONFLICT" << std::endl;
822
391
  Assert(!d_unitConflictId.isSet());
823
391
  d_unitConflictId.set(registerUnitClause(conflict_lit, kind));
824
391
  Debug("proof:sat:detailed") << "storeUnitConflict " << d_unitConflictId.get()
825
                              << "\n";
826
391
  return d_unitConflictId.get();
827
}
828
829
template <class Solver>
830
1768
void TSatProof<Solver>::finalizeProof(typename Solver::TCRef conflict_ref) {
831
1768
  Assert(d_resStack.size() == 0);
832
1768
  Assert(conflict_ref != Solver::TCRef_Undef);
833
  ClauseId conflict_id;
834
1768
  if (conflict_ref == Solver::TCRef_Lazy) {
835
391
    Assert(d_unitConflictId.isSet());
836
391
    conflict_id = d_unitConflictId.get();
837
838
391
    ResChain<Solver>* res = new ResChain<Solver>(conflict_id);
839
391
    typename Solver::TLit lit = d_idUnit[conflict_id];
840
391
    ClauseId res_id = resolveUnit(~lit);
841
391
    res->addStep(lit, res_id, !sign(lit));
842
391
    registerResolution(d_emptyClauseId, res);
843
391
    return;
844
845
  } else {
846
1377
    Assert(!d_unitConflictId.isSet());
847
1377
    conflict_id = registerClause(conflict_ref, LEARNT);  // FIXME
848
  }
849
850
1377
  if (Debug.isOn("proof:sat")) {
851
    Debug("proof:sat") << "proof::finalizeProof Final Conflict ";
852
    print(conflict_id);
853
    Debug("proof:sat") << std::endl;
854
  }
855
856
1377
  ResChain<Solver>* res = new ResChain<Solver>(conflict_id);
857
  // Here, the call to resolveUnit() can reallocate memory in the
858
  // clause allocator.  So reload conflict ptr each time.
859
8093
  for (int i = 0; i < getClause(conflict_ref).size(); ++i) {
860
6716
    const typename Solver::TClause& conflict = getClause(conflict_ref);
861
6716
    typename Solver::TLit lit = conflict[i];
862
6716
    ClauseId res_id = resolveUnit(~lit);
863
6716
    res->addStep(lit, res_id, !sign(lit));
864
  }
865
866
1377
  registerResolution(d_emptyClauseId, res);
867
}
868
869
/// CRef manager
870
template <class Solver>
871
186127
void TSatProof<Solver>::updateCRef(typename Solver::TCRef oldref,
872
                                   typename Solver::TCRef newref) {
873
186127
  if (d_clauseId.find(oldref) == d_clauseId.end()) {
874
    return;
875
  }
876
186127
  ClauseId id = getClauseIdForCRef(oldref);
877
186127
  Assert(d_temp_clauseId.find(newref) == d_temp_clauseId.end());
878
186127
  Assert(d_temp_idClause.find(id) == d_temp_idClause.end());
879
186127
  d_temp_clauseId[newref] = id;
880
186127
  d_temp_idClause[id] = newref;
881
}
882
883
template <class Solver>
884
822
void TSatProof<Solver>::finishUpdateCRef() {
885
822
  d_clauseId.swap(d_temp_clauseId);
886
822
  d_temp_clauseId.clear();
887
888
822
  d_idClause.swap(d_temp_idClause);
889
822
  d_temp_idClause.clear();
890
822
}
891
892
template <class Solver>
893
79185
void TSatProof<Solver>::markDeleted(typename Solver::TCRef clause) {
894
79185
  if (hasClauseIdForCRef(clause)) {
895
79185
    ClauseId id = getClauseIdForCRef(clause);
896
79185
    Assert(d_deleted.find(id) == d_deleted.end());
897
79185
    d_deleted.insert(id);
898
79185
    if (isLemmaClause(id)) {
899
53850
      const typename Solver::TClause& minisat_cl = getClause(clause);
900
53850
      prop::SatClause* sat_cl = new prop::SatClause();
901
53850
      toSatClause<Solver>(minisat_cl, *sat_cl);
902
107700
      d_deletedTheoryLemmas.insert(std::make_pair(id, sat_cl));
903
    }
904
  }
905
79185
}
906
907
template <class Solver>
908
void TSatProof<Solver>::constructProof(ClauseId conflict) {
909
  d_satProofConstructed = true;
910
  collectClauses(conflict);
911
}
912
913
template <class Solver>
914
908
void TSatProof<Solver>::refreshProof(ClauseId conflict) {
915
908
  IdToSatClause::const_iterator seen_lemma_it = d_seenLemmas.begin();
916
908
  IdToSatClause::const_iterator seen_lemma_end = d_seenLemmas.end();
917
918
1540
  for (; seen_lemma_it != seen_lemma_end; ++seen_lemma_it) {
919
316
    if (d_deletedTheoryLemmas.find(seen_lemma_it->first) == d_deletedTheoryLemmas.end())
920
15
      delete seen_lemma_it->second;
921
  }
922
923
908
  IdToSatClause::const_iterator seen_input_it = d_seenInputs.begin();
924
908
  IdToSatClause::const_iterator seen_input_end = d_seenInputs.end();
925
926
3102
  for (; seen_input_it != seen_input_end; ++seen_input_it) {
927
1097
    delete seen_input_it->second;
928
  }
929
930
908
  d_seenInputs.clear();
931
908
  d_seenLemmas.clear();
932
908
  d_seenLearnt.clear();
933
934
908
  collectClauses(conflict);
935
908
}
936
937
template <class Solver>
938
bool TSatProof<Solver>::proofConstructed() const {
939
  return d_satProofConstructed;
940
}
941
942
template <class Solver>
943
287628
prop::SatClause* TSatProof<Solver>::buildClause(ClauseId id) {
944
287628
  if (isUnit(id)) {
945
4504
    typename Solver::TLit lit = getUnit(id);
946
4504
    prop::SatLiteral sat_lit = toSatLiteral<Solver>(lit);
947
4504
    prop::SatClause* clause = new prop::SatClause();
948
4504
    clause->push_back(sat_lit);
949
4504
    return clause;
950
  }
951
952
283124
  if (isDeleted(id)) {
953
14381
    prop::SatClause* clause = d_deletedTheoryLemmas.find(id)->second;
954
14381
    return clause;
955
  }
956
957
268743
  typename Solver::TCRef ref = getClauseRef(id);
958
268743
  const typename Solver::TClause& minisat_cl = getClause(ref);
959
268743
  prop::SatClause* clause = new prop::SatClause();
960
268743
  toSatClause<Solver>(minisat_cl, *clause);
961
268743
  return clause;
962
}
963
964
template <class Solver>
965
bool TSatProof<Solver>::derivedEmptyClause() const {
966
  return hasResolutionChain(d_emptyClauseId);
967
}
968
969
template <class Solver>
970
1614021
void TSatProof<Solver>::collectClauses(ClauseId id) {
971
3764863
  if (d_seenInputs.find(id) != d_seenInputs.end() ||
972
3644194
      d_seenLemmas.find(id) != d_seenLemmas.end() ||
973
2030173
      d_seenLearnt.find(id) != d_seenLearnt.end()) {
974
1514325
    return;
975
  }
976
977
99696
  if (isInputClause(id)) {
978
27920
    d_seenInputs.insert(std::make_pair(id, buildClause(id)));
979
27920
    return;
980
71776
  } else if (isLemmaClause(id)) {
981
32104
    d_seenLemmas.insert(std::make_pair(id, buildClause(id)));
982
32104
    return;
983
39672
  } else if (!isAssumptionConflict(id)) {
984
39672
    d_seenLearnt.insert(id);
985
  }
986
987
39672
  const ResolutionChain& res = getResolutionChain(id);
988
39672
  const typename ResolutionChain::ResSteps& steps = res.getSteps();
989
39672
  ClauseId start = res.getStart();
990
39672
  collectClauses(start);
991
992
1613113
  for (size_t i = 0; i < steps.size(); i++) {
993
1573441
    collectClauses(steps[i].id);
994
  }
995
}
996
997
template <class Solver>
998
908
void TSatProof<Solver>::collectClausesUsed(IdToSatClause& inputs,
999
                                           IdToSatClause& lemmas) {
1000
908
  inputs = d_seenInputs;
1001
908
  lemmas = d_seenLemmas;
1002
908
}
1003
1004
template <class Solver>
1005
void TSatProof<Solver>::storeClauseGlue(ClauseId clause, int glue) {
1006
  Assert(d_glueMap.find(clause) == d_glueMap.end());
1007
  d_glueMap.insert(std::make_pair(clause, glue));
1008
}
1009
1010
template <class Solver>
1011
1826
TSatProof<Solver>::Statistics::Statistics(const std::string& prefix)
1012
    : d_numLearnedClauses("satproof::" + prefix + "::NumLearnedClauses", 0),
1013
      d_numLearnedInProof("satproof::" + prefix + "::NumLearnedInProof", 0),
1014
      d_numLemmasInProof("satproof::" + prefix + "::NumLemmasInProof", 0),
1015
      d_avgChainLength("satproof::" + prefix + "::AvgResChainLength"),
1016
      d_resChainLengths("satproof::" + prefix + "::ResChainLengthsHist"),
1017
      d_usedResChainLengths("satproof::" + prefix +
1018
                            "::UsedResChainLengthsHist"),
1019
      d_clauseGlue("satproof::" + prefix + "::ClauseGlueHist"),
1020
1826
      d_usedClauseGlue("satproof::" + prefix + "::UsedClauseGlueHist") {
1021
1826
  smtStatisticsRegistry()->registerStat(&d_numLearnedClauses);
1022
1826
  smtStatisticsRegistry()->registerStat(&d_numLearnedInProof);
1023
1826
  smtStatisticsRegistry()->registerStat(&d_numLemmasInProof);
1024
1826
  smtStatisticsRegistry()->registerStat(&d_avgChainLength);
1025
1826
  smtStatisticsRegistry()->registerStat(&d_resChainLengths);
1026
1826
  smtStatisticsRegistry()->registerStat(&d_usedResChainLengths);
1027
1826
  smtStatisticsRegistry()->registerStat(&d_clauseGlue);
1028
1826
  smtStatisticsRegistry()->registerStat(&d_usedClauseGlue);
1029
1826
}
1030
1031
template <class Solver>
1032
1826
TSatProof<Solver>::Statistics::~Statistics() {
1033
1826
  smtStatisticsRegistry()->unregisterStat(&d_numLearnedClauses);
1034
1826
  smtStatisticsRegistry()->unregisterStat(&d_numLearnedInProof);
1035
1826
  smtStatisticsRegistry()->unregisterStat(&d_numLemmasInProof);
1036
1826
  smtStatisticsRegistry()->unregisterStat(&d_avgChainLength);
1037
1826
  smtStatisticsRegistry()->unregisterStat(&d_resChainLengths);
1038
1826
  smtStatisticsRegistry()->unregisterStat(&d_usedResChainLengths);
1039
1826
  smtStatisticsRegistry()->unregisterStat(&d_clauseGlue);
1040
1826
  smtStatisticsRegistry()->unregisterStat(&d_usedClauseGlue);
1041
1826
}
1042
1043
inline std::ostream& operator<<(std::ostream& out, CVC4::ClauseKind k) {
1044
  switch (k) {
1045
    case CVC4::INPUT:
1046
      out << "INPUT";
1047
      break;
1048
    case CVC4::THEORY_LEMMA:
1049
      out << "THEORY_LEMMA";
1050
      break;
1051
    case CVC4::LEARNT:
1052
      out << "LEARNT";
1053
      break;
1054
    default:
1055
      out << "ClauseKind Unknown! [" << unsigned(k) << "]";
1056
  }
1057
1058
  return out;
1059
}
1060
1061
} /* CVC4 namespace */
1062
1063
#endif /* CVC4__SAT__PROOF_IMPLEMENTATION_H */