GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/booleans/circuit_propagator.cpp Lines: 346 372 93.0 %
Date: 2021-03-22 Branches: 854 1756 48.6 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file circuit_propagator.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Gereon Kremer, Morgan Deters, Dejan Jovanovic
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 A non-clausal circuit propagator for Boolean simplification
13
 **
14
 ** A non-clausal circuit propagator for Boolean simplification.
15
 **/
16
17
#include "theory/booleans/circuit_propagator.h"
18
19
#include <algorithm>
20
#include <stack>
21
#include <vector>
22
23
#include "expr/node_algorithm.h"
24
#include "expr/proof_node.h"
25
#include "expr/proof_node_manager.h"
26
#include "theory/booleans/proof_circuit_propagator.h"
27
#include "theory/eager_proof_generator.h"
28
#include "theory/theory.h"
29
#include "util/hash.h"
30
#include "util/utility.h"
31
32
using namespace std;
33
34
namespace CVC4 {
35
namespace theory {
36
namespace booleans {
37
38
9619
CircuitPropagator::CircuitPropagator(bool enableForward, bool enableBackward)
39
    : d_context(),
40
      d_propagationQueue(),
41
      d_propagationQueueClearer(&d_context, d_propagationQueue),
42
19238
      d_conflict(&d_context, TrustNode()),
43
      d_learnedLiterals(),
44
      d_learnedLiteralClearer(&d_context, d_learnedLiterals),
45
      d_backEdges(),
46
      d_backEdgesClearer(&d_context, d_backEdges),
47
      d_seen(&d_context),
48
      d_state(&d_context),
49
      d_forwardPropagation(enableForward),
50
      d_backwardPropagation(enableBackward),
51
      d_needsFinish(false),
52
      d_pnm(nullptr),
53
      d_epg(nullptr),
54
      d_proofInternal(nullptr),
55
28857
      d_proofExternal(nullptr)
56
{
57
9619
}
58
59
10353
void CircuitPropagator::finish()
60
{
61
10353
  Trace("circuit-prop") << "FINISH" << std::endl;
62
10353
  d_context.pop();
63
10353
}
64
65
562543
void CircuitPropagator::assertTrue(TNode assertion)
66
{
67
562543
  Trace("circuit-prop") << "TRUE: " << assertion << std::endl;
68
562543
  if (assertion.getKind() == kind::CONST_BOOLEAN && !assertion.getConst<bool>())
69
  {
70
579
    makeConflict(assertion);
71
  }
72
561964
  else if (assertion.getKind() == kind::AND)
73
  {
74
6714
    ProofCircuitPropagatorBackward prover{d_pnm, assertion, true};
75
3357
    if (isProofEnabled())
76
    {
77
825
      addProof(assertion, prover.assume(assertion));
78
    }
79
486906
    for (auto it = assertion.begin(); it != assertion.end(); ++it)
80
    {
81
483549
      addProof(*it, prover.andTrue(it));
82
483549
      assertTrue(*it);
83
    }
84
  }
85
  else
86
  {
87
    // Analyze the assertion for back-edges and all that
88
558607
    computeBackEdges(assertion);
89
    // Assign the given assertion to true
90
558607
    if (isProofEnabled())
91
    {
92
30344
      assignAndEnqueue(assertion, true, d_pnm->mkAssume(assertion));
93
    }
94
    else
95
    {
96
528263
      assignAndEnqueue(assertion, true, nullptr);
97
    }
98
  }
99
562543
}
100
101
1081918
void CircuitPropagator::assignAndEnqueue(TNode n,
102
                                         bool value,
103
                                         std::shared_ptr<ProofNode> proof)
104
{
105
2163836
  Trace("circuit-prop") << "CircuitPropagator::assign(" << n << ", "
106
1081918
                        << (value ? "true" : "false") << ")" << std::endl;
107
108
1081918
  if (n.getKind() == kind::CONST_BOOLEAN)
109
  {
110
    // Assigning a constant to the opposite value is dumb
111
11375
    if (value != n.getConst<bool>())
112
    {
113
      makeConflict(n);
114
      return;
115
    }
116
  }
117
118
1081918
  if (isProofEnabled())
119
  {
120
72591
    if (proof == nullptr)
121
    {
122
      Warning() << "CircuitPropagator: Proof is missing for " << n << std::endl;
123
      Assert(false);
124
    }
125
    else
126
    {
127
72591
      Assert(!proof->getResult().isNull());
128
145182
      Node expected = value ? Node(n) : n.negate();
129
72591
      if (proof->getResult() != expected)
130
      {
131
        Warning() << "CircuitPropagator: Incorrect proof: " << expected
132
                  << " vs. " << proof->getResult() << std::endl
133
                  << *proof << std::endl;
134
      }
135
72591
      addProof(expected, std::move(proof));
136
    }
137
  }
138
139
  // Get the current assignment
140
1081918
  AssignmentStatus state = d_state[n];
141
142
1081918
  if (state != UNASSIGNED)
143
  {
144
    // If the node is already assigned we might have a conflict
145
406560
    if (value != (state == ASSIGNED_TO_TRUE))
146
    {
147
270
      makeConflict(n);
148
    }
149
  }
150
  else
151
  {
152
    // If unassigned, mark it as assigned
153
675358
    d_state[n] = value ? ASSIGNED_TO_TRUE : ASSIGNED_TO_FALSE;
154
    // Add for further propagation
155
675358
    d_propagationQueue.push_back(n);
156
  }
157
}
158
159
849
void CircuitPropagator::makeConflict(Node n)
160
{
161
1667
  auto bfalse = NodeManager::currentNM()->mkConst(false);
162
849
  ProofGenerator* g = nullptr;
163
849
  if (isProofEnabled())
164
  {
165
253
    if (d_epg->hasProofFor(bfalse))
166
    {
167
31
      return;
168
    }
169
222
    ProofCircuitPropagator pcp(d_pnm);
170
222
    if (n == bfalse)
171
    {
172
142
      d_epg->setProofFor(bfalse, pcp.assume(bfalse));
173
    }
174
    else
175
    {
176
160
      d_epg->setProofFor(bfalse,
177
160
                         pcp.conflict(pcp.assume(n), pcp.assume(n.negate())));
178
    }
179
222
    g = d_proofInternal.get();
180
444
    Trace("circuit-prop") << "Added conflict " << *d_epg->getProofFor(bfalse)
181
222
                          << std::endl;
182
444
    Trace("circuit-prop") << "\texpanded " << *g->getProofFor(bfalse)
183
222
                          << std::endl;
184
  }
185
818
  d_conflict = TrustNode::mkTrustLemma(bfalse, g);
186
}
187
188
558607
void CircuitPropagator::computeBackEdges(TNode node)
189
{
190
1117214
  Debug("circuit-prop") << "CircuitPropagator::computeBackEdges(" << node << ")"
191
558607
                        << endl;
192
193
  // Vector of nodes to visit
194
1117214
  vector<TNode> toVisit;
195
196
  // Start with the top node
197
558607
  if (d_seen.find(node) == d_seen.end())
198
  {
199
544163
    toVisit.push_back(node);
200
544163
    d_seen.insert(node);
201
  }
202
203
  // Initialize the back-edges for the root, so we don't have a special case
204
558607
  d_backEdges[node];
205
206
  // Go through the visit list
207
1556459
  for (unsigned i = 0; i < toVisit.size(); ++i)
208
  {
209
    // Node we need to visit
210
1995704
    TNode current = toVisit[i];
211
1995704
    Debug("circuit-prop")
212
997852
        << "CircuitPropagator::computeBackEdges(): processing " << current
213
997852
        << endl;
214
997852
    Assert(d_seen.find(current) != d_seen.end());
215
216
    // If this not an atom visit all the children and compute the back edges
217
997852
    if (Theory::theoryOf(current) == THEORY_BOOL)
218
    {
219
2631314
      for (unsigned child = 0, child_end = current.getNumChildren();
220
2631314
           child < child_end;
221
           ++child)
222
      {
223
3555124
        TNode childNode = current[child];
224
        // Add the back edge
225
1777562
        d_backEdges[childNode].push_back(current);
226
        // Add to the queue if not seen yet
227
1777562
        if (d_seen.find(childNode) == d_seen.end())
228
        {
229
453689
          toVisit.push_back(childNode);
230
453689
          d_seen.insert(childNode);
231
        }
232
      }
233
    }
234
  }
235
558607
}
236
237
550538
void CircuitPropagator::propagateBackward(TNode parent, bool parentAssignment)
238
{
239
1101076
  Debug("circuit-prop") << "CircuitPropagator::propagateBackward(" << parent
240
550538
                        << ", " << parentAssignment << ")" << endl;
241
1101076
  ProofCircuitPropagatorBackward prover{d_pnm, parent, parentAssignment};
242
243
  // backward rules
244
550538
  switch (parent.getKind())
245
  {
246
5733
    case kind::AND:
247
5733
      if (parentAssignment)
248
      {
249
        // AND = TRUE: forall children c, assign(c = TRUE)
250
18508
        for (TNode::iterator i = parent.begin(), i_end = parent.end();
251
18508
             i != i_end;
252
             ++i)
253
        {
254
17626
          assignAndEnqueue(*i, true, prover.andTrue(i));
255
        }
256
      }
257
      else
258
      {
259
        // AND = FALSE: if all children BUT ONE == TRUE, assign(c = FALSE)
260
        TNode::iterator holdout =
261
10285
            find_if_unique(parent.begin(), parent.end(), [this](TNode x) {
262
20570
              return !isAssignedTo(x, true);
263
25421
            });
264
4851
        if (holdout != parent.end())
265
        {
266
400
          assignAndEnqueue(*holdout, false, prover.andFalse(parent, holdout));
267
        }
268
      }
269
5733
      break;
270
470615
    case kind::OR:
271
470615
      if (parentAssignment)
272
      {
273
        // OR = TRUE: if all children BUT ONE == FALSE, assign(c = TRUE)
274
        TNode::iterator holdout =
275
939839
            find_if_unique(parent.begin(), parent.end(), [this](TNode x) {
276
1879678
              return !isAssignedTo(x, false);
277
2349149
            });
278
469471
        if (holdout != parent.end())
279
        {
280
505
          assignAndEnqueue(*holdout, true, prover.orTrue(parent, holdout));
281
        }
282
      }
283
      else
284
      {
285
        // OR = FALSE: forall children c, assign(c = FALSE)
286
5931
        for (TNode::iterator i = parent.begin(), i_end = parent.end();
287
5931
             i != i_end;
288
             ++i)
289
        {
290
4787
          assignAndEnqueue(*i, false, prover.orFalse(i));
291
        }
292
      }
293
470615
      break;
294
69898
    case kind::NOT:
295
      // NOT = b: assign(c = !b)
296
69898
      assignAndEnqueue(
297
139796
          parent[0], !parentAssignment, prover.Not(!parentAssignment, parent));
298
69898
      break;
299
329
    case kind::ITE:
300
329
      if (isAssignedTo(parent[0], true))
301
      {
302
        // ITE c x y = v: if c is assigned and TRUE, assign(x = v)
303
11
        assignAndEnqueue(parent[1], parentAssignment, prover.iteC(true));
304
      }
305
318
      else if (isAssignedTo(parent[0], false))
306
      {
307
        // ITE c x y = v: if c is assigned and FALSE, assign(y = v)
308
3
        assignAndEnqueue(parent[2], parentAssignment, prover.iteC(false));
309
      }
310
315
      else if (isAssigned(parent[1]) && isAssigned(parent[2]))
311
      {
312
        if (getAssignment(parent[1]) == parentAssignment
313
            && getAssignment(parent[2]) != parentAssignment)
314
        {
315
          // ITE c x y = v: if c is unassigned, x and y are assigned, x==v and
316
          // y!=v, assign(c = TRUE)
317
          assignAndEnqueue(parent[0], true, prover.iteIsCase(1));
318
        }
319
        else if (getAssignment(parent[1]) != parentAssignment
320
                 && getAssignment(parent[2]) == parentAssignment)
321
        {
322
          // ITE c x y = v: if c is unassigned, x and y are assigned, x!=v and
323
          // y==v, assign(c = FALSE)
324
          assignAndEnqueue(parent[0], false, prover.iteIsCase(0));
325
        }
326
      }
327
329
      break;
328
1229
    case kind::EQUAL:
329
1229
      Assert(parent[0].getType().isBoolean());
330
1229
      if (parentAssignment)
331
      {
332
        // IFF x y = TRUE: if x [resp y] is assigned, assign(y = x.assignment
333
        // [resp x = y.assignment])
334
656
        if (isAssigned(parent[0]))
335
        {
336
122
          assignAndEnqueue(parent[1],
337
244
                           getAssignment(parent[0]),
338
244
                           prover.eqYFromX(getAssignment(parent[0]), parent));
339
        }
340
534
        else if (isAssigned(parent[1]))
341
        {
342
9
          assignAndEnqueue(parent[0],
343
18
                           getAssignment(parent[1]),
344
18
                           prover.eqXFromY(getAssignment(parent[1]), parent));
345
        }
346
      }
347
      else
348
      {
349
        // IFF x y = FALSE: if x [resp y] is assigned, assign(y = !x.assignment
350
        // [resp x = !y.assignment])
351
573
        if (isAssigned(parent[0]))
352
        {
353
11
          assignAndEnqueue(parent[1],
354
22
                           !getAssignment(parent[0]),
355
22
                           prover.neqYFromX(getAssignment(parent[0]), parent));
356
        }
357
562
        else if (isAssigned(parent[1]))
358
        {
359
3
          assignAndEnqueue(parent[0],
360
6
                           !getAssignment(parent[1]),
361
6
                           prover.neqXFromY(getAssignment(parent[1]), parent));
362
        }
363
      }
364
1229
      break;
365
2625
    case kind::IMPLIES:
366
2625
      if (parentAssignment)
367
      {
368
2055
        if (isAssignedTo(parent[0], true))
369
        {
370
          // IMPLIES x y = TRUE, and x == TRUE: assign(y = TRUE)
371
565
          assignAndEnqueue(parent[1], true, prover.impliesYFromX(parent));
372
        }
373
2055
        if (isAssignedTo(parent[1], false))
374
        {
375
          // IMPLIES x y = TRUE, and y == FALSE: assign(x = FALSE)
376
50
          assignAndEnqueue(parent[0], false, prover.impliesXFromY(parent));
377
        }
378
      }
379
      else
380
      {
381
        // IMPLIES x y = FALSE: assign(x = TRUE) and assign(y = FALSE)
382
570
        assignAndEnqueue(parent[0], true, prover.impliesNegX());
383
570
        assignAndEnqueue(parent[1], false, prover.impliesNegY());
384
      }
385
2625
      break;
386
109
    case kind::XOR:
387
109
      if (parentAssignment)
388
      {
389
98
        if (isAssigned(parent[0]))
390
        {
391
          // XOR x y = TRUE, and x assigned, assign(y = !assignment(x))
392
          assignAndEnqueue(
393
              parent[1],
394
              !getAssignment(parent[0]),
395
              prover.xorYFromX(
396
                  !parentAssignment, getAssignment(parent[0]), parent));
397
        }
398
98
        else if (isAssigned(parent[1]))
399
        {
400
          // XOR x y = TRUE, and y assigned, assign(x = !assignment(y))
401
6
          assignAndEnqueue(
402
              parent[0],
403
12
              !getAssignment(parent[1]),
404
30
              prover.xorXFromY(
405
18
                  !parentAssignment, getAssignment(parent[1]), parent));
406
        }
407
      }
408
      else
409
      {
410
11
        if (isAssigned(parent[0]))
411
        {
412
          // XOR x y = FALSE, and x assigned, assign(y = assignment(x))
413
5
          assignAndEnqueue(
414
              parent[1],
415
10
              getAssignment(parent[0]),
416
25
              prover.xorYFromX(
417
15
                  !parentAssignment, getAssignment(parent[0]), parent));
418
        }
419
6
        else if (isAssigned(parent[1]))
420
        {
421
          // XOR x y = FALSE, and y assigned, assign(x = assignment(y))
422
3
          assignAndEnqueue(
423
              parent[0],
424
6
              getAssignment(parent[1]),
425
15
              prover.xorXFromY(
426
9
                  !parentAssignment, getAssignment(parent[1]), parent));
427
        }
428
      }
429
109
      break;
430
    default: Unhandled();
431
  }
432
550538
}
433
434
672474
void CircuitPropagator::propagateForward(TNode child, bool childAssignment)
435
{
436
  // The assignment we have
437
1344948
  Debug("circuit-prop") << "CircuitPropagator::propagateForward(" << child
438
672474
                        << ", " << childAssignment << ")" << endl;
439
440
  // Get the back any nodes where this is child
441
672474
  const vector<Node>& parents = d_backEdges.find(child)->second;
442
443
  // Go through the parents and see if there is anything to propagate
444
672474
  vector<Node>::const_iterator parent_it = parents.begin();
445
672474
  vector<Node>::const_iterator parent_it_end = parents.end();
446
1723026
  for (; parent_it != parent_it_end && d_conflict.get().isNull(); ++parent_it)
447
  {
448
    // The current parent of the child
449
1050552
    TNode parent = *parent_it;
450
525276
    Debug("circuit-prop") << "Parent: " << parent << endl;
451
525276
    Assert(expr::hasSubterm(parent, child));
452
453
1050552
    ProofCircuitPropagatorForward prover{d_pnm, child, childAssignment, parent};
454
455
    // Forward rules
456
525276
    switch (parent.getKind())
457
    {
458
27303
      case kind::AND:
459
27303
        if (childAssignment)
460
        {
461
23204
          TNode::iterator holdout;
462
17682046
          holdout = find_if(parent.begin(), parent.end(), [this](TNode x) {
463
35317684
            return !isAssignedTo(x, true);
464
35340888
          });
465
466
23204
          if (holdout == parent.end())
467
          {  // all children are assigned TRUE
468
            // AND ...(x=TRUE)...: if all children now assigned to TRUE,
469
            // assign(AND = TRUE)
470
15760
            assignAndEnqueue(parent, true, prover.andAllTrue());
471
          }
472
7444
          else if (isAssignedTo(parent, false))
473
          {  // the AND is FALSE
474
            // is the holdout unique ?
475
            TNode::iterator other =
476
1268
                find_if(holdout + 1, parent.end(), [this](TNode x) {
477
2536
                  return !isAssignedTo(x, true);
478
3665
                });
479
1129
            if (other == parent.end())
480
            {  // the holdout is unique
481
              // AND ...(x=TRUE)...: if all children BUT ONE now assigned to
482
              // TRUE, and AND == FALSE, assign(last_holdout = FALSE)
483
412
              assignAndEnqueue(
484
824
                  *holdout, false, prover.andFalse(parent, holdout));
485
            }
486
          }
487
        }
488
        else
489
        {
490
          // AND ...(x=FALSE)...: assign(AND = FALSE)
491
4099
          assignAndEnqueue(parent, false, prover.andOneFalse());
492
        }
493
27303
        break;
494
422596
      case kind::OR:
495
422596
        if (childAssignment)
496
        {
497
          // OR ...(x=TRUE)...: assign(OR = TRUE)
498
243362
          assignAndEnqueue(parent, true, prover.orOneTrue());
499
        }
500
        else
501
        {
502
179234
          TNode::iterator holdout;
503
941860
          holdout = find_if(parent.begin(), parent.end(), [this](TNode x) {
504
1525252
            return !isAssignedTo(x, false);
505
1704486
          });
506
179234
          if (holdout == parent.end())
507
          {  // all children are assigned FALSE
508
            // OR ...(x=FALSE)...: if all children now assigned to FALSE,
509
            // assign(OR = FALSE)
510
4717
            assignAndEnqueue(parent, false, prover.orFalse());
511
          }
512
174517
          else if (isAssignedTo(parent, true))
513
          {  // the OR is TRUE
514
            // is the holdout unique ?
515
            TNode::iterator other =
516
207598
                find_if(holdout + 1, parent.end(), [this](TNode x) {
517
415196
                  return !isAssignedTo(x, false);
518
586207
                });
519
171011
            if (other == parent.end())
520
            {  // the holdout is unique
521
              // OR ...(x=FALSE)...: if all children BUT ONE now assigned to
522
              // FALSE, and OR == TRUE, assign(last_holdout = TRUE)
523
87441
              assignAndEnqueue(*holdout, true, prover.orTrue(parent, holdout));
524
            }
525
          }
526
        }
527
422596
        break;
528
529
69821
      case kind::NOT:
530
        // NOT (x=b): assign(NOT = !b)
531
69821
        assignAndEnqueue(
532
139642
            parent, !childAssignment, prover.Not(childAssignment, parent));
533
69821
        break;
534
535
62
      case kind::ITE:
536
62
        if (child == parent[0])
537
        {
538
32
          if (childAssignment)
539
          {
540
23
            if (isAssigned(parent[1]))
541
            {
542
              // ITE (c=TRUE) x y: if x is assigned, assign(ITE = x.assignment)
543
3
              assignAndEnqueue(parent,
544
6
                               getAssignment(parent[1]),
545
6
                               prover.iteEvalThen(getAssignment(parent[1])));
546
            }
547
          }
548
          else
549
          {
550
9
            if (isAssigned(parent[2]))
551
            {
552
              // ITE (c=FALSE) x y: if y is assigned, assign(ITE = y.assignment)
553
5
              assignAndEnqueue(parent,
554
10
                               getAssignment(parent[2]),
555
10
                               prover.iteEvalElse(getAssignment(parent[2])));
556
            }
557
          }
558
        }
559
62
        if (child == parent[1])
560
        {
561
20
          if (isAssignedTo(parent[0], true))
562
          {
563
            // ITE c (x=v) y: if c is assigned and TRUE, assign(ITE = v)
564
14
            assignAndEnqueue(
565
28
                parent, childAssignment, prover.iteEvalThen(childAssignment));
566
          }
567
        }
568
62
        if (child == parent[2])
569
        {
570
10
          Assert(child == parent[2]);
571
10
          if (isAssignedTo(parent[0], false))
572
          {
573
            // ITE c x (y=v): if c is assigned and FALSE, assign(ITE = v)
574
6
            assignAndEnqueue(
575
12
                parent, childAssignment, prover.iteEvalElse(childAssignment));
576
          }
577
        }
578
62
        break;
579
678
      case kind::EQUAL:
580
678
        Assert(parent[0].getType().isBoolean());
581
678
        if (isAssigned(parent[0]) && isAssigned(parent[1]))
582
        {
583
          // IFF x y: if x and y is assigned, assign(IFF = (x.assignment <=>
584
          // y.assignment))
585
390
          assignAndEnqueue(parent,
586
780
                           getAssignment(parent[0]) == getAssignment(parent[1]),
587
780
                           prover.eqEval(getAssignment(parent[0]),
588
780
                                         getAssignment(parent[1])));
589
        }
590
        else
591
        {
592
288
          if (isAssigned(parent))
593
          {
594
130
            if (child == parent[0])
595
            {
596
88
              if (getAssignment(parent))
597
              {
598
                // IFF (x = b) y: if IFF is assigned to TRUE, assign(y = b)
599
86
                assignAndEnqueue(parent[1],
600
                                 childAssignment,
601
172
                                 prover.eqYFromX(childAssignment, parent));
602
              }
603
              else
604
              {
605
                // IFF (x = b) y: if IFF is assigned to FALSE, assign(y = !b)
606
2
                assignAndEnqueue(parent[1],
607
2
                                 !childAssignment,
608
4
                                 prover.neqYFromX(childAssignment, parent));
609
              }
610
            }
611
            else
612
            {
613
42
              Assert(child == parent[1]);
614
42
              if (getAssignment(parent))
615
              {
616
                // IFF x y = b: if IFF is assigned to TRUE, assign(x = b)
617
42
                assignAndEnqueue(parent[0],
618
                                 childAssignment,
619
84
                                 prover.eqXFromY(childAssignment, parent));
620
              }
621
              else
622
              {
623
                // IFF x y = b y: if IFF is assigned to FALSE, assign(x = !b)
624
                assignAndEnqueue(parent[0],
625
                                 !childAssignment,
626
                                 prover.neqXFromY(childAssignment, parent));
627
              }
628
            }
629
          }
630
        }
631
678
        break;
632
4709
      case kind::IMPLIES:
633
4709
        if (isAssigned(parent[0]) && isAssigned(parent[1]))
634
        {
635
          // IMPLIES (x=v1) (y=v2): assign(IMPLIES = (!v1 || v2))
636
1852
          assignAndEnqueue(
637
              parent,
638
3704
              !getAssignment(parent[0]) || getAssignment(parent[1]),
639
3704
              prover.impliesEval(getAssignment(parent[0]),
640
3704
                                 getAssignment(parent[1])));
641
        }
642
        else
643
        {
644
10400
          if (child == parent[0] && childAssignment
645
10190
              && isAssignedTo(parent, true))
646
          {
647
            // IMPLIES (x=TRUE) y [with IMPLIES == TRUE]: assign(y = TRUE)
648
78
            assignAndEnqueue(parent[1], true, prover.impliesYFromX(parent));
649
          }
650
9599
          if (child == parent[1] && !childAssignment
651
8577
              && isAssignedTo(parent, true))
652
          {
653
            // IMPLIES x (y=FALSE) [with IMPLIES == TRUE]: assign(x = FALSE)
654
5
            assignAndEnqueue(parent[0], false, prover.impliesXFromY(parent));
655
          }
656
          // Note that IMPLIES == FALSE doesn't need any cases here
657
          // because if that assignment has been done, we've already
658
          // propagated all the children (in back-propagation).
659
        }
660
4709
        break;
661
107
      case kind::XOR:
662
107
        if (isAssigned(parent))
663
        {
664
35
          if (child == parent[0])
665
          {
666
            // XOR (x=v) y [with XOR assigned], assign(y = (v ^ XOR)
667
20
            assignAndEnqueue(
668
                parent[1],
669
40
                childAssignment != getAssignment(parent),
670
80
                prover.xorYFromX(
671
40
                    !getAssignment(parent), childAssignment, parent));
672
          }
673
          else
674
          {
675
15
            Assert(child == parent[1]);
676
            // XOR x (y=v) [with XOR assigned], assign(x = (v ^ XOR))
677
15
            assignAndEnqueue(
678
                parent[0],
679
30
                childAssignment != getAssignment(parent),
680
60
                prover.xorXFromY(
681
30
                    !getAssignment(parent), childAssignment, parent));
682
          }
683
        }
684
107
        if (isAssigned(parent[0]) && isAssigned(parent[1]))
685
        {
686
37
          assignAndEnqueue(parent,
687
74
                           getAssignment(parent[0]) != getAssignment(parent[1]),
688
74
                           prover.xorEval(getAssignment(parent[0]),
689
74
                                          getAssignment(parent[1])));
690
        }
691
107
        break;
692
      default: Unhandled();
693
    }
694
  }
695
672474
}
696
697
10353
TrustNode CircuitPropagator::propagate()
698
{
699
10353
  Debug("circuit-prop") << "CircuitPropagator::propagate()" << std::endl;
700
701
682827
  for (unsigned i = 0;
702
682827
       i < d_propagationQueue.size() && d_conflict.get().isNull();
703
       ++i)
704
  {
705
    // The current node we are propagating
706
1344948
    TNode current = d_propagationQueue[i];
707
1344948
    Debug("circuit-prop") << "CircuitPropagator::propagate(): processing "
708
672474
                          << current << std::endl;
709
672474
    bool assignment = getAssignment(current);
710
1344948
    Debug("circuit-prop") << "CircuitPropagator::propagate(): assigned to "
711
672474
                          << (assignment ? "true" : "false") << std::endl;
712
713
    // Is this an atom
714
2612639
    bool atom = Theory::theoryOf(current) != THEORY_BOOL || current.isVar()
715
2690025
                || (current.getKind() == kind::EQUAL
716
673832
                    && (current[0].isVar() && current[1].isVar()));
717
718
    // If an atom, add to the list for simplification
719
672474
    if (atom)
720
    {
721
225054
      Debug("circuit-prop")
722
112527
          << "CircuitPropagator::propagate(): adding to learned: "
723
112527
          << (assignment ? (Node)current : current.notNode()) << std::endl;
724
225054
      Node lit = assignment ? Node(current) : current.notNode();
725
726
112527
      if (isProofEnabled())
727
      {
728
24451
        if (d_epg->hasProofFor(lit))
729
        {
730
          // if we have a parent proof generator that provides proofs of the
731
          // inputs to this class, we must use the lazy proof chain
732
24451
          ProofGenerator* pg = d_proofInternal.get();
733
24451
          if (d_proofExternal != nullptr)
734
          {
735
24451
            d_proofExternal->addLazyStep(lit, pg);
736
24451
            pg = d_proofExternal.get();
737
          }
738
48902
          TrustNode tlit = TrustNode::mkTrustLemma(lit, pg);
739
24451
          d_learnedLiterals.push_back(tlit);
740
        }
741
        else
742
        {
743
          Warning() << "CircuitPropagator: Proof is missing for " << lit
744
                    << std::endl;
745
          TrustNode tlit = TrustNode::mkTrustLemma(lit, nullptr);
746
          d_learnedLiterals.push_back(tlit);
747
        }
748
      }
749
      else
750
      {
751
176152
        TrustNode tlit = TrustNode::mkTrustLemma(lit, nullptr);
752
88076
        d_learnedLiterals.push_back(tlit);
753
      }
754
112527
      Trace("circuit-prop") << "Added proof for " << lit << std::endl;
755
    }
756
757
    // Propagate this value to the children (if not an atom or a constant)
758
672474
    if (d_backwardPropagation && !atom && !current.isConst())
759
    {
760
550538
      propagateBackward(current, assignment);
761
    }
762
    // Propagate this value to the parents
763
672474
    if (d_forwardPropagation)
764
    {
765
672474
      propagateForward(current, assignment);
766
    }
767
  }
768
769
  // No conflict
770
10353
  return d_conflict;
771
}
772
773
962
void CircuitPropagator::setProof(ProofNodeManager* pnm,
774
                                 context::Context* ctx,
775
                                 ProofGenerator* defParent)
776
{
777
962
  d_pnm = pnm;
778
962
  d_epg.reset(new EagerProofGenerator(pnm, ctx));
779
1924
  d_proofInternal.reset(
780
962
      new LazyCDProofChain(pnm, true, ctx, d_epg.get(), true));
781
962
  if (defParent != nullptr)
782
  {
783
    // If we provide a parent proof generator (defParent), we want the ASSUME
784
    // leafs of proofs provided by this class to call the getProofFor method on
785
    // the parent. To do this, we use a LazyCDProofChain.
786
1924
    d_proofExternal.reset(
787
962
        new LazyCDProofChain(pnm, true, ctx, defParent, false));
788
  }
789
962
}
790
791
2314223
bool CircuitPropagator::isProofEnabled() const
792
{
793
2314223
  return d_proofInternal != nullptr;
794
}
795
796
556965
void CircuitPropagator::addProof(TNode f, std::shared_ptr<ProofNode> pf)
797
{
798
556965
  if (isProofEnabled())
799
  {
800
89062
    if (!d_epg->hasProofFor(f))
801
    {
802
74326
      Trace("circuit-prop") << "Adding proof for " << f << std::endl
803
37163
                            << "\t" << *pf << std::endl;
804
37163
      d_epg->setProofFor(f, std::move(pf));
805
    }
806
    else
807
    {
808
103798
      auto prf = d_epg->getProofFor(f);
809
103798
      Trace("circuit-prop") << "Ignoring proof, we already have" << std::endl
810
51899
                            << "\t" << *prf << std::endl;
811
    }
812
  }
813
556965
}
814
815
}  // namespace booleans
816
}  // namespace theory
817
26676
}  // namespace CVC4