Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * A non-clausal circuit propagator for Boolean simplification.
11 : : */
12 : :
13 : : #include "theory/booleans/circuit_propagator.h"
14 : :
15 : : #include <algorithm>
16 : : #include <stack>
17 : : #include <vector>
18 : :
19 : : #include "expr/node_algorithm.h"
20 : : #include "proof/eager_proof_generator.h"
21 : : #include "proof/proof_node.h"
22 : : #include "proof/proof_node_manager.h"
23 : : #include "theory/booleans/proof_circuit_propagator.h"
24 : : #include "theory/theory.h"
25 : : #include "util/hash.h"
26 : : #include "util/utility.h"
27 : :
28 : : using namespace std;
29 : :
30 : : namespace cvc5::internal {
31 : : namespace theory {
32 : : namespace booleans {
33 : :
34 : 41360 : CircuitPropagator::CircuitPropagator(Env& env,
35 : : bool enableForward,
36 : 41360 : bool enableBackward)
37 : : : EnvObj(env),
38 : 41360 : d_context(),
39 : 41360 : d_propagationQueue(),
40 : 41360 : d_propagationQueueClearer(&d_context, d_propagationQueue),
41 : 41360 : d_conflict(&d_context, TrustNode()),
42 : 41360 : d_learnedLiterals(),
43 : 41360 : d_learnedLiteralClearer(&d_context, d_learnedLiterals),
44 : 41360 : d_backEdges(),
45 : 41360 : d_backEdgesClearer(&d_context, d_backEdges),
46 : 41360 : d_seen(&d_context),
47 : 41360 : d_state(&d_context),
48 : 41360 : d_forwardPropagation(enableForward),
49 : 41360 : d_backwardPropagation(enableBackward),
50 : 41360 : d_needsFinish(false),
51 : 41360 : d_epg(nullptr),
52 : 41360 : d_proofInternal(nullptr),
53 : 82720 : d_proofExternal(nullptr)
54 : : {
55 : 41360 : }
56 : :
57 : 28608 : void CircuitPropagator::initialize()
58 : : {
59 [ + + ]: 28608 : if (d_needsFinish)
60 : : {
61 : 4781 : d_context.pop();
62 : : }
63 : 28608 : d_context.push();
64 : 28608 : d_needsFinish = true;
65 : 28608 : }
66 : :
67 : 421789 : void CircuitPropagator::assertTrue(TNode assertion)
68 : : {
69 [ + - ]: 421789 : Trace("circuit-prop") << "TRUE: " << assertion << std::endl;
70 [ + + ][ - + ]: 421789 : if (assertion.getKind() == Kind::CONST_BOOLEAN && !assertion.getConst<bool>())
[ - + ]
71 : : {
72 : 0 : makeConflict(assertion);
73 : : }
74 [ + + ]: 421789 : else if (assertion.getKind() == Kind::AND)
75 : : {
76 : : ProofCircuitPropagatorBackward prover{
77 : 2176 : d_env.getNodeManager(), d_env.getProofNodeManager(), assertion, true};
78 [ + + ]: 2176 : if (isProofEnabled())
79 : : {
80 : 1507 : addProof(assertion, prover.assume(assertion));
81 : : }
82 [ + + ]: 9015 : for (auto it = assertion.begin(); it != assertion.end(); ++it)
83 : : {
84 : 6839 : addProof(*it, prover.andTrue(it));
85 : 6839 : assertTrue(*it);
86 : : }
87 : 2176 : }
88 : : else
89 : : {
90 : : // Analyze the assertion for back-edges and all that
91 : 419613 : computeBackEdges(assertion);
92 : : // Assign the given assertion to true
93 : 419613 : assignAndEnqueue(assertion,
94 : : true,
95 : 419613 : isProofEnabled()
96 [ + + ][ + + ]: 839226 : ? d_env.getProofNodeManager()->mkAssume(assertion)
[ - - ]
97 : : : nullptr);
98 : : }
99 : 421789 : }
100 : :
101 : 729311 : void CircuitPropagator::assignAndEnqueue(TNode n,
102 : : bool value,
103 : : std::shared_ptr<ProofNode> proof)
104 : : {
105 [ + - ]: 1458622 : Trace("circuit-prop") << "CircuitPropagator::assign(" << n << ", "
106 [ - - ]: 729311 : << (value ? "true" : "false") << ")" << std::endl;
107 : :
108 [ + + ]: 729311 : if (n.getKind() == Kind::CONST_BOOLEAN)
109 : : {
110 : : // Assigning a constant to the opposite value is dumb
111 [ - + ]: 44092 : if (value != n.getConst<bool>())
112 : : {
113 : 0 : makeConflict(n);
114 : 0 : return;
115 : : }
116 : : }
117 : :
118 [ + + ]: 729311 : if (isProofEnabled())
119 : : {
120 [ - + ]: 367315 : if (proof == nullptr)
121 : : {
122 : 0 : warning() << "CircuitPropagator: Proof is missing for " << n << std::endl;
123 : 0 : DebugUnhandled();
124 : : }
125 : : else
126 : : {
127 [ - + ][ - + ]: 367315 : Assert(!proof->getResult().isNull());
[ - - ]
128 [ + + ]: 367315 : Node expected = value ? Node(n) : n.negate();
129 [ - + ]: 367315 : if (proof->getResult() != expected)
130 : : {
131 : 0 : warning() << "CircuitPropagator: Incorrect proof: " << expected
132 : 0 : << " vs. " << proof->getResult() << std::endl
133 : 0 : << *proof << std::endl;
134 : : }
135 : 367315 : addProof(expected, std::move(proof));
136 : 367315 : }
137 : : }
138 : :
139 : : // Get the current assignment
140 : 729311 : AssignmentStatus state = d_state[n];
141 : :
142 [ + + ]: 729311 : if (state != UNASSIGNED)
143 : : {
144 : : // If the node is already assigned we might have a conflict
145 [ + + ]: 215526 : if (value != (state == ASSIGNED_TO_TRUE))
146 : : {
147 : 1380 : makeConflict(n);
148 : : }
149 : : }
150 : : else
151 : : {
152 : : // If unassigned, mark it as assigned
153 [ + + ]: 513785 : d_state[n] = value ? ASSIGNED_TO_TRUE : ASSIGNED_TO_FALSE;
154 : : // Add for further propagation
155 : 513785 : d_propagationQueue.push_back(n);
156 : : }
157 : : }
158 : :
159 : 1380 : void CircuitPropagator::makeConflict(Node n)
160 : : {
161 : 1380 : auto bfalse = nodeManager()->mkConst(false);
162 : 1380 : ProofGenerator* g = nullptr;
163 [ + + ]: 1380 : if (isProofEnabled())
164 : : {
165 [ + + ]: 866 : if (d_epg->hasProofFor(bfalse))
166 : : {
167 : 30 : return;
168 : : }
169 : 836 : ProofCircuitPropagator pcp(d_env.getNodeManager(),
170 : 836 : d_env.getProofNodeManager());
171 [ - + ]: 836 : if (n == bfalse)
172 : : {
173 : 0 : d_epg->setProofFor(bfalse, pcp.assume(bfalse));
174 : : }
175 : : else
176 : : {
177 : : // Use nPf to ensure deterministic node ID assignments
178 : 836 : Pf nPf = pcp.assume(n);
179 : 836 : d_epg->setProofFor(bfalse, pcp.conflict(nPf, pcp.assume(n.negate())));
180 : 836 : }
181 [ + - ]: 836 : g = d_proofInternal.get();
182 : 1672 : Trace("circuit-prop") << "Added conflict " << *d_epg->getProofFor(bfalse)
183 : 836 : << std::endl;
184 : 1672 : Trace("circuit-prop") << "\texpanded " << *g->getProofFor(bfalse)
185 : 836 : << std::endl;
186 : : }
187 : 1350 : d_conflict = TrustNode::mkTrustLemma(bfalse, g);
188 [ + + ]: 1380 : }
189 : :
190 : 419613 : void CircuitPropagator::computeBackEdges(TNode node)
191 : : {
192 [ + - ]: 839226 : Trace("circuit-prop") << "CircuitPropagator::computeBackEdges(" << node << ")"
193 : 419613 : << endl;
194 : :
195 : : // Vector of nodes to visit
196 : 419613 : vector<TNode> toVisit;
197 : :
198 : : // Start with the top node
199 [ + + ]: 419613 : if (d_seen.find(node) == d_seen.end())
200 : : {
201 : 389628 : toVisit.push_back(node);
202 : 389628 : d_seen.insert(node);
203 : : }
204 : :
205 : : // Initialize the back-edges for the root, so we don't have a special case
206 : 419613 : d_backEdges[node];
207 : :
208 : : // Go through the visit list
209 [ + + ]: 1420867 : for (unsigned i = 0; i < toVisit.size(); ++i)
210 : : {
211 : : // Node we need to visit
212 : 1001254 : TNode current = toVisit[i];
213 [ + - ]: 2002508 : Trace("circuit-prop")
214 : 0 : << "CircuitPropagator::computeBackEdges(): processing " << current
215 : 1001254 : << endl;
216 [ - + ][ - + ]: 1001254 : 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 [ + + ]: 1001254 : if (Theory::theoryOf(current) == THEORY_BOOL)
220 : : {
221 : 2037939 : for (unsigned child = 0, child_end = current.getNumChildren();
222 [ + + ]: 2037939 : child < child_end;
223 : : ++child)
224 : : {
225 : 1376473 : TNode childNode = current[child];
226 : : // Add the back edge
227 : 1376473 : d_backEdges[childNode].push_back(current);
228 : : // Add to the queue if not seen yet
229 [ + + ]: 1376473 : if (d_seen.find(childNode) == d_seen.end())
230 : : {
231 : 611626 : toVisit.push_back(childNode);
232 : 611626 : d_seen.insert(childNode);
233 : : }
234 : 1376473 : }
235 : : }
236 : 1001254 : }
237 : 419613 : }
238 : :
239 : 280271 : void CircuitPropagator::propagateBackward(TNode parent, bool parentAssignment)
240 : : {
241 [ + - ]: 560542 : Trace("circuit-prop") << "CircuitPropagator::propagateBackward(" << parent
242 : 280271 : << ", " << parentAssignment << ")" << endl;
243 : 280271 : ProofCircuitPropagatorBackward prover{d_env.getNodeManager(),
244 : 280271 : d_env.getProofNodeManager(),
245 : : parent,
246 : 280271 : parentAssignment};
247 : :
248 : : // backward rules
249 [ + + ][ + + ]: 280271 : switch (parent.getKind())
[ + + ][ + - ]
250 : : {
251 : 10678 : case Kind::AND:
252 [ + + ]: 10678 : if (parentAssignment)
253 : : {
254 : : // AND = TRUE: forall children c, assign(c = TRUE)
255 : 2124 : for (TNode::iterator i = parent.begin(), i_end = parent.end();
256 [ + + ]: 38094 : i != i_end;
257 : 35970 : ++i)
258 : : {
259 : 35970 : 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 : 8554 : find_if_unique(parent.begin(), parent.end(), [this](TNode x) {
267 : 18684 : return !isAssignedTo(x, true);
268 : : });
269 [ + + ]: 8554 : if (holdout != parent.end())
270 : : {
271 : 1036 : assignAndEnqueue(*holdout, false, prover.andFalse(parent, holdout));
272 : : }
273 : : }
274 : 10678 : break;
275 : 197359 : case Kind::OR:
276 [ + + ]: 197359 : if (parentAssignment)
277 : : {
278 : : // OR = TRUE: if all children BUT ONE == FALSE, assign(c = TRUE)
279 : : TNode::iterator holdout =
280 : 195483 : find_if_unique(parent.begin(), parent.end(), [this](TNode x) {
281 : 394031 : return !isAssignedTo(x, false);
282 : : });
283 [ + + ]: 195483 : if (holdout != parent.end())
284 : : {
285 : 1592 : assignAndEnqueue(*holdout, true, prover.orTrue(parent, holdout));
286 : : }
287 : : }
288 : : else
289 : : {
290 : : // OR = FALSE: forall children c, assign(c = FALSE)
291 : 1876 : for (TNode::iterator i = parent.begin(), i_end = parent.end();
292 [ + + ]: 10607 : i != i_end;
293 : 8731 : ++i)
294 : : {
295 : 8731 : assignAndEnqueue(*i, false, prover.orFalse(i));
296 : : }
297 : : }
298 : 197359 : break;
299 : 58822 : case Kind::NOT:
300 : : // NOT = b: assign(c = !b)
301 : 58822 : assignAndEnqueue(
302 : 117644 : parent[0], !parentAssignment, prover.Not(!parentAssignment, parent));
303 : 58822 : break;
304 : 2634 : case Kind::ITE:
305 [ + + ]: 2634 : if (isAssignedTo(parent[0], true))
306 : : {
307 : : // ITE c x y = v: if c is assigned and TRUE, assign(x = v)
308 : 151 : assignAndEnqueue(parent[1], parentAssignment, prover.iteC(true));
309 : : }
310 [ + + ]: 2483 : else if (isAssignedTo(parent[0], false))
311 : : {
312 : : // ITE c x y = v: if c is assigned and FALSE, assign(y = v)
313 : 47 : assignAndEnqueue(parent[2], parentAssignment, prover.iteC(false));
314 : : }
315 : 2436 : else if (isAssigned(parent[1]) && isAssigned(parent[2]))
316 : : {
317 [ + + ][ - - ]: 30 : if (getAssignment(parent[1]) == parentAssignment
318 [ + + ][ + + ]: 30 : && 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 : 6 : assignAndEnqueue(parent[0], true, prover.iteIsCase(1));
323 : : }
324 [ + + ][ - - ]: 24 : else if (getAssignment(parent[1]) != parentAssignment
325 [ + + ][ + + ]: 24 : && 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 : 4 : assignAndEnqueue(parent[0], false, prover.iteIsCase(0));
330 : : }
331 : : }
332 : 2634 : break;
333 : 5138 : case Kind::EQUAL:
334 [ - + ][ - + ]: 5138 : Assert(parent[0].getType().isBoolean());
[ - - ]
335 [ + + ]: 5138 : if (parentAssignment)
336 : : {
337 : : // IFF x y = TRUE: if x [resp y] is assigned, assign(y = x.assignment
338 : : // [resp x = y.assignment])
339 [ + + ]: 4257 : if (isAssigned(parent[0]))
340 : : {
341 : 389 : assignAndEnqueue(parent[1],
342 : 778 : getAssignment(parent[0]),
343 : 778 : prover.eqYFromX(getAssignment(parent[0]), parent));
344 : : }
345 [ + + ]: 3868 : else if (isAssigned(parent[1]))
346 : : {
347 : 15 : assignAndEnqueue(parent[0],
348 : 30 : getAssignment(parent[1]),
349 : 30 : 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 [ + + ]: 881 : if (isAssigned(parent[0]))
357 : : {
358 : 35 : assignAndEnqueue(parent[1],
359 : 70 : !getAssignment(parent[0]),
360 : 70 : prover.neqYFromX(getAssignment(parent[0]), parent));
361 : : }
362 [ + + ]: 846 : else if (isAssigned(parent[1]))
363 : : {
364 : 14 : assignAndEnqueue(parent[0],
365 : 28 : !getAssignment(parent[1]),
366 : 28 : prover.neqXFromY(getAssignment(parent[1]), parent));
367 : : }
368 : : }
369 : 5138 : break;
370 : 5308 : case Kind::IMPLIES:
371 [ + + ]: 5308 : if (parentAssignment)
372 : : {
373 [ + + ]: 3649 : if (isAssignedTo(parent[0], true))
374 : : {
375 : : // IMPLIES x y = TRUE, and x == TRUE: assign(y = TRUE)
376 : 951 : assignAndEnqueue(parent[1], true, prover.impliesYFromX(parent));
377 : : }
378 [ + + ]: 3649 : if (isAssignedTo(parent[1], false))
379 : : {
380 : : // IMPLIES x y = TRUE, and y == FALSE: assign(x = FALSE)
381 : 191 : 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 : 1659 : assignAndEnqueue(parent[0], true, prover.impliesNegX());
388 : 1659 : assignAndEnqueue(parent[1], false, prover.impliesNegY());
389 : : }
390 : 5308 : break;
391 : 332 : case Kind::XOR:
392 [ + + ]: 332 : if (parentAssignment)
393 : : {
394 [ + + ]: 235 : 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 [ + + ]: 219 : else if (isAssigned(parent[1]))
404 : : {
405 : : // XOR x y = TRUE, and y assigned, assign(x = !assignment(y))
406 : 44 : assignAndEnqueue(
407 : : parent[0],
408 : 88 : !getAssignment(parent[1]),
409 : 132 : prover.xorXFromY(
410 : 88 : !parentAssignment, getAssignment(parent[1]), parent));
411 : : }
412 : : }
413 : : else
414 : : {
415 [ + + ]: 97 : if (isAssigned(parent[0]))
416 : : {
417 : : // XOR x y = FALSE, and x assigned, assign(y = assignment(x))
418 : 29 : assignAndEnqueue(
419 : : parent[1],
420 : 58 : getAssignment(parent[0]),
421 : 87 : prover.xorYFromX(
422 : 58 : !parentAssignment, getAssignment(parent[0]), parent));
423 : : }
424 [ + + ]: 68 : else if (isAssigned(parent[1]))
425 : : {
426 : : // XOR x y = FALSE, and y assigned, assign(x = assignment(y))
427 : 32 : assignAndEnqueue(
428 : : parent[0],
429 : 64 : getAssignment(parent[1]),
430 : 96 : prover.xorXFromY(
431 : 64 : !parentAssignment, getAssignment(parent[1]), parent));
432 : : }
433 : : }
434 : 332 : break;
435 : 0 : default: Unhandled();
436 : : }
437 : 280271 : }
438 : :
439 : 506295 : void CircuitPropagator::propagateForward(TNode child, bool childAssignment)
440 : : {
441 : : // The assignment we have
442 [ + - ]: 1012590 : Trace("circuit-prop") << "CircuitPropagator::propagateForward(" << child
443 : 506295 : << ", " << childAssignment << ")" << endl;
444 : :
445 : : // Get the back any nodes where this is child
446 : 506295 : const vector<Node>& parents = d_backEdges.find(child)->second;
447 : :
448 : : // Go through the parents and see if there is anything to propagate
449 : 506295 : vector<Node>::const_iterator parent_it = parents.begin();
450 : 506295 : vector<Node>::const_iterator parent_it_end = parents.end();
451 [ + + ][ + + ]: 752979 : for (; parent_it != parent_it_end && d_conflict.get().isNull(); ++parent_it)
[ + + ]
452 : : {
453 : : // The current parent of the child
454 : 246684 : TNode parent = *parent_it;
455 [ + - ]: 246684 : Trace("circuit-prop") << "Parent: " << parent << endl;
456 [ - + ][ - + ]: 246684 : Assert(expr::hasSubterm(parent, child));
[ - - ]
457 : :
458 : : ProofCircuitPropagatorForward prover{
459 : 493368 : d_env.getNodeManager(), d_env.getProofNodeManager(), child, parent};
460 : :
461 : : // Forward rules
462 [ + + ][ + + ]: 246684 : switch (parent.getKind())
[ + + ][ + - ]
463 : : {
464 : 57070 : case Kind::AND:
465 [ + + ]: 57070 : if (childAssignment)
466 : : {
467 : 49354 : TNode::iterator holdout;
468 : 49354 : holdout = find_if(parent.begin(), parent.end(), [this](TNode x) {
469 : 17120915 : return !isAssignedTo(x, true);
470 : : });
471 : :
472 [ + + ]: 49354 : if (holdout == parent.end())
473 : : { // all children are assigned TRUE
474 : : // AND ...(x=TRUE)...: if all children now assigned to TRUE,
475 : : // assign(AND = TRUE)
476 : 30766 : assignAndEnqueue(parent, true, prover.andAllTrue());
477 : : }
478 [ + + ]: 18588 : else if (isAssignedTo(parent, false))
479 : : { // the AND is FALSE
480 : : // is the holdout unique ?
481 : : TNode::iterator other =
482 : 2188 : find_if(holdout + 1, parent.end(), [this](TNode x) {
483 : 2508 : return !isAssignedTo(x, true);
484 : : });
485 [ + + ]: 2188 : if (other == parent.end())
486 : : { // the holdout is unique
487 : : // AND ...(x=TRUE)...: if all children BUT ONE now assigned to
488 : : // TRUE, and AND == FALSE, assign(last_holdout = FALSE)
489 : 715 : assignAndEnqueue(
490 : 1430 : *holdout, false, prover.andFalse(parent, holdout));
491 : : }
492 : : }
493 : : }
494 : : else
495 : : {
496 : : // AND ...(x=FALSE)...: assign(AND = FALSE)
497 : 7716 : assignAndEnqueue(parent, false, prover.andOneFalse());
498 : : }
499 : 57070 : break;
500 : 119336 : case Kind::OR:
501 [ + + ]: 119336 : if (childAssignment)
502 : : {
503 : : // OR ...(x=TRUE)...: assign(OR = TRUE)
504 : 62658 : assignAndEnqueue(parent, true, prover.orOneTrue());
505 : : }
506 : : else
507 : : {
508 : 56678 : TNode::iterator holdout;
509 : 56678 : holdout = find_if(parent.begin(), parent.end(), [this](TNode x) {
510 : 1375869 : return !isAssignedTo(x, false);
511 : : });
512 [ + + ]: 56678 : if (holdout == parent.end())
513 : : { // all children are assigned FALSE
514 : : // OR ...(x=FALSE)...: if all children now assigned to FALSE,
515 : : // assign(OR = FALSE)
516 : 8551 : assignAndEnqueue(parent, false, prover.orFalse());
517 : : }
518 [ + + ]: 48127 : else if (isAssignedTo(parent, true))
519 : : { // the OR is TRUE
520 : : // is the holdout unique ?
521 : : TNode::iterator other =
522 : 41410 : find_if(holdout + 1, parent.end(), [this](TNode x) {
523 : 48223 : return !isAssignedTo(x, false);
524 : : });
525 [ + + ]: 41410 : if (other == parent.end())
526 : : { // the holdout is unique
527 : : // OR ...(x=FALSE)...: if all children BUT ONE now assigned to
528 : : // FALSE, and OR == TRUE, assign(last_holdout = TRUE)
529 : 22142 : assignAndEnqueue(*holdout, true, prover.orTrue(parent, holdout));
530 : : }
531 : : }
532 : : }
533 : 119336 : break;
534 : :
535 : 58025 : case Kind::NOT:
536 : : // NOT (x=b): assign(NOT = !b)
537 : 58025 : assignAndEnqueue(
538 : 116050 : parent, !childAssignment, prover.Not(childAssignment, parent));
539 : 58025 : break;
540 : :
541 : 1083 : case Kind::ITE:
542 [ + + ]: 1083 : if (child == parent[0])
543 : : {
544 [ + + ]: 379 : if (childAssignment)
545 : : {
546 [ + + ]: 300 : if (isAssigned(parent[1]))
547 : : {
548 : : // ITE (c=TRUE) x y: if x is assigned, assign(ITE = x.assignment)
549 : 158 : assignAndEnqueue(parent,
550 : 316 : getAssignment(parent[1]),
551 : 316 : prover.iteEvalThen(getAssignment(parent[1])));
552 : : }
553 : : }
554 : : else
555 : : {
556 [ + + ]: 79 : if (isAssigned(parent[2]))
557 : : {
558 : : // ITE (c=FALSE) x y: if y is assigned, assign(ITE = y.assignment)
559 : 69 : assignAndEnqueue(parent,
560 : 138 : getAssignment(parent[2]),
561 : 138 : prover.iteEvalElse(getAssignment(parent[2])));
562 : : }
563 : : }
564 : : }
565 [ + + ]: 1083 : if (child == parent[1])
566 : : {
567 [ + + ]: 336 : if (isAssignedTo(parent[0], true))
568 : : {
569 : : // ITE c (x=v) y: if c is assigned and TRUE, assign(ITE = v)
570 : 162 : assignAndEnqueue(
571 : 324 : parent, childAssignment, prover.iteEvalThen(childAssignment));
572 : : }
573 : : }
574 [ + + ]: 1083 : if (child == parent[2])
575 : : {
576 [ - + ][ - + ]: 368 : Assert(child == parent[2]);
[ - - ]
577 [ + + ]: 368 : if (isAssignedTo(parent[0], false))
578 : : {
579 : : // ITE c x (y=v): if c is assigned and FALSE, assign(ITE = v)
580 : 63 : assignAndEnqueue(
581 : 126 : parent, childAssignment, prover.iteEvalElse(childAssignment));
582 : : }
583 : : }
584 : 1083 : break;
585 : 2804 : case Kind::EQUAL:
586 [ - + ][ - + ]: 2804 : Assert(parent[0].getType().isBoolean());
[ - - ]
587 : 2804 : if (isAssigned(parent[0]) && isAssigned(parent[1]))
588 : : {
589 : : // IFF x y: if x and y is assigned, assign(IFF = (x.assignment <=>
590 : : // y.assignment))
591 : 1451 : assignAndEnqueue(parent,
592 : 2902 : getAssignment(parent[0]) == getAssignment(parent[1]),
593 : 2902 : prover.eqEval(getAssignment(parent[0]),
594 : 2902 : getAssignment(parent[1])));
595 : : }
596 : : else
597 : : {
598 [ + + ]: 1353 : if (isAssigned(parent))
599 : : {
600 [ + + ]: 673 : if (child == parent[0])
601 : : {
602 [ + + ]: 464 : if (getAssignment(parent))
603 : : {
604 : : // IFF (x = b) y: if IFF is assigned to TRUE, assign(y = b)
605 : 434 : assignAndEnqueue(parent[1],
606 : : childAssignment,
607 : 868 : prover.eqYFromX(childAssignment, parent));
608 : : }
609 : : else
610 : : {
611 : : // IFF (x = b) y: if IFF is assigned to FALSE, assign(y = !b)
612 : 30 : assignAndEnqueue(parent[1],
613 : 30 : !childAssignment,
614 : 60 : prover.neqYFromX(childAssignment, parent));
615 : : }
616 : : }
617 : : else
618 : : {
619 [ - + ][ - + ]: 209 : Assert(child == parent[1]);
[ - - ]
620 [ + + ]: 209 : if (getAssignment(parent))
621 : : {
622 : : // IFF x y = b: if IFF is assigned to TRUE, assign(x = b)
623 : 198 : assignAndEnqueue(parent[0],
624 : : childAssignment,
625 : 396 : prover.eqXFromY(childAssignment, parent));
626 : : }
627 : : else
628 : : {
629 : : // IFF x y = b y: if IFF is assigned to FALSE, assign(x = !b)
630 : 11 : assignAndEnqueue(parent[0],
631 : 11 : !childAssignment,
632 : 22 : prover.neqXFromY(childAssignment, parent));
633 : : }
634 : : }
635 : : }
636 : : }
637 : 2804 : break;
638 : 7949 : case Kind::IMPLIES:
639 : 7949 : if (isAssigned(parent[0]) && isAssigned(parent[1]))
640 : : {
641 : : // IMPLIES (x=v1) (y=v2): assign(IMPLIES = (!v1 || v2))
642 : 4555 : assignAndEnqueue(
643 : : parent,
644 : 9110 : !getAssignment(parent[0]) || getAssignment(parent[1]),
645 : 9110 : prover.impliesEval(getAssignment(parent[0]),
646 : 9110 : getAssignment(parent[1])));
647 : : }
648 : : else
649 : : {
650 [ + + ][ + + ]: 5714 : if (child == parent[0] && childAssignment
[ - - ]
651 [ + + ][ + + ]: 5714 : && isAssignedTo(parent, true))
[ + + ][ + - ]
[ - - ]
652 : : {
653 : : // IMPLIES (x=TRUE) y [with IMPLIES == TRUE]: assign(y = TRUE)
654 : 200 : assignAndEnqueue(parent[1], true, prover.impliesYFromX(parent));
655 : : }
656 [ + + ][ + + ]: 4468 : if (child == parent[1] && !childAssignment
[ - - ]
657 [ + + ][ + + ]: 4468 : && isAssignedTo(parent, true))
[ + + ][ + - ]
[ - - ]
658 : : {
659 : : // IMPLIES x (y=FALSE) [with IMPLIES == TRUE]: assign(x = FALSE)
660 : 16 : assignAndEnqueue(parent[0], false, prover.impliesXFromY(parent));
661 : : }
662 : : // Note that IMPLIES == FALSE doesn't need any cases here
663 : : // because if that assignment has been done, we've already
664 : : // propagated all the children (in back-propagation).
665 : : }
666 : 7949 : break;
667 : 417 : case Kind::XOR:
668 [ + + ]: 417 : if (isAssigned(parent))
669 : : {
670 [ + + ]: 185 : if (child == parent[0])
671 : : {
672 : : // XOR (x=v) y [with XOR assigned], assign(y = (v ^ XOR)
673 : 115 : assignAndEnqueue(
674 : : parent[1],
675 : 230 : childAssignment != getAssignment(parent),
676 : 345 : prover.xorYFromX(
677 : 230 : !getAssignment(parent), childAssignment, parent));
678 : : }
679 : : else
680 : : {
681 [ - + ][ - + ]: 70 : Assert(child == parent[1]);
[ - - ]
682 : : // XOR x (y=v) [with XOR assigned], assign(x = (v ^ XOR))
683 : 70 : assignAndEnqueue(
684 : : parent[0],
685 : 140 : childAssignment != getAssignment(parent),
686 : 210 : prover.xorXFromY(
687 : 140 : !getAssignment(parent), childAssignment, parent));
688 : : }
689 : : }
690 : 417 : if (isAssigned(parent[0]) && isAssigned(parent[1]))
691 : : {
692 : 200 : assignAndEnqueue(parent,
693 : 400 : getAssignment(parent[0]) != getAssignment(parent[1]),
694 : 400 : prover.xorEval(getAssignment(parent[0]),
695 : 400 : getAssignment(parent[1])));
696 : : }
697 : 417 : break;
698 : 0 : default: Unhandled();
699 : : }
700 : 246684 : }
701 : 506295 : }
702 : :
703 : 28608 : TrustNode CircuitPropagator::propagate()
704 : : {
705 [ + - ]: 28608 : Trace("circuit-prop") << "CircuitPropagator::propagate()" << std::endl;
706 : :
707 : 534903 : for (unsigned i = 0;
708 [ + + ][ + + ]: 534903 : i < d_propagationQueue.size() && d_conflict.get().isNull();
[ + + ]
709 : : ++i)
710 : : {
711 : : // The current node we are propagating
712 : 506295 : TNode current = d_propagationQueue[i];
713 [ + - ]: 1012590 : Trace("circuit-prop") << "CircuitPropagator::propagate(): processing "
714 : 506295 : << current << std::endl;
715 : 506295 : bool assignment = getAssignment(current);
716 [ + - ]: 1012590 : Trace("circuit-prop") << "CircuitPropagator::propagate(): assigned to "
717 [ - - ]: 506295 : << (assignment ? "true" : "false") << std::endl;
718 : :
719 : : // Is this an atom
720 [ + + ][ - - ]: 830703 : bool atom = Theory::theoryOf(current) != THEORY_BOOL || current.isVar()
721 [ + + ][ + + ]: 836455 : || (current.getKind() == Kind::EQUAL
722 : 512047 : && (current[0].isVar() && current[1].isVar()));
723 : :
724 : : // If an atom, add to the list for simplification
725 : 506295 : if (atom
726 [ + + ][ + + ]: 511433 : || (current.getKind() == Kind::EQUAL
727 : 511433 : && (current[0].isVar() || current[1].isVar())))
728 : : {
729 [ + - ]: 402600 : Trace("circuit-prop")
730 : 0 : << "CircuitPropagator::propagate(): adding to learned: "
731 [ - - ][ - + ]: 201300 : << (assignment ? (Node)current : current.notNode()) << std::endl;
[ - - ]
732 [ + + ]: 201300 : Node lit = assignment ? Node(current) : current.notNode();
733 : :
734 [ + + ]: 201300 : if (isProofEnabled())
735 : : {
736 [ + - ]: 130505 : if (d_epg->hasProofFor(lit))
737 : : {
738 : : // if we have a parent proof generator that provides proofs of the
739 : : // inputs to this class, we must use the lazy proof chain
740 [ + - ]: 130505 : ProofGenerator* pg = d_proofInternal.get();
741 [ + - ]: 130505 : if (d_proofExternal != nullptr)
742 : : {
743 : 130505 : d_proofExternal->addLazyStep(lit, pg);
744 [ + - ]: 130505 : pg = d_proofExternal.get();
745 : : }
746 : 130505 : TrustNode tlit = TrustNode::mkTrustLemma(lit, pg);
747 : 130505 : d_learnedLiterals.push_back(tlit);
748 : 130505 : }
749 : : else
750 : : {
751 : 0 : warning() << "CircuitPropagator: Proof is missing for " << lit
752 : 0 : << std::endl;
753 : 0 : TrustNode tlit = TrustNode::mkTrustLemma(lit, nullptr);
754 : 0 : d_learnedLiterals.push_back(tlit);
755 : 0 : }
756 : : }
757 : : else
758 : : {
759 : 70795 : TrustNode tlit = TrustNode::mkTrustLemma(lit, nullptr);
760 : 70795 : d_learnedLiterals.push_back(tlit);
761 : 70795 : }
762 [ + - ]: 201300 : Trace("circuit-prop") << "Added proof for " << lit << std::endl;
763 : 201300 : }
764 : :
765 : : // Propagate this value to the children (if not an atom or a constant)
766 [ + - ][ + + ]: 506295 : if (d_backwardPropagation && !atom && !current.isConst())
[ + + ][ + + ]
767 : : {
768 : 280271 : propagateBackward(current, assignment);
769 : : }
770 : : // Propagate this value to the parents
771 [ + - ]: 506295 : if (d_forwardPropagation)
772 : : {
773 : 506295 : propagateForward(current, assignment);
774 : : }
775 : 506295 : }
776 : :
777 : : // No conflict
778 : 28608 : return d_conflict;
779 : : }
780 : :
781 : 15169 : void CircuitPropagator::enableProofs(context::Context* ctx,
782 : : ProofGenerator* defParent)
783 : : {
784 : 15169 : d_epg.reset(new EagerProofGenerator(d_env, ctx));
785 [ + - ]: 30338 : d_proofInternal.reset(new LazyCDProofChain(
786 : 30338 : d_env, true, ctx, d_epg.get(), true, "CircuitPropInternalLazyChain"));
787 [ + - ]: 15169 : if (defParent != nullptr)
788 : : {
789 : : // If we provide a parent proof generator (defParent), we want the ASSUME
790 : : // leafs of proofs provided by this class to call the getProofFor method on
791 : : // the parent. To do this, we use a LazyCDProofChain.
792 : 30338 : d_proofExternal.reset(new LazyCDProofChain(
793 : 15169 : d_env, true, ctx, defParent, false, "CircuitPropExternalLazyChain"));
794 : : }
795 : 15169 : }
796 : :
797 : 1729441 : bool CircuitPropagator::isProofEnabled() const
798 : : {
799 : 1729441 : return d_proofInternal != nullptr;
800 : : }
801 : :
802 : 375661 : void CircuitPropagator::addProof(TNode f, std::shared_ptr<ProofNode> pf)
803 : : {
804 [ + + ]: 375661 : if (isProofEnabled())
805 : : {
806 [ + + ]: 373587 : if (!d_epg->hasProofFor(f))
807 : : {
808 [ + - ]: 495926 : Trace("circuit-prop") << "Adding proof for " << f << std::endl
809 : 247963 : << "\t" << *pf << std::endl;
810 : 247963 : d_epg->setProofFor(f, std::move(pf));
811 : : }
812 [ - + ]: 125624 : else if (TraceIsOn("circuit-prop"))
813 : : {
814 : 0 : auto prf = d_epg->getProofFor(f);
815 [ - - ]: 0 : Trace("circuit-prop") << "Ignoring proof\n\t" << *pf
816 : 0 : << "\nwe already have\n\t" << *prf << std::endl;
817 : 0 : }
818 : : }
819 : 375661 : }
820 : :
821 : : } // namespace booleans
822 : : } // namespace theory
823 : : } // namespace cvc5::internal
|
