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