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