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-2025 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 : 72343 : CircuitPropagator::CircuitPropagator(Env& env, bool enableForward, bool enableBackward)
38 : : : EnvObj(env),
39 : : d_context(),
40 : : d_propagationQueue(),
41 : 72343 : d_propagationQueueClearer(&d_context, d_propagationQueue),
42 : 72343 : d_conflict(&d_context, TrustNode()),
43 : : d_learnedLiterals(),
44 : 72343 : d_learnedLiteralClearer(&d_context, d_learnedLiterals),
45 : : d_backEdges(),
46 : 72343 : 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 : 144686 : d_proofExternal(nullptr)
55 : : {
56 : 72343 : }
57 : :
58 : 42269 : void CircuitPropagator::initialize()
59 : : {
60 [ + + ]: 42269 : if (d_needsFinish)
61 : : {
62 : 7326 : d_context.pop();
63 : : }
64 : 42269 : d_context.push();
65 : 42269 : d_needsFinish = true;
66 : 42269 : }
67 : :
68 : 540983 : void CircuitPropagator::assertTrue(TNode assertion)
69 : : {
70 [ + - ]: 540983 : Trace("circuit-prop") << "TRUE: " << assertion << std::endl;
71 [ + + ][ - + ]: 540983 : if (assertion.getKind() == Kind::CONST_BOOLEAN && !assertion.getConst<bool>())
[ - + ]
72 : : {
73 : 0 : makeConflict(assertion);
74 : : }
75 [ + + ]: 540983 : else if (assertion.getKind() == Kind::AND)
76 : : {
77 : : ProofCircuitPropagatorBackward prover{
78 : 4924 : d_env.getNodeManager(), d_env.getProofNodeManager(), assertion, true};
79 [ + + ]: 2462 : if (isProofEnabled())
80 : : {
81 : 1642 : addProof(assertion, prover.assume(assertion));
82 : : }
83 [ + + ]: 56525 : for (auto it = assertion.begin(); it != assertion.end(); ++it)
84 : : {
85 : 54063 : addProof(*it, prover.andTrue(it));
86 : 54063 : assertTrue(*it);
87 : : }
88 : : }
89 : : else
90 : : {
91 : : // Analyze the assertion for back-edges and all that
92 : 538521 : computeBackEdges(assertion);
93 : : // Assign the given assertion to true
94 : 538521 : assignAndEnqueue(assertion,
95 : : true,
96 : 538521 : isProofEnabled()
97 [ + + ][ + + ]: 1077040 : ? d_env.getProofNodeManager()->mkAssume(assertion)
[ - - ]
98 : : : nullptr);
99 : : }
100 : 540983 : }
101 : :
102 : 1073040 : void CircuitPropagator::assignAndEnqueue(TNode n,
103 : : bool value,
104 : : std::shared_ptr<ProofNode> proof)
105 : : {
106 [ + - ]: 2146070 : Trace("circuit-prop") << "CircuitPropagator::assign(" << n << ", "
107 [ - - ]: 1073040 : << (value ? "true" : "false") << ")" << std::endl;
108 : :
109 [ + + ]: 1073040 : if (n.getKind() == Kind::CONST_BOOLEAN)
110 : : {
111 : : // Assigning a constant to the opposite value is dumb
112 [ - + ]: 61880 : if (value != n.getConst<bool>())
113 : : {
114 : 0 : makeConflict(n);
115 : 0 : return;
116 : : }
117 : : }
118 : :
119 [ + + ]: 1073040 : if (isProofEnabled())
120 : : {
121 [ - + ]: 639688 : if (proof == nullptr)
122 : : {
123 : 0 : warning() << "CircuitPropagator: Proof is missing for " << n << std::endl;
124 : 0 : Assert(false);
125 : : }
126 : : else
127 : : {
128 [ - + ][ - + ]: 639688 : Assert(!proof->getResult().isNull());
[ - - ]
129 [ + + ]: 639688 : Node expected = value ? Node(n) : n.negate();
130 [ - + ]: 639688 : 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 : 639688 : addProof(expected, std::move(proof));
137 : : }
138 : : }
139 : :
140 : : // Get the current assignment
141 : 1073040 : AssignmentStatus state = d_state[n];
142 : :
143 [ + + ]: 1073040 : if (state != UNASSIGNED)
144 : : {
145 : : // If the node is already assigned we might have a conflict
146 [ + + ]: 335947 : if (value != (state == ASSIGNED_TO_TRUE))
147 : : {
148 : 2698 : makeConflict(n);
149 : : }
150 : : }
151 : : else
152 : : {
153 : : // If unassigned, mark it as assigned
154 [ + + ]: 737089 : d_state[n] = value ? ASSIGNED_TO_TRUE : ASSIGNED_TO_FALSE;
155 : : // Add for further propagation
156 : 737089 : d_propagationQueue.push_back(n);
157 : : }
158 : : }
159 : :
160 : 2698 : void CircuitPropagator::makeConflict(Node n)
161 : : {
162 : 2698 : auto bfalse = nodeManager()->mkConst(false);
163 : 2698 : ProofGenerator* g = nullptr;
164 [ + + ]: 2698 : if (isProofEnabled())
165 : : {
166 [ + + ]: 1254 : if (d_epg->hasProofFor(bfalse))
167 : : {
168 : 35 : return;
169 : : }
170 : 1219 : ProofCircuitPropagator pcp(d_env.getNodeManager(),
171 : 1219 : d_env.getProofNodeManager());
172 [ - + ]: 1219 : if (n == bfalse)
173 : : {
174 : 0 : d_epg->setProofFor(bfalse, pcp.assume(bfalse));
175 : : }
176 : : else
177 : : {
178 : 2438 : d_epg->setProofFor(bfalse,
179 : 2438 : pcp.conflict(pcp.assume(n), pcp.assume(n.negate())));
180 : : }
181 [ + - ]: 1219 : g = d_proofInternal.get();
182 : 2438 : Trace("circuit-prop") << "Added conflict " << *d_epg->getProofFor(bfalse)
183 : 1219 : << std::endl;
184 : 2438 : Trace("circuit-prop") << "\texpanded " << *g->getProofFor(bfalse)
185 : 1219 : << std::endl;
186 : : }
187 : 2663 : d_conflict = TrustNode::mkTrustLemma(bfalse, g);
188 : : }
189 : :
190 : 538521 : void CircuitPropagator::computeBackEdges(TNode node)
191 : : {
192 [ + - ]: 1077040 : Trace("circuit-prop") << "CircuitPropagator::computeBackEdges(" << node << ")"
193 : 538521 : << endl;
194 : :
195 : : // Vector of nodes to visit
196 : 1077040 : vector<TNode> toVisit;
197 : :
198 : : // Start with the top node
199 [ + + ]: 538521 : if (d_seen.find(node) == d_seen.end())
200 : : {
201 : 500804 : toVisit.push_back(node);
202 : 500804 : d_seen.insert(node);
203 : : }
204 : :
205 : : // Initialize the back-edges for the root, so we don't have a special case
206 : 538521 : d_backEdges[node];
207 : :
208 : : // Go through the visit list
209 [ + + ]: 1828210 : for (unsigned i = 0; i < toVisit.size(); ++i)
210 : : {
211 : : // Node we need to visit
212 : 2579380 : TNode current = toVisit[i];
213 [ + - ]: 2579380 : Trace("circuit-prop")
214 : 0 : << "CircuitPropagator::computeBackEdges(): processing " << current
215 : 1289690 : << endl;
216 [ - + ][ - + ]: 1289690 : Assert(d_seen.find(current) != d_seen.end());
[ - - ]
217 : :
218 : : // If this not an atom visit all the children and compute the back edges
219 [ + + ]: 1289690 : if (Theory::theoryOf(current) == THEORY_BOOL)
220 : : {
221 : 2449230 : for (unsigned child = 0, child_end = current.getNumChildren();
222 [ + + ]: 2449230 : child < child_end;
223 : : ++child)
224 : : {
225 : 3248460 : TNode childNode = current[child];
226 : : // Add the back edge
227 : 1624230 : d_backEdges[childNode].push_back(current);
228 : : // Add to the queue if not seen yet
229 [ + + ]: 1624230 : if (d_seen.find(childNode) == d_seen.end())
230 : : {
231 : 788885 : toVisit.push_back(childNode);
232 : 788885 : d_seen.insert(childNode);
233 : : }
234 : : }
235 : : }
236 : : }
237 : 538521 : }
238 : :
239 : 376478 : void CircuitPropagator::propagateBackward(TNode parent, bool parentAssignment)
240 : : {
241 [ + - ]: 752956 : Trace("circuit-prop") << "CircuitPropagator::propagateBackward(" << parent
242 : 376478 : << ", " << parentAssignment << ")" << endl;
243 : 376478 : ProofCircuitPropagatorBackward prover{d_env.getNodeManager(),
244 : 376478 : d_env.getProofNodeManager(),
245 : : parent,
246 : 752956 : parentAssignment};
247 : :
248 : : // backward rules
249 [ + + ][ + + ]: 376478 : switch (parent.getKind())
[ + + ][ + - ]
250 : : {
251 : 12277 : case Kind::AND:
252 [ + + ]: 12277 : if (parentAssignment)
253 : : {
254 : : // AND = TRUE: forall children c, assign(c = TRUE)
255 : 64364 : for (TNode::iterator i = parent.begin(), i_end = parent.end();
256 [ + + ]: 64364 : i != i_end;
257 : 61927 : ++i)
258 : : {
259 : 61927 : assignAndEnqueue(*i, true, prover.andTrue(i));
260 : : }
261 : : }
262 : : else
263 : : {
264 : : // AND = FALSE: if all children BUT ONE == TRUE, assign(c = FALSE)
265 : : TNode::iterator holdout =
266 : 21497 : find_if_unique(parent.begin(), parent.end(), [this](TNode x) {
267 : 21497 : return !isAssignedTo(x, true);
268 : 9840 : });
269 [ + + ]: 9840 : if (holdout != parent.end())
270 : : {
271 : 1033 : assignAndEnqueue(*holdout, false, prover.andFalse(parent, holdout));
272 : : }
273 : : }
274 : 12277 : break;
275 : 208570 : case Kind::OR:
276 [ + + ]: 208570 : if (parentAssignment)
277 : : {
278 : : // OR = TRUE: if all children BUT ONE == FALSE, assign(c = TRUE)
279 : : TNode::iterator holdout =
280 : 414562 : find_if_unique(parent.begin(), parent.end(), [this](TNode x) {
281 : 414562 : return !isAssignedTo(x, false);
282 : 205558 : });
283 [ + + ]: 205558 : if (holdout != parent.end())
284 : : {
285 : 1761 : assignAndEnqueue(*holdout, true, prover.orTrue(parent, holdout));
286 : : }
287 : : }
288 : : else
289 : : {
290 : : // OR = FALSE: forall children c, assign(c = FALSE)
291 : 14729 : for (TNode::iterator i = parent.begin(), i_end = parent.end();
292 [ + + ]: 14729 : i != i_end;
293 : 11717 : ++i)
294 : : {
295 : 11717 : assignAndEnqueue(*i, false, prover.orFalse(i));
296 : : }
297 : : }
298 : 208570 : break;
299 : 140148 : case Kind::NOT:
300 : : // NOT = b: assign(c = !b)
301 : 140148 : assignAndEnqueue(
302 : 280296 : parent[0], !parentAssignment, prover.Not(!parentAssignment, parent));
303 : 140148 : break;
304 : 3061 : case Kind::ITE:
305 [ + + ]: 3061 : if (isAssignedTo(parent[0], true))
306 : : {
307 : : // ITE c x y = v: if c is assigned and TRUE, assign(x = v)
308 : 223 : assignAndEnqueue(parent[1], parentAssignment, prover.iteC(true));
309 : : }
310 [ + + ]: 2838 : else if (isAssignedTo(parent[0], false))
311 : : {
312 : : // ITE c x y = v: if c is assigned and FALSE, assign(y = v)
313 : 71 : assignAndEnqueue(parent[2], parentAssignment, prover.iteC(false));
314 : : }
315 : 2767 : else if (isAssigned(parent[1]) && isAssigned(parent[2]))
316 : : {
317 [ + + ][ - - ]: 62 : if (getAssignment(parent[1]) == parentAssignment
318 [ + + ][ + + ]: 62 : && getAssignment(parent[2]) != parentAssignment)
[ + + ][ + - ]
[ - - ]
319 : : {
320 : : // ITE c x y = v: if c is unassigned, x and y are assigned, x==v and
321 : : // y!=v, assign(c = TRUE)
322 : 4 : assignAndEnqueue(parent[0], true, prover.iteIsCase(1));
323 : : }
324 [ + + ][ - - ]: 58 : else if (getAssignment(parent[1]) != parentAssignment
325 [ + + ][ + - ]: 58 : && getAssignment(parent[2]) == parentAssignment)
[ + + ][ + - ]
[ - - ]
326 : : {
327 : : // ITE c x y = v: if c is unassigned, x and y are assigned, x!=v and
328 : : // y==v, assign(c = FALSE)
329 : 22 : assignAndEnqueue(parent[0], false, prover.iteIsCase(0));
330 : : }
331 : : }
332 : 3061 : break;
333 : 6100 : case Kind::EQUAL:
334 [ - + ][ - + ]: 6100 : Assert(parent[0].getType().isBoolean());
[ - - ]
335 [ + + ]: 6100 : if (parentAssignment)
336 : : {
337 : : // IFF x y = TRUE: if x [resp y] is assigned, assign(y = x.assignment
338 : : // [resp x = y.assignment])
339 [ + + ]: 5062 : if (isAssigned(parent[0]))
340 : : {
341 : 455 : assignAndEnqueue(parent[1],
342 : 910 : getAssignment(parent[0]),
343 : 910 : prover.eqYFromX(getAssignment(parent[0]), parent));
344 : : }
345 [ + + ]: 4607 : else if (isAssigned(parent[1]))
346 : : {
347 : 17 : assignAndEnqueue(parent[0],
348 : 34 : getAssignment(parent[1]),
349 : 34 : prover.eqXFromY(getAssignment(parent[1]), parent));
350 : : }
351 : : }
352 : : else
353 : : {
354 : : // IFF x y = FALSE: if x [resp y] is assigned, assign(y = !x.assignment
355 : : // [resp x = !y.assignment])
356 [ + + ]: 1038 : if (isAssigned(parent[0]))
357 : : {
358 : 48 : assignAndEnqueue(parent[1],
359 : 96 : !getAssignment(parent[0]),
360 : 96 : prover.neqYFromX(getAssignment(parent[0]), parent));
361 : : }
362 [ + + ]: 990 : else if (isAssigned(parent[1]))
363 : : {
364 : 25 : assignAndEnqueue(parent[0],
365 : 50 : !getAssignment(parent[1]),
366 : 50 : prover.neqXFromY(getAssignment(parent[1]), parent));
367 : : }
368 : : }
369 : 6100 : break;
370 : 5963 : case Kind::IMPLIES:
371 [ + + ]: 5963 : if (parentAssignment)
372 : : {
373 [ + + ]: 4103 : if (isAssignedTo(parent[0], true))
374 : : {
375 : : // IMPLIES x y = TRUE, and x == TRUE: assign(y = TRUE)
376 : 1129 : assignAndEnqueue(parent[1], true, prover.impliesYFromX(parent));
377 : : }
378 [ + + ]: 4103 : if (isAssignedTo(parent[1], false))
379 : : {
380 : : // IMPLIES x y = TRUE, and y == FALSE: assign(x = FALSE)
381 : 212 : assignAndEnqueue(parent[0], false, prover.impliesXFromY(parent));
382 : : }
383 : : }
384 : : else
385 : : {
386 : : // IMPLIES x y = FALSE: assign(x = TRUE) and assign(y = FALSE)
387 : 1860 : assignAndEnqueue(parent[0], true, prover.impliesNegX());
388 : 1860 : assignAndEnqueue(parent[1], false, prover.impliesNegY());
389 : : }
390 : 5963 : break;
391 : 359 : case Kind::XOR:
392 [ + + ]: 359 : if (parentAssignment)
393 : : {
394 [ + + ]: 252 : if (isAssigned(parent[0]))
395 : : {
396 : : // XOR x y = TRUE, and x assigned, assign(y = !assignment(x))
397 : 16 : assignAndEnqueue(
398 : : parent[1],
399 : 32 : !getAssignment(parent[0]),
400 : 48 : prover.xorYFromX(
401 : 32 : !parentAssignment, getAssignment(parent[0]), parent));
402 : : }
403 [ + + ]: 236 : else if (isAssigned(parent[1]))
404 : : {
405 : : // XOR x y = TRUE, and y assigned, assign(x = !assignment(y))
406 : 46 : assignAndEnqueue(
407 : : parent[0],
408 : 92 : !getAssignment(parent[1]),
409 : 138 : prover.xorXFromY(
410 : 92 : !parentAssignment, getAssignment(parent[1]), parent));
411 : : }
412 : : }
413 : : else
414 : : {
415 [ + + ]: 107 : if (isAssigned(parent[0]))
416 : : {
417 : : // XOR x y = FALSE, and x assigned, assign(y = assignment(x))
418 : 31 : assignAndEnqueue(
419 : : parent[1],
420 : 62 : getAssignment(parent[0]),
421 : 93 : prover.xorYFromX(
422 : 62 : !parentAssignment, getAssignment(parent[0]), parent));
423 : : }
424 [ + + ]: 76 : else if (isAssigned(parent[1]))
425 : : {
426 : : // XOR x y = FALSE, and y assigned, assign(x = assignment(y))
427 : 33 : assignAndEnqueue(
428 : : parent[0],
429 : 66 : getAssignment(parent[1]),
430 : 99 : prover.xorXFromY(
431 : 66 : !parentAssignment, getAssignment(parent[1]), parent));
432 : : }
433 : : }
434 : 359 : break;
435 : 0 : default: Unhandled();
436 : : }
437 : 376478 : }
438 : :
439 : 723682 : void CircuitPropagator::propagateForward(TNode child, bool childAssignment)
440 : : {
441 : : // The assignment we have
442 [ + - ]: 1447360 : Trace("circuit-prop") << "CircuitPropagator::propagateForward(" << child
443 : 723682 : << ", " << childAssignment << ")" << endl;
444 : :
445 : : // Get the back any nodes where this is child
446 : 723682 : const vector<Node>& parents = d_backEdges.find(child)->second;
447 : :
448 : : // Go through the parents and see if there is anything to propagate
449 : 723682 : vector<Node>::const_iterator parent_it = parents.begin();
450 : 723682 : vector<Node>::const_iterator parent_it_end = parents.end();
451 [ + + ][ + + ]: 1089310 : for (; parent_it != parent_it_end && d_conflict.get().isNull(); ++parent_it)
[ + + ]
452 : : {
453 : : // The current parent of the child
454 : 731248 : TNode parent = *parent_it;
455 [ + - ]: 365624 : Trace("circuit-prop") << "Parent: " << parent << endl;
456 [ - + ][ - + ]: 365624 : Assert(expr::hasSubterm(parent, child));
[ - - ]
457 : :
458 : 365624 : ProofCircuitPropagatorForward prover{d_env.getNodeManager(),
459 : 365624 : d_env.getProofNodeManager(),
460 : : child,
461 : : childAssignment,
462 : 1096870 : parent};
463 : :
464 : : // Forward rules
465 [ + + ][ + + ]: 365624 : switch (parent.getKind())
[ + + ][ + - ]
466 : : {
467 : 85865 : case Kind::AND:
468 [ + + ]: 85865 : if (childAssignment)
469 : : {
470 : 77035 : TNode::iterator holdout;
471 : 71616000 : holdout = find_if(parent.begin(), parent.end(), [this](TNode x) {
472 : 71616000 : return !isAssignedTo(x, true);
473 : 77035 : });
474 : :
475 [ + + ]: 77035 : if (holdout == parent.end())
476 : : { // all children are assigned TRUE
477 : : // AND ...(x=TRUE)...: if all children now assigned to TRUE,
478 : : // assign(AND = TRUE)
479 : 55988 : assignAndEnqueue(parent, true, prover.andAllTrue());
480 : : }
481 [ + + ]: 21047 : else if (isAssignedTo(parent, false))
482 : : { // the AND is FALSE
483 : : // is the holdout unique ?
484 : : TNode::iterator other =
485 : 2863 : find_if(holdout + 1, parent.end(), [this](TNode x) {
486 : 2863 : return !isAssignedTo(x, true);
487 : 2503 : });
488 [ + + ]: 2503 : if (other == parent.end())
489 : : { // the holdout is unique
490 : : // AND ...(x=TRUE)...: if all children BUT ONE now assigned to
491 : : // TRUE, and AND == FALSE, assign(last_holdout = FALSE)
492 : 837 : assignAndEnqueue(
493 : 1674 : *holdout, false, prover.andFalse(parent, holdout));
494 : : }
495 : : }
496 : : }
497 : : else
498 : : {
499 : : // AND ...(x=FALSE)...: assign(AND = FALSE)
500 : 8830 : assignAndEnqueue(parent, false, prover.andOneFalse());
501 : : }
502 : 85865 : break;
503 : 125168 : case Kind::OR:
504 [ + + ]: 125168 : if (childAssignment)
505 : : {
506 : : // OR ...(x=TRUE)...: assign(OR = TRUE)
507 : 63915 : assignAndEnqueue(parent, true, prover.orOneTrue());
508 : : }
509 : : else
510 : : {
511 : 61253 : TNode::iterator holdout;
512 : 1564780 : holdout = find_if(parent.begin(), parent.end(), [this](TNode x) {
513 : 1564780 : return !isAssignedTo(x, false);
514 : 61253 : });
515 [ + + ]: 61253 : if (holdout == parent.end())
516 : : { // all children are assigned FALSE
517 : : // OR ...(x=FALSE)...: if all children now assigned to FALSE,
518 : : // assign(OR = FALSE)
519 : 10837 : assignAndEnqueue(parent, false, prover.orFalse());
520 : : }
521 [ + + ]: 50416 : else if (isAssignedTo(parent, true))
522 : : { // the OR is TRUE
523 : : // is the holdout unique ?
524 : : TNode::iterator other =
525 : 49853 : find_if(holdout + 1, parent.end(), [this](TNode x) {
526 : 49853 : return !isAssignedTo(x, false);
527 : 42562 : });
528 [ + + ]: 42562 : if (other == parent.end())
529 : : { // the holdout is unique
530 : : // OR ...(x=FALSE)...: if all children BUT ONE now assigned to
531 : : // FALSE, and OR == TRUE, assign(last_holdout = TRUE)
532 : 22404 : assignAndEnqueue(*holdout, true, prover.orTrue(parent, holdout));
533 : : }
534 : : }
535 : : }
536 : 125168 : break;
537 : :
538 : 139992 : case Kind::NOT:
539 : : // NOT (x=b): assign(NOT = !b)
540 : 139992 : assignAndEnqueue(
541 : 279984 : parent, !childAssignment, prover.Not(childAssignment, parent));
542 : 139992 : break;
543 : :
544 : 1568 : case Kind::ITE:
545 [ + + ]: 1568 : if (child == parent[0])
546 : : {
547 [ + + ]: 527 : if (childAssignment)
548 : : {
549 [ + + ]: 357 : if (isAssigned(parent[1]))
550 : : {
551 : : // ITE (c=TRUE) x y: if x is assigned, assign(ITE = x.assignment)
552 : 216 : assignAndEnqueue(parent,
553 : 432 : getAssignment(parent[1]),
554 : 432 : prover.iteEvalThen(getAssignment(parent[1])));
555 : : }
556 : : }
557 : : else
558 : : {
559 [ + + ]: 170 : if (isAssigned(parent[2]))
560 : : {
561 : : // ITE (c=FALSE) x y: if y is assigned, assign(ITE = y.assignment)
562 : 122 : assignAndEnqueue(parent,
563 : 244 : getAssignment(parent[2]),
564 : 244 : prover.iteEvalElse(getAssignment(parent[2])));
565 : : }
566 : : }
567 : : }
568 [ + + ]: 1568 : if (child == parent[1])
569 : : {
570 [ + + ]: 559 : if (isAssignedTo(parent[0], true))
571 : : {
572 : : // ITE c (x=v) y: if c is assigned and TRUE, assign(ITE = v)
573 : 269 : assignAndEnqueue(
574 : 538 : parent, childAssignment, prover.iteEvalThen(childAssignment));
575 : : }
576 : : }
577 [ + + ]: 1568 : if (child == parent[2])
578 : : {
579 [ - + ][ - + ]: 482 : Assert(child == parent[2]);
[ - - ]
580 [ + + ]: 482 : if (isAssignedTo(parent[0], false))
581 : : {
582 : : // ITE c x (y=v): if c is assigned and FALSE, assign(ITE = v)
583 : 118 : assignAndEnqueue(
584 : 236 : parent, childAssignment, prover.iteEvalElse(childAssignment));
585 : : }
586 : : }
587 : 1568 : break;
588 : 3293 : case Kind::EQUAL:
589 [ - + ][ - + ]: 3293 : Assert(parent[0].getType().isBoolean());
[ - - ]
590 : 3293 : if (isAssigned(parent[0]) && isAssigned(parent[1]))
591 : : {
592 : : // IFF x y: if x and y is assigned, assign(IFF = (x.assignment <=>
593 : : // y.assignment))
594 : 1679 : assignAndEnqueue(parent,
595 : 3358 : getAssignment(parent[0]) == getAssignment(parent[1]),
596 : 3358 : prover.eqEval(getAssignment(parent[0]),
597 : 3358 : getAssignment(parent[1])));
598 : : }
599 : : else
600 : : {
601 [ + + ]: 1614 : if (isAssigned(parent))
602 : : {
603 [ + + ]: 843 : if (child == parent[0])
604 : : {
605 [ + + ]: 564 : if (getAssignment(parent))
606 : : {
607 : : // IFF (x = b) y: if IFF is assigned to TRUE, assign(y = b)
608 : 538 : assignAndEnqueue(parent[1],
609 : : childAssignment,
610 : 1076 : prover.eqYFromX(childAssignment, parent));
611 : : }
612 : : else
613 : : {
614 : : // IFF (x = b) y: if IFF is assigned to FALSE, assign(y = !b)
615 : 26 : assignAndEnqueue(parent[1],
616 : 26 : !childAssignment,
617 : 52 : prover.neqYFromX(childAssignment, parent));
618 : : }
619 : : }
620 : : else
621 : : {
622 [ - + ][ - + ]: 279 : Assert(child == parent[1]);
[ - - ]
623 [ + + ]: 279 : if (getAssignment(parent))
624 : : {
625 : : // IFF x y = b: if IFF is assigned to TRUE, assign(x = b)
626 : 233 : assignAndEnqueue(parent[0],
627 : : childAssignment,
628 : 466 : prover.eqXFromY(childAssignment, parent));
629 : : }
630 : : else
631 : : {
632 : : // IFF x y = b y: if IFF is assigned to FALSE, assign(x = !b)
633 : 46 : assignAndEnqueue(parent[0],
634 : 46 : !childAssignment,
635 : 92 : prover.neqXFromY(childAssignment, parent));
636 : : }
637 : : }
638 : : }
639 : : }
640 : 3293 : break;
641 : 9281 : case Kind::IMPLIES:
642 : 9281 : if (isAssigned(parent[0]) && isAssigned(parent[1]))
643 : : {
644 : : // IMPLIES (x=v1) (y=v2): assign(IMPLIES = (!v1 || v2))
645 : 5173 : assignAndEnqueue(
646 : : parent,
647 : 10346 : !getAssignment(parent[0]) || getAssignment(parent[1]),
648 : 10346 : prover.impliesEval(getAssignment(parent[0]),
649 : 10346 : getAssignment(parent[1])));
650 : : }
651 : : else
652 : : {
653 [ + + ][ + + ]: 6904 : if (child == parent[0] && childAssignment
[ - - ]
654 [ + + ][ + + ]: 6904 : && isAssignedTo(parent, true))
[ + + ][ + - ]
[ - - ]
655 : : {
656 : : // IMPLIES (x=TRUE) y [with IMPLIES == TRUE]: assign(y = TRUE)
657 : 226 : assignAndEnqueue(parent[1], true, prover.impliesYFromX(parent));
658 : : }
659 [ + + ][ + + ]: 5420 : if (child == parent[1] && !childAssignment
[ - - ]
660 [ + + ][ + + ]: 5420 : && isAssignedTo(parent, true))
[ + + ][ + - ]
[ - - ]
661 : : {
662 : : // IMPLIES x (y=FALSE) [with IMPLIES == TRUE]: assign(x = FALSE)
663 : 18 : assignAndEnqueue(parent[0], false, prover.impliesXFromY(parent));
664 : : }
665 : : // Note that IMPLIES == FALSE doesn't need any cases here
666 : : // because if that assignment has been done, we've already
667 : : // propagated all the children (in back-propagation).
668 : : }
669 : 9281 : break;
670 : 457 : case Kind::XOR:
671 [ + + ]: 457 : if (isAssigned(parent))
672 : : {
673 [ + + ]: 197 : if (child == parent[0])
674 : : {
675 : : // XOR (x=v) y [with XOR assigned], assign(y = (v ^ XOR)
676 : 121 : assignAndEnqueue(
677 : : parent[1],
678 : 242 : childAssignment != getAssignment(parent),
679 : 363 : prover.xorYFromX(
680 : 242 : !getAssignment(parent), childAssignment, parent));
681 : : }
682 : : else
683 : : {
684 [ - + ][ - + ]: 76 : Assert(child == parent[1]);
[ - - ]
685 : : // XOR x (y=v) [with XOR assigned], assign(x = (v ^ XOR))
686 : 76 : assignAndEnqueue(
687 : : parent[0],
688 : 152 : childAssignment != getAssignment(parent),
689 : 228 : prover.xorXFromY(
690 : 152 : !getAssignment(parent), childAssignment, parent));
691 : : }
692 : : }
693 : 457 : if (isAssigned(parent[0]) && isAssigned(parent[1]))
694 : : {
695 : 213 : assignAndEnqueue(parent,
696 : 426 : getAssignment(parent[0]) != getAssignment(parent[1]),
697 : 426 : prover.xorEval(getAssignment(parent[0]),
698 : 426 : getAssignment(parent[1])));
699 : : }
700 : 457 : break;
701 : 0 : default: Unhandled();
702 : : }
703 : : }
704 : 723682 : }
705 : :
706 : 42269 : TrustNode CircuitPropagator::propagate()
707 : : {
708 [ + - ]: 42269 : Trace("circuit-prop") << "CircuitPropagator::propagate()" << std::endl;
709 : :
710 : 765951 : for (unsigned i = 0;
711 [ + + ][ + + ]: 765951 : i < d_propagationQueue.size() && d_conflict.get().isNull();
[ + + ]
712 : : ++i)
713 : : {
714 : : // The current node we are propagating
715 : 1447360 : TNode current = d_propagationQueue[i];
716 [ + - ]: 1447360 : Trace("circuit-prop") << "CircuitPropagator::propagate(): processing "
717 : 723682 : << current << std::endl;
718 : 723682 : bool assignment = getAssignment(current);
719 [ + - ]: 1447360 : Trace("circuit-prop") << "CircuitPropagator::propagate(): assigned to "
720 [ - - ]: 723682 : << (assignment ? "true" : "false") << std::endl;
721 : :
722 : : // Is this an atom
723 [ + + ][ - - ]: 1159560 : bool atom = Theory::theoryOf(current) != THEORY_BOOL || current.isVar()
724 [ + + ][ + + ]: 1166370 : || (current.getKind() == Kind::EQUAL
725 : 730486 : && (current[0].isVar() && current[1].isVar()));
726 : :
727 : : // If an atom, add to the list for simplification
728 : 723682 : if (atom
729 [ + + ][ + + ]: 729782 : || (current.getKind() == Kind::EQUAL
730 : 729782 : && (current[0].isVar() || current[1].isVar())))
731 : : {
732 [ + - ]: 619750 : Trace("circuit-prop")
733 : 0 : << "CircuitPropagator::propagate(): adding to learned: "
734 [ - - ][ - + ]: 309875 : << (assignment ? (Node)current : current.notNode()) << std::endl;
[ - - ]
735 [ + + ]: 309875 : Node lit = assignment ? Node(current) : current.notNode();
736 : :
737 [ + + ]: 309875 : if (isProofEnabled())
738 : : {
739 [ + - ]: 218519 : if (d_epg->hasProofFor(lit))
740 : : {
741 : : // if we have a parent proof generator that provides proofs of the
742 : : // inputs to this class, we must use the lazy proof chain
743 [ + - ]: 218519 : ProofGenerator* pg = d_proofInternal.get();
744 [ + - ]: 218519 : if (d_proofExternal != nullptr)
745 : : {
746 : 218519 : d_proofExternal->addLazyStep(lit, pg);
747 [ + - ]: 218519 : pg = d_proofExternal.get();
748 : : }
749 : 437038 : TrustNode tlit = TrustNode::mkTrustLemma(lit, pg);
750 : 218519 : d_learnedLiterals.push_back(tlit);
751 : : }
752 : : else
753 : : {
754 : 0 : warning() << "CircuitPropagator: Proof is missing for " << lit
755 : 0 : << std::endl;
756 : 0 : TrustNode tlit = TrustNode::mkTrustLemma(lit, nullptr);
757 : 0 : d_learnedLiterals.push_back(tlit);
758 : : }
759 : : }
760 : : else
761 : : {
762 : 182712 : TrustNode tlit = TrustNode::mkTrustLemma(lit, nullptr);
763 : 91356 : d_learnedLiterals.push_back(tlit);
764 : : }
765 [ + - ]: 309875 : Trace("circuit-prop") << "Added proof for " << lit << std::endl;
766 : : }
767 : :
768 : : // Propagate this value to the children (if not an atom or a constant)
769 [ + - ][ + + ]: 723682 : if (d_backwardPropagation && !atom && !current.isConst())
[ + + ][ + + ]
770 : : {
771 : 376478 : propagateBackward(current, assignment);
772 : : }
773 : : // Propagate this value to the parents
774 [ + - ]: 723682 : if (d_forwardPropagation)
775 : : {
776 : 723682 : propagateForward(current, assignment);
777 : : }
778 : : }
779 : :
780 : : // No conflict
781 : 42269 : return d_conflict;
782 : : }
783 : :
784 : 20410 : void CircuitPropagator::enableProofs(context::Context* ctx,
785 : : ProofGenerator* defParent)
786 : : {
787 : 20410 : d_epg.reset(new EagerProofGenerator(d_env, ctx));
788 : 40820 : d_proofInternal.reset(new LazyCDProofChain(
789 [ + - ]: 40820 : d_env, true, ctx, d_epg.get(), true, "CircuitPropInternalLazyChain"));
790 [ + - ]: 20410 : if (defParent != nullptr)
791 : : {
792 : : // If we provide a parent proof generator (defParent), we want the ASSUME
793 : : // leafs of proofs provided by this class to call the getProofFor method on
794 : : // the parent. To do this, we use a LazyCDProofChain.
795 : 40820 : d_proofExternal.reset(new LazyCDProofChain(
796 : 20410 : d_env, true, ctx, defParent, false, "CircuitPropExternalLazyChain"));
797 : : }
798 : 20410 : }
799 : :
800 : 2621980 : bool CircuitPropagator::isProofEnabled() const
801 : : {
802 : 2621980 : return d_proofInternal != nullptr;
803 : : }
804 : :
805 : 695393 : void CircuitPropagator::addProof(TNode f, std::shared_ptr<ProofNode> pf)
806 : : {
807 [ + + ]: 695393 : if (isProofEnabled())
808 : : {
809 [ + + ]: 684810 : if (!d_epg->hasProofFor(f))
810 : : {
811 [ + - ]: 708398 : Trace("circuit-prop") << "Adding proof for " << f << std::endl
812 : 354199 : << "\t" << *pf << std::endl;
813 : 354199 : d_epg->setProofFor(f, std::move(pf));
814 : : }
815 [ - + ]: 330611 : else if (TraceIsOn("circuit-prop"))
816 : : {
817 : 0 : auto prf = d_epg->getProofFor(f);
818 [ - - ]: 0 : Trace("circuit-prop") << "Ignoring proof\n\t" << *pf
819 : 0 : << "\nwe already have\n\t" << *prf << std::endl;
820 : : }
821 : : }
822 : 695393 : }
823 : :
824 : : } // namespace booleans
825 : : } // namespace theory
826 : : } // namespace cvc5::internal
|
