GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/booleans/proof_circuit_propagator.cpp Lines: 228 249 91.6 %
Date: 2021-03-23 Branches: 544 1098 49.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file proof_circuit_propagator.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Gereon Kremer
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 Proofs for the non-clausal circuit propagator.
13
 **
14
 ** Proofs for the non-clausal circuit propagator.
15
 **/
16
17
#include "theory/booleans/proof_circuit_propagator.h"
18
19
#include <sstream>
20
21
#include "expr/proof_node.h"
22
#include "expr/proof_node_manager.h"
23
24
namespace CVC4 {
25
namespace theory {
26
namespace booleans {
27
28
namespace {
29
30
/** Shorthand to create a Node from a constant number */
31
template <typename T>
32
24567
Node mkRat(T val)
33
{
34
24567
  return NodeManager::currentNM()->mkConst<Rational>(val);
35
}
36
37
/**
38
 * Collect all children from parent except for one particular child (the
39
 * "holdout"). The holdout is given as iterator, and should be an iterator into
40
 * the [parent.begin(),parent.end()] range.
41
 */
42
652
inline std::vector<Node> collectButHoldout(TNode parent,
43
                                           TNode::iterator holdout)
44
{
45
652
  std::vector<Node> lits;
46
2209
  for (TNode::iterator i = parent.begin(), i_end = parent.end(); i != i_end;
47
       ++i)
48
  {
49
1557
    if (i != holdout)
50
    {
51
905
      lits.emplace_back(*i);
52
    }
53
  }
54
652
  return lits;
55
}
56
57
}  // namespace
58
59
1079393
ProofCircuitPropagator::ProofCircuitPropagator(ProofNodeManager* pnm)
60
1079393
    : d_pnm(pnm)
61
{
62
1079393
}
63
64
1006860
bool ProofCircuitPropagator::disabled() const { return d_pnm == nullptr; }
65
66
7228367
std::shared_ptr<ProofNode> ProofCircuitPropagator::assume(Node n)
67
{
68
7228367
  return d_pnm->mkAssume(n);
69
}
70
71
80
std::shared_ptr<ProofNode> ProofCircuitPropagator::conflict(
72
    const std::shared_ptr<ProofNode>& a, const std::shared_ptr<ProofNode>& b)
73
{
74
80
  if (a->getResult().notNode() == b->getResult())
75
  {
76
61
    return mkProof(PfRule::CONTRA, {a, b});
77
  }
78
19
  Assert(a->getResult() == b->getResult().notNode());
79
19
  return mkProof(PfRule::CONTRA, {b, a});
80
}
81
82
812
std::shared_ptr<ProofNode> ProofCircuitPropagator::andFalse(
83
    Node parent, TNode::iterator holdout)
84
{
85
812
  if (disabled())
86
  {
87
563
    return nullptr;
88
  }
89
  return mkNot(
90
498
      mkCResolution(mkProof(PfRule::NOT_AND, {assume(parent.notNode())}),
91
498
                    collectButHoldout(parent, holdout),
92
249
                    false));
93
}
94
95
87946
std::shared_ptr<ProofNode> ProofCircuitPropagator::orTrue(
96
    Node parent, TNode::iterator holdout)
97
{
98
87946
  if (disabled())
99
  {
100
87543
    return nullptr;
101
  }
102
  return mkCResolution(
103
403
      assume(parent), collectButHoldout(parent, holdout), true);
104
}
105
106
139719
std::shared_ptr<ProofNode> ProofCircuitPropagator::Not(bool negate, Node parent)
107
{
108
139719
  if (disabled())
109
  {
110
114570
    return nullptr;
111
  }
112
25149
  return mkNot(assume(negate ? Node(parent[0]) : parent));
113
}
114
115
55
std::shared_ptr<ProofNode> ProofCircuitPropagator::impliesXFromY(Node parent)
116
{
117
55
  if (disabled())
118
  {
119
29
    return nullptr;
120
  }
121
104
  return mkNot(mkResolution(
122
78
      mkProof(PfRule::IMPLIES_ELIM, {assume(parent)}), parent[1], true));
123
}
124
125
643
std::shared_ptr<ProofNode> ProofCircuitPropagator::impliesYFromX(Node parent)
126
{
127
643
  if (disabled())
128
  {
129
449
    return nullptr;
130
  }
131
  return mkResolution(
132
194
      mkProof(PfRule::IMPLIES_ELIM, {assume(parent)}), parent[0], false);
133
}
134
135
51
std::shared_ptr<ProofNode> ProofCircuitPropagator::eqXFromY(bool y, Node parent)
136
{
137
51
  if (disabled())
138
  {
139
28
    return nullptr;
140
  }
141
23
  if (y)
142
  {
143
    return mkProof(
144
        PfRule::EQ_RESOLVE,
145
17
        {assume(parent[1]), mkProof(PfRule::SYMM, {assume(parent)})});
146
  }
147
24
  return mkNot(mkResolution(
148
18
      mkProof(PfRule::EQUIV_ELIM1, {assume(parent)}), parent[1], true));
149
}
150
151
208
std::shared_ptr<ProofNode> ProofCircuitPropagator::eqYFromX(bool x, Node parent)
152
{
153
208
  if (disabled())
154
  {
155
130
    return nullptr;
156
  }
157
78
  if (x)
158
  {
159
60
    return mkProof(PfRule::EQ_RESOLVE, {assume(parent[0]), assume(parent)});
160
  }
161
72
  return mkNot(mkResolution(
162
54
      mkProof(PfRule::EQUIV_ELIM2, {assume(parent)}), parent[0], true));
163
}
164
165
3
std::shared_ptr<ProofNode> ProofCircuitPropagator::neqXFromY(bool y,
166
                                                             Node parent)
167
{
168
3
  if (disabled())
169
  {
170
2
    return nullptr;
171
  }
172
  return mkResolution(
173
5
      mkProof(y ? PfRule::NOT_EQUIV_ELIM2 : PfRule::NOT_EQUIV_ELIM1,
174
3
              {assume(parent.notNode())}),
175
      parent[1],
176
3
      !y);
177
}
178
179
13
std::shared_ptr<ProofNode> ProofCircuitPropagator::neqYFromX(bool x,
180
                                                             Node parent)
181
{
182
13
  if (disabled())
183
  {
184
9
    return nullptr;
185
  }
186
  return mkResolution(
187
20
      mkProof(x ? PfRule::NOT_EQUIV_ELIM2 : PfRule::NOT_EQUIV_ELIM1,
188
12
              {assume(parent.notNode())}),
189
      parent[0],
190
12
      !x);
191
}
192
193
24
std::shared_ptr<ProofNode> ProofCircuitPropagator::xorXFromY(bool negated,
194
                                                             bool y,
195
                                                             Node parent)
196
{
197
24
  if (disabled())
198
  {
199
16
    return nullptr;
200
  }
201
8
  if (y)
202
  {
203
32
    return mkNot(mkResolution(
204
40
        mkProof(negated ? PfRule::NOT_XOR_ELIM1 : PfRule::XOR_ELIM2,
205
24
                {assume(negated ? parent.notNode() : Node(parent))}),
206
        parent[1],
207
8
        false));
208
  }
209
  return mkResolution(
210
      mkProof(negated ? PfRule::NOT_XOR_ELIM2 : PfRule::XOR_ELIM1,
211
              {assume(negated ? parent.notNode() : Node(parent))}),
212
      parent[1],
213
      true);
214
}
215
216
25
std::shared_ptr<ProofNode> ProofCircuitPropagator::xorYFromX(bool negated,
217
                                                             bool x,
218
                                                             Node parent)
219
{
220
25
  if (disabled())
221
  {
222
16
    return nullptr;
223
  }
224
9
  if (x)
225
  {
226
    return mkResolution(
227
20
        mkProof(negated ? PfRule::NOT_XOR_ELIM2 : PfRule::XOR_ELIM2,
228
12
                {assume(negated ? parent.notNode() : Node(parent))}),
229
        parent[0],
230
12
        false);
231
  }
232
  return mkNot(
233
25
      mkResolution(mkProof(negated ? PfRule::NOT_XOR_ELIM1 : PfRule::XOR_ELIM1,
234
15
                           {assume(negated ? parent.notNode() : Node(parent))}),
235
                   parent[0],
236
5
                   true));
237
}
238
239
38658
std::shared_ptr<ProofNode> ProofCircuitPropagator::mkProof(
240
    PfRule rule,
241
    const std::vector<std::shared_ptr<ProofNode>>& children,
242
    const std::vector<Node>& args)
243
{
244
38658
  if (Trace.isOn("circuit-prop"))
245
  {
246
    std::stringstream ss;
247
    ss << "Constructing (" << rule;
248
    for (const auto& c : children)
249
    {
250
      ss << " " << *c;
251
    }
252
    if (!args.empty())
253
    {
254
      ss << " :args";
255
      for (const auto& a : args)
256
      {
257
        ss << " " << a;
258
      }
259
    }
260
    ss << ")";
261
    Trace("circuit-prop") << ss.str() << std::endl;
262
  }
263
38658
  return d_pnm->mkNode(rule, children, args);
264
}
265
266
2407
std::shared_ptr<ProofNode> ProofCircuitPropagator::mkCResolution(
267
    const std::shared_ptr<ProofNode>& clause,
268
    const std::vector<Node>& lits,
269
    const std::vector<bool>& polarity)
270
{
271
2407
  auto* nm = NodeManager::currentNM();
272
4814
  std::vector<std::shared_ptr<ProofNode>> children = {clause};
273
4814
  std::vector<Node> args;
274
2407
  Assert(lits.size() == polarity.size());
275
194695
  for (std::size_t i = 0, n = lits.size(); i < n; ++i)
276
  {
277
192288
    bool pol = polarity[i];
278
384576
    Node lit = lits[i];
279
192288
    if (polarity[i])
280
    {
281
191352
      if (lit.getKind() == Kind::NOT)
282
      {
283
173612
        lit = lit[0];
284
173612
        pol = !pol;
285
173612
        children.emplace_back(assume(lit));
286
      }
287
      else
288
      {
289
17740
        children.emplace_back(assume(lit.notNode()));
290
      }
291
    }
292
    else
293
    {
294
936
      children.emplace_back(assume(lit));
295
    }
296
192288
    args.emplace_back(nm->mkConst(pol));
297
192288
    args.emplace_back(lit);
298
  }
299
4814
  return mkProof(PfRule::CHAIN_RESOLUTION, children, args);
300
}
301
302
1881
std::shared_ptr<ProofNode> ProofCircuitPropagator::mkCResolution(
303
    const std::shared_ptr<ProofNode>& clause,
304
    const std::vector<Node>& lits,
305
    bool polarity)
306
{
307
1881
  return mkCResolution(clause, lits, std::vector<bool>(lits.size(), polarity));
308
}
309
310
2998
std::shared_ptr<ProofNode> ProofCircuitPropagator::mkResolution(
311
    const std::shared_ptr<ProofNode>& clause, const Node& lit, bool polarity)
312
{
313
2998
  auto* nm = NodeManager::currentNM();
314
2998
  if (polarity)
315
  {
316
1295
    if (lit.getKind() == Kind::NOT)
317
    {
318
      return mkProof(PfRule::RESOLUTION,
319
                     {clause, assume(lit[0])},
320
313
                     {nm->mkConst(false), lit[0]});
321
    }
322
    return mkProof(PfRule::RESOLUTION,
323
1964
                   {clause, assume(lit.notNode())},
324
2946
                   {nm->mkConst(true), lit});
325
  }
326
  return mkProof(
327
1703
      PfRule::RESOLUTION, {clause, assume(lit)}, {nm->mkConst(false), lit});
328
}
329
330
28361
std::shared_ptr<ProofNode> ProofCircuitPropagator::mkNot(
331
    const std::shared_ptr<ProofNode>& n)
332
{
333
56722
  Node m = n->getResult();
334
28361
  if (m.getKind() == Kind::NOT && m[0].getKind() == Kind::NOT)
335
  {
336
815
    return mkProof(PfRule::NOT_NOT_ELIM, {n});
337
  }
338
27546
  return n;
339
}
340
341
553895
ProofCircuitPropagatorBackward::ProofCircuitPropagatorBackward(
342
553895
    ProofNodeManager* pnm, TNode parent, bool parentAssignment)
343
    : ProofCircuitPropagator(pnm),
344
      d_parent(parent),
345
553895
      d_parentAssignment(parentAssignment)
346
{
347
553895
}
348
349
501175
std::shared_ptr<ProofNode> ProofCircuitPropagatorBackward::andTrue(
350
    TNode::iterator i)
351
{
352
501175
  if (disabled())
353
  {
354
480347
    return nullptr;
355
  }
356
  return mkProof(
357
20828
      PfRule::AND_ELIM, {assume(d_parent)}, {mkRat(i - d_parent.begin())});
358
}
359
360
4787
std::shared_ptr<ProofNode> ProofCircuitPropagatorBackward::orFalse(
361
    TNode::iterator i)
362
{
363
4787
  if (disabled())
364
  {
365
3546
    return nullptr;
366
  }
367
7446
  return mkNot(mkProof(PfRule::NOT_OR_ELIM,
368
2482
                       {assume(d_parent.notNode())},
369
4964
                       {mkRat(i - d_parent.begin())}));
370
}
371
372
14
std::shared_ptr<ProofNode> ProofCircuitPropagatorBackward::iteC(bool c)
373
{
374
14
  if (disabled())
375
  {
376
8
    return nullptr;
377
  }
378
6
  if (d_parentAssignment)
379
  {
380
    return mkResolution(
381
8
        mkProof(c ? PfRule::ITE_ELIM1 : PfRule::ITE_ELIM2, {assume(d_parent)}),
382
        d_parent[0],
383
12
        !c);
384
  }
385
10
  return mkResolution(mkProof(c ? PfRule::NOT_ITE_ELIM1 : PfRule::NOT_ITE_ELIM2,
386
6
                              {assume(d_parent.notNode())}),
387
                      d_parent[0],
388
6
                      !c);
389
}
390
391
std::shared_ptr<ProofNode> ProofCircuitPropagatorBackward::iteIsCase(unsigned c)
392
{
393
  if (disabled())
394
  {
395
    return nullptr;
396
  }
397
  if (d_parentAssignment)
398
  {
399
    return mkResolution(
400
        mkProof(PfRule::ITE_ELIM2, {assume(d_parent)}), d_parent[c + 1], false);
401
  }
402
  return mkResolution(
403
      mkProof(PfRule::NOT_ITE_ELIM2, {assume(d_parent.notNode())}),
404
      d_parent[c + 1],
405
      false);
406
}
407
408
570
std::shared_ptr<ProofNode> ProofCircuitPropagatorBackward::impliesNegX()
409
{
410
570
  if (disabled())
411
  {
412
385
    return nullptr;
413
  }
414
  return mkNot(
415
185
      mkProof(PfRule::NOT_IMPLIES_ELIM1, {assume(d_parent.notNode())}));
416
}
417
418
570
std::shared_ptr<ProofNode> ProofCircuitPropagatorBackward::impliesNegY()
419
{
420
570
  if (disabled())
421
  {
422
385
    return nullptr;
423
  }
424
  return mkNot(
425
185
      mkProof(PfRule::NOT_IMPLIES_ELIM2, {assume(d_parent.notNode())}));
426
}
427
428
525276
ProofCircuitPropagatorForward::ProofCircuitPropagatorForward(
429
525276
    ProofNodeManager* pnm, Node child, bool childAssignment, Node parent)
430
    : ProofCircuitPropagator{pnm},
431
      d_child(child),
432
      d_childAssignment(childAssignment),
433
525276
      d_parent(parent)
434
{
435
525276
}
436
437
15760
std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::andAllTrue()
438
{
439
15760
  if (disabled())
440
  {
441
10937
    return nullptr;
442
  }
443
9646
  std::vector<std::shared_ptr<ProofNode>> children;
444
6988111
  for (const auto& child : d_parent)
445
  {
446
6983288
    children.emplace_back(assume(child));
447
  }
448
4823
  return mkProof(PfRule::AND_INTRO, children);
449
}
450
451
4099
std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::andOneFalse()
452
{
453
4099
  if (disabled())
454
  {
455
2890
    return nullptr;
456
  }
457
1209
  auto it = std::find(d_parent.begin(), d_parent.end(), d_child);
458
  return mkResolution(
459
4836
      mkProof(
460
2418
          PfRule::CNF_AND_POS, {}, {d_parent, mkRat(it - d_parent.begin())}),
461
      d_child,
462
2418
      true);
463
}
464
465
243362
std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::orOneTrue()
466
{
467
243362
  if (disabled())
468
  {
469
242073
    return nullptr;
470
  }
471
1289
  auto it = std::find(d_parent.begin(), d_parent.end(), d_child);
472
3867
  return mkNot(mkResolution(
473
2578
      mkProof(PfRule::CNF_OR_NEG, {}, {d_parent, mkRat(it - d_parent.begin())}),
474
      d_child,
475
2578
      false));
476
}
477
478
4717
std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::orFalse()
479
{
480
4717
  if (disabled())
481
  {
482
3488
    return nullptr;
483
  }
484
2458
  std::vector<Node> children(d_parent.begin(), d_parent.end());
485
  return mkCResolution(
486
1229
      mkProof(PfRule::CNF_OR_POS, {}, {d_parent}), children, true);
487
}
488
489
17
std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::iteEvalThen(bool x)
490
{
491
17
  if (disabled())
492
  {
493
10
    return nullptr;
494
  }
495
  return mkCResolution(
496
14
      mkProof(x ? PfRule::CNF_ITE_NEG1 : PfRule::CNF_ITE_POS1, {}, {d_parent}),
497
      {d_parent[0], d_parent[1]},
498
21
      {false, !x});
499
}
500
501
11
std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::iteEvalElse(bool y)
502
{
503
11
  if (disabled())
504
  {
505
7
    return nullptr;
506
  }
507
  return mkCResolution(
508
8
      mkProof(y ? PfRule::CNF_ITE_NEG2 : PfRule::CNF_ITE_POS2, {}, {d_parent}),
509
      {d_parent[0], d_parent[2]},
510
12
      {true, !y});
511
}
512
513
390
std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::eqEval(bool x, bool y)
514
{
515
390
  if (disabled())
516
  {
517
242
    return nullptr;
518
  }
519
148
  if (x == y)
520
  {
521
    return mkCResolution(
522
417
        mkProof(x ? PfRule::CNF_EQUIV_NEG2 : PfRule::CNF_EQUIV_NEG1,
523
                {},
524
139
                {d_parent}),
525
        {d_parent[0], d_parent[1]},
526
417
        {!x, !y});
527
  }
528
  return mkCResolution(
529
27
      mkProof(
530
9
          x ? PfRule::CNF_EQUIV_POS1 : PfRule::CNF_EQUIV_POS2, {}, {d_parent}),
531
      {d_parent[0], d_parent[1]},
532
27
      {!x, !y});
533
}
534
535
1852
std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::impliesEval(
536
    bool premise, bool conclusion)
537
{
538
1852
  if (disabled())
539
  {
540
1270
    return nullptr;
541
  }
542
582
  if (!premise)
543
  {
544
    return mkResolution(
545
30
        mkProof(PfRule::CNF_IMPLIES_NEG1, {}, {d_parent}), d_parent[0], true);
546
  }
547
552
  if (conclusion)
548
  {
549
    return mkResolution(
550
198
        mkProof(PfRule::CNF_IMPLIES_NEG2, {}, {d_parent}), d_parent[1], false);
551
  }
552
708
  return mkCResolution(mkProof(PfRule::CNF_IMPLIES_POS, {}, {d_parent}),
553
                       {d_parent[0], d_parent[1]},
554
1062
                       {false, true});
555
}
556
557
37
std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::xorEval(bool x,
558
                                                                  bool y)
559
{
560
37
  if (disabled())
561
  {
562
24
    return nullptr;
563
  }
564
13
  if (x && y)
565
  {
566
8
    return mkCResolution(mkProof(PfRule::CNF_XOR_POS2, {}, {d_parent}),
567
                         {d_parent[0], d_parent[1]},
568
12
                         {false, false});
569
  }
570
9
  else if (x && !y)
571
  {
572
2
    return mkCResolution(mkProof(PfRule::CNF_XOR_NEG1, {}, {d_parent}),
573
                         {d_parent[0], d_parent[1]},
574
3
                         {false, true});
575
  }
576
8
  else if (!x && y)
577
  {
578
12
    return mkCResolution(mkProof(PfRule::CNF_XOR_NEG2, {}, {d_parent}),
579
                         {d_parent[0], d_parent[1]},
580
18
                         {true, false});
581
  }
582
2
  Assert(!x && !y);
583
4
  return mkCResolution(mkProof(PfRule::CNF_XOR_POS1, {}, {d_parent}),
584
                       {d_parent[0], d_parent[1]},
585
6
                       {true, true});
586
}
587
588
}  // namespace booleans
589
}  // namespace theory
590
26685
}  // namespace CVC4