1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Gereon Kremer |
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 |
|
* Proofs for the non-clausal circuit propagator. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/booleans/proof_circuit_propagator.h" |
17 |
|
|
18 |
|
#include <sstream> |
19 |
|
|
20 |
|
#include "proof/proof_node.h" |
21 |
|
#include "proof/proof_node_manager.h" |
22 |
|
#include "util/rational.h" |
23 |
|
|
24 |
|
namespace cvc5 { |
25 |
|
namespace theory { |
26 |
|
namespace booleans { |
27 |
|
|
28 |
|
namespace { |
29 |
|
|
30 |
|
/** Shorthand to create a Node from a constant number */ |
31 |
|
template <typename T> |
32 |
1438 |
Node mkRat(T val) |
33 |
|
{ |
34 |
1438 |
return NodeManager::currentNM()->mkConst<Rational>(val); |
35 |
|
} |
36 |
|
|
37 |
|
/** |
38 |
|
* Collect all children from parent except for one particular child (the |
39 |
|
* "holdout"). The holdout is given as iterator, and should be an iterator into |
40 |
|
* the [parent.begin(),parent.end()] range. |
41 |
|
*/ |
42 |
|
inline std::vector<Node> collectButHoldout(TNode parent, |
43 |
|
TNode::iterator holdout) |
44 |
|
{ |
45 |
|
std::vector<Node> lits; |
46 |
|
for (TNode::iterator i = parent.begin(), i_end = parent.end(); i != i_end; |
47 |
|
++i) |
48 |
|
{ |
49 |
|
if (i != holdout) |
50 |
|
{ |
51 |
|
lits.emplace_back(*i); |
52 |
|
} |
53 |
|
} |
54 |
|
return lits; |
55 |
|
} |
56 |
|
|
57 |
|
} // namespace |
58 |
|
|
59 |
1025935 |
ProofCircuitPropagator::ProofCircuitPropagator(ProofNodeManager* pnm) |
60 |
1025935 |
: d_pnm(pnm) |
61 |
|
{ |
62 |
1025935 |
} |
63 |
|
|
64 |
946151 |
bool ProofCircuitPropagator::disabled() const { return d_pnm == nullptr; } |
65 |
|
|
66 |
4574 |
std::shared_ptr<ProofNode> ProofCircuitPropagator::assume(Node n) |
67 |
|
{ |
68 |
4574 |
return d_pnm->mkAssume(n); |
69 |
|
} |
70 |
|
|
71 |
11 |
std::shared_ptr<ProofNode> ProofCircuitPropagator::conflict( |
72 |
|
const std::shared_ptr<ProofNode>& a, const std::shared_ptr<ProofNode>& b) |
73 |
|
{ |
74 |
11 |
if (a->getResult().notNode() == b->getResult()) |
75 |
|
{ |
76 |
2 |
return mkProof(PfRule::CONTRA, {a, b}); |
77 |
|
} |
78 |
9 |
Assert(a->getResult() == b->getResult().notNode()); |
79 |
9 |
return mkProof(PfRule::CONTRA, {b, a}); |
80 |
|
} |
81 |
|
|
82 |
547 |
std::shared_ptr<ProofNode> ProofCircuitPropagator::andFalse( |
83 |
|
Node parent, TNode::iterator holdout) |
84 |
|
{ |
85 |
547 |
if (disabled()) |
86 |
|
{ |
87 |
547 |
return nullptr; |
88 |
|
} |
89 |
|
return mkNot( |
90 |
|
mkCResolution(mkProof(PfRule::NOT_AND, {assume(parent.notNode())}), |
91 |
|
collectButHoldout(parent, holdout), |
92 |
|
false)); |
93 |
|
} |
94 |
|
|
95 |
87522 |
std::shared_ptr<ProofNode> ProofCircuitPropagator::orTrue( |
96 |
|
Node parent, TNode::iterator holdout) |
97 |
|
{ |
98 |
87522 |
if (disabled()) |
99 |
|
{ |
100 |
87522 |
return nullptr; |
101 |
|
} |
102 |
|
return mkCResolution( |
103 |
|
assume(parent), collectButHoldout(parent, holdout), true); |
104 |
|
} |
105 |
|
|
106 |
112593 |
std::shared_ptr<ProofNode> ProofCircuitPropagator::Not(bool negate, Node parent) |
107 |
|
{ |
108 |
112593 |
if (disabled()) |
109 |
|
{ |
110 |
112179 |
return nullptr; |
111 |
|
} |
112 |
414 |
return mkNot(assume(negate ? Node(parent[0]) : parent)); |
113 |
|
} |
114 |
|
|
115 |
29 |
std::shared_ptr<ProofNode> ProofCircuitPropagator::impliesXFromY(Node parent) |
116 |
|
{ |
117 |
29 |
if (disabled()) |
118 |
|
{ |
119 |
29 |
return nullptr; |
120 |
|
} |
121 |
|
return mkNot(mkResolution( |
122 |
|
mkProof(PfRule::IMPLIES_ELIM, {assume(parent)}), parent[1], true)); |
123 |
|
} |
124 |
|
|
125 |
449 |
std::shared_ptr<ProofNode> ProofCircuitPropagator::impliesYFromX(Node parent) |
126 |
|
{ |
127 |
449 |
if (disabled()) |
128 |
|
{ |
129 |
449 |
return nullptr; |
130 |
|
} |
131 |
|
return mkResolution( |
132 |
|
mkProof(PfRule::IMPLIES_ELIM, {assume(parent)}), parent[0], false); |
133 |
|
} |
134 |
|
|
135 |
50 |
std::shared_ptr<ProofNode> ProofCircuitPropagator::eqXFromY(bool y, Node parent) |
136 |
|
{ |
137 |
50 |
if (disabled()) |
138 |
|
{ |
139 |
27 |
return nullptr; |
140 |
|
} |
141 |
23 |
if (y) |
142 |
|
{ |
143 |
|
return mkProof( |
144 |
|
PfRule::EQ_RESOLVE, |
145 |
23 |
{assume(parent[1]), mkProof(PfRule::SYMM, {assume(parent)})}); |
146 |
|
} |
147 |
|
return mkNot(mkResolution( |
148 |
|
mkProof(PfRule::EQUIV_ELIM1, {assume(parent)}), parent[1], true)); |
149 |
|
} |
150 |
|
|
151 |
543 |
std::shared_ptr<ProofNode> ProofCircuitPropagator::eqYFromX(bool x, Node parent) |
152 |
|
{ |
153 |
543 |
if (disabled()) |
154 |
|
{ |
155 |
124 |
return nullptr; |
156 |
|
} |
157 |
419 |
if (x) |
158 |
|
{ |
159 |
411 |
return mkProof(PfRule::EQ_RESOLVE, {assume(parent[0]), assume(parent)}); |
160 |
|
} |
161 |
32 |
return mkNot(mkResolution( |
162 |
24 |
mkProof(PfRule::EQUIV_ELIM2, {assume(parent)}), parent[0], true)); |
163 |
|
} |
164 |
|
|
165 |
6 |
std::shared_ptr<ProofNode> ProofCircuitPropagator::neqXFromY(bool y, |
166 |
|
Node parent) |
167 |
|
{ |
168 |
6 |
if (disabled()) |
169 |
|
{ |
170 |
2 |
return nullptr; |
171 |
|
} |
172 |
16 |
return mkNot(mkResolution( |
173 |
20 |
mkProof(y ? PfRule::NOT_EQUIV_ELIM2 : PfRule::NOT_EQUIV_ELIM1, |
174 |
12 |
{assume(parent.notNode())}), |
175 |
|
parent[1], |
176 |
8 |
!y)); |
177 |
|
} |
178 |
|
|
179 |
21 |
std::shared_ptr<ProofNode> ProofCircuitPropagator::neqYFromX(bool x, |
180 |
|
Node parent) |
181 |
|
{ |
182 |
21 |
if (disabled()) |
183 |
|
{ |
184 |
5 |
return nullptr; |
185 |
|
} |
186 |
64 |
return mkNot(mkResolution( |
187 |
80 |
mkProof(x ? PfRule::NOT_EQUIV_ELIM2 : PfRule::NOT_EQUIV_ELIM1, |
188 |
48 |
{assume(parent.notNode())}), |
189 |
|
parent[0], |
190 |
32 |
!x)); |
191 |
|
} |
192 |
|
|
193 |
16 |
std::shared_ptr<ProofNode> ProofCircuitPropagator::xorXFromY(bool negated, |
194 |
|
bool y, |
195 |
|
Node parent) |
196 |
|
{ |
197 |
16 |
if (disabled()) |
198 |
|
{ |
199 |
16 |
return nullptr; |
200 |
|
} |
201 |
|
if (y) |
202 |
|
{ |
203 |
|
return mkNot(mkResolution( |
204 |
|
mkProof(negated ? PfRule::NOT_XOR_ELIM1 : PfRule::XOR_ELIM2, |
205 |
|
{assume(negated ? parent.notNode() : Node(parent))}), |
206 |
|
parent[1], |
207 |
|
false)); |
208 |
|
} |
209 |
|
return mkResolution( |
210 |
|
mkProof(negated ? PfRule::NOT_XOR_ELIM2 : PfRule::XOR_ELIM1, |
211 |
|
{assume(negated ? parent.notNode() : Node(parent))}), |
212 |
|
parent[1], |
213 |
|
true); |
214 |
|
} |
215 |
|
|
216 |
16 |
std::shared_ptr<ProofNode> ProofCircuitPropagator::xorYFromX(bool negated, |
217 |
|
bool x, |
218 |
|
Node parent) |
219 |
|
{ |
220 |
16 |
if (disabled()) |
221 |
|
{ |
222 |
16 |
return nullptr; |
223 |
|
} |
224 |
|
if (x) |
225 |
|
{ |
226 |
|
return mkResolution( |
227 |
|
mkProof(negated ? PfRule::NOT_XOR_ELIM2 : PfRule::XOR_ELIM2, |
228 |
|
{assume(negated ? parent.notNode() : Node(parent))}), |
229 |
|
parent[0], |
230 |
|
false); |
231 |
|
} |
232 |
|
return mkNot( |
233 |
|
mkResolution(mkProof(negated ? PfRule::NOT_XOR_ELIM1 : PfRule::XOR_ELIM1, |
234 |
|
{assume(negated ? parent.notNode() : Node(parent))}), |
235 |
|
parent[0], |
236 |
|
true)); |
237 |
|
} |
238 |
|
|
239 |
3687 |
std::shared_ptr<ProofNode> ProofCircuitPropagator::mkProof( |
240 |
|
PfRule rule, |
241 |
|
const std::vector<std::shared_ptr<ProofNode>>& children, |
242 |
|
const std::vector<Node>& args) |
243 |
|
{ |
244 |
3687 |
if (Trace.isOn("circuit-prop")) |
245 |
|
{ |
246 |
|
std::stringstream ss; |
247 |
|
ss << "Constructing (" << rule; |
248 |
|
for (const auto& c : children) |
249 |
|
{ |
250 |
|
ss << " " << *c; |
251 |
|
} |
252 |
|
if (!args.empty()) |
253 |
|
{ |
254 |
|
ss << " :args"; |
255 |
|
for (const auto& a : args) |
256 |
|
{ |
257 |
|
ss << " " << a; |
258 |
|
} |
259 |
|
} |
260 |
|
ss << ")"; |
261 |
|
Trace("circuit-prop") << ss.str() << std::endl; |
262 |
|
} |
263 |
3687 |
return d_pnm->mkNode(rule, children, args); |
264 |
|
} |
265 |
|
|
266 |
854 |
std::shared_ptr<ProofNode> ProofCircuitPropagator::mkCResolution( |
267 |
|
const std::shared_ptr<ProofNode>& clause, |
268 |
|
const std::vector<Node>& lits, |
269 |
|
const std::vector<bool>& polarity) |
270 |
|
{ |
271 |
854 |
auto* nm = NodeManager::currentNM(); |
272 |
1708 |
std::vector<std::shared_ptr<ProofNode>> children = {clause}; |
273 |
1708 |
std::vector<Node> args; |
274 |
854 |
Assert(lits.size() == polarity.size()); |
275 |
2562 |
for (std::size_t i = 0, n = lits.size(); i < n; ++i) |
276 |
|
{ |
277 |
1708 |
bool pol = polarity[i]; |
278 |
3416 |
Node lit = lits[i]; |
279 |
1708 |
if (polarity[i]) |
280 |
|
{ |
281 |
262 |
if (lit.getKind() == Kind::NOT) |
282 |
|
{ |
283 |
18 |
lit = lit[0]; |
284 |
18 |
pol = !pol; |
285 |
18 |
children.emplace_back(assume(lit)); |
286 |
|
} |
287 |
|
else |
288 |
|
{ |
289 |
244 |
children.emplace_back(assume(lit.notNode())); |
290 |
|
} |
291 |
|
} |
292 |
|
else |
293 |
|
{ |
294 |
1446 |
children.emplace_back(assume(lit)); |
295 |
|
} |
296 |
1708 |
args.emplace_back(nm->mkConst(pol)); |
297 |
1708 |
args.emplace_back(lit); |
298 |
|
} |
299 |
1708 |
return mkProof(PfRule::CHAIN_RESOLUTION, children, args); |
300 |
|
} |
301 |
|
|
302 |
|
std::shared_ptr<ProofNode> ProofCircuitPropagator::mkCResolution( |
303 |
|
const std::shared_ptr<ProofNode>& clause, |
304 |
|
const std::vector<Node>& lits, |
305 |
|
bool polarity) |
306 |
|
{ |
307 |
|
return mkCResolution(clause, lits, std::vector<bool>(lits.size(), polarity)); |
308 |
|
} |
309 |
|
|
310 |
28 |
std::shared_ptr<ProofNode> ProofCircuitPropagator::mkResolution( |
311 |
|
const std::shared_ptr<ProofNode>& clause, const Node& lit, bool polarity) |
312 |
|
{ |
313 |
28 |
auto* nm = NodeManager::currentNM(); |
314 |
28 |
if (polarity) |
315 |
|
{ |
316 |
12 |
if (lit.getKind() == Kind::NOT) |
317 |
|
{ |
318 |
|
return mkProof(PfRule::RESOLUTION, |
319 |
|
{clause, assume(lit[0])}, |
320 |
4 |
{nm->mkConst(false), lit[0]}); |
321 |
|
} |
322 |
|
return mkProof(PfRule::RESOLUTION, |
323 |
16 |
{clause, assume(lit.notNode())}, |
324 |
24 |
{nm->mkConst(true), lit}); |
325 |
|
} |
326 |
|
return mkProof( |
327 |
16 |
PfRule::RESOLUTION, {clause, assume(lit)}, {nm->mkConst(false), lit}); |
328 |
|
} |
329 |
|
|
330 |
442 |
std::shared_ptr<ProofNode> ProofCircuitPropagator::mkNot( |
331 |
|
const std::shared_ptr<ProofNode>& n) |
332 |
|
{ |
333 |
884 |
Node m = n->getResult(); |
334 |
442 |
if (m.getKind() == Kind::NOT && m[0].getKind() == Kind::NOT) |
335 |
|
{ |
336 |
17 |
return mkProof(PfRule::NOT_NOT_ELIM, {n}); |
337 |
|
} |
338 |
425 |
return n; |
339 |
|
} |
340 |
|
|
341 |
529014 |
ProofCircuitPropagatorBackward::ProofCircuitPropagatorBackward( |
342 |
529014 |
ProofNodeManager* pnm, TNode parent, bool parentAssignment) |
343 |
|
: ProofCircuitPropagator(pnm), |
344 |
|
d_parent(parent), |
345 |
529014 |
d_parentAssignment(parentAssignment) |
346 |
|
{ |
347 |
529014 |
} |
348 |
|
|
349 |
480886 |
std::shared_ptr<ProofNode> ProofCircuitPropagatorBackward::andTrue( |
350 |
|
TNode::iterator i) |
351 |
|
{ |
352 |
480886 |
if (disabled()) |
353 |
|
{ |
354 |
479448 |
return nullptr; |
355 |
|
} |
356 |
|
return mkProof( |
357 |
1438 |
PfRule::AND_ELIM, {assume(d_parent)}, {mkRat(i - d_parent.begin())}); |
358 |
|
} |
359 |
|
|
360 |
2201 |
std::shared_ptr<ProofNode> ProofCircuitPropagatorBackward::orFalse( |
361 |
|
TNode::iterator i) |
362 |
|
{ |
363 |
2201 |
if (disabled()) |
364 |
|
{ |
365 |
2201 |
return nullptr; |
366 |
|
} |
367 |
|
return mkNot(mkProof(PfRule::NOT_OR_ELIM, |
368 |
|
{assume(d_parent.notNode())}, |
369 |
|
{mkRat(i - d_parent.begin())})); |
370 |
|
} |
371 |
|
|
372 |
8 |
std::shared_ptr<ProofNode> ProofCircuitPropagatorBackward::iteC(bool c) |
373 |
|
{ |
374 |
8 |
if (disabled()) |
375 |
|
{ |
376 |
8 |
return nullptr; |
377 |
|
} |
378 |
|
if (d_parentAssignment) |
379 |
|
{ |
380 |
|
return mkResolution( |
381 |
|
mkProof(c ? PfRule::ITE_ELIM1 : PfRule::ITE_ELIM2, {assume(d_parent)}), |
382 |
|
d_parent[0], |
383 |
|
!c); |
384 |
|
} |
385 |
|
return mkResolution(mkProof(c ? PfRule::NOT_ITE_ELIM1 : PfRule::NOT_ITE_ELIM2, |
386 |
|
{assume(d_parent.notNode())}), |
387 |
|
d_parent[0], |
388 |
|
!c); |
389 |
|
} |
390 |
|
|
391 |
|
std::shared_ptr<ProofNode> ProofCircuitPropagatorBackward::iteIsCase(unsigned c) |
392 |
|
{ |
393 |
|
if (disabled()) |
394 |
|
{ |
395 |
|
return nullptr; |
396 |
|
} |
397 |
|
if (d_parentAssignment) |
398 |
|
{ |
399 |
|
return mkResolution( |
400 |
|
mkProof(PfRule::ITE_ELIM2, {assume(d_parent)}), d_parent[c + 1], false); |
401 |
|
} |
402 |
|
return mkResolution( |
403 |
|
mkProof(PfRule::NOT_ITE_ELIM2, {assume(d_parent.notNode())}), |
404 |
|
d_parent[c + 1], |
405 |
|
false); |
406 |
|
} |
407 |
|
|
408 |
395 |
std::shared_ptr<ProofNode> ProofCircuitPropagatorBackward::impliesNegX() |
409 |
|
{ |
410 |
395 |
if (disabled()) |
411 |
|
{ |
412 |
395 |
return nullptr; |
413 |
|
} |
414 |
|
return mkNot( |
415 |
|
mkProof(PfRule::NOT_IMPLIES_ELIM1, {assume(d_parent.notNode())})); |
416 |
|
} |
417 |
|
|
418 |
395 |
std::shared_ptr<ProofNode> ProofCircuitPropagatorBackward::impliesNegY() |
419 |
|
{ |
420 |
395 |
if (disabled()) |
421 |
|
{ |
422 |
395 |
return nullptr; |
423 |
|
} |
424 |
|
return mkNot( |
425 |
|
mkProof(PfRule::NOT_IMPLIES_ELIM2, {assume(d_parent.notNode())})); |
426 |
|
} |
427 |
|
|
428 |
496905 |
ProofCircuitPropagatorForward::ProofCircuitPropagatorForward( |
429 |
496905 |
ProofNodeManager* pnm, Node child, bool childAssignment, Node parent) |
430 |
|
: ProofCircuitPropagator{pnm}, |
431 |
|
d_child(child), |
432 |
|
d_childAssignment(childAssignment), |
433 |
496905 |
d_parent(parent) |
434 |
|
{ |
435 |
496905 |
} |
436 |
|
|
437 |
10994 |
std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::andAllTrue() |
438 |
|
{ |
439 |
10994 |
if (disabled()) |
440 |
|
{ |
441 |
10994 |
return nullptr; |
442 |
|
} |
443 |
|
std::vector<std::shared_ptr<ProofNode>> children; |
444 |
|
for (const auto& child : d_parent) |
445 |
|
{ |
446 |
|
children.emplace_back(assume(child)); |
447 |
|
} |
448 |
|
return mkProof(PfRule::AND_INTRO, children); |
449 |
|
} |
450 |
|
|
451 |
2873 |
std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::andOneFalse() |
452 |
|
{ |
453 |
2873 |
if (disabled()) |
454 |
|
{ |
455 |
2873 |
return nullptr; |
456 |
|
} |
457 |
|
auto it = std::find(d_parent.begin(), d_parent.end(), d_child); |
458 |
|
return mkResolution( |
459 |
|
mkProof( |
460 |
|
PfRule::CNF_AND_POS, {}, {d_parent, mkRat(it - d_parent.begin())}), |
461 |
|
d_child, |
462 |
|
true); |
463 |
|
} |
464 |
|
|
465 |
242050 |
std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::orOneTrue() |
466 |
|
{ |
467 |
242050 |
if (disabled()) |
468 |
|
{ |
469 |
242050 |
return nullptr; |
470 |
|
} |
471 |
|
auto it = std::find(d_parent.begin(), d_parent.end(), d_child); |
472 |
|
return mkNot(mkResolution( |
473 |
|
mkProof(PfRule::CNF_OR_NEG, {}, {d_parent, mkRat(it - d_parent.begin())}), |
474 |
|
d_child, |
475 |
|
false)); |
476 |
|
} |
477 |
|
|
478 |
2159 |
std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::orFalse() |
479 |
|
{ |
480 |
2159 |
if (disabled()) |
481 |
|
{ |
482 |
2159 |
return nullptr; |
483 |
|
} |
484 |
|
std::vector<Node> children(d_parent.begin(), d_parent.end()); |
485 |
|
return mkCResolution( |
486 |
|
mkProof(PfRule::CNF_OR_POS, {}, {d_parent}), children, true); |
487 |
|
} |
488 |
|
|
489 |
10 |
std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::iteEvalThen(bool x) |
490 |
|
{ |
491 |
10 |
if (disabled()) |
492 |
|
{ |
493 |
10 |
return nullptr; |
494 |
|
} |
495 |
|
return mkCResolution( |
496 |
|
mkProof(x ? PfRule::CNF_ITE_NEG1 : PfRule::CNF_ITE_POS1, {}, {d_parent}), |
497 |
|
{d_parent[0], d_parent[1]}, |
498 |
|
{false, !x}); |
499 |
|
} |
500 |
|
|
501 |
7 |
std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::iteEvalElse(bool y) |
502 |
|
{ |
503 |
7 |
if (disabled()) |
504 |
|
{ |
505 |
7 |
return nullptr; |
506 |
|
} |
507 |
|
return mkCResolution( |
508 |
|
mkProof(y ? PfRule::CNF_ITE_NEG2 : PfRule::CNF_ITE_POS2, {}, {d_parent}), |
509 |
|
{d_parent[0], d_parent[2]}, |
510 |
|
{true, !y}); |
511 |
|
} |
512 |
|
|
513 |
1067 |
std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::eqEval(bool x, bool y) |
514 |
|
{ |
515 |
1067 |
if (disabled()) |
516 |
|
{ |
517 |
213 |
return nullptr; |
518 |
|
} |
519 |
854 |
if (x == y) |
520 |
|
{ |
521 |
|
return mkCResolution( |
522 |
2514 |
mkProof(x ? PfRule::CNF_EQUIV_NEG2 : PfRule::CNF_EQUIV_NEG1, |
523 |
|
{}, |
524 |
838 |
{d_parent}), |
525 |
|
{d_parent[0], d_parent[1]}, |
526 |
2514 |
{!x, !y}); |
527 |
|
} |
528 |
|
return mkCResolution( |
529 |
48 |
mkProof( |
530 |
16 |
x ? PfRule::CNF_EQUIV_POS1 : PfRule::CNF_EQUIV_POS2, {}, {d_parent}), |
531 |
|
{d_parent[0], d_parent[1]}, |
532 |
48 |
{!x, !y}); |
533 |
|
} |
534 |
|
|
535 |
1290 |
std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::impliesEval( |
536 |
|
bool premise, bool conclusion) |
537 |
|
{ |
538 |
1290 |
if (disabled()) |
539 |
|
{ |
540 |
1290 |
return nullptr; |
541 |
|
} |
542 |
|
if (!premise) |
543 |
|
{ |
544 |
|
return mkResolution( |
545 |
|
mkProof(PfRule::CNF_IMPLIES_NEG1, {}, {d_parent}), d_parent[0], true); |
546 |
|
} |
547 |
|
if (conclusion) |
548 |
|
{ |
549 |
|
return mkResolution( |
550 |
|
mkProof(PfRule::CNF_IMPLIES_NEG2, {}, {d_parent}), d_parent[1], false); |
551 |
|
} |
552 |
|
return mkCResolution(mkProof(PfRule::CNF_IMPLIES_POS, {}, {d_parent}), |
553 |
|
{d_parent[0], d_parent[1]}, |
554 |
|
{false, true}); |
555 |
|
} |
556 |
|
|
557 |
24 |
std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::xorEval(bool x, |
558 |
|
bool y) |
559 |
|
{ |
560 |
24 |
if (disabled()) |
561 |
|
{ |
562 |
24 |
return nullptr; |
563 |
|
} |
564 |
|
if (x && y) |
565 |
|
{ |
566 |
|
return mkCResolution(mkProof(PfRule::CNF_XOR_POS2, {}, {d_parent}), |
567 |
|
{d_parent[0], d_parent[1]}, |
568 |
|
{false, false}); |
569 |
|
} |
570 |
|
else if (x && !y) |
571 |
|
{ |
572 |
|
return mkCResolution(mkProof(PfRule::CNF_XOR_NEG1, {}, {d_parent}), |
573 |
|
{d_parent[0], d_parent[1]}, |
574 |
|
{false, true}); |
575 |
|
} |
576 |
|
else if (!x && y) |
577 |
|
{ |
578 |
|
return mkCResolution(mkProof(PfRule::CNF_XOR_NEG2, {}, {d_parent}), |
579 |
|
{d_parent[0], d_parent[1]}, |
580 |
|
{true, false}); |
581 |
|
} |
582 |
|
Assert(!x && !y); |
583 |
|
return mkCResolution(mkProof(PfRule::CNF_XOR_POS1, {}, {d_parent}), |
584 |
|
{d_parent[0], d_parent[1]}, |
585 |
|
{true, true}); |
586 |
|
} |
587 |
|
|
588 |
|
} // namespace booleans |
589 |
|
} // namespace theory |
590 |
22746 |
} // namespace cvc5 |