GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/booleans/proof_checker.cpp Lines: 462 530 87.2 %
Date: 2021-03-23 Branches: 1039 3294 31.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file proof_checker.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Haniel Barbosa, Andrew Reynolds, Mathias Preiner
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 equality proof checker
13
 **/
14
15
#include "theory/booleans/proof_checker.h"
16
#include "expr/skolem_manager.h"
17
#include "theory/rewriter.h"
18
19
namespace CVC4 {
20
namespace theory {
21
namespace booleans {
22
23
962
void BoolProofRuleChecker::registerTo(ProofChecker* pc)
24
{
25
962
  pc->registerChecker(PfRule::SPLIT, this);
26
962
  pc->registerChecker(PfRule::RESOLUTION, this);
27
962
  pc->registerChecker(PfRule::CHAIN_RESOLUTION, this);
28
962
  pc->registerChecker(PfRule::MACRO_RESOLUTION, this);
29
962
  pc->registerChecker(PfRule::FACTORING, this);
30
962
  pc->registerChecker(PfRule::REORDERING, this);
31
962
  pc->registerChecker(PfRule::EQ_RESOLVE, this);
32
962
  pc->registerChecker(PfRule::MODUS_PONENS, this);
33
962
  pc->registerChecker(PfRule::NOT_NOT_ELIM, this);
34
962
  pc->registerChecker(PfRule::CONTRA, this);
35
962
  pc->registerChecker(PfRule::AND_ELIM, this);
36
962
  pc->registerChecker(PfRule::AND_INTRO, this);
37
962
  pc->registerChecker(PfRule::NOT_OR_ELIM, this);
38
962
  pc->registerChecker(PfRule::IMPLIES_ELIM, this);
39
962
  pc->registerChecker(PfRule::NOT_IMPLIES_ELIM1, this);
40
962
  pc->registerChecker(PfRule::NOT_IMPLIES_ELIM2, this);
41
962
  pc->registerChecker(PfRule::EQUIV_ELIM1, this);
42
962
  pc->registerChecker(PfRule::EQUIV_ELIM2, this);
43
962
  pc->registerChecker(PfRule::NOT_EQUIV_ELIM1, this);
44
962
  pc->registerChecker(PfRule::NOT_EQUIV_ELIM2, this);
45
962
  pc->registerChecker(PfRule::XOR_ELIM1, this);
46
962
  pc->registerChecker(PfRule::XOR_ELIM2, this);
47
962
  pc->registerChecker(PfRule::NOT_XOR_ELIM1, this);
48
962
  pc->registerChecker(PfRule::NOT_XOR_ELIM2, this);
49
962
  pc->registerChecker(PfRule::ITE_ELIM1, this);
50
962
  pc->registerChecker(PfRule::ITE_ELIM2, this);
51
962
  pc->registerChecker(PfRule::NOT_ITE_ELIM1, this);
52
962
  pc->registerChecker(PfRule::NOT_ITE_ELIM2, this);
53
962
  pc->registerChecker(PfRule::NOT_AND, this);
54
962
  pc->registerChecker(PfRule::CNF_AND_POS, this);
55
962
  pc->registerChecker(PfRule::CNF_AND_NEG, this);
56
962
  pc->registerChecker(PfRule::CNF_OR_POS, this);
57
962
  pc->registerChecker(PfRule::CNF_OR_NEG, this);
58
962
  pc->registerChecker(PfRule::CNF_IMPLIES_POS, this);
59
962
  pc->registerChecker(PfRule::CNF_IMPLIES_NEG1, this);
60
962
  pc->registerChecker(PfRule::CNF_IMPLIES_NEG2, this);
61
962
  pc->registerChecker(PfRule::CNF_EQUIV_POS1, this);
62
962
  pc->registerChecker(PfRule::CNF_EQUIV_POS2, this);
63
962
  pc->registerChecker(PfRule::CNF_EQUIV_NEG1, this);
64
962
  pc->registerChecker(PfRule::CNF_EQUIV_NEG2, this);
65
962
  pc->registerChecker(PfRule::CNF_XOR_POS1, this);
66
962
  pc->registerChecker(PfRule::CNF_XOR_POS2, this);
67
962
  pc->registerChecker(PfRule::CNF_XOR_NEG1, this);
68
962
  pc->registerChecker(PfRule::CNF_XOR_NEG2, this);
69
962
  pc->registerChecker(PfRule::CNF_ITE_POS1, this);
70
962
  pc->registerChecker(PfRule::CNF_ITE_POS2, this);
71
962
  pc->registerChecker(PfRule::CNF_ITE_POS3, this);
72
962
  pc->registerChecker(PfRule::CNF_ITE_NEG1, this);
73
962
  pc->registerChecker(PfRule::CNF_ITE_NEG2, this);
74
962
  pc->registerChecker(PfRule::CNF_ITE_NEG3, this);
75
962
}
76
77
1656979
Node BoolProofRuleChecker::checkInternal(PfRule id,
78
                                         const std::vector<Node>& children,
79
                                         const std::vector<Node>& args)
80
{
81
1656979
  if (id == PfRule::RESOLUTION)
82
  {
83
21225
    Assert(children.size() == 2);
84
21225
    Assert(args.size() == 2);
85
21225
    NodeManager* nm = NodeManager::currentNM();
86
42450
    std::vector<Node> disjuncts;
87
42450
    Node pivots[2];
88
21225
    if (args[0] == nm->mkConst(true))
89
    {
90
19047
      pivots[0] = args[1];
91
19047
      pivots[1] = args[1].notNode();
92
    }
93
    else
94
    {
95
2178
      Assert(args[0] == nm->mkConst(false));
96
2178
      pivots[0] = args[1].notNode();
97
2178
      pivots[1] = args[1];
98
    }
99
63675
    for (unsigned i = 0; i < 2; ++i)
100
    {
101
      // determine whether the clause is a singleton for effects of resolution,
102
      // which is the case if it's not an OR node or it is an OR node but it is
103
      // equal to the pivot
104
84900
      std::vector<Node> lits;
105
42450
      if (children[i].getKind() == kind::OR && pivots[i] != children[i])
106
      {
107
39287
        lits.insert(lits.end(), children[i].begin(), children[i].end());
108
      }
109
      else
110
      {
111
3163
        lits.push_back(children[i]);
112
      }
113
252949
      for (unsigned j = 0, size = lits.size(); j < size; ++j)
114
      {
115
210499
        if (pivots[i] != lits[j])
116
        {
117
168049
          disjuncts.push_back(lits[j]);
118
        }
119
        else
120
        {
121
          // just eliminate first occurrence
122
42450
          pivots[i] = Node::null();
123
        }
124
      }
125
    }
126
21225
    return disjuncts.empty()
127
               ? nm->mkConst(false)
128
24388
               : disjuncts.size() == 1 ? disjuncts[0]
129
45613
                                       : nm->mkNode(kind::OR, disjuncts);
130
  }
131
1635754
  if (id == PfRule::FACTORING)
132
  {
133
65662
    Assert(children.size() == 1);
134
65662
    Assert(args.empty());
135
65662
    if (children[0].getKind() != kind::OR)
136
    {
137
      return Node::null();
138
    }
139
    // remove duplicates while keeping the order of children
140
131324
    std::unordered_set<TNode, TNodeHashFunction> clauseSet;
141
131324
    std::vector<Node> disjuncts;
142
65662
    unsigned size = children[0].getNumChildren();
143
1139857
    for (unsigned i = 0; i < size; ++i)
144
    {
145
1074195
      if (clauseSet.count(children[0][i]))
146
      {
147
380576
        continue;
148
      }
149
693619
      disjuncts.push_back(children[0][i]);
150
693619
      clauseSet.insert(children[0][i]);
151
    }
152
65662
    if (disjuncts.size() == size)
153
    {
154
      return Node::null();
155
    }
156
65662
    NodeManager* nm = NodeManager::currentNM();
157
65662
    return disjuncts.empty()
158
               ? nm->mkConst<bool>(false)
159
66561
               : disjuncts.size() == 1 ? disjuncts[0]
160
132223
                                       : nm->mkNode(kind::OR, disjuncts);
161
  }
162
1570092
  if (id == PfRule::REORDERING)
163
  {
164
450523
    Assert(children.size() == 1);
165
450523
    Assert(args.size() == 1);
166
901046
    std::unordered_set<Node, NodeHashFunction> clauseSet1, clauseSet2;
167
450523
    if (children[0].getKind() == kind::OR)
168
    {
169
450523
      clauseSet1.insert(children[0].begin(), children[0].end());
170
    }
171
    else
172
    {
173
      clauseSet1.insert(children[0]);
174
    }
175
450523
    if (args[0].getKind() == kind::OR)
176
    {
177
450523
      clauseSet2.insert(args[0].begin(), args[0].end());
178
    }
179
    else
180
    {
181
      clauseSet2.insert(args[0]);
182
    }
183
450523
    if (clauseSet1 != clauseSet2)
184
    {
185
      Trace("bool-pfcheck") << id << ": clause set1: " << clauseSet1 << "\n"
186
                            << id << ": clause set2: " << clauseSet2 << "\n";
187
      return Node::null();
188
    }
189
450523
    return args[0];
190
  }
191
1119569
  if (id == PfRule::CHAIN_RESOLUTION)
192
  {
193
105327
    Assert(children.size() > 1);
194
105327
    Assert(args.size() == 2 * (children.size() - 1));
195
105327
    Trace("bool-pfcheck") << "chain_res:\n" << push;
196
105327
    NodeManager* nm = NodeManager::currentNM();
197
210654
    Node trueNode = nm->mkConst(true);
198
210654
    Node falseNode = nm->mkConst(false);
199
210654
    std::vector<Node> clauseNodes;
200
    // literals to be removed from the virtual lhs clause of the resolution
201
210654
    std::unordered_map<Node, unsigned, NodeHashFunction> lhsElim;
202
1105607
    for (std::size_t i = 0, argsSize = args.size(); i < argsSize; i = i + 2)
203
    {
204
      // whether pivot should occur as is or negated depends on the polarity of
205
      // each step in the chain
206
1000280
      if (args[i] == trueNode)
207
      {
208
344372
        lhsElim[args[i + 1]]++;
209
      }
210
      else
211
      {
212
655908
        Assert(args[i] == falseNode);
213
655908
        lhsElim[args[i + 1].notNode()]++;
214
      }
215
    }
216
105327
    if (Trace.isOn("bool-pfcheck"))
217
    {
218
      Trace("bool-pfcheck")
219
          << "Original elimination multiset for lhs clause:\n";
220
      for (const auto& pair : lhsElim)
221
      {
222
        Trace("bool-pfcheck")
223
            << "\t- " << pair.first << " {" << pair.second << "}\n";
224
      }
225
    }
226
1210934
    for (std::size_t i = 0, childrenSize = children.size(); i < childrenSize;
227
         ++i)
228
    {
229
      // literal to be removed from rhs clause. They will be negated
230
2211214
      Node rhsElim = Node::null();
231
1105607
      if (Trace.isOn("bool-pfcheck"))
232
      {
233
        Trace("bool-pfcheck") << i << ": current lhsElim:\n";
234
        for (const auto& pair : lhsElim)
235
        {
236
          Trace("bool-pfcheck")
237
              << "\t- " << pair.first << " {" << pair.second << "}\n";
238
        }
239
      }
240
1105607
      if (i > 0)
241
      {
242
1000280
        std::size_t index = 2 * (i - 1);
243
1656188
        rhsElim = args[index] == trueNode ? args[index + 1].notNode()
244
655908
                                          : args[index + 1];
245
1000280
        Trace("bool-pfcheck") << i << ": rhs elim: " << rhsElim << "\n";
246
      }
247
      // Only add to conclusion nodes that are not in elimination set. First get
248
      // the nodes.
249
      //
250
      // Since a Node cannot hold an OR with a single child we need to
251
      // disambiguate singleton clauses that are OR nodes from non-singleton
252
      // clauses (i.e. unit clauses in the SAT solver).
253
      //
254
      // If the child is not an OR, it is a singleton clause and we take the
255
      // child itself as the clause. Otherwise the child can only be a singleton
256
      // clause if the child itself is used as a resolution literal, i.e. if the
257
      // child is in lhsElim or is equal to rhsElim (which means that the
258
      // negation of the child is in lhsElim).
259
2211214
      std::vector<Node> lits;
260
2737134
      if (children[i].getKind() == kind::OR && lhsElim.count(children[i]) == 0
261
1631527
          && children[i] != rhsElim)
262
      {
263
522582
        lits.insert(lits.end(), children[i].begin(), children[i].end());
264
      }
265
      else
266
      {
267
583025
        lits.push_back(children[i]);
268
      }
269
1105607
      Trace("bool-pfcheck") << i << ": clause lits: " << lits << "\n";
270
2211214
      std::vector<Node> added;
271
4557635
      for (std::size_t j = 0, size = lits.size(); j < size; ++j)
272
      {
273
4452308
        if (lits[j] == rhsElim)
274
        {
275
1000280
          rhsElim = Node::null();
276
1000280
          continue;
277
        }
278
2451748
        auto it = lhsElim.find(lits[j]);
279
2451748
        if (it == lhsElim.end())
280
        {
281
1451468
          clauseNodes.push_back(lits[j]);
282
1451468
          added.push_back(lits[j]);
283
        }
284
        else
285
        {
286
          // remove occurrence
287
1000280
          it->second--;
288
1000280
          if (it->second == 0)
289
          {
290
899747
            lhsElim.erase(it);
291
          }
292
        }
293
      }
294
1105607
      Trace("bool-pfcheck") << i << ": added lits: " << added << "\n\n";
295
    }
296
105327
    Trace("bool-pfcheck") << "clause: " << clauseNodes << "\n" << pop;
297
105327
    return clauseNodes.empty()
298
               ? nm->mkConst(false)
299
125846
               : clauseNodes.size() == 1 ? clauseNodes[0]
300
231173
                                         : nm->mkNode(kind::OR, clauseNodes);
301
  }
302
1014242
  if (id == PfRule::MACRO_RESOLUTION)
303
  {
304
133798
    Assert(children.size() > 1);
305
133798
    Assert(args.size() == 2 * (children.size() - 1) + 1);
306
133798
    Trace("bool-pfcheck") << "macro_res: " << args[0] << "\n" << push;
307
133798
    NodeManager* nm = NodeManager::currentNM();
308
267596
    Node trueNode = nm->mkConst(true);
309
267596
    Node falseNode = nm->mkConst(false);
310
267596
    std::vector<Node> clauseNodes;
311
2247313
    for (std::size_t i = 0, childrenSize = children.size(); i < childrenSize;
312
         ++i)
313
    {
314
4227030
      std::unordered_set<Node, NodeHashFunction> elim;
315
      // literals to be removed from "first" clause
316
2113515
      if (i < childrenSize - 1)
317
      {
318
51545041
        for (std::size_t j = (2 * i) + 1, argsSize = args.size(); j < argsSize;
319
49565324
             j = j + 2)
320
        {
321
          // whether pivot should occur as is or negated depends on the polarity
322
          // of each step in the macro
323
49565324
          if (args[j] == trueNode)
324
          {
325
20735979
            elim.insert(args[j + 1]);
326
          }
327
          else
328
          {
329
28829345
            Assert(args[j] == falseNode);
330
28829345
            elim.insert(args[j + 1].notNode());
331
          }
332
        }
333
      }
334
      // literal to be removed from "second" clause. They will be negated
335
2113515
      if (i > 0)
336
      {
337
1979717
        std::size_t index = 2 * (i - 1) + 1;
338
2795666
        Node pivot = args[index] == trueNode ? args[index + 1].notNode()
339
4775383
                                             : args[index + 1];
340
1979717
        elim.insert(pivot);
341
      }
342
2113515
      Trace("bool-pfcheck") << i << ": elimination set: " << elim << "\n";
343
      // only add to conclusion nodes that are not in elimination set. First get
344
      // the nodes.
345
      //
346
      // Since a Node cannot hold an OR with a single child we need to
347
      // disambiguate singleton clauses that are OR nodes from non-singleton
348
      // clauses (i.e. unit clauses in the SAT solver).
349
      //
350
      // If the child is not an OR, it is a singleton clause and we take the
351
      // child itself as the clause. Otherwise the child can only be a singleton
352
      // clause if the child itself is used as a resolution literal, i.e. if the
353
      // child is in lhsElim or is equal to rhsElim (which means that the
354
      // negation of the child is in lhsElim).
355
4227030
      std::vector<Node> lits;
356
2113515
      if (children[i].getKind() == kind::OR && !elim.count(children[i]))
357
      {
358
1149651
        lits.insert(lits.end(), children[i].begin(), children[i].end());
359
      }
360
      else
361
      {
362
963864
        lits.push_back(children[i]);
363
      }
364
2113515
      Trace("bool-pfcheck") << i << ": clause lits: " << lits << "\n";
365
4227030
      std::vector<Node> added;
366
8040640
      for (std::size_t j = 0, size = lits.size(); j < size; ++j)
367
      {
368
        // only add if literal does not occur in elimination set
369
5927125
        if (elim.count(lits[j]) == 0)
370
        {
371
1389920
          clauseNodes.push_back(lits[j]);
372
1389920
          added.push_back(lits[j]);
373
          // eliminate duplicates
374
1389920
          elim.insert(lits[j]);
375
        }
376
      }
377
2113515
      Trace("bool-pfcheck") << i << ": added lits: " << added << "\n\n";
378
    }
379
133798
    Trace("bool-pfcheck") << "clause: " << clauseNodes << "\n";
380
    // check that set representation is the same as of the given conclusion
381
    std::unordered_set<Node, NodeHashFunction> clauseComputed{
382
267596
        clauseNodes.begin(), clauseNodes.end()};
383
133798
    Trace("bool-pfcheck") << "clauseSet: " << clauseComputed << "\n" << pop;
384
133798
    if (clauseComputed.empty())
385
    {
386
      // conclusion differ
387
2687
      if (args[0] != falseNode)
388
      {
389
        return Node::null();
390
      }
391
2687
      return args[0];
392
    }
393
131111
    if (clauseComputed.size() == 1)
394
    {
395
      // conclusion differ
396
68093
      if (args[0] != *clauseComputed.begin())
397
      {
398
        return Node::null();
399
      }
400
68093
      return args[0];
401
    }
402
    // At this point, should amount to them differing only on order. So the
403
    // original result can't be a singleton clause
404
126036
    if (args[0].getKind() != kind::OR
405
63018
        || clauseComputed.size() != args[0].getNumChildren())
406
    {
407
      return Node::null();
408
    }
409
63018
    std::unordered_set<Node, NodeHashFunction> clauseGiven{args[0].begin(),
410
126036
                                                           args[0].end()};
411
63018
    return clauseComputed == clauseGiven ? args[0] : Node::null();
412
  }
413
880444
  if (id == PfRule::SPLIT)
414
  {
415
10026
    Assert(children.empty());
416
10026
    Assert(args.size() == 1);
417
    return NodeManager::currentNM()->mkNode(
418
10026
        kind::OR, args[0], args[0].notNode());
419
  }
420
870418
  if (id == PfRule::CONTRA)
421
  {
422
11233
    Assert(children.size() == 2);
423
11233
    if (children[1].getKind() == Kind::NOT && children[0] == children[1][0])
424
    {
425
11233
      return NodeManager::currentNM()->mkConst(false);
426
    }
427
    return Node::null();
428
  }
429
859185
  if (id == PfRule::EQ_RESOLVE)
430
  {
431
173825
    Assert(children.size() == 2);
432
173825
    Assert(args.empty());
433
173825
    if (children[1].getKind() != kind::EQUAL || children[0] != children[1][0])
434
    {
435
      return Node::null();
436
    }
437
173825
    return children[1][1];
438
  }
439
685360
  if (id == PfRule::MODUS_PONENS)
440
  {
441
52146
    Assert(children.size() == 2);
442
52146
    Assert(args.empty());
443
52146
    if (children[1].getKind() != kind::IMPLIES || children[0] != children[1][0])
444
    {
445
      return Node::null();
446
    }
447
52146
    return children[1][1];
448
  }
449
633214
  if (id == PfRule::NOT_NOT_ELIM)
450
  {
451
2510
    Assert(children.size() == 1);
452
2510
    Assert(args.empty());
453
2510
    if (children[0].getKind() != kind::NOT || children[0][0].getKind() != kind::NOT)
454
    {
455
      return Node::null();
456
    }
457
2510
    return children[0][0][0];
458
  }
459
  // natural deduction rules
460
630704
  if (id == PfRule::AND_ELIM)
461
  {
462
304437
    Assert(children.size() == 1);
463
304437
    Assert(args.size() == 1);
464
    uint32_t i;
465
304437
    if (children[0].getKind() != kind::AND || !getUInt32(args[0], i))
466
    {
467
      return Node::null();
468
    }
469
304437
    if (i >= children[0].getNumChildren())
470
    {
471
      return Node::null();
472
    }
473
304437
    return children[0][i];
474
  }
475
326267
  if (id == PfRule::AND_INTRO)
476
  {
477
62804
    Assert(children.size() >= 1);
478
62804
    return children.size() == 1
479
               ? children[0]
480
62804
               : NodeManager::currentNM()->mkNode(kind::AND, children);
481
  }
482
263463
  if (id == PfRule::NOT_OR_ELIM)
483
  {
484
6523
    Assert(children.size() == 1);
485
6523
    Assert(args.size() == 1);
486
    uint32_t i;
487
13046
    if (children[0].getKind() != kind::NOT
488
13046
        || children[0][0].getKind() != kind::OR || !getUInt32(args[0], i))
489
    {
490
      return Node::null();
491
    }
492
6523
    if (i >= children[0][0].getNumChildren())
493
    {
494
      return Node::null();
495
    }
496
6523
    return children[0][0][i].notNode();
497
  }
498
256940
  if (id == PfRule::IMPLIES_ELIM)
499
  {
500
41464
    Assert(children.size() == 1);
501
41464
    Assert(args.empty());
502
41464
    if (children[0].getKind() != kind::IMPLIES)
503
    {
504
      return Node::null();
505
    }
506
    return NodeManager::currentNM()->mkNode(
507
41464
        kind::OR, children[0][0].notNode(), children[0][1]);
508
  }
509
215476
  if (id == PfRule::NOT_IMPLIES_ELIM1)
510
  {
511
442
    Assert(children.size() == 1);
512
442
    Assert(args.empty());
513
884
    if (children[0].getKind() != kind::NOT
514
884
        || children[0][0].getKind() != kind::IMPLIES)
515
    {
516
      return Node::null();
517
    }
518
442
    return children[0][0][0];
519
  }
520
215034
  if (id == PfRule::NOT_IMPLIES_ELIM2)
521
  {
522
340
    Assert(children.size() == 1);
523
340
    Assert(args.empty());
524
680
    if (children[0].getKind() != kind::NOT
525
680
        || children[0][0].getKind() != kind::IMPLIES)
526
    {
527
      return Node::null();
528
    }
529
340
    return children[0][0][1].notNode();
530
  }
531
214694
  if (id == PfRule::EQUIV_ELIM1)
532
  {
533
1018
    Assert(children.size() == 1);
534
1018
    Assert(args.empty());
535
1018
    if (children[0].getKind() != kind::EQUAL)
536
    {
537
      return Node::null();
538
    }
539
    return NodeManager::currentNM()->mkNode(
540
1018
        kind::OR, children[0][0].notNode(), children[0][1]);
541
  }
542
213676
  if (id == PfRule::EQUIV_ELIM2)
543
  {
544
1273
    Assert(children.size() == 1);
545
1273
    Assert(args.empty());
546
1273
    if (children[0].getKind() != kind::EQUAL)
547
    {
548
      return Node::null();
549
    }
550
    return NodeManager::currentNM()->mkNode(
551
1273
        kind::OR, children[0][0], children[0][1].notNode());
552
  }
553
212403
  if (id == PfRule::NOT_EQUIV_ELIM1)
554
  {
555
20
    Assert(children.size() == 1);
556
20
    Assert(args.empty());
557
40
    if (children[0].getKind() != kind::NOT
558
40
        || children[0][0].getKind() != kind::EQUAL)
559
    {
560
      return Node::null();
561
    }
562
    return NodeManager::currentNM()->mkNode(
563
20
        kind::OR, children[0][0][0], children[0][0][1]);
564
  }
565
212383
  if (id == PfRule::NOT_EQUIV_ELIM2)
566
  {
567
53
    Assert(children.size() == 1);
568
53
    Assert(args.empty());
569
106
    if (children[0].getKind() != kind::NOT
570
106
        || children[0][0].getKind() != kind::EQUAL)
571
    {
572
      return Node::null();
573
    }
574
    return NodeManager::currentNM()->mkNode(
575
53
        kind::OR, children[0][0][0].notNode(), children[0][0][1].notNode());
576
  }
577
212330
  if (id == PfRule::XOR_ELIM1)
578
  {
579
13
    Assert(children.size() == 1);
580
13
    Assert(args.empty());
581
13
    if (children[0].getKind() != kind::XOR)
582
    {
583
      return Node::null();
584
    }
585
    return NodeManager::currentNM()->mkNode(
586
13
        kind::OR, children[0][0], children[0][1]);
587
  }
588
212317
  if (id == PfRule::XOR_ELIM2)
589
  {
590
22
    Assert(children.size() == 1);
591
22
    Assert(args.empty());
592
22
    if (children[0].getKind() != kind::XOR)
593
    {
594
      return Node::null();
595
    }
596
    return NodeManager::currentNM()->mkNode(
597
22
        kind::OR, children[0][0].notNode(), children[0][1].notNode());
598
  }
599
212295
  if (id == PfRule::NOT_XOR_ELIM1)
600
  {
601
5
    Assert(children.size() == 1);
602
5
    Assert(args.empty());
603
10
    if (children[0].getKind() != kind::NOT
604
10
        || children[0][0].getKind() != kind::XOR)
605
    {
606
      return Node::null();
607
    }
608
    return NodeManager::currentNM()->mkNode(
609
5
        kind::OR, children[0][0][0], children[0][0][1].notNode());
610
  }
611
212290
  if (id == PfRule::NOT_XOR_ELIM2)
612
  {
613
3
    Assert(children.size() == 1);
614
3
    Assert(args.empty());
615
6
    if (children[0].getKind() != kind::NOT
616
6
        || children[0][0].getKind() != kind::XOR)
617
    {
618
      return Node::null();
619
    }
620
    return NodeManager::currentNM()->mkNode(
621
3
        kind::OR, children[0][0][0].notNode(), children[0][0][1]);
622
  }
623
212287
  if (id == PfRule::ITE_ELIM1)
624
  {
625
6854
    Assert(children.size() == 1);
626
6854
    Assert(args.empty());
627
6854
    if (children[0].getKind() != kind::ITE)
628
    {
629
      return Node::null();
630
    }
631
    return NodeManager::currentNM()->mkNode(
632
6854
        kind::OR, children[0][0].notNode(), children[0][1]);
633
  }
634
205433
  if (id == PfRule::ITE_ELIM2)
635
  {
636
16787
    Assert(children.size() == 1);
637
16787
    Assert(args.empty());
638
16787
    if (children[0].getKind() != kind::ITE)
639
    {
640
      return Node::null();
641
    }
642
    return NodeManager::currentNM()->mkNode(
643
16787
        kind::OR, children[0][0], children[0][2]);
644
  }
645
188646
  if (id == PfRule::NOT_ITE_ELIM1)
646
  {
647
3
    Assert(children.size() == 1);
648
3
    Assert(args.empty());
649
6
    if (children[0].getKind() != kind::NOT
650
6
        || children[0][0].getKind() != kind::ITE)
651
    {
652
      return Node::null();
653
    }
654
    return NodeManager::currentNM()->mkNode(
655
3
        kind::OR, children[0][0][0].notNode(), children[0][0][1].notNode());
656
  }
657
188643
  if (id == PfRule::NOT_ITE_ELIM2)
658
  {
659
3
    Assert(children.size() == 1);
660
3
    Assert(args.empty());
661
6
    if (children[0].getKind() != kind::NOT
662
6
        || children[0][0].getKind() != kind::ITE)
663
    {
664
      return Node::null();
665
    }
666
    return NodeManager::currentNM()->mkNode(
667
3
        kind::OR, children[0][0][0], children[0][0][2].notNode());
668
  }
669
  // De Morgan
670
188640
  if (id == PfRule::NOT_AND)
671
  {
672
39529
    Assert(children.size() == 1);
673
39529
    Assert(args.empty());
674
79058
    if (children[0].getKind() != kind::NOT
675
79058
        || children[0][0].getKind() != kind::AND)
676
    {
677
      return Node::null();
678
    }
679
79058
    std::vector<Node> disjuncts;
680
274167
    for (std::size_t i = 0, size = children[0][0].getNumChildren(); i < size;
681
         ++i)
682
    {
683
234638
      disjuncts.push_back(children[0][0][i].notNode());
684
    }
685
39529
    return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
686
  }
687
  // valid clauses rules for Tseitin CNF transformation
688
149111
  if (id == PfRule::CNF_AND_POS)
689
  {
690
45944
    Assert(children.empty());
691
45944
    Assert(args.size() == 2);
692
    uint32_t i;
693
45944
    if (args[0].getKind() != kind::AND || !getUInt32(args[1], i))
694
    {
695
      return Node::null();
696
    }
697
45944
    if (i >= args[0].getNumChildren())
698
    {
699
      return Node::null();
700
    }
701
    return NodeManager::currentNM()->mkNode(
702
45944
        kind::OR, args[0].notNode(), args[0][i]);
703
  }
704
103167
  if (id == PfRule::CNF_AND_NEG)
705
  {
706
31879
    Assert(children.empty());
707
31879
    Assert(args.size() == 1);
708
31879
    if (args[0].getKind() != kind::AND)
709
    {
710
      return Node::null();
711
    }
712
63758
    std::vector<Node> disjuncts{args[0]};
713
221995
    for (unsigned i = 0, size = args[0].getNumChildren(); i < size; ++i)
714
    {
715
190116
      disjuncts.push_back(args[0][i].notNode());
716
    }
717
31879
    return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
718
  }
719
71288
  if (id == PfRule::CNF_OR_POS)
720
  {
721
13853
    Assert(children.empty());
722
13853
    Assert(args.size() == 1);
723
13853
    if (args[0].getKind() != kind::OR)
724
    {
725
      return Node::null();
726
    }
727
27706
    std::vector<Node> disjuncts{args[0].notNode()};
728
240241
    for (unsigned i = 0, size = args[0].getNumChildren(); i < size; ++i)
729
    {
730
226388
      disjuncts.push_back(args[0][i]);
731
    }
732
13853
    return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
733
  }
734
57435
  if (id == PfRule::CNF_OR_NEG)
735
  {
736
38193
    Assert(children.empty());
737
38193
    Assert(args.size() == 2);
738
    uint32_t i;
739
38193
    if (args[0].getKind() != kind::OR || !getUInt32(args[1], i))
740
    {
741
      return Node::null();
742
    }
743
38193
    if (i >= args[0].getNumChildren())
744
    {
745
      return Node::null();
746
    }
747
    return NodeManager::currentNM()->mkNode(
748
38193
        kind::OR, args[0], args[0][i].notNode());
749
  }
750
19242
  if (id == PfRule::CNF_IMPLIES_POS)
751
  {
752
1297
    Assert(children.empty());
753
1297
    Assert(args.size() == 1);
754
1297
    if (args[0].getKind() != kind::IMPLIES)
755
    {
756
      return Node::null();
757
    }
758
    std::vector<Node> disjuncts{
759
2594
        args[0].notNode(), args[0][0].notNode(), args[0][1]};
760
1297
    return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
761
  }
762
17945
  if (id == PfRule::CNF_IMPLIES_NEG1)
763
  {
764
977
    Assert(children.empty());
765
977
    Assert(args.size() == 1);
766
977
    if (args[0].getKind() != kind::IMPLIES)
767
    {
768
      return Node::null();
769
    }
770
1954
    std::vector<Node> disjuncts{args[0], args[0][0]};
771
977
    return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
772
  }
773
16968
  if (id == PfRule::CNF_IMPLIES_NEG2)
774
  {
775
1716
    Assert(children.empty());
776
1716
    Assert(args.size() == 1);
777
1716
    if (args[0].getKind() != kind::IMPLIES)
778
    {
779
      return Node::null();
780
    }
781
3432
    std::vector<Node> disjuncts{args[0], args[0][1].notNode()};
782
1716
    return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
783
  }
784
15252
  if (id == PfRule::CNF_EQUIV_POS1)
785
  {
786
1417
    Assert(children.empty());
787
1417
    Assert(args.size() == 1);
788
1417
    if (args[0].getKind() != kind::EQUAL)
789
    {
790
      return Node::null();
791
    }
792
    std::vector<Node> disjuncts{
793
2834
        args[0].notNode(), args[0][0].notNode(), args[0][1]};
794
1417
    return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
795
  }
796
13835
  if (id == PfRule::CNF_EQUIV_POS2)
797
  {
798
999
    Assert(children.empty());
799
999
    Assert(args.size() == 1);
800
999
    if (args[0].getKind() != kind::EQUAL)
801
    {
802
      return Node::null();
803
    }
804
    std::vector<Node> disjuncts{
805
1998
        args[0].notNode(), args[0][0], args[0][1].notNode()};
806
999
    return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
807
  }
808
12836
  if (id == PfRule::CNF_EQUIV_NEG1)
809
  {
810
913
    Assert(children.empty());
811
913
    Assert(args.size() == 1);
812
913
    if (args[0].getKind() != kind::EQUAL)
813
    {
814
      return Node::null();
815
    }
816
1826
    std::vector<Node> disjuncts{args[0], args[0][0], args[0][1]};
817
913
    return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
818
  }
819
11923
  if (id == PfRule::CNF_EQUIV_NEG2)
820
  {
821
2312
    Assert(children.empty());
822
2312
    Assert(args.size() == 1);
823
2312
    if (args[0].getKind() != kind::EQUAL)
824
    {
825
      return Node::null();
826
    }
827
    std::vector<Node> disjuncts{
828
4624
        args[0], args[0][0].notNode(), args[0][1].notNode()};
829
2312
    return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
830
  }
831
9611
  if (id == PfRule::CNF_XOR_POS1)
832
  {
833
157
    Assert(children.empty());
834
157
    Assert(args.size() == 1);
835
157
    if (args[0].getKind() != kind::XOR)
836
    {
837
      return Node::null();
838
    }
839
314
    std::vector<Node> disjuncts{args[0].notNode(), args[0][0], args[0][1]};
840
157
    return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
841
  }
842
9454
  if (id == PfRule::CNF_XOR_POS2)
843
  {
844
162
    Assert(children.empty());
845
162
    Assert(args.size() == 1);
846
162
    if (args[0].getKind() != kind::XOR)
847
    {
848
      return Node::null();
849
    }
850
    std::vector<Node> disjuncts{
851
324
        args[0].notNode(), args[0][0].notNode(), args[0][1].notNode()};
852
162
    return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
853
  }
854
9292
  if (id == PfRule::CNF_XOR_NEG1)
855
  {
856
157
    Assert(children.empty());
857
157
    Assert(args.size() == 1);
858
157
    if (args[0].getKind() != kind::XOR)
859
    {
860
      return Node::null();
861
    }
862
314
    std::vector<Node> disjuncts{args[0], args[0][0].notNode(), args[0][1]};
863
157
    return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
864
  }
865
9135
  if (id == PfRule::CNF_XOR_NEG2)
866
  {
867
163
    Assert(children.empty());
868
163
    Assert(args.size() == 1);
869
163
    if (args[0].getKind() != kind::XOR)
870
    {
871
      return Node::null();
872
    }
873
326
    std::vector<Node> disjuncts{args[0], args[0][0], args[0][1].notNode()};
874
163
    return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
875
  }
876
8972
  if (id == PfRule::CNF_ITE_POS1)
877
  {
878
1565
    Assert(children.empty());
879
1565
    Assert(args.size() == 1);
880
1565
    if (args[0].getKind() != kind::ITE)
881
    {
882
      return Node::null();
883
    }
884
    std::vector<Node> disjuncts{
885
3130
        args[0].notNode(), args[0][0].notNode(), args[0][1]};
886
1565
    return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
887
  }
888
7407
  if (id == PfRule::CNF_ITE_POS2)
889
  {
890
1304
    Assert(children.empty());
891
1304
    Assert(args.size() == 1);
892
1304
    if (args[0].getKind() != kind::ITE)
893
    {
894
      return Node::null();
895
    }
896
2608
    std::vector<Node> disjuncts{args[0].notNode(), args[0][0], args[0][2]};
897
1304
    return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
898
  }
899
6103
  if (id == PfRule::CNF_ITE_POS3)
900
  {
901
1604
    Assert(children.empty());
902
1604
    Assert(args.size() == 1);
903
1604
    if (args[0].getKind() != kind::ITE)
904
    {
905
      return Node::null();
906
    }
907
3208
    std::vector<Node> disjuncts{args[0].notNode(), args[0][1], args[0][2]};
908
1604
    return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
909
  }
910
4499
  if (id == PfRule::CNF_ITE_NEG1)
911
  {
912
1581
    Assert(children.empty());
913
1581
    Assert(args.size() == 1);
914
1581
    if (args[0].getKind() != kind::ITE)
915
    {
916
      return Node::null();
917
    }
918
    std::vector<Node> disjuncts{
919
3162
        args[0], args[0][0].notNode(), args[0][1].notNode()};
920
1581
    return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
921
  }
922
2918
  if (id == PfRule::CNF_ITE_NEG2)
923
  {
924
1301
    Assert(children.empty());
925
1301
    Assert(args.size() == 1);
926
1301
    if (args[0].getKind() != kind::ITE)
927
    {
928
      return Node::null();
929
    }
930
2602
    std::vector<Node> disjuncts{args[0], args[0][0], args[0][2].notNode()};
931
1301
    return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
932
  }
933
1617
  if (id == PfRule::CNF_ITE_NEG3)
934
  {
935
1617
    Assert(children.empty());
936
1617
    Assert(args.size() == 1);
937
1617
    if (args[0].getKind() != kind::ITE)
938
    {
939
      return Node::null();
940
    }
941
    std::vector<Node> disjuncts{
942
3234
        args[0], args[0][1].notNode(), args[0][2].notNode()};
943
1617
    return NodeManager::currentNM()->mkNode(kind::OR, disjuncts);
944
  }
945
  // no rule
946
  return Node::null();
947
}
948
949
}  // namespace booleans
950
}  // namespace theory
951
26685
}  // namespace CVC4