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 |
18629 |
CircuitPropagator::CircuitPropagator(Env& env, bool enableForward, bool enableBackward) |
38 |
|
: EnvObj(env), |
39 |
|
d_context(), |
40 |
|
d_propagationQueue(), |
41 |
|
d_propagationQueueClearer(&d_context, d_propagationQueue), |
42 |
37258 |
d_conflict(&d_context, TrustNode()), |
43 |
|
d_learnedLiterals(), |
44 |
|
d_learnedLiteralClearer(&d_context, d_learnedLiterals), |
45 |
|
d_backEdges(), |
46 |
|
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_pnm(nullptr), |
53 |
|
d_epg(nullptr), |
54 |
|
d_proofInternal(nullptr), |
55 |
55887 |
d_proofExternal(nullptr) |
56 |
|
{ |
57 |
18629 |
} |
58 |
|
|
59 |
16303 |
void CircuitPropagator::finish() |
60 |
|
{ |
61 |
16303 |
Trace("circuit-prop") << "FINISH" << std::endl; |
62 |
16303 |
d_context.pop(); |
63 |
16303 |
} |
64 |
|
|
65 |
217385 |
void CircuitPropagator::assertTrue(TNode assertion) |
66 |
|
{ |
67 |
217385 |
Trace("circuit-prop") << "TRUE: " << assertion << std::endl; |
68 |
217385 |
if (assertion.getKind() == kind::CONST_BOOLEAN && !assertion.getConst<bool>()) |
69 |
|
{ |
70 |
927 |
makeConflict(assertion); |
71 |
|
} |
72 |
216458 |
else if (assertion.getKind() == kind::AND) |
73 |
|
{ |
74 |
15254 |
ProofCircuitPropagatorBackward prover{d_pnm, assertion, true}; |
75 |
7627 |
if (isProofEnabled()) |
76 |
|
{ |
77 |
4324 |
addProof(assertion, prover.assume(assertion)); |
78 |
|
} |
79 |
133087 |
for (auto it = assertion.begin(); it != assertion.end(); ++it) |
80 |
|
{ |
81 |
125460 |
addProof(*it, prover.andTrue(it)); |
82 |
125460 |
assertTrue(*it); |
83 |
|
} |
84 |
|
} |
85 |
|
else |
86 |
|
{ |
87 |
|
// Analyze the assertion for back-edges and all that |
88 |
208831 |
computeBackEdges(assertion); |
89 |
|
// Assign the given assertion to true |
90 |
208831 |
if (isProofEnabled()) |
91 |
|
{ |
92 |
56046 |
assignAndEnqueue(assertion, true, d_pnm->mkAssume(assertion)); |
93 |
|
} |
94 |
|
else |
95 |
|
{ |
96 |
152785 |
assignAndEnqueue(assertion, true, nullptr); |
97 |
|
} |
98 |
|
} |
99 |
217385 |
} |
100 |
|
|
101 |
452402 |
void CircuitPropagator::assignAndEnqueue(TNode n, |
102 |
|
bool value, |
103 |
|
std::shared_ptr<ProofNode> proof) |
104 |
|
{ |
105 |
904804 |
Trace("circuit-prop") << "CircuitPropagator::assign(" << n << ", " |
106 |
452402 |
<< (value ? "true" : "false") << ")" << std::endl; |
107 |
|
|
108 |
452402 |
if (n.getKind() == kind::CONST_BOOLEAN) |
109 |
|
{ |
110 |
|
// Assigning a constant to the opposite value is dumb |
111 |
17258 |
if (value != n.getConst<bool>()) |
112 |
|
{ |
113 |
|
makeConflict(n); |
114 |
|
return; |
115 |
|
} |
116 |
|
} |
117 |
|
|
118 |
452402 |
if (isProofEnabled()) |
119 |
|
{ |
120 |
120478 |
if (proof == nullptr) |
121 |
|
{ |
122 |
|
warning() << "CircuitPropagator: Proof is missing for " << n << std::endl; |
123 |
|
Assert(false); |
124 |
|
} |
125 |
|
else |
126 |
|
{ |
127 |
120478 |
Assert(!proof->getResult().isNull()); |
128 |
240956 |
Node expected = value ? Node(n) : n.negate(); |
129 |
120478 |
if (proof->getResult() != expected) |
130 |
|
{ |
131 |
|
warning() << "CircuitPropagator: Incorrect proof: " << expected |
132 |
|
<< " vs. " << proof->getResult() << std::endl |
133 |
|
<< *proof << std::endl; |
134 |
|
} |
135 |
120478 |
addProof(expected, std::move(proof)); |
136 |
|
} |
137 |
|
} |
138 |
|
|
139 |
|
// Get the current assignment |
140 |
452402 |
AssignmentStatus state = d_state[n]; |
141 |
|
|
142 |
452402 |
if (state != UNASSIGNED) |
143 |
|
{ |
144 |
|
// If the node is already assigned we might have a conflict |
145 |
157789 |
if (value != (state == ASSIGNED_TO_TRUE)) |
146 |
|
{ |
147 |
1740 |
makeConflict(n); |
148 |
|
} |
149 |
|
} |
150 |
|
else |
151 |
|
{ |
152 |
|
// If unassigned, mark it as assigned |
153 |
294613 |
d_state[n] = value ? ASSIGNED_TO_TRUE : ASSIGNED_TO_FALSE; |
154 |
|
// Add for further propagation |
155 |
294613 |
d_propagationQueue.push_back(n); |
156 |
|
} |
157 |
|
} |
158 |
|
|
159 |
2667 |
void CircuitPropagator::makeConflict(Node n) |
160 |
|
{ |
161 |
5311 |
auto bfalse = NodeManager::currentNM()->mkConst(false); |
162 |
2667 |
ProofGenerator* g = nullptr; |
163 |
2667 |
if (isProofEnabled()) |
164 |
|
{ |
165 |
2028 |
if (d_epg->hasProofFor(bfalse)) |
166 |
|
{ |
167 |
23 |
return; |
168 |
|
} |
169 |
2005 |
ProofCircuitPropagator pcp(d_pnm); |
170 |
2005 |
if (n == bfalse) |
171 |
|
{ |
172 |
455 |
d_epg->setProofFor(bfalse, pcp.assume(bfalse)); |
173 |
|
} |
174 |
|
else |
175 |
|
{ |
176 |
3100 |
d_epg->setProofFor(bfalse, |
177 |
3100 |
pcp.conflict(pcp.assume(n), pcp.assume(n.negate()))); |
178 |
|
} |
179 |
2005 |
g = d_proofInternal.get(); |
180 |
4010 |
Trace("circuit-prop") << "Added conflict " << *d_epg->getProofFor(bfalse) |
181 |
2005 |
<< std::endl; |
182 |
4010 |
Trace("circuit-prop") << "\texpanded " << *g->getProofFor(bfalse) |
183 |
2005 |
<< std::endl; |
184 |
|
} |
185 |
2644 |
d_conflict = TrustNode::mkTrustLemma(bfalse, g); |
186 |
|
} |
187 |
|
|
188 |
208831 |
void CircuitPropagator::computeBackEdges(TNode node) |
189 |
|
{ |
190 |
417662 |
Debug("circuit-prop") << "CircuitPropagator::computeBackEdges(" << node << ")" |
191 |
208831 |
<< endl; |
192 |
|
|
193 |
|
// Vector of nodes to visit |
194 |
417662 |
vector<TNode> toVisit; |
195 |
|
|
196 |
|
// Start with the top node |
197 |
208831 |
if (d_seen.find(node) == d_seen.end()) |
198 |
|
{ |
199 |
200505 |
toVisit.push_back(node); |
200 |
200505 |
d_seen.insert(node); |
201 |
|
} |
202 |
|
|
203 |
|
// Initialize the back-edges for the root, so we don't have a special case |
204 |
208831 |
d_backEdges[node]; |
205 |
|
|
206 |
|
// Go through the visit list |
207 |
755840 |
for (unsigned i = 0; i < toVisit.size(); ++i) |
208 |
|
{ |
209 |
|
// Node we need to visit |
210 |
1094018 |
TNode current = toVisit[i]; |
211 |
1094018 |
Debug("circuit-prop") |
212 |
547009 |
<< "CircuitPropagator::computeBackEdges(): processing " << current |
213 |
547009 |
<< endl; |
214 |
547009 |
Assert(d_seen.find(current) != d_seen.end()); |
215 |
|
|
216 |
|
// If this not an atom visit all the children and compute the back edges |
217 |
547009 |
if (Theory::theoryOf(current) == THEORY_BOOL) |
218 |
|
{ |
219 |
1141611 |
for (unsigned child = 0, child_end = current.getNumChildren(); |
220 |
1141611 |
child < child_end; |
221 |
|
++child) |
222 |
|
{ |
223 |
1493830 |
TNode childNode = current[child]; |
224 |
|
// Add the back edge |
225 |
746915 |
d_backEdges[childNode].push_back(current); |
226 |
|
// Add to the queue if not seen yet |
227 |
746915 |
if (d_seen.find(childNode) == d_seen.end()) |
228 |
|
{ |
229 |
346504 |
toVisit.push_back(childNode); |
230 |
346504 |
d_seen.insert(childNode); |
231 |
|
} |
232 |
|
} |
233 |
|
} |
234 |
|
} |
235 |
208831 |
} |
236 |
|
|
237 |
172435 |
void CircuitPropagator::propagateBackward(TNode parent, bool parentAssignment) |
238 |
|
{ |
239 |
344870 |
Debug("circuit-prop") << "CircuitPropagator::propagateBackward(" << parent |
240 |
172435 |
<< ", " << parentAssignment << ")" << endl; |
241 |
344870 |
ProofCircuitPropagatorBackward prover{d_pnm, parent, parentAssignment}; |
242 |
|
|
243 |
|
// backward rules |
244 |
172435 |
switch (parent.getKind()) |
245 |
|
{ |
246 |
6162 |
case kind::AND: |
247 |
6162 |
if (parentAssignment) |
248 |
|
{ |
249 |
|
// AND = TRUE: forall children c, assign(c = TRUE) |
250 |
21007 |
for (TNode::iterator i = parent.begin(), i_end = parent.end(); |
251 |
21007 |
i != i_end; |
252 |
|
++i) |
253 |
|
{ |
254 |
19983 |
assignAndEnqueue(*i, true, prover.andTrue(i)); |
255 |
|
} |
256 |
|
} |
257 |
|
else |
258 |
|
{ |
259 |
|
// AND = FALSE: if all children BUT ONE == TRUE, assign(c = FALSE) |
260 |
|
TNode::iterator holdout = |
261 |
10859 |
find_if_unique(parent.begin(), parent.end(), [this](TNode x) { |
262 |
21718 |
return !isAssignedTo(x, true); |
263 |
26856 |
}); |
264 |
5138 |
if (holdout != parent.end()) |
265 |
|
{ |
266 |
463 |
assignAndEnqueue(*holdout, false, prover.andFalse(parent, holdout)); |
267 |
|
} |
268 |
|
} |
269 |
6162 |
break; |
270 |
100592 |
case kind::OR: |
271 |
100592 |
if (parentAssignment) |
272 |
|
{ |
273 |
|
// OR = TRUE: if all children BUT ONE == FALSE, assign(c = TRUE) |
274 |
|
TNode::iterator holdout = |
275 |
199037 |
find_if_unique(parent.begin(), parent.end(), [this](TNode x) { |
276 |
398074 |
return !isAssignedTo(x, false); |
277 |
497132 |
}); |
278 |
99058 |
if (holdout != parent.end()) |
279 |
|
{ |
280 |
710 |
assignAndEnqueue(*holdout, true, prover.orTrue(parent, holdout)); |
281 |
|
} |
282 |
|
} |
283 |
|
else |
284 |
|
{ |
285 |
|
// OR = FALSE: forall children c, assign(c = FALSE) |
286 |
6179 |
for (TNode::iterator i = parent.begin(), i_end = parent.end(); |
287 |
6179 |
i != i_end; |
288 |
|
++i) |
289 |
|
{ |
290 |
4645 |
assignAndEnqueue(*i, false, prover.orFalse(i)); |
291 |
|
} |
292 |
|
} |
293 |
100592 |
break; |
294 |
50099 |
case kind::NOT: |
295 |
|
// NOT = b: assign(c = !b) |
296 |
50099 |
assignAndEnqueue( |
297 |
100198 |
parent[0], !parentAssignment, prover.Not(!parentAssignment, parent)); |
298 |
50099 |
break; |
299 |
6001 |
case kind::ITE: |
300 |
6001 |
if (isAssignedTo(parent[0], true)) |
301 |
|
{ |
302 |
|
// ITE c x y = v: if c is assigned and TRUE, assign(x = v) |
303 |
959 |
assignAndEnqueue(parent[1], parentAssignment, prover.iteC(true)); |
304 |
|
} |
305 |
5042 |
else if (isAssignedTo(parent[0], false)) |
306 |
|
{ |
307 |
|
// ITE c x y = v: if c is assigned and FALSE, assign(y = v) |
308 |
313 |
assignAndEnqueue(parent[2], parentAssignment, prover.iteC(false)); |
309 |
|
} |
310 |
4729 |
else if (isAssigned(parent[1]) && isAssigned(parent[2])) |
311 |
|
{ |
312 |
390 |
if (getAssignment(parent[1]) == parentAssignment |
313 |
390 |
&& getAssignment(parent[2]) != parentAssignment) |
314 |
|
{ |
315 |
|
// ITE c x y = v: if c is unassigned, x and y are assigned, x==v and |
316 |
|
// y!=v, assign(c = TRUE) |
317 |
14 |
assignAndEnqueue(parent[0], true, prover.iteIsCase(1)); |
318 |
|
} |
319 |
348 |
else if (getAssignment(parent[1]) != parentAssignment |
320 |
348 |
&& getAssignment(parent[2]) == parentAssignment) |
321 |
|
{ |
322 |
|
// ITE c x y = v: if c is unassigned, x and y are assigned, x!=v and |
323 |
|
// y==v, assign(c = FALSE) |
324 |
14 |
assignAndEnqueue(parent[0], false, prover.iteIsCase(0)); |
325 |
|
} |
326 |
|
} |
327 |
6001 |
break; |
328 |
3541 |
case kind::EQUAL: |
329 |
3541 |
Assert(parent[0].getType().isBoolean()); |
330 |
3541 |
if (parentAssignment) |
331 |
|
{ |
332 |
|
// IFF x y = TRUE: if x [resp y] is assigned, assign(y = x.assignment |
333 |
|
// [resp x = y.assignment]) |
334 |
2924 |
if (isAssigned(parent[0])) |
335 |
|
{ |
336 |
611 |
assignAndEnqueue(parent[1], |
337 |
1222 |
getAssignment(parent[0]), |
338 |
1222 |
prover.eqYFromX(getAssignment(parent[0]), parent)); |
339 |
|
} |
340 |
2313 |
else if (isAssigned(parent[1])) |
341 |
|
{ |
342 |
81 |
assignAndEnqueue(parent[0], |
343 |
162 |
getAssignment(parent[1]), |
344 |
162 |
prover.eqXFromY(getAssignment(parent[1]), parent)); |
345 |
|
} |
346 |
|
} |
347 |
|
else |
348 |
|
{ |
349 |
|
// IFF x y = FALSE: if x [resp y] is assigned, assign(y = !x.assignment |
350 |
|
// [resp x = !y.assignment]) |
351 |
617 |
if (isAssigned(parent[0])) |
352 |
|
{ |
353 |
12 |
assignAndEnqueue(parent[1], |
354 |
24 |
!getAssignment(parent[0]), |
355 |
24 |
prover.neqYFromX(getAssignment(parent[0]), parent)); |
356 |
|
} |
357 |
605 |
else if (isAssigned(parent[1])) |
358 |
|
{ |
359 |
7 |
assignAndEnqueue(parent[0], |
360 |
14 |
!getAssignment(parent[1]), |
361 |
14 |
prover.neqXFromY(getAssignment(parent[1]), parent)); |
362 |
|
} |
363 |
|
} |
364 |
3541 |
break; |
365 |
5912 |
case kind::IMPLIES: |
366 |
5912 |
if (parentAssignment) |
367 |
|
{ |
368 |
5310 |
if (isAssignedTo(parent[0], true)) |
369 |
|
{ |
370 |
|
// IMPLIES x y = TRUE, and x == TRUE: assign(y = TRUE) |
371 |
572 |
assignAndEnqueue(parent[1], true, prover.impliesYFromX(parent)); |
372 |
|
} |
373 |
5310 |
if (isAssignedTo(parent[1], false)) |
374 |
|
{ |
375 |
|
// IMPLIES x y = TRUE, and y == FALSE: assign(x = FALSE) |
376 |
50 |
assignAndEnqueue(parent[0], false, prover.impliesXFromY(parent)); |
377 |
|
} |
378 |
|
} |
379 |
|
else |
380 |
|
{ |
381 |
|
// IMPLIES x y = FALSE: assign(x = TRUE) and assign(y = FALSE) |
382 |
602 |
assignAndEnqueue(parent[0], true, prover.impliesNegX()); |
383 |
602 |
assignAndEnqueue(parent[1], false, prover.impliesNegY()); |
384 |
|
} |
385 |
5912 |
break; |
386 |
128 |
case kind::XOR: |
387 |
128 |
if (parentAssignment) |
388 |
|
{ |
389 |
111 |
if (isAssigned(parent[0])) |
390 |
|
{ |
391 |
|
// XOR x y = TRUE, and x assigned, assign(y = !assignment(x)) |
392 |
4 |
assignAndEnqueue( |
393 |
|
parent[1], |
394 |
8 |
!getAssignment(parent[0]), |
395 |
20 |
prover.xorYFromX( |
396 |
12 |
!parentAssignment, getAssignment(parent[0]), parent)); |
397 |
|
} |
398 |
107 |
else if (isAssigned(parent[1])) |
399 |
|
{ |
400 |
|
// XOR x y = TRUE, and y assigned, assign(x = !assignment(y)) |
401 |
6 |
assignAndEnqueue( |
402 |
|
parent[0], |
403 |
12 |
!getAssignment(parent[1]), |
404 |
30 |
prover.xorXFromY( |
405 |
18 |
!parentAssignment, getAssignment(parent[1]), parent)); |
406 |
|
} |
407 |
|
} |
408 |
|
else |
409 |
|
{ |
410 |
17 |
if (isAssigned(parent[0])) |
411 |
|
{ |
412 |
|
// XOR x y = FALSE, and x assigned, assign(y = assignment(x)) |
413 |
7 |
assignAndEnqueue( |
414 |
|
parent[1], |
415 |
14 |
getAssignment(parent[0]), |
416 |
35 |
prover.xorYFromX( |
417 |
21 |
!parentAssignment, getAssignment(parent[0]), parent)); |
418 |
|
} |
419 |
10 |
else if (isAssigned(parent[1])) |
420 |
|
{ |
421 |
|
// XOR x y = FALSE, and y assigned, assign(x = assignment(y)) |
422 |
3 |
assignAndEnqueue( |
423 |
|
parent[0], |
424 |
6 |
getAssignment(parent[1]), |
425 |
15 |
prover.xorXFromY( |
426 |
9 |
!parentAssignment, getAssignment(parent[1]), parent)); |
427 |
|
} |
428 |
|
} |
429 |
128 |
break; |
430 |
|
default: Unhandled(); |
431 |
|
} |
432 |
172435 |
} |
433 |
|
|
434 |
286693 |
void CircuitPropagator::propagateForward(TNode child, bool childAssignment) |
435 |
|
{ |
436 |
|
// The assignment we have |
437 |
573386 |
Debug("circuit-prop") << "CircuitPropagator::propagateForward(" << child |
438 |
286693 |
<< ", " << childAssignment << ")" << endl; |
439 |
|
|
440 |
|
// Get the back any nodes where this is child |
441 |
286693 |
const vector<Node>& parents = d_backEdges.find(child)->second; |
442 |
|
|
443 |
|
// Go through the parents and see if there is anything to propagate |
444 |
286693 |
vector<Node>::const_iterator parent_it = parents.begin(); |
445 |
286693 |
vector<Node>::const_iterator parent_it_end = parents.end(); |
446 |
681707 |
for (; parent_it != parent_it_end && d_conflict.get().isNull(); ++parent_it) |
447 |
|
{ |
448 |
|
// The current parent of the child |
449 |
395014 |
TNode parent = *parent_it; |
450 |
197507 |
Debug("circuit-prop") << "Parent: " << parent << endl; |
451 |
197507 |
Assert(expr::hasSubterm(parent, child)); |
452 |
|
|
453 |
395014 |
ProofCircuitPropagatorForward prover{d_pnm, child, childAssignment, parent}; |
454 |
|
|
455 |
|
// Forward rules |
456 |
197507 |
switch (parent.getKind()) |
457 |
|
{ |
458 |
30180 |
case kind::AND: |
459 |
30180 |
if (childAssignment) |
460 |
|
{ |
461 |
25712 |
TNode::iterator holdout; |
462 |
19411173 |
holdout = find_if(parent.begin(), parent.end(), [this](TNode x) { |
463 |
38770922 |
return !isAssignedTo(x, true); |
464 |
38796634 |
}); |
465 |
|
|
466 |
25712 |
if (holdout == parent.end()) |
467 |
|
{ // all children are assigned TRUE |
468 |
|
// AND ...(x=TRUE)...: if all children now assigned to TRUE, |
469 |
|
// assign(AND = TRUE) |
470 |
17820 |
assignAndEnqueue(parent, true, prover.andAllTrue()); |
471 |
|
} |
472 |
7892 |
else if (isAssignedTo(parent, false)) |
473 |
|
{ // the AND is FALSE |
474 |
|
// is the holdout unique ? |
475 |
|
TNode::iterator other = |
476 |
1300 |
find_if(holdout + 1, parent.end(), [this](TNode x) { |
477 |
2600 |
return !isAssignedTo(x, true); |
478 |
3787 |
}); |
479 |
1187 |
if (other == parent.end()) |
480 |
|
{ // the holdout is unique |
481 |
|
// AND ...(x=TRUE)...: if all children BUT ONE now assigned to |
482 |
|
// TRUE, and AND == FALSE, assign(last_holdout = FALSE) |
483 |
470 |
assignAndEnqueue( |
484 |
940 |
*holdout, false, prover.andFalse(parent, holdout)); |
485 |
|
} |
486 |
|
} |
487 |
|
} |
488 |
|
else |
489 |
|
{ |
490 |
|
// AND ...(x=FALSE)...: assign(AND = FALSE) |
491 |
4468 |
assignAndEnqueue(parent, false, prover.andOneFalse()); |
492 |
|
} |
493 |
30180 |
break; |
494 |
104586 |
case kind::OR: |
495 |
104586 |
if (childAssignment) |
496 |
|
{ |
497 |
|
// OR ...(x=TRUE)...: assign(OR = TRUE) |
498 |
59198 |
assignAndEnqueue(parent, true, prover.orOneTrue()); |
499 |
|
} |
500 |
|
else |
501 |
|
{ |
502 |
45388 |
TNode::iterator holdout; |
503 |
499145 |
holdout = find_if(parent.begin(), parent.end(), [this](TNode x) { |
504 |
907514 |
return !isAssignedTo(x, false); |
505 |
952902 |
}); |
506 |
45388 |
if (holdout == parent.end()) |
507 |
|
{ // all children are assigned FALSE |
508 |
|
// OR ...(x=FALSE)...: if all children now assigned to FALSE, |
509 |
|
// assign(OR = FALSE) |
510 |
4265 |
assignAndEnqueue(parent, false, prover.orFalse()); |
511 |
|
} |
512 |
41123 |
else if (isAssignedTo(parent, true)) |
513 |
|
{ // the OR is TRUE |
514 |
|
// is the holdout unique ? |
515 |
|
TNode::iterator other = |
516 |
42000 |
find_if(holdout + 1, parent.end(), [this](TNode x) { |
517 |
84000 |
return !isAssignedTo(x, false); |
518 |
121476 |
}); |
519 |
37476 |
if (other == parent.end()) |
520 |
|
{ // the holdout is unique |
521 |
|
// OR ...(x=FALSE)...: if all children BUT ONE now assigned to |
522 |
|
// FALSE, and OR == TRUE, assign(last_holdout = TRUE) |
523 |
21376 |
assignAndEnqueue(*holdout, true, prover.orTrue(parent, holdout)); |
524 |
|
} |
525 |
|
} |
526 |
|
} |
527 |
104586 |
break; |
528 |
|
|
529 |
49167 |
case kind::NOT: |
530 |
|
// NOT (x=b): assign(NOT = !b) |
531 |
49167 |
assignAndEnqueue( |
532 |
98334 |
parent, !childAssignment, prover.Not(childAssignment, parent)); |
533 |
49167 |
break; |
534 |
|
|
535 |
5560 |
case kind::ITE: |
536 |
5560 |
if (child == parent[0]) |
537 |
|
{ |
538 |
1844 |
if (childAssignment) |
539 |
|
{ |
540 |
983 |
if (isAssigned(parent[1])) |
541 |
|
{ |
542 |
|
// ITE (c=TRUE) x y: if x is assigned, assign(ITE = x.assignment) |
543 |
799 |
assignAndEnqueue(parent, |
544 |
1598 |
getAssignment(parent[1]), |
545 |
1598 |
prover.iteEvalThen(getAssignment(parent[1]))); |
546 |
|
} |
547 |
|
} |
548 |
|
else |
549 |
|
{ |
550 |
861 |
if (isAssigned(parent[2])) |
551 |
|
{ |
552 |
|
// ITE (c=FALSE) x y: if y is assigned, assign(ITE = y.assignment) |
553 |
451 |
assignAndEnqueue(parent, |
554 |
902 |
getAssignment(parent[2]), |
555 |
902 |
prover.iteEvalElse(getAssignment(parent[2]))); |
556 |
|
} |
557 |
|
} |
558 |
|
} |
559 |
5560 |
if (child == parent[1]) |
560 |
|
{ |
561 |
1908 |
if (isAssignedTo(parent[0], true)) |
562 |
|
{ |
563 |
|
// ITE c (x=v) y: if c is assigned and TRUE, assign(ITE = v) |
564 |
546 |
assignAndEnqueue( |
565 |
1092 |
parent, childAssignment, prover.iteEvalThen(childAssignment)); |
566 |
|
} |
567 |
|
} |
568 |
5560 |
if (child == parent[2]) |
569 |
|
{ |
570 |
1808 |
Assert(child == parent[2]); |
571 |
1808 |
if (isAssignedTo(parent[0], false)) |
572 |
|
{ |
573 |
|
// ITE c x (y=v): if c is assigned and FALSE, assign(ITE = v) |
574 |
412 |
assignAndEnqueue( |
575 |
824 |
parent, childAssignment, prover.iteEvalElse(childAssignment)); |
576 |
|
} |
577 |
|
} |
578 |
5560 |
break; |
579 |
3109 |
case kind::EQUAL: |
580 |
3109 |
Assert(parent[0].getType().isBoolean()); |
581 |
3109 |
if (isAssigned(parent[0]) && isAssigned(parent[1])) |
582 |
|
{ |
583 |
|
// IFF x y: if x and y is assigned, assign(IFF = (x.assignment <=> |
584 |
|
// y.assignment)) |
585 |
2048 |
assignAndEnqueue(parent, |
586 |
4096 |
getAssignment(parent[0]) == getAssignment(parent[1]), |
587 |
4096 |
prover.eqEval(getAssignment(parent[0]), |
588 |
4096 |
getAssignment(parent[1]))); |
589 |
|
} |
590 |
|
else |
591 |
|
{ |
592 |
1061 |
if (isAssigned(parent)) |
593 |
|
{ |
594 |
694 |
if (child == parent[0]) |
595 |
|
{ |
596 |
452 |
if (getAssignment(parent)) |
597 |
|
{ |
598 |
|
// IFF (x = b) y: if IFF is assigned to TRUE, assign(y = b) |
599 |
392 |
assignAndEnqueue(parent[1], |
600 |
|
childAssignment, |
601 |
784 |
prover.eqYFromX(childAssignment, parent)); |
602 |
|
} |
603 |
|
else |
604 |
|
{ |
605 |
|
// IFF (x = b) y: if IFF is assigned to FALSE, assign(y = !b) |
606 |
60 |
assignAndEnqueue(parent[1], |
607 |
60 |
!childAssignment, |
608 |
120 |
prover.neqYFromX(childAssignment, parent)); |
609 |
|
} |
610 |
|
} |
611 |
|
else |
612 |
|
{ |
613 |
242 |
Assert(child == parent[1]); |
614 |
242 |
if (getAssignment(parent)) |
615 |
|
{ |
616 |
|
// IFF x y = b: if IFF is assigned to TRUE, assign(x = b) |
617 |
204 |
assignAndEnqueue(parent[0], |
618 |
|
childAssignment, |
619 |
408 |
prover.eqXFromY(childAssignment, parent)); |
620 |
|
} |
621 |
|
else |
622 |
|
{ |
623 |
|
// IFF x y = b y: if IFF is assigned to FALSE, assign(x = !b) |
624 |
38 |
assignAndEnqueue(parent[0], |
625 |
38 |
!childAssignment, |
626 |
76 |
prover.neqXFromY(childAssignment, parent)); |
627 |
|
} |
628 |
|
} |
629 |
|
} |
630 |
|
} |
631 |
3109 |
break; |
632 |
4782 |
case kind::IMPLIES: |
633 |
4782 |
if (isAssigned(parent[0]) && isAssigned(parent[1])) |
634 |
|
{ |
635 |
|
// IMPLIES (x=v1) (y=v2): assign(IMPLIES = (!v1 || v2)) |
636 |
1918 |
assignAndEnqueue( |
637 |
|
parent, |
638 |
3836 |
!getAssignment(parent[0]) || getAssignment(parent[1]), |
639 |
3836 |
prover.impliesEval(getAssignment(parent[0]), |
640 |
3836 |
getAssignment(parent[1]))); |
641 |
|
} |
642 |
|
else |
643 |
|
{ |
644 |
10432 |
if (child == parent[0] && childAssignment |
645 |
10213 |
&& isAssignedTo(parent, true)) |
646 |
|
{ |
647 |
|
// IMPLIES (x=TRUE) y [with IMPLIES == TRUE]: assign(y = TRUE) |
648 |
80 |
assignAndEnqueue(parent[1], true, prover.impliesYFromX(parent)); |
649 |
|
} |
650 |
9616 |
if (child == parent[1] && !childAssignment |
651 |
8599 |
&& isAssignedTo(parent, true)) |
652 |
|
{ |
653 |
|
// IMPLIES x (y=FALSE) [with IMPLIES == TRUE]: assign(x = FALSE) |
654 |
6 |
assignAndEnqueue(parent[0], false, prover.impliesXFromY(parent)); |
655 |
|
} |
656 |
|
// Note that IMPLIES == FALSE doesn't need any cases here |
657 |
|
// because if that assignment has been done, we've already |
658 |
|
// propagated all the children (in back-propagation). |
659 |
|
} |
660 |
4782 |
break; |
661 |
123 |
case kind::XOR: |
662 |
123 |
if (isAssigned(parent)) |
663 |
|
{ |
664 |
47 |
if (child == parent[0]) |
665 |
|
{ |
666 |
|
// XOR (x=v) y [with XOR assigned], assign(y = (v ^ XOR) |
667 |
26 |
assignAndEnqueue( |
668 |
|
parent[1], |
669 |
52 |
childAssignment != getAssignment(parent), |
670 |
104 |
prover.xorYFromX( |
671 |
52 |
!getAssignment(parent), childAssignment, parent)); |
672 |
|
} |
673 |
|
else |
674 |
|
{ |
675 |
21 |
Assert(child == parent[1]); |
676 |
|
// XOR x (y=v) [with XOR assigned], assign(x = (v ^ XOR)) |
677 |
21 |
assignAndEnqueue( |
678 |
|
parent[0], |
679 |
42 |
childAssignment != getAssignment(parent), |
680 |
84 |
prover.xorXFromY( |
681 |
42 |
!getAssignment(parent), childAssignment, parent)); |
682 |
|
} |
683 |
|
} |
684 |
123 |
if (isAssigned(parent[0]) && isAssigned(parent[1])) |
685 |
|
{ |
686 |
49 |
assignAndEnqueue(parent, |
687 |
98 |
getAssignment(parent[0]) != getAssignment(parent[1]), |
688 |
98 |
prover.xorEval(getAssignment(parent[0]), |
689 |
98 |
getAssignment(parent[1]))); |
690 |
|
} |
691 |
123 |
break; |
692 |
|
default: Unhandled(); |
693 |
|
} |
694 |
|
} |
695 |
286693 |
} |
696 |
|
|
697 |
16303 |
TrustNode CircuitPropagator::propagate() |
698 |
|
{ |
699 |
16303 |
Debug("circuit-prop") << "CircuitPropagator::propagate()" << std::endl; |
700 |
|
|
701 |
302996 |
for (unsigned i = 0; |
702 |
302996 |
i < d_propagationQueue.size() && d_conflict.get().isNull(); |
703 |
|
++i) |
704 |
|
{ |
705 |
|
// The current node we are propagating |
706 |
573386 |
TNode current = d_propagationQueue[i]; |
707 |
573386 |
Debug("circuit-prop") << "CircuitPropagator::propagate(): processing " |
708 |
286693 |
<< current << std::endl; |
709 |
286693 |
bool assignment = getAssignment(current); |
710 |
573386 |
Debug("circuit-prop") << "CircuitPropagator::propagate(): assigned to " |
711 |
286693 |
<< (assignment ? "true" : "false") << std::endl; |
712 |
|
|
713 |
|
// Is this an atom |
714 |
1063770 |
bool atom = Theory::theoryOf(current) != THEORY_BOOL || current.isVar() |
715 |
1147958 |
|| (current.getKind() == kind::EQUAL |
716 |
291420 |
&& (current[0].isVar() && current[1].isVar())); |
717 |
|
|
718 |
|
// If an atom, add to the list for simplification |
719 |
286693 |
if (atom |
720 |
388866 |
|| (current.getKind() == kind::EQUAL |
721 |
290234 |
&& (current[0].isVar() || current[1].isVar()))) |
722 |
|
{ |
723 |
204346 |
Debug("circuit-prop") |
724 |
102173 |
<< "CircuitPropagator::propagate(): adding to learned: " |
725 |
102173 |
<< (assignment ? (Node)current : current.notNode()) << std::endl; |
726 |
204346 |
Node lit = assignment ? Node(current) : current.notNode(); |
727 |
|
|
728 |
102173 |
if (isProofEnabled()) |
729 |
|
{ |
730 |
35613 |
if (d_epg->hasProofFor(lit)) |
731 |
|
{ |
732 |
|
// if we have a parent proof generator that provides proofs of the |
733 |
|
// inputs to this class, we must use the lazy proof chain |
734 |
35613 |
ProofGenerator* pg = d_proofInternal.get(); |
735 |
35613 |
if (d_proofExternal != nullptr) |
736 |
|
{ |
737 |
35613 |
d_proofExternal->addLazyStep(lit, pg); |
738 |
35613 |
pg = d_proofExternal.get(); |
739 |
|
} |
740 |
71226 |
TrustNode tlit = TrustNode::mkTrustLemma(lit, pg); |
741 |
35613 |
d_learnedLiterals.push_back(tlit); |
742 |
|
} |
743 |
|
else |
744 |
|
{ |
745 |
|
warning() << "CircuitPropagator: Proof is missing for " << lit |
746 |
|
<< std::endl; |
747 |
|
TrustNode tlit = TrustNode::mkTrustLemma(lit, nullptr); |
748 |
|
d_learnedLiterals.push_back(tlit); |
749 |
|
} |
750 |
|
} |
751 |
|
else |
752 |
|
{ |
753 |
133120 |
TrustNode tlit = TrustNode::mkTrustLemma(lit, nullptr); |
754 |
66560 |
d_learnedLiterals.push_back(tlit); |
755 |
|
} |
756 |
102173 |
Trace("circuit-prop") << "Added proof for " << lit << std::endl; |
757 |
|
} |
758 |
|
|
759 |
|
// Propagate this value to the children (if not an atom or a constant) |
760 |
286693 |
if (d_backwardPropagation && !atom && !current.isConst()) |
761 |
|
{ |
762 |
172435 |
propagateBackward(current, assignment); |
763 |
|
} |
764 |
|
// Propagate this value to the parents |
765 |
286693 |
if (d_forwardPropagation) |
766 |
|
{ |
767 |
286693 |
propagateForward(current, assignment); |
768 |
|
} |
769 |
|
} |
770 |
|
|
771 |
|
// No conflict |
772 |
16303 |
return d_conflict; |
773 |
|
} |
774 |
|
|
775 |
7987 |
void CircuitPropagator::setProof(ProofNodeManager* pnm, |
776 |
|
context::Context* ctx, |
777 |
|
ProofGenerator* defParent) |
778 |
|
{ |
779 |
7987 |
d_pnm = pnm; |
780 |
7987 |
d_epg.reset(new EagerProofGenerator(pnm, ctx)); |
781 |
23961 |
d_proofInternal.reset(new LazyCDProofChain( |
782 |
15974 |
pnm, true, ctx, d_epg.get(), true, "CircuitPropInternalLazyChain")); |
783 |
7987 |
if (defParent != nullptr) |
784 |
|
{ |
785 |
|
// If we provide a parent proof generator (defParent), we want the ASSUME |
786 |
|
// leafs of proofs provided by this class to call the getProofFor method on |
787 |
|
// the parent. To do this, we use a LazyCDProofChain. |
788 |
15974 |
d_proofExternal.reset(new LazyCDProofChain( |
789 |
7987 |
pnm, true, ctx, defParent, false, "CircuitPropExternalLazyChain")); |
790 |
|
} |
791 |
7987 |
} |
792 |
|
|
793 |
1023962 |
bool CircuitPropagator::isProofEnabled() const |
794 |
|
{ |
795 |
1023962 |
return d_proofInternal != nullptr; |
796 |
|
} |
797 |
|
|
798 |
250262 |
void CircuitPropagator::addProof(TNode f, std::shared_ptr<ProofNode> pf) |
799 |
|
{ |
800 |
250262 |
if (isProofEnabled()) |
801 |
|
{ |
802 |
159510 |
if (!d_epg->hasProofFor(f)) |
803 |
|
{ |
804 |
147274 |
Trace("circuit-prop") << "Adding proof for " << f << std::endl |
805 |
73637 |
<< "\t" << *pf << std::endl; |
806 |
73637 |
d_epg->setProofFor(f, std::move(pf)); |
807 |
|
} |
808 |
|
else |
809 |
|
{ |
810 |
171746 |
auto prf = d_epg->getProofFor(f); |
811 |
171746 |
Trace("circuit-prop") << "Ignoring proof, we already have" << std::endl |
812 |
85873 |
<< "\t" << *prf << std::endl; |
813 |
|
} |
814 |
|
} |
815 |
250262 |
} |
816 |
|
|
817 |
|
} // namespace booleans |
818 |
|
} // namespace theory |
819 |
31125 |
} // namespace cvc5 |