GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/prop/sat_proof_manager.cpp Lines: 299 420 71.2 %
Date: 2021-03-22 Branches: 610 2078 29.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sat_proof_manager.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Haniel Barbosa, Andrew Reynolds
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 Implementation of the proof manager for Minisat
13
 **/
14
15
#include "prop/sat_proof_manager.h"
16
17
#include "expr/proof_node_algorithm.h"
18
#include "options/proof_options.h"
19
#include "prop/cnf_stream.h"
20
#include "prop/minisat/minisat.h"
21
#include "theory/theory_proof_step_buffer.h"
22
23
namespace CVC4 {
24
namespace prop {
25
26
966
SatProofManager::SatProofManager(Minisat::Solver* solver,
27
                                 CnfStream* cnfStream,
28
                                 context::UserContext* userContext,
29
966
                                 ProofNodeManager* pnm)
30
    : d_solver(solver),
31
      d_cnfStream(cnfStream),
32
      d_pnm(pnm),
33
      d_resChains(pnm, true, userContext),
34
      d_resChainPg(userContext, pnm),
35
      d_assumptions(userContext),
36
966
      d_conflictLit(undefSatVariable)
37
{
38
966
  d_false = NodeManager::currentNM()->mkConst(false);
39
966
}
40
41
void SatProofManager::printClause(const Minisat::Clause& clause)
42
{
43
  for (unsigned i = 0, size = clause.size(); i < size; ++i)
44
  {
45
    SatLiteral satLit = MinisatSatSolver::toSatLiteral(clause[i]);
46
    Trace("sat-proof") << satLit << " ";
47
  }
48
}
49
50
1135517
Node SatProofManager::getClauseNode(SatLiteral satLit)
51
{
52
1135517
  Assert(d_cnfStream->getNodeCache().find(satLit)
53
         != d_cnfStream->getNodeCache().end())
54
      << "SatProofManager::getClauseNode: literal " << satLit
55
      << " undefined.\n";
56
1135517
  return d_cnfStream->getNodeCache()[satLit];
57
}
58
59
2652171
Node SatProofManager::getClauseNode(const Minisat::Clause& clause)
60
{
61
5304342
  std::vector<Node> clauseNodes;
62
11097890
  for (unsigned i = 0, size = clause.size(); i < size; ++i)
63
  {
64
8445719
    SatLiteral satLit = MinisatSatSolver::toSatLiteral(clause[i]);
65
8445719
    Assert(d_cnfStream->getNodeCache().find(satLit)
66
           != d_cnfStream->getNodeCache().end())
67
        << "SatProofManager::getClauseNode: literal " << satLit
68
        << " undefined\n";
69
8445719
    clauseNodes.push_back(d_cnfStream->getNodeCache()[satLit]);
70
  }
71
  // order children by node id
72
2652171
  std::sort(clauseNodes.begin(), clauseNodes.end());
73
5304342
  return NodeManager::currentNM()->mkNode(kind::OR, clauseNodes);
74
}
75
76
14803
void SatProofManager::startResChain(const Minisat::Clause& start)
77
{
78
14803
  if (Trace.isOn("sat-proof"))
79
  {
80
    Trace("sat-proof") << "SatProofManager::startResChain: ";
81
    printClause(start);
82
    Trace("sat-proof") << "\n";
83
  }
84
14803
  d_resLinks.emplace_back(getClauseNode(start), Node::null(), true);
85
14803
}
86
87
166199
void SatProofManager::addResolutionStep(Minisat::Lit lit, bool redundant)
88
{
89
166199
  SatLiteral satLit = MinisatSatSolver::toSatLiteral(lit);
90
332398
  Node litNode = d_cnfStream->getNodeCache()[satLit];
91
166199
  bool negated = satLit.isNegated();
92
166199
  Assert(!negated || litNode.getKind() == kind::NOT);
93
166199
  if (!redundant)
94
  {
95
272914
    Trace("sat-proof") << "SatProofManager::addResolutionStep: {"
96
272914
                       << satLit.isNegated() << "} [" << satLit << "] "
97
136457
                       << ~satLit << "\n";
98
    // if lit is negated then the chain resolution construction will use it as a
99
    // pivot occurring as is in the second clause and the node under the
100
    // negation in the first clause
101
272914
    d_resLinks.emplace_back(d_cnfStream->getNodeCache()[~satLit],
102
272914
                            negated ? litNode[0] : litNode,
103
409371
                            !satLit.isNegated());
104
  }
105
  else
106
  {
107
59484
    Trace("sat-proof") << "SatProofManager::addResolutionStep: redundant lit "
108
29742
                       << satLit << " stored\n";
109
29742
    d_redundantLits.push_back(satLit);
110
  }
111
166199
}
112
113
119942
void SatProofManager::addResolutionStep(const Minisat::Clause& clause,
114
                                        Minisat::Lit lit)
115
{
116
119942
  SatLiteral satLit = MinisatSatSolver::toSatLiteral(lit);
117
239884
  Node litNode = d_cnfStream->getNodeCache()[satLit];
118
119942
  bool negated = satLit.isNegated();
119
119942
  Assert(!negated || litNode.getKind() == kind::NOT);
120
239884
  Node clauseNode = getClauseNode(clause);
121
  // if lit is negative then the chain resolution construction will use it as a
122
  // pivot occurring as is in the second clause and the node under the
123
  // negation in the first clause, which means that the third argument of the
124
  // tuple must be false
125
119942
  d_resLinks.emplace_back(clauseNode, negated ? litNode[0] : litNode, negated);
126
119942
  if (Trace.isOn("sat-proof"))
127
  {
128
    Trace("sat-proof") << "SatProofManager::addResolutionStep: {"
129
                       << satLit.isNegated() << "} [" << ~satLit << "] ";
130
    printClause(clause);
131
    Trace("sat-proof") << "\nSatProofManager::addResolutionStep:\t"
132
                       << clauseNode << "\n";
133
  }
134
119942
}
135
136
2125
void SatProofManager::endResChain(Minisat::Lit lit)
137
{
138
2125
  SatLiteral satLit = MinisatSatSolver::toSatLiteral(lit);
139
4250
  Trace("sat-proof") << "SatProofManager::endResChain: chain_res for "
140
2125
                     << satLit;
141
2125
  endResChain(getClauseNode(satLit), {satLit});
142
2125
}
143
144
12678
void SatProofManager::endResChain(const Minisat::Clause& clause)
145
{
146
12678
  if (Trace.isOn("sat-proof"))
147
  {
148
    Trace("sat-proof") << "SatProofManager::endResChain: chain_res for ";
149
    printClause(clause);
150
  }
151
25356
  std::set<SatLiteral> clauseLits;
152
102463
  for (unsigned i = 0, size = clause.size(); i < size; ++i)
153
  {
154
89785
    clauseLits.insert(MinisatSatSolver::toSatLiteral(clause[i]));
155
  }
156
12678
  endResChain(getClauseNode(clause), clauseLits);
157
12678
}
158
159
14803
void SatProofManager::endResChain(Node conclusion,
160
                                  const std::set<SatLiteral>& conclusionLits)
161
{
162
14803
  Trace("sat-proof") << ", " << conclusion << "\n";
163
  // first process redundant literals
164
29463
  std::set<SatLiteral> visited;
165
14803
  unsigned pos = d_resLinks.size();
166
44545
  for (SatLiteral satLit : d_redundantLits)
167
  {
168
29742
    processRedundantLit(satLit, conclusionLits, visited, pos);
169
  }
170
14803
  d_redundantLits.clear();
171
  // build resolution chain
172
14803
  NodeManager* nm = NodeManager::currentNM();
173
  // the conclusion is stored already in the arguments because of the
174
  // possibility of reordering
175
29463
  std::vector<Node> children, args{conclusion};
176
378640
  for (unsigned i = 0, size = d_resLinks.size(); i < size; ++i)
177
  {
178
727674
    Node clause, pivot;
179
    bool posFirst;
180
363837
    std::tie(clause, pivot, posFirst) = d_resLinks[i];
181
363837
    children.push_back(clause);
182
363837
    Trace("sat-proof") << "SatProofManager::endResChain:   ";
183
363837
    if (i > 0)
184
    {
185
698068
      Trace("sat-proof") << "{" << posFirst << "} ["
186
349034
                         << d_cnfStream->getTranslationCache()[pivot] << "] ";
187
    }
188
    // special case for clause (or l1 ... ln) being a single literal
189
    // corresponding itself to a clause, which is indicated by the pivot being
190
    // of the form (not (or l1 ... ln))
191
727674
    if (clause.getKind() == kind::OR
192
1091511
        && !(pivot.getKind() == kind::NOT && pivot[0].getKind() == kind::OR
193
363837
             && pivot[0] == clause))
194
    {
195
1102833
      for (unsigned j = 0, sizeJ = clause.getNumChildren(); j < sizeJ; ++j)
196
      {
197
902845
        Trace("sat-proof") << d_cnfStream->getTranslationCache()[clause[j]];
198
902845
        if (j < sizeJ - 1)
199
        {
200
702857
          Trace("sat-proof") << ", ";
201
        }
202
      }
203
    }
204
    else
205
    {
206
327698
      Assert(d_cnfStream->getTranslationCache().find(clause)
207
             != d_cnfStream->getTranslationCache().end())
208
163849
          << "clause node " << clause
209
163849
          << " treated as unit has no literal. Pivot is " << pivot << "\n";
210
163849
      Trace("sat-proof") << d_cnfStream->getTranslationCache()[clause];
211
    }
212
363837
    Trace("sat-proof") << " : ";
213
363837
    if (i > 0)
214
    {
215
349034
      args.push_back(nm->mkConst(posFirst));
216
349034
      args.push_back(pivot);
217
349034
      Trace("sat-proof") << "{" << posFirst << "} [" << pivot << "] ";
218
    }
219
363837
    Trace("sat-proof") << clause << "\n";
220
  }
221
  // clearing
222
14803
  d_resLinks.clear();
223
  // whether no-op
224
14803
  if (children.size() == 1)
225
  {
226
4
    Trace("sat-proof") << "SatProofManager::endResChain: no-op. The conclusion "
227
2
                       << conclusion << " is set-equal to premise "
228
2
                       << children[0] << "\n";
229
2
    return;
230
  }
231
  // whether trivial cycle
232
378213
  for (const Node& child : children)
233
  {
234
363553
    if (conclusion == child)
235
    {
236
282
      Trace("sat-proof")
237
141
          << "SatProofManager::endResChain: no-op. The conclusion "
238
141
          << conclusion << " is equal to a premise\n";
239
141
      return;
240
    }
241
  }
242
14660
  if (Trace.isOn("sat-proof") && d_resChains.hasGenerator(conclusion))
243
  {
244
    Trace("sat-proof") << "SatProofManager::endResChain: replacing proof of "
245
                       << conclusion << "\n";
246
  }
247
  // since the conclusion can be both reordered and without duplicates and the
248
  // SAT solver does not record this information, we use a MACRO_RESOLUTION
249
  // step, which bypasses these. Note that we could generate a chain resolution
250
  // rule here by explicitly computing the detailed steps, but leave this for
251
  // post-processing.
252
29320
  ProofStep ps(PfRule::MACRO_RESOLUTION, children, args);
253
14660
  d_resChainPg.addStep(conclusion, ps);
254
  // the premises of this resolution may not have been justified yet, so we do
255
  // not pass assumptions to check closedness
256
14660
  d_resChains.addLazyStep(conclusion, &d_resChainPg);
257
}
258
259
120709
void SatProofManager::processRedundantLit(
260
    SatLiteral lit,
261
    const std::set<SatLiteral>& conclusionLits,
262
    std::set<SatLiteral>& visited,
263
    unsigned pos)
264
{
265
241418
  Trace("sat-proof") << push
266
120709
                     << "SatProofManager::processRedundantLit: Lit: " << lit
267
120709
                     << "\n";
268
120709
  if (visited.count(lit))
269
  {
270
28074
    Trace("sat-proof") << "already visited\n" << pop;
271
84028
    return;
272
  }
273
  Minisat::Solver::TCRef reasonRef =
274
92635
      d_solver->reason(Minisat::var(MinisatSatSolver::toMinisatLit(lit)));
275
92635
  if (reasonRef == Minisat::Solver::TCRef_Undef)
276
  {
277
55760
    Trace("sat-proof") << "unit, add link to lit " << lit << " at pos: " << pos
278
27880
                       << "\n"
279
27880
                       << pop;
280
27880
    visited.insert(lit);
281
55760
    Node litNode = d_cnfStream->getNodeCache()[lit];
282
27880
    bool negated = lit.isNegated();
283
27880
    Assert(!negated || litNode.getKind() == kind::NOT);
284
285
83640
    d_resLinks.emplace(d_resLinks.begin() + pos,
286
55760
                       d_cnfStream->getNodeCache()[~lit],
287
55760
                       negated ? litNode[0] : litNode,
288
139400
                       !negated);
289
27880
    return;
290
  }
291
64755
  Assert(reasonRef >= 0 && reasonRef < d_solver->ca.size())
292
      << "reasonRef " << reasonRef << " and d_satSolver->ca.size() "
293
      << d_solver->ca.size() << "\n";
294
64755
  const Minisat::Clause& reason = d_solver->ca[reasonRef];
295
64755
  if (Trace.isOn("sat-proof"))
296
  {
297
    Trace("sat-proof") << "reason: ";
298
    printClause(reason);
299
    Trace("sat-proof") << "\n";
300
  }
301
  // check if redundant literals in the reason. The first literal is the one we
302
  // will be eliminating, so we check the others
303
221322
  for (unsigned i = 1, size = reason.size(); i < size; ++i)
304
  {
305
156567
    SatLiteral satLit = MinisatSatSolver::toSatLiteral(reason[i]);
306
    // if literal does not occur in the conclusion we process it as well
307
156567
    if (!conclusionLits.count(satLit))
308
    {
309
90967
      processRedundantLit(satLit, conclusionLits, visited, pos);
310
    }
311
  }
312
64755
  Assert(!visited.count(lit));
313
64755
  visited.insert(lit);
314
129510
  Trace("sat-proof") << "clause, add link to lit " << lit << " at pos: " << pos
315
64755
                     << "\n"
316
64755
                     << pop;
317
  // add the step before steps for children. Note that the step is with the
318
  // reason, not only with ~lit, since the learned clause is built under the
319
  // assumption that the redundant literal is removed via the resolution with
320
  // the explanation of its negation
321
129510
  Node clauseNode = getClauseNode(reason);
322
129510
  Node litNode = d_cnfStream->getNodeCache()[lit];
323
64755
  bool negated = lit.isNegated();
324
64755
  Assert(!negated || litNode.getKind() == kind::NOT);
325
194265
  d_resLinks.emplace(d_resLinks.begin() + pos,
326
                     clauseNode,
327
129510
                     negated ? litNode[0] : litNode,
328
259020
                     !negated);
329
}
330
331
1091224
void SatProofManager::explainLit(
332
    SatLiteral lit, std::unordered_set<TNode, TNodeHashFunction>& premises)
333
{
334
1091224
  Trace("sat-proof") << push << "SatProofManager::explainLit: Lit: " << lit;
335
1767374
  Node litNode = getClauseNode(lit);
336
1091224
  Trace("sat-proof") << " [" << litNode << "]\n";
337
  Minisat::Solver::TCRef reasonRef =
338
1091224
      d_solver->reason(Minisat::var(MinisatSatSolver::toMinisatLit(lit)));
339
1091224
  if (reasonRef == Minisat::Solver::TCRef_Undef)
340
  {
341
415072
    Trace("sat-proof") << "SatProofManager::explainLit: no SAT reason\n" << pop;
342
415072
    return;
343
  }
344
676152
  Assert(reasonRef >= 0 && reasonRef < d_solver->ca.size())
345
      << "reasonRef " << reasonRef << " and d_satSolver->ca.size() "
346
      << d_solver->ca.size() << "\n";
347
676152
  const Minisat::Clause& reason = d_solver->ca[reasonRef];
348
676152
  unsigned size = reason.size();
349
676152
  if (Trace.isOn("sat-proof"))
350
  {
351
    Trace("sat-proof") << "SatProofManager::explainLit: with clause: ";
352
    printClause(reason);
353
    Trace("sat-proof") << "\n";
354
  }
355
#ifdef CVC4_ASSERTIONS
356
  // pedantically check that the negation of the literal to explain *does not*
357
  // occur in the reason, otherwise we will loop forever
358
2439272
  for (unsigned i = 0; i < size; ++i)
359
  {
360
1763120
    AlwaysAssert(~MinisatSatSolver::toSatLiteral(reason[i]) != lit)
361
        << "cyclic justification\n";
362
  }
363
#endif
364
  // add the reason clause first
365
1352302
  std::vector<Node> children{getClauseNode(reason)}, args;
366
  // save in the premises
367
676152
  premises.insert(children.back());
368
  // Since explainLit calls can reallocate memory in the
369
  // SAT solver, we directly get the literals we need to explain so we no
370
  // longer depend on the reference to reason
371
1352302
  std::vector<Node> toExplain{children.back().begin(), children.back().end()};
372
676152
  NodeManager* nm = NodeManager::currentNM();
373
676152
  Trace("sat-proof") << push;
374
2439272
  for (unsigned i = 0; i < size; ++i)
375
  {
376
#ifdef CVC4_ASSERTIONS
377
    // pedantically make sure that the reason stays the same
378
1763120
    const Minisat::Clause& reloadedReason = d_solver->ca[reasonRef];
379
1763120
    AlwaysAssert(size == static_cast<unsigned>(reloadedReason.size()));
380
1763120
    AlwaysAssert(children[0] == getClauseNode(reloadedReason));
381
#endif
382
1763120
    SatLiteral curr_lit = d_cnfStream->getTranslationCache()[toExplain[i]];
383
    // ignore the lit we are trying to explain...
384
1763120
    if (curr_lit == lit)
385
    {
386
676152
      continue;
387
    }
388
2173936
    std::unordered_set<TNode, TNodeHashFunction> childPremises;
389
1086968
    explainLit(~curr_lit, childPremises);
390
    // save to resolution chain premises / arguments
391
1086968
    Assert(d_cnfStream->getNodeCache().find(curr_lit)
392
           != d_cnfStream->getNodeCache().end());
393
1086968
    children.push_back(d_cnfStream->getNodeCache()[~curr_lit]);
394
2173936
    Node currLitNode = d_cnfStream->getNodeCache()[curr_lit];
395
1086968
    bool negated = curr_lit.isNegated();
396
1086968
    Assert(!negated || currLitNode.getKind() == kind::NOT);
397
    // note this is the opposite of what is done in addResolutionStep. This is
398
    // because here the clause, which contains the literal being analyzed, is
399
    // the first clause rather than the second
400
1086968
    args.push_back(nm->mkConst(!negated));
401
1086968
    args.push_back(negated ? currLitNode[0] : currLitNode);
402
    // add child premises and the child itself
403
1086968
    premises.insert(childPremises.begin(), childPremises.end());
404
1086968
    premises.insert(d_cnfStream->getNodeCache()[~curr_lit]);
405
  }
406
676152
  if (Trace.isOn("sat-proof"))
407
  {
408
    Trace("sat-proof") << pop << "SatProofManager::explainLit: chain_res for "
409
                       << lit << ", " << litNode << " with clauses:\n";
410
    for (unsigned i = 0, csize = children.size(); i < csize; ++i)
411
    {
412
      Trace("sat-proof") << "SatProofManager::explainLit:   " << children[i];
413
      if (i > 0)
414
      {
415
        Trace("sat-proof") << " [" << args[i - 1] << "]";
416
      }
417
      Trace("sat-proof") << "\n";
418
    }
419
  }
420
  // if justification of children contains the expected conclusion, avoid the
421
  // cyclic proof by aborting.
422
676152
  if (premises.count(litNode))
423
  {
424
4
    Trace("sat-proof") << "SatProofManager::explainLit: CYCLIC PROOF of " << lit
425
2
                       << " [" << litNode << "], ABORT\n"
426
2
                       << pop;
427
2
    return;
428
  }
429
676150
  Trace("sat-proof") << pop;
430
  // create step
431
676150
  args.insert(args.begin(), litNode);
432
1352300
  ProofStep ps(PfRule::MACRO_RESOLUTION, children, args);
433
676150
  d_resChainPg.addStep(litNode, ps);
434
  // the premises in the limit of the justification may correspond to other
435
  // links in the chain which have, themselves, literals yet to be justified. So
436
  // we are not ready yet to check closedness w.r.t. CNF transformation of the
437
  // preprocessed assertions
438
676150
  d_resChains.addLazyStep(litNode, &d_resChainPg);
439
}
440
441
1073
void SatProofManager::finalizeProof(Node inConflictNode,
442
                                    const std::vector<SatLiteral>& inConflict)
443
{
444
2146
  Trace("sat-proof")
445
1073
      << "SatProofManager::finalizeProof: conflicting clause node: "
446
1073
      << inConflictNode << "\n";
447
  // nothing to do
448
1073
  if (inConflictNode == d_false)
449
  {
450
268
    return;
451
  }
452
805
  if (Trace.isOn("sat-proof-debug2"))
453
  {
454
    Trace("sat-proof-debug2")
455
        << push << "SatProofManager::finalizeProof: saved proofs in chain:\n";
456
    std::map<Node, std::shared_ptr<ProofNode>> links = d_resChains.getLinks();
457
    std::unordered_set<Node, NodeHashFunction> skip;
458
    for (const std::pair<const Node, std::shared_ptr<ProofNode>>& link : links)
459
    {
460
      if (skip.count(link.first))
461
      {
462
        continue;
463
      }
464
      auto it = d_cnfStream->getTranslationCache().find(link.first);
465
      if (it != d_cnfStream->getTranslationCache().end())
466
      {
467
        Trace("sat-proof-debug2")
468
            << "SatProofManager::finalizeProof:  " << it->second;
469
      }
470
      // a refl step added due to double elim negation, ignore
471
      else if (link.second->getRule() == PfRule::REFL)
472
      {
473
        continue;
474
      }
475
      // a clause
476
      else
477
      {
478
        Trace("sat-proof-debug2") << "SatProofManager::finalizeProof:";
479
        Assert(link.first.getKind() == kind::OR) << link.first;
480
        for (const Node& n : link.first)
481
        {
482
          it = d_cnfStream->getTranslationCache().find(n);
483
          Assert(it != d_cnfStream->getTranslationCache().end());
484
          Trace("sat-proof-debug2") << it->second << " ";
485
        }
486
      }
487
      Trace("sat-proof-debug2") << "\n";
488
      Trace("sat-proof-debug2")
489
          << "SatProofManager::finalizeProof: " << link.first << "\n";
490
      // get resolution
491
      Node cur = link.first;
492
      std::shared_ptr<ProofNode> pfn = link.second;
493
      while (pfn->getRule() != PfRule::MACRO_RESOLUTION)
494
      {
495
        Assert(pfn->getChildren().size() == 1
496
               && pfn->getChildren()[0]->getRule() == PfRule::ASSUME)
497
            << *link.second.get() << "\n"
498
            << *pfn.get();
499
        cur = pfn->getChildren()[0]->getResult();
500
        // retrieve justification of assumption in the links
501
        Assert(links.find(cur) != links.end());
502
        pfn = links[cur];
503
        // ignore it in the rest of the outside loop
504
        skip.insert(cur);
505
      }
506
      std::vector<Node> fassumps;
507
      expr::getFreeAssumptions(pfn.get(), fassumps);
508
      Trace("sat-proof-debug2") << push;
509
      for (const Node& fa : fassumps)
510
      {
511
        Trace("sat-proof-debug2") << "SatProofManager::finalizeProof:   - ";
512
        it = d_cnfStream->getTranslationCache().find(fa);
513
        if (it != d_cnfStream->getTranslationCache().end())
514
        {
515
          Trace("sat-proof-debug2") << it->second << "\n";
516
          continue;
517
        }
518
        // then it's a clause
519
        Assert(fa.getKind() == kind::OR);
520
        for (const Node& n : fa)
521
        {
522
          it = d_cnfStream->getTranslationCache().find(n);
523
          Assert(it != d_cnfStream->getTranslationCache().end());
524
          Trace("sat-proof-debug2") << it->second << " ";
525
        }
526
        Trace("sat-proof-debug2") << "\n";
527
      }
528
      Trace("sat-proof-debug2") << pop;
529
      Trace("sat-proof-debug2")
530
          << "SatProofManager::finalizeProof:  " << *pfn.get() << "\n=======\n";
531
      ;
532
    }
533
    Trace("sat-proof-debug2") << pop;
534
  }
535
  // We will resolve away of the literals l_1...l_n in inConflict. At this point
536
  // each ~l_i must be either explainable, the result of a previously saved
537
  // resolution chain, or an input. In account of it possibly being the first,
538
  // we call explainLit on each ~l_i while accumulating the children and
539
  // arguments for the resolution step to conclude false.
540
1610
  std::vector<Node> children{inConflictNode}, args;
541
1610
  std::unordered_set<TNode, TNodeHashFunction> premises;
542
805
  NodeManager* nm = NodeManager::currentNM();
543
4175
  for (unsigned i = 0, size = inConflict.size(); i < size; ++i)
544
  {
545
3370
    Assert(d_cnfStream->getNodeCache().find(inConflict[i])
546
           != d_cnfStream->getNodeCache().end());
547
6740
    std::unordered_set<TNode, TNodeHashFunction> childPremises;
548
3370
    explainLit(~inConflict[i], childPremises);
549
6740
    Node negatedLitNode = d_cnfStream->getNodeCache()[~inConflict[i]];
550
    // save to resolution chain premises / arguments
551
3370
    children.push_back(negatedLitNode);
552
6740
    Node litNode = d_cnfStream->getNodeCache()[inConflict[i]];
553
3370
    bool negated = inConflict[i].isNegated();
554
3370
    Assert(!negated || litNode.getKind() == kind::NOT);
555
    // note this is the opposite of what is done in addResolutionStep. This is
556
    // because here the clause, which contains the literal being analyzed, is
557
    // the first clause rather than the second
558
3370
    args.push_back(nm->mkConst(!negated));
559
3370
    args.push_back(negated ? litNode[0] : litNode);
560
    // add child premises and the child itself
561
3370
    premises.insert(childPremises.begin(), childPremises.end());
562
3370
    premises.insert(negatedLitNode);
563
3370
    Trace("sat-proof") << "===========\n";
564
  }
565
805
  if (Trace.isOn("sat-proof"))
566
  {
567
    Trace("sat-proof") << "SatProofManager::finalizeProof: chain_res for false "
568
                          "with clauses:\n";
569
    for (unsigned i = 0, size = children.size(); i < size; ++i)
570
    {
571
      Trace("sat-proof") << "SatProofManager::finalizeProof:   " << children[i];
572
      if (i > 0)
573
      {
574
        Trace("sat-proof") << " [" << args[i - 1] << "]";
575
      }
576
      Trace("sat-proof") << "\n";
577
    }
578
  }
579
  // create step
580
805
  args.insert(args.begin(), d_false);
581
1610
  ProofStep ps(PfRule::MACRO_RESOLUTION, children, args);
582
805
  d_resChainPg.addStep(d_false, ps);
583
  // not yet ready to check closedness because maybe only now we will justify
584
  // literals used in resolutions
585
805
  d_resChains.addLazyStep(d_false, &d_resChainPg);
586
  // Fix point justification of literals in leaves of the proof of false
587
  bool expanded;
588
999
  do
589
  {
590
999
    expanded = false;
591
999
    Trace("sat-proof") << "expand assumptions to prove false\n";
592
1998
    std::shared_ptr<ProofNode> pfn = d_resChains.getProofFor(d_false);
593
999
    Assert(pfn);
594
999
    Trace("sat-proof-debug") << "sat proof of flase: " << *pfn.get() << "\n";
595
1998
    std::vector<Node> fassumps;
596
999
    expr::getFreeAssumptions(pfn.get(), fassumps);
597
999
    if (Trace.isOn("sat-proof"))
598
    {
599
      for (const Node& fa : fassumps)
600
      {
601
        Trace("sat-proof") << "- ";
602
        auto it = d_cnfStream->getTranslationCache().find(fa);
603
        if (it != d_cnfStream->getTranslationCache().end())
604
        {
605
          Trace("sat-proof") << it->second << "\n";
606
          Trace("sat-proof") << "- " << fa << "\n";
607
          continue;
608
        }
609
        // then it's a clause
610
        Assert(fa.getKind() == kind::OR);
611
        for (const Node& n : fa)
612
        {
613
          it = d_cnfStream->getTranslationCache().find(n);
614
          Assert(it != d_cnfStream->getTranslationCache().end());
615
          Trace("sat-proof") << it->second << " ";
616
        }
617
        Trace("sat-proof") << "\n";
618
        Trace("sat-proof") << "- " << fa << "\n";
619
      }
620
    }
621
622
    // for each assumption, see if it has a reason
623
71426
    for (const Node& fa : fassumps)
624
    {
625
      // ignore already processed assumptions
626
87361
      if (premises.count(fa))
627
      {
628
16934
        Trace("sat-proof") << "already processed assumption " << fa << "\n";
629
86475
        continue;
630
      }
631
      // ignore input assumptions. This is necessary to avoid rare collisions
632
      // between input clauses and literals that are equivalent at the node
633
      // level. In trying to justify the literal below if, it was previously
634
      // propagated (say, in a previous check-sat call that survived the
635
      // user-context changes) but no longer holds, then we may introduce a
636
      // bogus proof for it, rather than keeping it as an input.
637
106100
      if (d_assumptions.contains(fa))
638
      {
639
52607
        Trace("sat-proof") << "input assumption " << fa << "\n";
640
52607
        continue;
641
      }
642
      // ignore non-literals
643
886
      auto it = d_cnfStream->getTranslationCache().find(fa);
644
886
      if (it == d_cnfStream->getTranslationCache().end())
645
      {
646
        Trace("sat-proof") << "no lit assumption " << fa << "\n";
647
        premises.insert(fa);
648
        continue;
649
      }
650
1772
      Trace("sat-proof") << "lit assumption (" << it->second << "), " << fa
651
886
                         << "\n";
652
      // mark another iteration for the loop, as some resolution link may be
653
      // connected because of the new justifications
654
886
      expanded = true;
655
1772
      std::unordered_set<TNode, TNodeHashFunction> childPremises;
656
886
      explainLit(it->second, childPremises);
657
      // add the premises used in the justification. We know they will have
658
      // been as expanded as possible
659
886
      premises.insert(childPremises.begin(), childPremises.end());
660
      // add free assumption itself
661
886
      premises.insert(fa);
662
    }
663
  } while (expanded);
664
  // now we should be able to close it
665
805
  if (options::proofEagerChecking())
666
  {
667
    std::vector<Node> assumptionsVec;
668
    for (const Node& a : d_assumptions)
669
    {
670
      assumptionsVec.push_back(a);
671
    }
672
    d_resChains.addLazyStep(d_false, &d_resChainPg, assumptionsVec);
673
  }
674
}
675
676
44
void SatProofManager::storeUnitConflict(Minisat::Lit inConflict)
677
{
678
44
  Assert(d_conflictLit == undefSatVariable);
679
44
  d_conflictLit = MinisatSatSolver::toSatLiteral(inConflict);
680
44
}
681
682
44
void SatProofManager::finalizeProof()
683
{
684
44
  Assert(d_conflictLit != undefSatVariable);
685
88
  Trace("sat-proof")
686
44
      << "SatProofManager::finalizeProof: conflicting (lazy) satLit: "
687
44
      << d_conflictLit << "\n";
688
44
  finalizeProof(getClauseNode(d_conflictLit), {d_conflictLit});
689
44
}
690
691
308
void SatProofManager::finalizeProof(Minisat::Lit inConflict, bool adding)
692
{
693
308
  SatLiteral satLit = MinisatSatSolver::toSatLiteral(inConflict);
694
616
  Trace("sat-proof") << "SatProofManager::finalizeProof: conflicting satLit: "
695
308
                     << satLit << "\n";
696
616
  Node clauseNode = getClauseNode(satLit);
697
308
  if (adding)
698
  {
699
308
    registerSatAssumptions({clauseNode});
700
  }
701
308
  finalizeProof(clauseNode, {satLit});
702
308
}
703
704
721
void SatProofManager::finalizeProof(const Minisat::Clause& inConflict,
705
                                    bool adding)
706
{
707
721
  if (Trace.isOn("sat-proof"))
708
  {
709
    Trace("sat-proof")
710
        << "SatProofManager::finalizeProof: conflicting clause: ";
711
    printClause(inConflict);
712
    Trace("sat-proof") << "\n";
713
  }
714
1442
  std::vector<SatLiteral> clause;
715
4007
  for (unsigned i = 0, size = inConflict.size(); i < size; ++i)
716
  {
717
3286
    clause.push_back(MinisatSatSolver::toSatLiteral(inConflict[i]));
718
  }
719
1442
  Node clauseNode = getClauseNode(inConflict);
720
721
  if (adding)
721
  {
722
16
    registerSatAssumptions({clauseNode});
723
  }
724
721
  finalizeProof(clauseNode, clause);
725
721
}
726
727
2292
std::shared_ptr<ProofNode> SatProofManager::getProof()
728
{
729
2292
  std::shared_ptr<ProofNode> pfn = d_resChains.getProofFor(d_false);
730
2292
  if (!pfn)
731
  {
732
604
    pfn = d_pnm->mkAssume(d_false);
733
  }
734
2292
  return pfn;
735
}
736
737
20908
void SatProofManager::registerSatLitAssumption(Minisat::Lit lit)
738
{
739
41816
  Trace("sat-proof") << "SatProofManager::registerSatLitAssumption: - "
740
41816
                     << getClauseNode(MinisatSatSolver::toSatLiteral(lit))
741
20908
                     << "\n";
742
20908
  d_assumptions.insert(getClauseNode(MinisatSatSolver::toSatLiteral(lit)));
743
20908
}
744
745
247335
void SatProofManager::registerSatAssumptions(const std::vector<Node>& assumps)
746
{
747
494670
  for (const Node& a : assumps)
748
  {
749
494670
    Trace("sat-proof") << "SatProofManager::registerSatAssumptions: - " << a
750
247335
                       << "\n";
751
247335
    d_assumptions.insert(a);
752
  }
753
247335
}
754
755
}  // namespace prop
756
26676
}  // namespace CVC4