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 : 74489 : CircuitPropagator::CircuitPropagator(Env& env, bool enableForward, bool enableBackward)
38 : : : EnvObj(env),
39 : 74489 : d_context(),
40 : 74489 : d_propagationQueue(),
41 : 74489 : d_propagationQueueClearer(&d_context, d_propagationQueue),
42 : 74489 : d_conflict(&d_context, TrustNode()),
43 : 74489 : d_learnedLiterals(),
44 : 74489 : d_learnedLiteralClearer(&d_context, d_learnedLiterals),
45 : 74489 : d_backEdges(),
46 : 74489 : d_backEdgesClearer(&d_context, d_backEdges),
47 : 74489 : d_seen(&d_context),
48 : 74489 : d_state(&d_context),
49 : 74489 : d_forwardPropagation(enableForward),
50 : 74489 : d_backwardPropagation(enableBackward),
51 : 74489 : d_needsFinish(false),
52 : 74489 : d_epg(nullptr),
53 : 74489 : d_proofInternal(nullptr),
54 : 148978 : d_proofExternal(nullptr)
55 : : {
56 : 74489 : }
57 : :
58 : 40059 : void CircuitPropagator::initialize()
59 : : {
60 [ + + ]: 40059 : if (d_needsFinish)
61 : : {
62 : 6732 : d_context.pop();
63 : : }
64 : 40059 : d_context.push();
65 : 40059 : d_needsFinish = true;
66 : 40059 : }
67 : :
68 : 455854 : void CircuitPropagator::assertTrue(TNode assertion)
69 : : {
70 [ + - ]: 455854 : Trace("circuit-prop") << "TRUE: " << assertion << std::endl;
71 [ + + ][ - + ]: 455854 : if (assertion.getKind() == Kind::CONST_BOOLEAN && !assertion.getConst<bool>())
[ - + ]
72 : : {
73 : 0 : makeConflict(assertion);
74 : : }
75 [ + + ]: 455854 : else if (assertion.getKind() == Kind::AND)
76 : : {
77 : : ProofCircuitPropagatorBackward prover{
78 : 2184 : d_env.getNodeManager(), d_env.getProofNodeManager(), assertion, true};
79 [ + + ]: 2184 : if (isProofEnabled())
80 : : {
81 : 1352 : addProof(assertion, prover.assume(assertion));
82 : : }
83 [ + + ]: 9205 : for (auto it = assertion.begin(); it != assertion.end(); ++it)
84 : : {
85 : 7021 : addProof(*it, prover.andTrue(it));
86 : 7021 : assertTrue(*it);
87 : : }
88 : 2184 : }
89 : : else
90 : : {
91 : : // Analyze the assertion for back-edges and all that
92 : 453670 : computeBackEdges(assertion);
93 : : // Assign the given assertion to true
94 : 453670 : assignAndEnqueue(assertion,
95 : : true,
96 : 453670 : isProofEnabled()
97 [ + + ][ + + ]: 907340 : ? d_env.getProofNodeManager()->mkAssume(assertion)
[ - - ]
98 : : : nullptr);
99 : : }
100 : 455854 : }
101 : :
102 : 779888 : void CircuitPropagator::assignAndEnqueue(TNode n,
103 : : bool value,
104 : : std::shared_ptr<ProofNode> proof)
105 : : {
106 [ + - ]: 1559776 : Trace("circuit-prop") << "CircuitPropagator::assign(" << n << ", "
107 [ - - ]: 779888 : << (value ? "true" : "false") << ")" << std::endl;
108 : :
109 [ + + ]: 779888 : if (n.getKind() == Kind::CONST_BOOLEAN)
110 : : {
111 : : // Assigning a constant to the opposite value is dumb
112 [ - + ]: 59008 : if (value != n.getConst<bool>())
113 : : {
114 : 0 : makeConflict(n);
115 : 0 : return;
116 : : }
117 : : }
118 : :
119 [ + + ]: 779888 : if (isProofEnabled())
120 : : {
121 [ - + ]: 381404 : if (proof == nullptr)
122 : : {
123 : 0 : warning() << "CircuitPropagator: Proof is missing for " << n << std::endl;
124 : 0 : DebugUnhandled();
125 : : }
126 : : else
127 : : {
128 [ - + ][ - + ]: 381404 : Assert(!proof->getResult().isNull());
[ - - ]
129 [ + + ]: 381404 : Node expected = value ? Node(n) : n.negate();
130 [ - + ]: 381404 : 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 : 381404 : addProof(expected, std::move(proof));
137 : 381404 : }
138 : : }
139 : :
140 : : // Get the current assignment
141 : 779888 : AssignmentStatus state = d_state[n];
142 : :
143 [ + + ]: 779888 : if (state != UNASSIGNED)
144 : : {
145 : : // If the node is already assigned we might have a conflict
146 [ + + ]: 228282 : if (value != (state == ASSIGNED_TO_TRUE))
147 : : {
148 : 2256 : makeConflict(n);
149 : : }
150 : : }
151 : : else
152 : : {
153 : : // If unassigned, mark it as assigned
154 [ + + ]: 551606 : d_state[n] = value ? ASSIGNED_TO_TRUE : ASSIGNED_TO_FALSE;
155 : : // Add for further propagation
156 : 551606 : d_propagationQueue.push_back(n);
157 : : }
158 : : }
159 : :
160 : 2256 : void CircuitPropagator::makeConflict(Node n)
161 : : {
162 : 2256 : auto bfalse = nodeManager()->mkConst(false);
163 : 2256 : ProofGenerator* g = nullptr;
164 [ + + ]: 2256 : if (isProofEnabled())
165 : : {
166 [ + + ]: 1134 : if (d_epg->hasProofFor(bfalse))
167 : : {
168 : 30 : return;
169 : : }
170 : 1104 : ProofCircuitPropagator pcp(d_env.getNodeManager(),
171 : 1104 : d_env.getProofNodeManager());
172 [ - + ]: 1104 : if (n == bfalse)
173 : : {
174 : 0 : d_epg->setProofFor(bfalse, pcp.assume(bfalse));
175 : : }
176 : : else
177 : : {
178 : 2208 : d_epg->setProofFor(bfalse,
179 : 2208 : pcp.conflict(pcp.assume(n), pcp.assume(n.negate())));
180 : : }
181 [ + - ]: 1104 : g = d_proofInternal.get();
182 : 2208 : Trace("circuit-prop") << "Added conflict " << *d_epg->getProofFor(bfalse)
183 : 1104 : << std::endl;
184 : 2208 : Trace("circuit-prop") << "\texpanded " << *g->getProofFor(bfalse)
185 : 1104 : << std::endl;
186 : : }
187 : 2226 : d_conflict = TrustNode::mkTrustLemma(bfalse, g);
188 [ + + ]: 2256 : }
189 : :
190 : 453670 : void CircuitPropagator::computeBackEdges(TNode node)
191 : : {
192 [ + - ]: 907340 : Trace("circuit-prop") << "CircuitPropagator::computeBackEdges(" << node << ")"
193 : 453670 : << endl;
194 : :
195 : : // Vector of nodes to visit
196 : 453670 : vector<TNode> toVisit;
197 : :
198 : : // Start with the top node
199 [ + + ]: 453670 : if (d_seen.find(node) == d_seen.end())
200 : : {
201 : 419240 : toVisit.push_back(node);
202 : 419240 : d_seen.insert(node);
203 : : }
204 : :
205 : : // Initialize the back-edges for the root, so we don't have a special case
206 : 453670 : d_backEdges[node];
207 : :
208 : : // Go through the visit list
209 [ + + ]: 1493558 : for (unsigned i = 0; i < toVisit.size(); ++i)
210 : : {
211 : : // Node we need to visit
212 : 1039888 : TNode current = toVisit[i];
213 [ + - ]: 2079776 : Trace("circuit-prop")
214 : 0 : << "CircuitPropagator::computeBackEdges(): processing " << current
215 : 1039888 : << endl;
216 [ - + ][ - + ]: 1039888 : 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 [ + + ]: 1039888 : if (Theory::theoryOf(current) == THEORY_BOOL)
220 : : {
221 : 2070843 : for (unsigned child = 0, child_end = current.getNumChildren();
222 [ + + ]: 2070843 : child < child_end;
223 : : ++child)
224 : : {
225 : 1386616 : TNode childNode = current[child];
226 : : // Add the back edge
227 : 1386616 : d_backEdges[childNode].push_back(current);
228 : : // Add to the queue if not seen yet
229 [ + + ]: 1386616 : if (d_seen.find(childNode) == d_seen.end())
230 : : {
231 : 620648 : toVisit.push_back(childNode);
232 : 620648 : d_seen.insert(childNode);
233 : : }
234 : 1386616 : }
235 : : }
236 : 1039888 : }
237 : 453670 : }
238 : :
239 : 288031 : void CircuitPropagator::propagateBackward(TNode parent, bool parentAssignment)
240 : : {
241 [ + - ]: 576062 : Trace("circuit-prop") << "CircuitPropagator::propagateBackward(" << parent
242 : 288031 : << ", " << parentAssignment << ")" << endl;
243 : 288031 : ProofCircuitPropagatorBackward prover{d_env.getNodeManager(),
244 : 288031 : d_env.getProofNodeManager(),
245 : : parent,
246 : 288031 : parentAssignment};
247 : :
248 : : // backward rules
249 [ + + ][ + + ]: 288031 : switch (parent.getKind())
[ + + ][ + - ]
250 : : {
251 : 10566 : case Kind::AND:
252 [ + + ]: 10566 : if (parentAssignment)
253 : : {
254 : : // AND = TRUE: forall children c, assign(c = TRUE)
255 : 2106 : for (TNode::iterator i = parent.begin(), i_end = parent.end();
256 [ + + ]: 38068 : i != i_end;
257 : 35962 : ++i)
258 : : {
259 : 35962 : 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 : 8460 : find_if_unique(parent.begin(), parent.end(), [this](TNode x) {
267 : 18496 : return !isAssignedTo(x, true);
268 : : });
269 [ + + ]: 8460 : if (holdout != parent.end())
270 : : {
271 : 900 : assignAndEnqueue(*holdout, false, prover.andFalse(parent, holdout));
272 : : }
273 : : }
274 : 10566 : break;
275 : 197780 : case Kind::OR:
276 [ + + ]: 197780 : if (parentAssignment)
277 : : {
278 : : // OR = TRUE: if all children BUT ONE == FALSE, assign(c = TRUE)
279 : : TNode::iterator holdout =
280 : 195487 : find_if_unique(parent.begin(), parent.end(), [this](TNode x) {
281 : 394039 : return !isAssignedTo(x, false);
282 : : });
283 [ + + ]: 195487 : if (holdout != parent.end())
284 : : {
285 : 1584 : assignAndEnqueue(*holdout, true, prover.orTrue(parent, holdout));
286 : : }
287 : : }
288 : : else
289 : : {
290 : : // OR = FALSE: forall children c, assign(c = FALSE)
291 : 2293 : for (TNode::iterator i = parent.begin(), i_end = parent.end();
292 [ + + ]: 11830 : i != i_end;
293 : 9537 : ++i)
294 : : {
295 : 9537 : assignAndEnqueue(*i, false, prover.orFalse(i));
296 : : }
297 : : }
298 : 197780 : break;
299 : 66061 : case Kind::NOT:
300 : : // NOT = b: assign(c = !b)
301 : 66061 : assignAndEnqueue(
302 : 132122 : parent[0], !parentAssignment, prover.Not(!parentAssignment, parent));
303 : 66061 : break;
304 : 2854 : case Kind::ITE:
305 [ + + ]: 2854 : if (isAssignedTo(parent[0], true))
306 : : {
307 : : // ITE c x y = v: if c is assigned and TRUE, assign(x = v)
308 : 215 : assignAndEnqueue(parent[1], parentAssignment, prover.iteC(true));
309 : : }
310 [ + + ]: 2639 : else if (isAssignedTo(parent[0], false))
311 : : {
312 : : // ITE c x y = v: if c is assigned and FALSE, assign(y = v)
313 : 69 : assignAndEnqueue(parent[2], parentAssignment, prover.iteC(false));
314 : : }
315 : 2570 : else if (isAssigned(parent[1]) && isAssigned(parent[2]))
316 : : {
317 [ + + ][ - - ]: 60 : if (getAssignment(parent[1]) == parentAssignment
318 [ + + ][ + + ]: 60 : && 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 [ + + ][ - - ]: 56 : else if (getAssignment(parent[1]) != parentAssignment
325 [ + + ][ + - ]: 56 : && 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 : 2854 : break;
333 : 5145 : case Kind::EQUAL:
334 [ - + ][ - + ]: 5145 : Assert(parent[0].getType().isBoolean());
[ - - ]
335 [ + + ]: 5145 : if (parentAssignment)
336 : : {
337 : : // IFF x y = TRUE: if x [resp y] is assigned, assign(y = x.assignment
338 : : // [resp x = y.assignment])
339 [ + + ]: 4271 : if (isAssigned(parent[0]))
340 : : {
341 : 419 : assignAndEnqueue(parent[1],
342 : 838 : getAssignment(parent[0]),
343 : 838 : prover.eqYFromX(getAssignment(parent[0]), parent));
344 : : }
345 [ + + ]: 3852 : 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 [ + + ]: 874 : 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 [ + + ]: 839 : 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 : 5145 : break;
370 : 5293 : case Kind::IMPLIES:
371 [ + + ]: 5293 : if (parentAssignment)
372 : : {
373 [ + + ]: 3648 : 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 [ + + ]: 3648 : 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 : 1645 : assignAndEnqueue(parent[0], true, prover.impliesNegX());
388 : 1645 : assignAndEnqueue(parent[1], false, prover.impliesNegY());
389 : : }
390 : 5293 : 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 : 288031 : }
438 : :
439 : 541069 : void CircuitPropagator::propagateForward(TNode child, bool childAssignment)
440 : : {
441 : : // The assignment we have
442 [ + - ]: 1082138 : Trace("circuit-prop") << "CircuitPropagator::propagateForward(" << child
443 : 541069 : << ", " << childAssignment << ")" << endl;
444 : :
445 : : // Get the back any nodes where this is child
446 : 541069 : const vector<Node>& parents = d_backEdges.find(child)->second;
447 : :
448 : : // Go through the parents and see if there is anything to propagate
449 : 541069 : vector<Node>::const_iterator parent_it = parents.begin();
450 : 541069 : vector<Node>::const_iterator parent_it_end = parents.end();
451 [ + + ][ + + ]: 796229 : for (; parent_it != parent_it_end && d_conflict.get().isNull(); ++parent_it)
[ + + ]
452 : : {
453 : : // The current parent of the child
454 : 255160 : TNode parent = *parent_it;
455 [ + - ]: 255160 : Trace("circuit-prop") << "Parent: " << parent << endl;
456 [ - + ][ - + ]: 255160 : Assert(expr::hasSubterm(parent, child));
[ - - ]
457 : :
458 : : ProofCircuitPropagatorForward prover{
459 : 510320 : d_env.getNodeManager(), d_env.getProofNodeManager(), child, parent};
460 : :
461 : : // Forward rules
462 [ + + ][ + + ]: 255160 : switch (parent.getKind())
[ + + ][ + - ]
463 : : {
464 : 57072 : case Kind::AND:
465 [ + + ]: 57072 : if (childAssignment)
466 : : {
467 : 49226 : TNode::iterator holdout;
468 : 49226 : holdout = find_if(parent.begin(), parent.end(), [this](TNode x) {
469 : 17120911 : return !isAssignedTo(x, true);
470 : : });
471 : :
472 [ + + ]: 49226 : 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 : 30792 : assignAndEnqueue(parent, true, prover.andAllTrue());
477 : : }
478 [ + + ]: 18434 : 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 : 2506 : 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 : 7846 : assignAndEnqueue(parent, false, prover.andOneFalse());
498 : : }
499 : 57072 : break;
500 : 119700 : case Kind::OR:
501 [ + + ]: 119700 : if (childAssignment)
502 : : {
503 : : // OR ...(x=TRUE)...: assign(OR = TRUE)
504 : 62602 : assignAndEnqueue(parent, true, prover.orOneTrue());
505 : : }
506 : : else
507 : : {
508 : 57098 : TNode::iterator holdout;
509 : 57098 : holdout = find_if(parent.begin(), parent.end(), [this](TNode x) {
510 : 1376571 : return !isAssignedTo(x, false);
511 : : });
512 [ + + ]: 57098 : 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 : 8959 : assignAndEnqueue(parent, false, prover.orFalse());
517 : : }
518 [ + + ]: 48139 : else if (isAssignedTo(parent, true))
519 : : { // the OR is TRUE
520 : : // is the holdout unique ?
521 : : TNode::iterator other =
522 : 41420 : find_if(holdout + 1, parent.end(), [this](TNode x) {
523 : 48233 : return !isAssignedTo(x, false);
524 : : });
525 [ + + ]: 41420 : 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 : 22152 : assignAndEnqueue(*holdout, true, prover.orTrue(parent, holdout));
530 : : }
531 : : }
532 : : }
533 : 119700 : break;
534 : :
535 : 65700 : case Kind::NOT:
536 : : // NOT (x=b): assign(NOT = !b)
537 : 65700 : assignAndEnqueue(
538 : 131400 : parent, !childAssignment, prover.Not(childAssignment, parent));
539 : 65700 : break;
540 : :
541 : 1452 : case Kind::ITE:
542 [ + + ]: 1452 : if (child == parent[0])
543 : : {
544 [ + + ]: 506 : if (childAssignment)
545 : : {
546 [ + + ]: 341 : if (isAssigned(parent[1]))
547 : : {
548 : : // ITE (c=TRUE) x y: if x is assigned, assign(ITE = x.assignment)
549 : 214 : assignAndEnqueue(parent,
550 : 428 : getAssignment(parent[1]),
551 : 428 : prover.iteEvalThen(getAssignment(parent[1])));
552 : : }
553 : : }
554 : : else
555 : : {
556 [ + + ]: 165 : if (isAssigned(parent[2]))
557 : : {
558 : : // ITE (c=FALSE) x y: if y is assigned, assign(ITE = y.assignment)
559 : 119 : assignAndEnqueue(parent,
560 : 238 : getAssignment(parent[2]),
561 : 238 : prover.iteEvalElse(getAssignment(parent[2])));
562 : : }
563 : : }
564 : : }
565 [ + + ]: 1452 : if (child == parent[1])
566 : : {
567 [ + + ]: 502 : if (isAssignedTo(parent[0], true))
568 : : {
569 : : // ITE c (x=v) y: if c is assigned and TRUE, assign(ITE = v)
570 : 260 : assignAndEnqueue(
571 : 520 : parent, childAssignment, prover.iteEvalThen(childAssignment));
572 : : }
573 : : }
574 [ + + ]: 1452 : if (child == parent[2])
575 : : {
576 [ - + ][ - + ]: 444 : Assert(child == parent[2]);
[ - - ]
577 [ + + ]: 444 : if (isAssignedTo(parent[0], false))
578 : : {
579 : : // ITE c x (y=v): if c is assigned and FALSE, assign(ITE = v)
580 : 115 : assignAndEnqueue(
581 : 230 : parent, childAssignment, prover.iteEvalElse(childAssignment));
582 : : }
583 : : }
584 : 1452 : break;
585 : 2899 : case Kind::EQUAL:
586 [ - + ][ - + ]: 2899 : Assert(parent[0].getType().isBoolean());
[ - - ]
587 : 2899 : 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 : 1497 : assignAndEnqueue(parent,
592 : 2994 : getAssignment(parent[0]) == getAssignment(parent[1]),
593 : 2994 : prover.eqEval(getAssignment(parent[0]),
594 : 2994 : getAssignment(parent[1])));
595 : : }
596 : : else
597 : : {
598 [ + + ]: 1402 : if (isAssigned(parent))
599 : : {
600 [ + + ]: 729 : if (child == parent[0])
601 : : {
602 [ + + ]: 490 : if (getAssignment(parent))
603 : : {
604 : : // IFF (x = b) y: if IFF is assigned to TRUE, assign(y = b)
605 : 466 : assignAndEnqueue(parent[1],
606 : : childAssignment,
607 : 932 : prover.eqYFromX(childAssignment, parent));
608 : : }
609 : : else
610 : : {
611 : : // IFF (x = b) y: if IFF is assigned to FALSE, assign(y = !b)
612 : 24 : assignAndEnqueue(parent[1],
613 : 24 : !childAssignment,
614 : 48 : prover.neqYFromX(childAssignment, parent));
615 : : }
616 : : }
617 : : else
618 : : {
619 [ - + ][ - + ]: 239 : Assert(child == parent[1]);
[ - - ]
620 [ + + ]: 239 : if (getAssignment(parent))
621 : : {
622 : : // IFF x y = b: if IFF is assigned to TRUE, assign(x = b)
623 : 200 : assignAndEnqueue(parent[0],
624 : : childAssignment,
625 : 400 : prover.eqXFromY(childAssignment, parent));
626 : : }
627 : : else
628 : : {
629 : : // IFF x y = b y: if IFF is assigned to FALSE, assign(x = !b)
630 : 39 : assignAndEnqueue(parent[0],
631 : 39 : !childAssignment,
632 : 78 : prover.neqXFromY(childAssignment, parent));
633 : : }
634 : : }
635 : : }
636 : : }
637 : 2899 : break;
638 : 7920 : case Kind::IMPLIES:
639 : 7920 : if (isAssigned(parent[0]) && isAssigned(parent[1]))
640 : : {
641 : : // IMPLIES (x=v1) (y=v2): assign(IMPLIES = (!v1 || v2))
642 : 4527 : assignAndEnqueue(
643 : : parent,
644 : 9054 : !getAssignment(parent[0]) || getAssignment(parent[1]),
645 : 9054 : prover.impliesEval(getAssignment(parent[0]),
646 : 9054 : getAssignment(parent[1])));
647 : : }
648 : : else
649 : : {
650 [ + + ][ + + ]: 5713 : if (child == parent[0] && childAssignment
[ - - ]
651 [ + + ][ + + ]: 5713 : && 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 [ + + ][ + + ]: 4466 : if (child == parent[1] && !childAssignment
[ - - ]
657 [ + + ][ + + ]: 4466 : && 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 : 7920 : 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 : 255160 : }
701 : 541069 : }
702 : :
703 : 40059 : TrustNode CircuitPropagator::propagate()
704 : : {
705 [ + - ]: 40059 : Trace("circuit-prop") << "CircuitPropagator::propagate()" << std::endl;
706 : :
707 : 581128 : for (unsigned i = 0;
708 [ + + ][ + + ]: 581128 : i < d_propagationQueue.size() && d_conflict.get().isNull();
[ + + ]
709 : : ++i)
710 : : {
711 : : // The current node we are propagating
712 : 541069 : TNode current = d_propagationQueue[i];
713 [ + - ]: 1082138 : Trace("circuit-prop") << "CircuitPropagator::propagate(): processing "
714 : 541069 : << current << std::endl;
715 : 541069 : bool assignment = getAssignment(current);
716 [ + - ]: 1082138 : Trace("circuit-prop") << "CircuitPropagator::propagate(): assigned to "
717 [ - - ]: 541069 : << (assignment ? "true" : "false") << std::endl;
718 : :
719 : : // Is this an atom
720 [ + + ][ - - ]: 885120 : bool atom = Theory::theoryOf(current) != THEORY_BOOL || current.isVar()
721 [ + + ][ + + ]: 890907 : || (current.getKind() == Kind::EQUAL
722 : 546856 : && (current[0].isVar() && current[1].isVar()));
723 : :
724 : : // If an atom, add to the list for simplification
725 : 541069 : if (atom
726 [ + + ][ + + ]: 546214 : || (current.getKind() == Kind::EQUAL
727 : 546214 : && (current[0].isVar() || current[1].isVar())))
728 : : {
729 [ + - ]: 434826 : Trace("circuit-prop")
730 : 0 : << "CircuitPropagator::propagate(): adding to learned: "
731 [ - - ][ - + ]: 217413 : << (assignment ? (Node)current : current.notNode()) << std::endl;
[ - - ]
732 [ + + ]: 217413 : Node lit = assignment ? Node(current) : current.notNode();
733 : :
734 [ + + ]: 217413 : if (isProofEnabled())
735 : : {
736 [ + - ]: 135600 : 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 [ + - ]: 135600 : ProofGenerator* pg = d_proofInternal.get();
741 [ + - ]: 135600 : if (d_proofExternal != nullptr)
742 : : {
743 : 135600 : d_proofExternal->addLazyStep(lit, pg);
744 [ + - ]: 135600 : pg = d_proofExternal.get();
745 : : }
746 : 135600 : TrustNode tlit = TrustNode::mkTrustLemma(lit, pg);
747 : 135600 : d_learnedLiterals.push_back(tlit);
748 : 135600 : }
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 : 81813 : TrustNode tlit = TrustNode::mkTrustLemma(lit, nullptr);
760 : 81813 : d_learnedLiterals.push_back(tlit);
761 : 81813 : }
762 [ + - ]: 217413 : Trace("circuit-prop") << "Added proof for " << lit << std::endl;
763 : 217413 : }
764 : :
765 : : // Propagate this value to the children (if not an atom or a constant)
766 [ + - ][ + + ]: 541069 : if (d_backwardPropagation && !atom && !current.isConst())
[ + + ][ + + ]
767 : : {
768 : 288031 : propagateBackward(current, assignment);
769 : : }
770 : : // Propagate this value to the parents
771 [ + - ]: 541069 : if (d_forwardPropagation)
772 : : {
773 : 541069 : propagateForward(current, assignment);
774 : : }
775 : 541069 : }
776 : :
777 : : // No conflict
778 : 40059 : return d_conflict;
779 : : }
780 : :
781 : 18858 : void CircuitPropagator::enableProofs(context::Context* ctx,
782 : : ProofGenerator* defParent)
783 : : {
784 : 18858 : d_epg.reset(new EagerProofGenerator(d_env, ctx));
785 [ + - ]: 37716 : d_proofInternal.reset(new LazyCDProofChain(
786 : 37716 : d_env, true, ctx, d_epg.get(), true, "CircuitPropInternalLazyChain"));
787 [ + - ]: 18858 : 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 : 37716 : d_proofExternal.reset(new LazyCDProofChain(
793 : 18858 : d_env, true, ctx, defParent, false, "CircuitPropExternalLazyChain"));
794 : : }
795 : 18858 : }
796 : :
797 : 1845188 : bool CircuitPropagator::isProofEnabled() const
798 : : {
799 : 1845188 : return d_proofInternal != nullptr;
800 : : }
801 : :
802 : 389777 : void CircuitPropagator::addProof(TNode f, std::shared_ptr<ProofNode> pf)
803 : : {
804 [ + + ]: 389777 : if (isProofEnabled())
805 : : {
806 [ + + ]: 387205 : if (!d_epg->hasProofFor(f))
807 : : {
808 [ + - ]: 510392 : Trace("circuit-prop") << "Adding proof for " << f << std::endl
809 : 255196 : << "\t" << *pf << std::endl;
810 : 255196 : d_epg->setProofFor(f, std::move(pf));
811 : : }
812 [ - + ]: 132009 : 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 : 389777 : }
820 : :
821 : : } // namespace booleans
822 : : } // namespace theory
823 : : } // namespace cvc5::internal
|
