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