GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/prop/proof_cnf_stream.cpp Lines: 571 614 93.0 %
Date: 2021-03-22 Branches: 1481 3324 44.6 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file proof_cnf_stream.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Haniel Barbosa, Andrew Reynolds, Tim King
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-producing CNF stream
13
 **/
14
15
#include "prop/proof_cnf_stream.h"
16
17
#include "options/smt_options.h"
18
#include "prop/minisat/minisat.h"
19
#include "theory/builtin/proof_checker.h"
20
21
namespace CVC4 {
22
namespace prop {
23
24
966
ProofCnfStream::ProofCnfStream(context::UserContext* u,
25
                               CnfStream& cnfStream,
26
                               SatProofManager* satPM,
27
966
                               ProofNodeManager* pnm)
28
    : d_cnfStream(cnfStream),
29
      d_satPM(satPM),
30
      d_proof(pnm, nullptr, u, "ProofCnfStream::LazyCDProof"),
31
966
      d_blocked(u)
32
{
33
966
}
34
35
389236
void ProofCnfStream::addBlocked(std::shared_ptr<ProofNode> pfn)
36
{
37
389236
  d_blocked.insert(pfn);
38
389236
}
39
40
523730
bool ProofCnfStream::isBlocked(std::shared_ptr<ProofNode> pfn)
41
{
42
523730
  return d_blocked.contains(pfn);
43
}
44
45
77610
std::shared_ptr<ProofNode> ProofCnfStream::getProofFor(Node f)
46
{
47
77610
  return d_proof.getProofFor(f);
48
}
49
50
406158
bool ProofCnfStream::hasProofFor(Node f)
51
{
52
406158
  return d_proof.hasStep(f) || d_proof.hasGenerator(f);
53
}
54
55
std::string ProofCnfStream::identify() const { return "ProofCnfStream"; }
56
57
221516
void ProofCnfStream::normalizeAndRegister(TNode clauseNode)
58
{
59
443032
  Node normClauseNode = d_psb.factorReorderElimDoubleNeg(clauseNode);
60
221516
  if (Trace.isOn("cnf") && normClauseNode != clauseNode)
61
  {
62
    Trace("cnf") << push
63
                 << "ProofCnfStream::normalizeAndRegister: steps to normalized "
64
                 << normClauseNode << "\n"
65
                 << pop;
66
  }
67
221516
  d_satPM->registerSatAssumptions({normClauseNode});
68
221516
}
69
70
82889
void ProofCnfStream::convertAndAssert(TNode node,
71
                                      bool negated,
72
                                      bool removable,
73
                                      ProofGenerator* pg)
74
{
75
165778
  Trace("cnf") << "ProofCnfStream::convertAndAssert(" << node
76
165778
               << ", negated = " << (negated ? "true" : "false")
77
82889
               << ", removable = " << (removable ? "true" : "false") << ")\n";
78
82889
  d_cnfStream.d_removable = removable;
79
82889
  if (pg)
80
  {
81
131572
    Trace("cnf") << "ProofCnfStream::convertAndAssert: pg: " << pg->identify()
82
65786
                 << "\n";
83
131572
    Node toJustify = negated ? node.notNode() : static_cast<Node>(node);
84
65786
    d_proof.addLazyStep(toJustify,
85
                        pg,
86
                        PfRule::ASSUME,
87
                        true,
88
                        "ProofCnfStream::convertAndAssert:cnf");
89
  }
90
82889
  convertAndAssert(node, negated);
91
  // process saved steps in buffer
92
82889
  const std::vector<std::pair<Node, ProofStep>>& steps = d_psb.getSteps();
93
942943
  for (const std::pair<Node, ProofStep>& step : steps)
94
  {
95
860054
    d_proof.addStep(step.first, step.second);
96
  }
97
82889
  d_psb.clear();
98
82889
}
99
100
138036
void ProofCnfStream::convertAndAssert(TNode node, bool negated)
101
{
102
276072
  Trace("cnf") << "ProofCnfStream::convertAndAssert(" << node
103
138036
               << ", negated = " << (negated ? "true" : "false") << ")\n";
104
138036
  switch (node.getKind())
105
  {
106
19380
    case kind::AND: convertAndAssertAnd(node, negated); break;
107
38066
    case kind::OR: convertAndAssertOr(node, negated); break;
108
9
    case kind::XOR: convertAndAssertXor(node, negated); break;
109
13315
    case kind::IMPLIES: convertAndAssertImplies(node, negated); break;
110
4092
    case kind::ITE: convertAndAssertIte(node, negated); break;
111
21564
    case kind::NOT:
112
    {
113
      // track double negation elimination
114
21564
      if (negated)
115
      {
116
603
        d_proof.addStep(node[0], PfRule::NOT_NOT_ELIM, {node.notNode()}, {});
117
1206
        Trace("cnf")
118
603
            << "ProofCnfStream::convertAndAssert: NOT_NOT_ELIM added norm "
119
603
            << node[0] << "\n";
120
      }
121
21564
      convertAndAssert(node[0], !negated);
122
21564
      break;
123
    }
124
26261
    case kind::EQUAL:
125
26261
      if (node[0].getType().isBoolean())
126
      {
127
1055
        convertAndAssertIff(node, negated);
128
1055
        break;
129
      }
130
      CVC4_FALLTHROUGH;
131
    default:
132
    {
133
      // negate
134
81110
      Node nnode = negated ? node.negate() : static_cast<Node>(node);
135
      // Atoms
136
40555
      SatLiteral lit = toCNF(node, negated);
137
40555
      bool added = d_cnfStream.assertClause(nnode, lit);
138
40555
      if (negated && added && nnode != node.notNode())
139
      {
140
        // track double negation elimination
141
        //    (not (not n))
142
        //   -------------- NOT_NOT_ELIM
143
        //        n
144
        d_proof.addStep(nnode, PfRule::NOT_NOT_ELIM, {node.notNode()}, {});
145
        Trace("cnf")
146
            << "ProofCnfStream::convertAndAssert: NOT_NOT_ELIM added norm "
147
            << nnode << "\n";
148
      }
149
40555
      if (added)
150
      {
151
        // note that we do not need to do the normalization here since this is
152
        // not a clause and double negation is tracked in a dedicated manner
153
        // above
154
24529
        d_satPM->registerSatAssumptions({nnode});
155
40555
      }
156
    }
157
  }
158
138036
}
159
160
19380
void ProofCnfStream::convertAndAssertAnd(TNode node, bool negated)
161
{
162
38760
  Trace("cnf") << "ProofCnfStream::convertAndAssertAnd(" << node
163
19380
               << ", negated = " << (negated ? "true" : "false") << ")\n";
164
19380
  Assert(node.getKind() == kind::AND);
165
19380
  if (!negated)
166
  {
167
    // If the node is a conjunction, we handle each conjunct separately
168
2058
    NodeManager* nm = NodeManager::currentNM();
169
34693
    for (unsigned i = 0, size = node.getNumChildren(); i < size; ++i)
170
    {
171
      // Create a proof step for each n_i
172
65270
      Node iNode = nm->mkConst<Rational>(i);
173
32635
      d_proof.addStep(node[i], PfRule::AND_ELIM, {node}, {iNode});
174
65270
      Trace("cnf") << "ProofCnfStream::convertAndAssertAnd: AND_ELIM " << i
175
32635
                   << " added norm " << node[i] << "\n";
176
32635
      convertAndAssert(node[i], false);
177
    }
178
  }
179
  else
180
  {
181
    // If the node is a disjunction, we construct a clause and assert it
182
17322
    unsigned i, size = node.getNumChildren();
183
34644
    SatClause clause(size);
184
184090
    for (i = 0; i < size; ++i)
185
    {
186
166768
      clause[i] = toCNF(node[i], true);
187
    }
188
17322
    bool added = d_cnfStream.assertClause(node.negate(), clause);
189
    // register proof step
190
17322
    if (added)
191
    {
192
34568
      std::vector<Node> disjuncts;
193
183916
      for (i = 0; i < size; ++i)
194
      {
195
166632
        disjuncts.push_back(node[i].notNode());
196
      }
197
34568
      Node clauseNode = NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
198
17284
      d_proof.addStep(clauseNode, PfRule::NOT_AND, {node.notNode()}, {});
199
34568
      Trace("cnf") << "ProofCnfStream::convertAndAssertAnd: NOT_AND added "
200
17284
                   << clauseNode << "\n";
201
17284
      normalizeAndRegister(clauseNode);
202
    }
203
  }
204
19380
}
205
206
38066
void ProofCnfStream::convertAndAssertOr(TNode node, bool negated)
207
{
208
76132
  Trace("cnf") << "ProofCnfStream::convertAndAssertOr(" << node
209
38066
               << ", negated = " << (negated ? "true" : "false") << ")\n";
210
38066
  Assert(node.getKind() == kind::OR);
211
38066
  if (!negated)
212
  {
213
    // If the node is a disjunction, we construct a clause and assert it
214
37978
    unsigned size = node.getNumChildren();
215
75956
    SatClause clause(size);
216
155417
    for (unsigned i = 0; i < size; ++i)
217
    {
218
117439
      clause[i] = toCNF(node[i], false);
219
    }
220
37978
    normalizeAndRegister(node);
221
37978
    d_cnfStream.assertClause(node, clause);
222
  }
223
  else
224
  {
225
    // If the node is a negated disjunction, we handle it as a conjunction of
226
    // the negated arguments
227
88
    NodeManager* nm = NodeManager::currentNM();
228
882
    for (unsigned i = 0, size = node.getNumChildren(); i < size; ++i)
229
    {
230
      // Create a proof step for each (not n_i)
231
1588
      Node iNode = nm->mkConst<Rational>(i);
232
3970
      d_proof.addStep(
233
3176
          node[i].notNode(), PfRule::NOT_OR_ELIM, {node.notNode()}, {iNode});
234
1588
      Trace("cnf") << "ProofCnfStream::convertAndAssertOr: NOT_OR_ELIM " << i
235
794
                   << " added norm  " << node[i].notNode() << "\n";
236
794
      convertAndAssert(node[i], true);
237
    }
238
  }
239
38066
}
240
241
9
void ProofCnfStream::convertAndAssertXor(TNode node, bool negated)
242
{
243
18
  Trace("cnf") << "ProofCnfStream::convertAndAssertXor(" << node
244
9
               << ", negated = " << (negated ? "true" : "false") << ")\n";
245
9
  if (!negated)
246
  {
247
    // p XOR q
248
9
    SatLiteral p = toCNF(node[0], false);
249
9
    SatLiteral q = toCNF(node[1], false);
250
    bool added;
251
9
    NodeManager* nm = NodeManager::currentNM();
252
    // Construct the clause (~p v ~q)
253
18
    SatClause clause1(2);
254
9
    clause1[0] = ~p;
255
9
    clause1[1] = ~q;
256
9
    added = d_cnfStream.assertClause(node, clause1);
257
9
    if (added)
258
    {
259
      Node clauseNode =
260
16
          nm->mkNode(kind::OR, node[0].notNode(), node[1].notNode());
261
8
      d_proof.addStep(clauseNode, PfRule::XOR_ELIM2, {node}, {});
262
16
      Trace("cnf") << "ProofCnfStream::convertAndAssertXor: XOR_ELIM2 added "
263
8
                   << clauseNode << "\n";
264
8
      normalizeAndRegister(clauseNode);
265
    }
266
    // Construct the clause (p v q)
267
18
    SatClause clause2(2);
268
9
    clause2[0] = p;
269
9
    clause2[1] = q;
270
9
    added = d_cnfStream.assertClause(node, clause2);
271
9
    if (added)
272
    {
273
16
      Node clauseNode = nm->mkNode(kind::OR, node[0], node[1]);
274
8
      d_proof.addStep(clauseNode, PfRule::XOR_ELIM1, {node}, {});
275
16
      Trace("cnf") << "ProofCnfStream::convertAndAssertXor: XOR_ELIM1 added "
276
8
                   << clauseNode << "\n";
277
8
      normalizeAndRegister(clauseNode);
278
    }
279
  }
280
  else
281
  {
282
    // ~(p XOR q) is the same as p <=> q
283
    SatLiteral p = toCNF(node[0], false);
284
    SatLiteral q = toCNF(node[1], false);
285
    bool added;
286
    NodeManager* nm = NodeManager::currentNM();
287
    // Construct the clause ~p v q
288
    SatClause clause1(2);
289
    clause1[0] = ~p;
290
    clause1[1] = q;
291
    added = d_cnfStream.assertClause(node.negate(), clause1);
292
    if (added)
293
    {
294
      Node clauseNode = nm->mkNode(kind::OR, node[0].notNode(), node[1]);
295
      d_proof.addStep(clauseNode, PfRule::NOT_XOR_ELIM2, {node.notNode()}, {});
296
      Trace("cnf")
297
          << "ProofCnfStream::convertAndAssertXor: NOT_XOR_ELIM2 added "
298
          << clauseNode << "\n";
299
      normalizeAndRegister(clauseNode);
300
    }
301
    // Construct the clause ~q v p
302
    SatClause clause2(2);
303
    clause2[0] = p;
304
    clause2[1] = ~q;
305
    added = d_cnfStream.assertClause(node.negate(), clause2);
306
    if (added)
307
    {
308
      Node clauseNode = nm->mkNode(kind::OR, node[0], node[1].notNode());
309
      d_proof.addStep(clauseNode, PfRule::NOT_XOR_ELIM1, {node.notNode()}, {});
310
      Trace("cnf")
311
          << "ProofCnfStream::convertAndAssertXor: NOT_XOR_ELIM1 added "
312
          << clauseNode << "\n";
313
      normalizeAndRegister(clauseNode);
314
    }
315
  }
316
9
}
317
318
1055
void ProofCnfStream::convertAndAssertIff(TNode node, bool negated)
319
{
320
2110
  Trace("cnf") << "ProofCnfStream::convertAndAssertIff(" << node
321
1055
               << ", negated = " << (negated ? "true" : "false") << ")\n";
322
1055
  if (!negated)
323
  {
324
    // p <=> q
325
1041
    Trace("cnf") << push;
326
1041
    SatLiteral p = toCNF(node[0], false);
327
1041
    SatLiteral q = toCNF(node[1], false);
328
1041
    Trace("cnf") << pop;
329
    bool added;
330
1041
    NodeManager* nm = NodeManager::currentNM();
331
    // Construct the clauses ~p v q
332
2082
    SatClause clause1(2);
333
1041
    clause1[0] = ~p;
334
1041
    clause1[1] = q;
335
1041
    added = d_cnfStream.assertClause(node, clause1);
336
1041
    if (added)
337
    {
338
1168
      Node clauseNode = nm->mkNode(kind::OR, node[0].notNode(), node[1]);
339
584
      d_proof.addStep(clauseNode, PfRule::EQUIV_ELIM1, {node}, {});
340
1168
      Trace("cnf") << "ProofCnfStream::convertAndAssertIff: EQUIV_ELIM1 added "
341
584
                   << clauseNode << "\n";
342
584
      normalizeAndRegister(clauseNode);
343
    }
344
    // Construct the clauses ~q v p
345
2082
    SatClause clause2(2);
346
1041
    clause2[0] = p;
347
1041
    clause2[1] = ~q;
348
1041
    added = d_cnfStream.assertClause(node, clause2);
349
1041
    if (added)
350
    {
351
1978
      Node clauseNode = nm->mkNode(kind::OR, node[0], node[1].notNode());
352
989
      d_proof.addStep(clauseNode, PfRule::EQUIV_ELIM2, {node}, {});
353
1978
      Trace("cnf") << "ProofCnfStream::convertAndAssertIff: EQUIV_ELIM2 added "
354
989
                   << clauseNode << "\n";
355
989
      normalizeAndRegister(clauseNode);
356
    }
357
  }
358
  else
359
  {
360
    // ~(p <=> q) is the same as p XOR q
361
14
    Trace("cnf") << push;
362
14
    SatLiteral p = toCNF(node[0], false);
363
14
    SatLiteral q = toCNF(node[1], false);
364
14
    Trace("cnf") << pop;
365
    bool added;
366
14
    NodeManager* nm = NodeManager::currentNM();
367
    // Construct the clauses ~p v ~q
368
28
    SatClause clause1(2);
369
14
    clause1[0] = ~p;
370
14
    clause1[1] = ~q;
371
14
    added = d_cnfStream.assertClause(node.negate(), clause1);
372
14
    if (added)
373
    {
374
      Node clauseNode =
375
26
          nm->mkNode(kind::OR, node[0].notNode(), node[1].notNode());
376
26
      d_proof.addStep(
377
13
          clauseNode, PfRule::NOT_EQUIV_ELIM2, {node.notNode()}, {});
378
26
      Trace("cnf")
379
13
          << "ProofCnfStream::convertAndAssertIff: NOT_EQUIV_ELIM2 added "
380
13
          << clauseNode << "\n";
381
13
      normalizeAndRegister(clauseNode);
382
    }
383
    // Construct the clauses q v p
384
28
    SatClause clause2(2);
385
14
    clause2[0] = p;
386
14
    clause2[1] = q;
387
14
    added = d_cnfStream.assertClause(node.negate(), clause2);
388
14
    if (added)
389
    {
390
24
      Node clauseNode = nm->mkNode(kind::OR, node[0], node[1]);
391
24
      d_proof.addStep(
392
12
          clauseNode, PfRule::NOT_EQUIV_ELIM1, {node.notNode()}, {});
393
24
      Trace("cnf")
394
12
          << "ProofCnfStream::convertAndAssertIff: NOT_EQUIV_ELIM1 added "
395
12
          << clauseNode << "\n";
396
12
      normalizeAndRegister(clauseNode);
397
    }
398
  }
399
1055
}
400
401
13315
void ProofCnfStream::convertAndAssertImplies(TNode node, bool negated)
402
{
403
26630
  Trace("cnf") << "ProofCnfStream::convertAndAssertImplies(" << node
404
13315
               << ", negated = " << (negated ? "true" : "false") << ")\n";
405
13315
  if (!negated)
406
  {
407
    // ~p v q
408
13238
    SatLiteral p = toCNF(node[0], false);
409
13238
    SatLiteral q = toCNF(node[1], false);
410
    // Construct the clause ~p || q
411
26476
    SatClause clause(2);
412
13238
    clause[0] = ~p;
413
13238
    clause[1] = q;
414
13238
    bool added = d_cnfStream.assertClause(node, clause);
415
13238
    if (added)
416
    {
417
      Node clauseNode = NodeManager::currentNM()->mkNode(
418
26074
          kind::OR, node[0].notNode(), node[1]);
419
13037
      d_proof.addStep(clauseNode, PfRule::IMPLIES_ELIM, {node}, {});
420
26074
      Trace("cnf")
421
13037
          << "ProofCnfStream::convertAndAssertImplies: IMPLIES_ELIM added "
422
13037
          << clauseNode << "\n";
423
13037
      normalizeAndRegister(clauseNode);
424
    }
425
  }
426
  else
427
  {
428
    // ~(p => q) is the same as p ^ ~q
429
    // process p
430
77
    convertAndAssert(node[0], false);
431
77
    d_proof.addStep(node[0], PfRule::NOT_IMPLIES_ELIM1, {node.notNode()}, {});
432
154
    Trace("cnf")
433
77
        << "ProofCnfStream::convertAndAssertImplies: NOT_IMPLIES_ELIM1 added "
434
77
        << node[0] << "\n";
435
    // process ~q
436
77
    convertAndAssert(node[1], true);
437
308
    d_proof.addStep(
438
231
        node[1].notNode(), PfRule::NOT_IMPLIES_ELIM2, {node.notNode()}, {});
439
154
    Trace("cnf")
440
77
        << "ProofCnfStream::convertAndAssertImplies: NOT_IMPLIES_ELIM2 added "
441
77
        << node[1].notNode() << "\n";
442
  }
443
13315
}
444
445
4092
void ProofCnfStream::convertAndAssertIte(TNode node, bool negated)
446
{
447
8184
  Trace("cnf") << "ProofCnfStream::convertAndAssertIte(" << node
448
4092
               << ", negated = " << (negated ? "true" : "false") << ")\n";
449
  // ITE(p, q, r)
450
4092
  SatLiteral p = toCNF(node[0], false);
451
4092
  SatLiteral q = toCNF(node[1], negated);
452
4092
  SatLiteral r = toCNF(node[2], negated);
453
  bool added;
454
4092
  NodeManager* nm = NodeManager::currentNM();
455
  // Construct the clauses:
456
  // (~p v q) and (p v r)
457
  //
458
  // Note that below q and r can be used directly because whether they are
459
  // negated has been push to the literal definitions above
460
8184
  Node nnode = negated ? node.negate() : static_cast<Node>(node);
461
  // (~p v q)
462
8184
  SatClause clause1(2);
463
4092
  clause1[0] = ~p;
464
4092
  clause1[1] = q;
465
4092
  added = d_cnfStream.assertClause(nnode, clause1);
466
4092
  if (added)
467
  {
468
    // redo the negation here to avoid silent double negation elimination
469
4056
    if (!negated)
470
    {
471
8108
      Node clauseNode = nm->mkNode(kind::OR, node[0].notNode(), node[1]);
472
4054
      d_proof.addStep(clauseNode, PfRule::ITE_ELIM1, {node}, {});
473
8108
      Trace("cnf") << "ProofCnfStream::convertAndAssertIte: ITE_ELIM1 added "
474
4054
                   << clauseNode << "\n";
475
4054
      normalizeAndRegister(clauseNode);
476
    }
477
    else
478
    {
479
      Node clauseNode =
480
4
          nm->mkNode(kind::OR, node[0].notNode(), node[1].notNode());
481
2
      d_proof.addStep(clauseNode, PfRule::NOT_ITE_ELIM1, {node.notNode()}, {});
482
4
      Trace("cnf")
483
2
          << "ProofCnfStream::convertAndAssertIte: NOT_ITE_ELIM1 added "
484
2
          << clauseNode << "\n";
485
2
      normalizeAndRegister(clauseNode);
486
    }
487
  }
488
  // (p v r)
489
8184
  SatClause clause2(2);
490
4092
  clause2[0] = p;
491
4092
  clause2[1] = r;
492
4092
  added = d_cnfStream.assertClause(nnode, clause2);
493
4092
  if (added)
494
  {
495
    // redo the negation here to avoid silent double negation elimination
496
4036
    if (!negated)
497
    {
498
8068
      Node clauseNode = nm->mkNode(kind::OR, node[0], node[2]);
499
4034
      d_proof.addStep(clauseNode, PfRule::ITE_ELIM2, {node}, {});
500
8068
      Trace("cnf") << "ProofCnfStream::convertAndAssertIte: ITE_ELIM2 added "
501
4034
                   << clauseNode << "\n";
502
4034
      normalizeAndRegister(clauseNode);
503
    }
504
    else
505
    {
506
4
      Node clauseNode = nm->mkNode(kind::OR, node[0], node[2].notNode());
507
2
      d_proof.addStep(clauseNode, PfRule::NOT_ITE_ELIM2, {node.notNode()}, {});
508
4
      Trace("cnf")
509
2
          << "ProofCnfStream::convertAndAssertIte: NOT_ITE_ELIM2 added "
510
2
          << clauseNode << "\n";
511
2
      normalizeAndRegister(clauseNode);
512
    }
513
  }
514
4092
}
515
516
19676
void ProofCnfStream::convertPropagation(theory::TrustNode trn)
517
{
518
39352
  Node proven = trn.getProven();
519
39352
  Trace("cnf") << "ProofCnfStream::convertPropagation: proven explanation"
520
19676
               << proven << "\n";
521
19676
  Assert(trn.getGenerator());
522
19676
  Assert(trn.getGenerator()->getProofFor(proven)->isClosed());
523
39352
  Trace("cnf-steps") << proven << " by explainPropagation "
524
19676
                     << trn.identifyGenerator() << std::endl;
525
19676
  d_proof.addLazyStep(proven,
526
                      trn.getGenerator(),
527
                      PfRule::ASSUME,
528
                      true,
529
                      "ProofCnfStream::convertPropagation");
530
  // since the propagation is added directly to the SAT solver via theoryProxy,
531
  // do the transformation of the lemma E1 ^ ... ^ En => P into CNF here
532
19676
  NodeManager* nm = NodeManager::currentNM();
533
39352
  Node clauseImpliesElim = nm->mkNode(kind::OR, proven[0].notNode(), proven[1]);
534
39352
  Trace("cnf") << "ProofCnfStream::convertPropagation: adding "
535
39352
               << PfRule::IMPLIES_ELIM << " rule to conclude "
536
19676
               << clauseImpliesElim << "\n";
537
19676
  d_proof.addStep(clauseImpliesElim, PfRule::IMPLIES_ELIM, {proven}, {});
538
39352
  Node clauseExp;
539
  // need to eliminate AND
540
19676
  if (proven[0].getKind() == kind::AND)
541
  {
542
37362
    std::vector<Node> disjunctsAndNeg{proven[0]};
543
37362
    std::vector<Node> disjunctsRes;
544
174797
    for (unsigned i = 0, size = proven[0].getNumChildren(); i < size; ++i)
545
    {
546
156116
      disjunctsAndNeg.push_back(proven[0][i].notNode());
547
156116
      disjunctsRes.push_back(proven[0][i].notNode());
548
    }
549
18681
    disjunctsRes.push_back(proven[1]);
550
37362
    Node clauseAndNeg = nm->mkNode(kind::OR, disjunctsAndNeg);
551
    // add proof steps to convert into clause
552
18681
    d_proof.addStep(clauseAndNeg, PfRule::CNF_AND_NEG, {}, {proven[0]});
553
18681
    clauseExp = nm->mkNode(kind::OR, disjunctsRes);
554
93405
    d_proof.addStep(clauseExp,
555
                    PfRule::RESOLUTION,
556
                    {clauseAndNeg, clauseImpliesElim},
557
74724
                    {nm->mkConst(true), proven[0]});
558
  }
559
  else
560
  {
561
995
    clauseExp = clauseImpliesElim;
562
  }
563
19676
  normalizeAndRegister(clauseExp);
564
  // consume steps
565
19676
  const std::vector<std::pair<Node, ProofStep>>& steps = d_psb.getSteps();
566
222887
  for (const std::pair<Node, ProofStep>& step : steps)
567
  {
568
203211
    d_proof.addStep(step.first, step.second);
569
  }
570
19676
  d_psb.clear();
571
19676
}
572
573
18987
void ProofCnfStream::ensureLiteral(TNode n)
574
{
575
18987
  Trace("cnf") << "ProofCnfStream::ensureLiteral(" << n << ")\n";
576
18987
  if (d_cnfStream.hasLiteral(n))
577
  {
578
18250
    d_cnfStream.ensureMappingForLiteral(n);
579
18250
    return;
580
  }
581
  // remove top level negation. We don't need to track this because it's a
582
  // literal.
583
737
  n = n.getKind() == kind::NOT ? n[0] : n;
584
737
  if (theory::Theory::theoryOf(n) == theory::THEORY_BOOL && !n.isVar())
585
  {
586
    // These are not removable
587
    d_cnfStream.d_removable = false;
588
    SatLiteral lit = toCNF(n, false);
589
    // Store backward-mappings
590
    // These may already exist
591
    d_cnfStream.d_literalToNodeMap.insert_safe(lit, n);
592
    d_cnfStream.d_literalToNodeMap.insert_safe(~lit, n.notNode());
593
  }
594
  else
595
  {
596
737
    d_cnfStream.convertAtom(n);
597
  }
598
}
599
600
483153
SatLiteral ProofCnfStream::toCNF(TNode node, bool negated)
601
{
602
966306
  Trace("cnf") << "toCNF(" << node
603
483153
               << ", negated = " << (negated ? "true" : "false") << ")\n";
604
483153
  SatLiteral lit;
605
  // If the node has already has a literal, return it (maybe negated)
606
483153
  if (d_cnfStream.hasLiteral(node))
607
  {
608
354769
    Trace("cnf") << "toCNF(): already translated\n";
609
354769
    lit = d_cnfStream.getLiteral(node);
610
    // Return the (maybe negated) literal
611
354769
    return !negated ? lit : ~lit;
612
  }
613
614
  // Handle each Boolean operator case
615
128384
  switch (node.getKind())
616
  {
617
15872
    case kind::AND: lit = handleAnd(node); break;
618
13393
    case kind::OR: lit = handleOr(node); break;
619
166
    case kind::XOR: lit = handleXor(node); break;
620
952
    case kind::IMPLIES: lit = handleImplies(node); break;
621
1631
    case kind::ITE: lit = handleIte(node); break;
622
17538
    case kind::NOT: lit = ~toCNF(node[0]); break;
623
41780
    case kind::EQUAL:
624
123710
      lit = node[0].getType().isBoolean() ? handleIff(node)
625
81930
                                          : d_cnfStream.convertAtom(node);
626
41780
      break;
627
37052
    default:
628
    {
629
37052
      lit = d_cnfStream.convertAtom(node);
630
    }
631
37052
    break;
632
  }
633
  // Return the (maybe negated) literal
634
128384
  return !negated ? lit : ~lit;
635
}
636
637
15872
SatLiteral ProofCnfStream::handleAnd(TNode node)
638
{
639
15872
  Assert(!d_cnfStream.hasLiteral(node)) << "Atom already mapped!";
640
15872
  Assert(node.getKind() == kind::AND) << "Expecting an AND expression!";
641
15872
  Assert(node.getNumChildren() > 1) << "Expecting more than 1 child!";
642
15872
  Assert(!d_cnfStream.d_removable)
643
      << "Removable clauses cannot contain Boolean structure";
644
15872
  Trace("cnf") << "ProofCnfStream::handleAnd(" << node << ")\n";
645
  // Number of children
646
15872
  unsigned size = node.getNumChildren();
647
  // Transform all the children first (remembering the negation)
648
31744
  SatClause clause(size + 1);
649
66765
  for (unsigned i = 0; i < size; ++i)
650
  {
651
50893
    Trace("cnf") << push;
652
50893
    clause[i] = ~toCNF(node[i]);
653
50893
    Trace("cnf") << pop;
654
  }
655
  // Create literal for the node
656
15872
  SatLiteral lit = d_cnfStream.newLiteral(node);
657
  bool added;
658
15872
  NodeManager* nm = NodeManager::currentNM();
659
  // lit -> (a_1 & a_2 & a_3 & ... & a_n)
660
  // ~lit | (a_1 & a_2 & a_3 & ... & a_n)
661
  // (~lit | a_1) & (~lit | a_2) & ... & (~lit | a_n)
662
66765
  for (unsigned i = 0; i < size; ++i)
663
  {
664
50893
    Trace("cnf") << push;
665
50893
    added = d_cnfStream.assertClause(node.negate(), ~lit, ~clause[i]);
666
50893
    Trace("cnf") << pop;
667
50893
    if (added)
668
    {
669
89904
      Node clauseNode = nm->mkNode(kind::OR, node.notNode(), node[i]);
670
89904
      Node iNode = nm->mkConst<Rational>(i);
671
44952
      d_proof.addStep(clauseNode, PfRule::CNF_AND_POS, {}, {node, iNode});
672
89904
      Trace("cnf") << "ProofCnfStream::handleAnd: CNF_AND_POS " << i
673
44952
                   << " added " << clauseNode << "\n";
674
44952
      normalizeAndRegister(clauseNode);
675
    }
676
  }
677
  // lit <- (a_1 & a_2 & a_3 & ... a_n)
678
  // lit | ~(a_1 & a_2 & a_3 & ... & a_n)
679
  // lit | ~a_1 | ~a_2 | ~a_3 | ... | ~a_n
680
15872
  clause[size] = lit;
681
  // This needs to go last, as the clause might get modified by the SAT solver
682
15872
  Trace("cnf") << push;
683
15872
  added = d_cnfStream.assertClause(node, clause);
684
15872
  Trace("cnf") << pop;
685
15872
  if (added)
686
  {
687
30202
    std::vector<Node> disjuncts{node};
688
63319
    for (unsigned i = 0; i < size; ++i)
689
    {
690
48218
      disjuncts.push_back(node[i].notNode());
691
    }
692
30202
    Node clauseNode = nm->mkNode(kind::OR, disjuncts);
693
15101
    d_proof.addStep(clauseNode, PfRule::CNF_AND_NEG, {}, {node});
694
30202
    Trace("cnf") << "ProofCnfStream::handleAnd: CNF_AND_NEG added "
695
15101
                 << clauseNode << "\n";
696
15101
    normalizeAndRegister(clauseNode);
697
  }
698
31744
  return lit;
699
}
700
701
13393
SatLiteral ProofCnfStream::handleOr(TNode node)
702
{
703
13393
  Assert(!d_cnfStream.hasLiteral(node)) << "Atom already mapped!";
704
13393
  Assert(node.getKind() == kind::OR) << "Expecting an OR expression!";
705
13393
  Assert(node.getNumChildren() > 1) << "Expecting more then 1 child!";
706
13393
  Assert(!d_cnfStream.d_removable)
707
      << "Removable clauses can not contain Boolean structure";
708
13393
  Trace("cnf") << "ProofCnfStream::handleOr(" << node << ")\n";
709
  // Number of children
710
13393
  unsigned size = node.getNumChildren();
711
  // Transform all the children first
712
26786
  SatClause clause(size + 1);
713
52084
  for (unsigned i = 0; i < size; ++i)
714
  {
715
38691
    clause[i] = toCNF(node[i]);
716
  }
717
  // Create literal for the node
718
13393
  SatLiteral lit = d_cnfStream.newLiteral(node);
719
  bool added;
720
13393
  NodeManager* nm = NodeManager::currentNM();
721
  // lit <- (a_1 | a_2 | a_3 | ... | a_n)
722
  // lit | ~(a_1 | a_2 | a_3 | ... | a_n)
723
  // (lit | ~a_1) & (lit | ~a_2) & (lit & ~a_3) & ... & (lit & ~a_n)
724
52084
  for (unsigned i = 0; i < size; ++i)
725
  {
726
38691
    added = d_cnfStream.assertClause(node, lit, ~clause[i]);
727
38691
    if (added)
728
    {
729
67878
      Node clauseNode = nm->mkNode(kind::OR, node, node[i].notNode());
730
67878
      Node iNode = nm->mkConst<Rational>(i);
731
33939
      d_proof.addStep(clauseNode, PfRule::CNF_OR_NEG, {}, {node, iNode});
732
67878
      Trace("cnf") << "ProofCnfStream::handleOr: CNF_OR_NEG " << i << " added "
733
33939
                   << clauseNode << "\n";
734
33939
      normalizeAndRegister(clauseNode);
735
    }
736
  }
737
  // lit -> (a_1 | a_2 | a_3 | ... | a_n)
738
  // ~lit | a_1 | a_2 | a_3 | ... | a_n
739
13393
  clause[size] = ~lit;
740
  // This needs to go last, as the clause might get modified by the SAT solver
741
13393
  added = d_cnfStream.assertClause(node.negate(), clause);
742
13393
  if (added)
743
  {
744
25248
    std::vector<Node> disjuncts{node.notNode()};
745
48681
    for (unsigned i = 0; i < size; ++i)
746
    {
747
36057
      disjuncts.push_back(node[i]);
748
    }
749
25248
    Node clauseNode = nm->mkNode(kind::OR, disjuncts);
750
12624
    d_proof.addStep(clauseNode, PfRule::CNF_OR_POS, {}, {node});
751
25248
    Trace("cnf") << "ProofCnfStream::handleOr: CNF_OR_POS added " << clauseNode
752
12624
                 << "\n";
753
12624
    normalizeAndRegister(clauseNode);
754
  }
755
26786
  return lit;
756
}
757
758
166
SatLiteral ProofCnfStream::handleXor(TNode node)
759
{
760
166
  Assert(!d_cnfStream.hasLiteral(node)) << "Atom already mapped!";
761
166
  Assert(node.getKind() == kind::XOR) << "Expecting an XOR expression!";
762
166
  Assert(node.getNumChildren() == 2) << "Expecting exactly 2 children!";
763
166
  Assert(!d_cnfStream.d_removable)
764
      << "Removable clauses can not contain Boolean structure";
765
166
  Trace("cnf") << "ProofCnfStream::handleXor(" << node << ")\n";
766
166
  SatLiteral a = toCNF(node[0]);
767
166
  SatLiteral b = toCNF(node[1]);
768
166
  SatLiteral lit = d_cnfStream.newLiteral(node);
769
  bool added;
770
166
  added = d_cnfStream.assertClause(node.negate(), a, b, ~lit);
771
166
  if (added)
772
  {
773
    Node clauseNode = NodeManager::currentNM()->mkNode(
774
310
        kind::OR, node.notNode(), node[0], node[1]);
775
155
    d_proof.addStep(clauseNode, PfRule::CNF_XOR_POS1, {}, {node});
776
310
    Trace("cnf") << "ProofCnfStream::handleXor: CNF_XOR_POS1 added "
777
155
                 << clauseNode << "\n";
778
155
    normalizeAndRegister(clauseNode);
779
  }
780
166
  added = d_cnfStream.assertClause(node.negate(), ~a, ~b, ~lit);
781
166
  if (added)
782
  {
783
    Node clauseNode = NodeManager::currentNM()->mkNode(
784
316
        kind::OR, node.notNode(), node[0].notNode(), node[1].notNode());
785
158
    d_proof.addStep(clauseNode, PfRule::CNF_XOR_POS2, {}, {node});
786
316
    Trace("cnf") << "ProofCnfStream::handleXor: CNF_XOR_POS2 added "
787
158
                 << clauseNode << "\n";
788
158
    normalizeAndRegister(clauseNode);
789
  }
790
166
  added = d_cnfStream.assertClause(node, a, ~b, lit);
791
166
  if (added)
792
  {
793
    Node clauseNode = NodeManager::currentNM()->mkNode(
794
314
        kind::OR, node, node[0], node[1].notNode());
795
157
    d_proof.addStep(clauseNode, PfRule::CNF_XOR_NEG2, {}, {node});
796
314
    Trace("cnf") << "ProofCnfStream::handleXor: CNF_XOR_NEG2 added "
797
157
                 << clauseNode << "\n";
798
157
    normalizeAndRegister(clauseNode);
799
  }
800
166
  added = d_cnfStream.assertClause(node, ~a, b, lit);
801
166
  if (added)
802
  {
803
    Node clauseNode = NodeManager::currentNM()->mkNode(
804
312
        kind::OR, node, node[0].notNode(), node[1]);
805
156
    d_proof.addStep(clauseNode, PfRule::CNF_XOR_NEG1, {}, {node});
806
312
    Trace("cnf") << "ProofCnfStream::handleXor: CNF_XOR_NEG1 added "
807
156
                 << clauseNode << "\n";
808
156
    normalizeAndRegister(clauseNode);
809
  }
810
166
  return lit;
811
}
812
813
1630
SatLiteral ProofCnfStream::handleIff(TNode node)
814
{
815
1630
  Assert(!d_cnfStream.hasLiteral(node)) << "Atom already mapped!";
816
1630
  Assert(node.getKind() == kind::EQUAL) << "Expecting an EQUAL expression!";
817
1630
  Assert(node.getNumChildren() == 2) << "Expecting exactly 2 children!";
818
1630
  Trace("cnf") << "handleIff(" << node << ")\n";
819
  // Convert the children to CNF
820
1630
  SatLiteral a = toCNF(node[0]);
821
1630
  SatLiteral b = toCNF(node[1]);
822
  // Create literal for the node
823
1630
  SatLiteral lit = d_cnfStream.newLiteral(node);
824
  bool added;
825
1630
  NodeManager* nm = NodeManager::currentNM();
826
  // lit -> ((a-> b) & (b->a))
827
  // ~lit | ((~a | b) & (~b | a))
828
  // (~a | b | ~lit) & (~b | a | ~lit)
829
1630
  added = d_cnfStream.assertClause(node.negate(), ~a, b, ~lit);
830
1630
  if (added)
831
  {
832
    Node clauseNode =
833
2826
        nm->mkNode(kind::OR, node.notNode(), node[0].notNode(), node[1]);
834
1413
    d_proof.addStep(clauseNode, PfRule::CNF_EQUIV_POS1, {}, {node});
835
2826
    Trace("cnf") << "ProofCnfStream::handleIff: CNF_EQUIV_POS1 added "
836
1413
                 << clauseNode << "\n";
837
1413
    normalizeAndRegister(clauseNode);
838
  }
839
1630
  added = d_cnfStream.assertClause(node.negate(), a, ~b, ~lit);
840
1630
  if (added)
841
  {
842
    Node clauseNode =
843
1988
        nm->mkNode(kind::OR, node.notNode(), node[0], node[1].notNode());
844
994
    d_proof.addStep(clauseNode, PfRule::CNF_EQUIV_POS2, {}, {node});
845
1988
    Trace("cnf") << "ProofCnfStream::handleIff: CNF_EQUIV_POS2 added "
846
994
                 << clauseNode << "\n";
847
994
    normalizeAndRegister(clauseNode);
848
  }
849
  // (a<->b) -> lit
850
  // ~((a & b) | (~a & ~b)) | lit
851
  // (~(a & b)) & (~(~a & ~b)) | lit
852
  // ((~a | ~b) & (a | b)) | lit
853
  // (~a | ~b | lit) & (a | b | lit)
854
1630
  added = d_cnfStream.assertClause(node, ~a, ~b, lit);
855
1630
  if (added)
856
  {
857
    Node clauseNode =
858
3068
        nm->mkNode(kind::OR, node, node[0].notNode(), node[1].notNode());
859
1534
    d_proof.addStep(clauseNode, PfRule::CNF_EQUIV_NEG2, {}, {node});
860
3068
    Trace("cnf") << "ProofCnfStream::handleIff: CNF_EQUIV_NEG2 added "
861
1534
                 << clauseNode << "\n";
862
1534
    normalizeAndRegister(clauseNode);
863
  }
864
1630
  added = d_cnfStream.assertClause(node, a, b, lit);
865
1630
  if (added)
866
  {
867
1748
    Node clauseNode = nm->mkNode(kind::OR, node, node[0], node[1]);
868
874
    d_proof.addStep(clauseNode, PfRule::CNF_EQUIV_NEG1, {}, {node});
869
1748
    Trace("cnf") << "ProofCnfStream::handleIff: CNF_EQUIV_NEG1 added "
870
874
                 << clauseNode << "\n";
871
874
    normalizeAndRegister(clauseNode);
872
  }
873
1630
  return lit;
874
}
875
876
952
SatLiteral ProofCnfStream::handleImplies(TNode node)
877
{
878
952
  Assert(!d_cnfStream.hasLiteral(node)) << "Atom already mapped!";
879
952
  Assert(node.getKind() == kind::IMPLIES) << "Expecting an IMPLIES expression!";
880
952
  Assert(node.getNumChildren() == 2) << "Expecting exactly 2 children!";
881
952
  Assert(!d_cnfStream.d_removable)
882
      << "Removable clauses can not contain Boolean structure";
883
952
  Trace("cnf") << "ProofCnfStream::handleImplies(" << node << ")\n";
884
  // Convert the children to cnf
885
952
  SatLiteral a = toCNF(node[0]);
886
952
  SatLiteral b = toCNF(node[1]);
887
952
  SatLiteral lit = d_cnfStream.newLiteral(node);
888
  bool added;
889
952
  NodeManager* nm = NodeManager::currentNM();
890
  // lit -> (a->b)
891
  // ~lit | ~ a | b
892
952
  added = d_cnfStream.assertClause(node.negate(), ~lit, ~a, b);
893
952
  if (added)
894
  {
895
    Node clauseNode =
896
1886
        nm->mkNode(kind::OR, node.notNode(), node[0].notNode(), node[1]);
897
943
    d_proof.addStep(clauseNode, PfRule::CNF_IMPLIES_POS, {}, {node});
898
1886
    Trace("cnf") << "ProofCnfStream::handleImplies: CNF_IMPLIES_POS added "
899
943
                 << clauseNode << "\n";
900
943
    normalizeAndRegister(clauseNode);
901
  }
902
  // (a->b) -> lit
903
  // ~(~a | b) | lit
904
  // (a | l) & (~b | l)
905
952
  added = d_cnfStream.assertClause(node, a, lit);
906
952
  if (added)
907
  {
908
1894
    Node clauseNode = nm->mkNode(kind::OR, node, node[0]);
909
947
    d_proof.addStep(clauseNode, PfRule::CNF_IMPLIES_NEG1, {}, {node});
910
1894
    Trace("cnf") << "ProofCnfStream::handleImplies: CNF_IMPLIES_NEG1 added "
911
947
                 << clauseNode << "\n";
912
947
    normalizeAndRegister(clauseNode);
913
  }
914
952
  added = d_cnfStream.assertClause(node, ~b, lit);
915
952
  if (added)
916
  {
917
1902
    Node clauseNode = nm->mkNode(kind::OR, node, node[1].notNode());
918
951
    d_proof.addStep(clauseNode, PfRule::CNF_IMPLIES_NEG2, {}, {node});
919
1902
    Trace("cnf") << "ProofCnfStream::handleImplies: CNF_IMPLIES_NEG2 added "
920
951
                 << clauseNode << "\n";
921
951
    normalizeAndRegister(clauseNode);
922
  }
923
952
  return lit;
924
}
925
926
1631
SatLiteral ProofCnfStream::handleIte(TNode node)
927
{
928
1631
  Assert(!d_cnfStream.hasLiteral(node)) << "Atom already mapped!";
929
1631
  Assert(node.getKind() == kind::ITE);
930
1631
  Assert(node.getNumChildren() == 3);
931
1631
  Assert(!d_cnfStream.d_removable)
932
      << "Removable clauses can not contain Boolean structure";
933
3262
  Trace("cnf") << "handleIte(" << node[0] << " " << node[1] << " " << node[2]
934
1631
               << ")\n";
935
1631
  SatLiteral condLit = toCNF(node[0]);
936
1631
  SatLiteral thenLit = toCNF(node[1]);
937
1631
  SatLiteral elseLit = toCNF(node[2]);
938
  // create literal to the node
939
1631
  SatLiteral lit = d_cnfStream.newLiteral(node);
940
  bool added;
941
1631
  NodeManager* nm = NodeManager::currentNM();
942
  // If ITE is true then one of the branches is true and the condition
943
  // implies which one
944
  // lit -> (ite b t e)
945
  // lit -> (t | e) & (b -> t) & (!b -> e)
946
  // lit -> (t | e) & (!b | t) & (b | e)
947
  // (!lit | t | e) & (!lit | !b | t) & (!lit | b | e)
948
1631
  added = d_cnfStream.assertClause(node.negate(), ~lit, thenLit, elseLit);
949
1631
  if (added)
950
  {
951
3208
    Node clauseNode = nm->mkNode(kind::OR, node.notNode(), node[1], node[2]);
952
1604
    d_proof.addStep(clauseNode, PfRule::CNF_ITE_POS3, {}, {node});
953
3208
    Trace("cnf") << "ProofCnfStream::handleIte: CNF_ITE_POS3 added "
954
1604
                 << clauseNode << "\n";
955
1604
    normalizeAndRegister(clauseNode);
956
  }
957
1631
  added = d_cnfStream.assertClause(node.negate(), ~lit, ~condLit, thenLit);
958
1631
  if (added)
959
  {
960
    Node clauseNode =
961
3128
        nm->mkNode(kind::OR, node.notNode(), node[0].notNode(), node[1]);
962
1564
    d_proof.addStep(clauseNode, PfRule::CNF_ITE_POS1, {}, {node});
963
3128
    Trace("cnf") << "ProofCnfStream::handleIte: CNF_ITE_POS1 added "
964
1564
                 << clauseNode << "\n";
965
1564
    normalizeAndRegister(clauseNode);
966
  }
967
1631
  added = d_cnfStream.assertClause(node.negate(), ~lit, condLit, elseLit);
968
1631
  if (added)
969
  {
970
2602
    Node clauseNode = nm->mkNode(kind::OR, node.notNode(), node[0], node[2]);
971
1301
    d_proof.addStep(clauseNode, PfRule::CNF_ITE_POS2, {}, {node});
972
2602
    Trace("cnf") << "ProofCnfStream::handleIte: CNF_ITE_POS2 added "
973
1301
                 << clauseNode << "\n";
974
1301
    normalizeAndRegister(clauseNode);
975
  }
976
  // If ITE is false then one of the branches is false and the condition
977
  // implies which one
978
  // !lit -> !(ite b t e)
979
  // !lit -> (!t | !e) & (b -> !t) & (!b -> !e)
980
  // !lit -> (!t | !e) & (!b | !t) & (b | !e)
981
  // (lit | !t | !e) & (lit | !b | !t) & (lit | b | !e)
982
1631
  added = d_cnfStream.assertClause(node, lit, ~thenLit, ~elseLit);
983
1631
  if (added)
984
  {
985
    Node clauseNode =
986
3216
        nm->mkNode(kind::OR, node, node[1].notNode(), node[2].notNode());
987
1608
    d_proof.addStep(clauseNode, PfRule::CNF_ITE_NEG3, {}, {node});
988
3216
    Trace("cnf") << "ProofCnfStream::handleIte: CNF_ITE_NEG3 added "
989
1608
                 << clauseNode << "\n";
990
1608
    normalizeAndRegister(clauseNode);
991
  }
992
1631
  added = d_cnfStream.assertClause(node, lit, ~condLit, ~thenLit);
993
1631
  if (added)
994
  {
995
    Node clauseNode =
996
3120
        nm->mkNode(kind::OR, node, node[0].notNode(), node[1].notNode());
997
1560
    d_proof.addStep(clauseNode, PfRule::CNF_ITE_NEG1, {}, {node});
998
3120
    Trace("cnf") << "ProofCnfStream::handleIte: CNF_ITE_NEG1 added "
999
1560
                 << clauseNode << "\n";
1000
1560
    normalizeAndRegister(clauseNode);
1001
  }
1002
1631
  added = d_cnfStream.assertClause(node, lit, condLit, ~elseLit);
1003
1631
  if (added)
1004
  {
1005
2600
    Node clauseNode = nm->mkNode(kind::OR, node, node[0], node[2].notNode());
1006
1300
    d_proof.addStep(clauseNode, PfRule::CNF_ITE_NEG2, {}, {node});
1007
2600
    Trace("cnf") << "ProofCnfStream::handleIte: CNF_ITE_NEG2 added "
1008
1300
                 << clauseNode << "\n";
1009
1300
    normalizeAndRegister(clauseNode);
1010
  }
1011
1631
  return lit;
1012
}
1013
1014
}  // namespace prop
1015
26676
}  // namespace CVC4