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 |
48393 |
Node mkRat(T val) |
33 |
|
{ |
34 |
48393 |
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 |
1391 |
inline std::vector<Node> collectButHoldout(TNode parent, |
43 |
|
TNode::iterator holdout) |
44 |
|
{ |
45 |
1391 |
std::vector<Node> lits; |
46 |
4442 |
for (TNode::iterator i = parent.begin(), i_end = parent.end(); i != i_end; |
47 |
|
++i) |
48 |
|
{ |
49 |
3051 |
if (i != holdout) |
50 |
|
{ |
51 |
1660 |
lits.emplace_back(*i); |
52 |
|
} |
53 |
|
} |
54 |
1391 |
return lits; |
55 |
|
} |
56 |
|
|
57 |
|
} // namespace |
58 |
|
|
59 |
379538 |
ProofCircuitPropagator::ProofCircuitPropagator(ProofNodeManager* pnm) |
60 |
379538 |
: d_pnm(pnm) |
61 |
|
{ |
62 |
379538 |
} |
63 |
|
|
64 |
368963 |
bool ProofCircuitPropagator::disabled() const { return d_pnm == nullptr; } |
65 |
|
|
66 |
9001657 |
std::shared_ptr<ProofNode> ProofCircuitPropagator::assume(Node n) |
67 |
|
{ |
68 |
9001657 |
return d_pnm->mkAssume(n); |
69 |
|
} |
70 |
|
|
71 |
1550 |
std::shared_ptr<ProofNode> ProofCircuitPropagator::conflict( |
72 |
|
const std::shared_ptr<ProofNode>& a, const std::shared_ptr<ProofNode>& b) |
73 |
|
{ |
74 |
1550 |
if (a->getResult().notNode() == b->getResult()) |
75 |
|
{ |
76 |
1365 |
return mkProof(PfRule::CONTRA, {a, b}); |
77 |
|
} |
78 |
185 |
Assert(a->getResult() == b->getResult().notNode()); |
79 |
185 |
return mkProof(PfRule::CONTRA, {b, a}); |
80 |
|
} |
81 |
|
|
82 |
933 |
std::shared_ptr<ProofNode> ProofCircuitPropagator::andFalse( |
83 |
|
Node parent, TNode::iterator holdout) |
84 |
|
{ |
85 |
933 |
if (disabled()) |
86 |
|
{ |
87 |
547 |
return nullptr; |
88 |
|
} |
89 |
|
return mkNot( |
90 |
772 |
mkCResolution(mkProof(PfRule::NOT_AND, {assume(parent.notNode())}), |
91 |
772 |
collectButHoldout(parent, holdout), |
92 |
386 |
false)); |
93 |
|
} |
94 |
|
|
95 |
22086 |
std::shared_ptr<ProofNode> ProofCircuitPropagator::orTrue( |
96 |
|
Node parent, TNode::iterator holdout) |
97 |
|
{ |
98 |
22086 |
if (disabled()) |
99 |
|
{ |
100 |
21081 |
return nullptr; |
101 |
|
} |
102 |
|
return mkCResolution( |
103 |
1005 |
assume(parent), collectButHoldout(parent, holdout), true); |
104 |
|
} |
105 |
|
|
106 |
99222 |
std::shared_ptr<ProofNode> ProofCircuitPropagator::Not(bool negate, Node parent) |
107 |
|
{ |
108 |
99222 |
if (disabled()) |
109 |
|
{ |
110 |
66707 |
return nullptr; |
111 |
|
} |
112 |
32515 |
return mkNot(assume(negate ? Node(parent[0]) : parent)); |
113 |
|
} |
114 |
|
|
115 |
56 |
std::shared_ptr<ProofNode> ProofCircuitPropagator::impliesXFromY(Node parent) |
116 |
|
{ |
117 |
56 |
if (disabled()) |
118 |
|
{ |
119 |
29 |
return nullptr; |
120 |
|
} |
121 |
108 |
return mkNot(mkResolution( |
122 |
81 |
mkProof(PfRule::IMPLIES_ELIM, {assume(parent)}), parent[1], true)); |
123 |
|
} |
124 |
|
|
125 |
652 |
std::shared_ptr<ProofNode> ProofCircuitPropagator::impliesYFromX(Node parent) |
126 |
|
{ |
127 |
652 |
if (disabled()) |
128 |
|
{ |
129 |
449 |
return nullptr; |
130 |
|
} |
131 |
|
return mkResolution( |
132 |
203 |
mkProof(PfRule::IMPLIES_ELIM, {assume(parent)}), parent[0], false); |
133 |
|
} |
134 |
|
|
135 |
285 |
std::shared_ptr<ProofNode> ProofCircuitPropagator::eqXFromY(bool y, Node parent) |
136 |
|
{ |
137 |
285 |
if (disabled()) |
138 |
|
{ |
139 |
27 |
return nullptr; |
140 |
|
} |
141 |
258 |
if (y) |
142 |
|
{ |
143 |
|
return mkProof( |
144 |
|
PfRule::EQ_RESOLVE, |
145 |
105 |
{assume(parent[1]), mkProof(PfRule::SYMM, {assume(parent)})}); |
146 |
|
} |
147 |
612 |
return mkNot(mkResolution( |
148 |
459 |
mkProof(PfRule::EQUIV_ELIM1, {assume(parent)}), parent[1], true)); |
149 |
|
} |
150 |
|
|
151 |
1003 |
std::shared_ptr<ProofNode> ProofCircuitPropagator::eqYFromX(bool x, Node parent) |
152 |
|
{ |
153 |
1003 |
if (disabled()) |
154 |
|
{ |
155 |
124 |
return nullptr; |
156 |
|
} |
157 |
879 |
if (x) |
158 |
|
{ |
159 |
654 |
return mkProof(PfRule::EQ_RESOLVE, {assume(parent[0]), assume(parent)}); |
160 |
|
} |
161 |
900 |
return mkNot(mkResolution( |
162 |
675 |
mkProof(PfRule::EQUIV_ELIM2, {assume(parent)}), parent[0], true)); |
163 |
|
} |
164 |
|
|
165 |
45 |
std::shared_ptr<ProofNode> ProofCircuitPropagator::neqXFromY(bool y, |
166 |
|
Node parent) |
167 |
|
{ |
168 |
45 |
if (disabled()) |
169 |
|
{ |
170 |
2 |
return nullptr; |
171 |
|
} |
172 |
172 |
return mkNot(mkResolution( |
173 |
215 |
mkProof(y ? PfRule::NOT_EQUIV_ELIM2 : PfRule::NOT_EQUIV_ELIM1, |
174 |
129 |
{assume(parent.notNode())}), |
175 |
|
parent[1], |
176 |
86 |
!y)); |
177 |
|
} |
178 |
|
|
179 |
72 |
std::shared_ptr<ProofNode> ProofCircuitPropagator::neqYFromX(bool x, |
180 |
|
Node parent) |
181 |
|
{ |
182 |
72 |
if (disabled()) |
183 |
|
{ |
184 |
5 |
return nullptr; |
185 |
|
} |
186 |
268 |
return mkNot(mkResolution( |
187 |
335 |
mkProof(x ? PfRule::NOT_EQUIV_ELIM2 : PfRule::NOT_EQUIV_ELIM1, |
188 |
201 |
{assume(parent.notNode())}), |
189 |
|
parent[0], |
190 |
134 |
!x)); |
191 |
|
} |
192 |
|
|
193 |
30 |
std::shared_ptr<ProofNode> ProofCircuitPropagator::xorXFromY(bool negated, |
194 |
|
bool y, |
195 |
|
Node parent) |
196 |
|
{ |
197 |
30 |
if (disabled()) |
198 |
|
{ |
199 |
18 |
return nullptr; |
200 |
|
} |
201 |
12 |
if (y) |
202 |
|
{ |
203 |
32 |
return mkNot(mkResolution( |
204 |
40 |
mkProof(negated ? PfRule::NOT_XOR_ELIM1 : PfRule::XOR_ELIM2, |
205 |
24 |
{assume(negated ? parent.notNode() : Node(parent))}), |
206 |
|
parent[1], |
207 |
8 |
false)); |
208 |
|
} |
209 |
|
return mkNot( |
210 |
20 |
mkResolution(mkProof(negated ? PfRule::NOT_XOR_ELIM2 : PfRule::XOR_ELIM1, |
211 |
12 |
{assume(negated ? parent.notNode() : Node(parent))}), |
212 |
|
parent[1], |
213 |
4 |
true)); |
214 |
|
} |
215 |
|
|
216 |
37 |
std::shared_ptr<ProofNode> ProofCircuitPropagator::xorYFromX(bool negated, |
217 |
|
bool x, |
218 |
|
Node parent) |
219 |
|
{ |
220 |
37 |
if (disabled()) |
221 |
|
{ |
222 |
20 |
return nullptr; |
223 |
|
} |
224 |
17 |
if (x) |
225 |
|
{ |
226 |
32 |
return mkNot(mkResolution( |
227 |
40 |
mkProof(negated ? PfRule::NOT_XOR_ELIM2 : PfRule::XOR_ELIM2, |
228 |
24 |
{assume(negated ? parent.notNode() : Node(parent))}), |
229 |
|
parent[0], |
230 |
8 |
false)); |
231 |
|
} |
232 |
|
return mkNot( |
233 |
45 |
mkResolution(mkProof(negated ? PfRule::NOT_XOR_ELIM1 : PfRule::XOR_ELIM1, |
234 |
27 |
{assume(negated ? parent.notNode() : Node(parent))}), |
235 |
|
parent[0], |
236 |
9 |
true)); |
237 |
|
} |
238 |
|
|
239 |
82095 |
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 |
82095 |
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 |
82095 |
return d_pnm->mkNode(rule, children, args); |
264 |
|
} |
265 |
|
|
266 |
7940 |
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 |
7940 |
auto* nm = NodeManager::currentNM(); |
272 |
15880 |
std::vector<std::shared_ptr<ProofNode>> children = {clause}; |
273 |
15880 |
std::vector<Node> args; |
274 |
7940 |
Assert(lits.size() == polarity.size()); |
275 |
204060 |
for (std::size_t i = 0, n = lits.size(); i < n; ++i) |
276 |
|
{ |
277 |
196120 |
bool pol = polarity[i]; |
278 |
392240 |
Node lit = lits[i]; |
279 |
196120 |
if (polarity[i]) |
280 |
|
{ |
281 |
190406 |
if (lit.getKind() == Kind::NOT) |
282 |
|
{ |
283 |
167301 |
lit = lit[0]; |
284 |
167301 |
pol = !pol; |
285 |
167301 |
children.emplace_back(assume(lit)); |
286 |
|
} |
287 |
|
else |
288 |
|
{ |
289 |
23105 |
children.emplace_back(assume(lit.notNode())); |
290 |
|
} |
291 |
|
} |
292 |
|
else |
293 |
|
{ |
294 |
5714 |
children.emplace_back(assume(lit)); |
295 |
|
} |
296 |
196120 |
args.emplace_back(nm->mkConst(pol)); |
297 |
196120 |
args.emplace_back(lit); |
298 |
|
} |
299 |
15880 |
return mkProof(PfRule::CHAIN_RESOLUTION, children, args); |
300 |
|
} |
301 |
|
|
302 |
3499 |
std::shared_ptr<ProofNode> ProofCircuitPropagator::mkCResolution( |
303 |
|
const std::shared_ptr<ProofNode>& clause, |
304 |
|
const std::vector<Node>& lits, |
305 |
|
bool polarity) |
306 |
|
{ |
307 |
3499 |
return mkCResolution(clause, lits, std::vector<bool>(lits.size(), polarity)); |
308 |
|
} |
309 |
|
|
310 |
6033 |
std::shared_ptr<ProofNode> ProofCircuitPropagator::mkResolution( |
311 |
|
const std::shared_ptr<ProofNode>& clause, const Node& lit, bool polarity) |
312 |
|
{ |
313 |
6033 |
auto* nm = NodeManager::currentNM(); |
314 |
6033 |
if (polarity) |
315 |
|
{ |
316 |
2438 |
if (lit.getKind() == Kind::NOT) |
317 |
|
{ |
318 |
|
return mkProof(PfRule::RESOLUTION, |
319 |
|
{clause, assume(lit[0])}, |
320 |
335 |
{nm->mkConst(false), lit[0]}); |
321 |
|
} |
322 |
|
return mkProof(PfRule::RESOLUTION, |
323 |
4206 |
{clause, assume(lit.notNode())}, |
324 |
6309 |
{nm->mkConst(true), lit}); |
325 |
|
} |
326 |
|
return mkProof( |
327 |
3595 |
PfRule::RESOLUTION, {clause, assume(lit)}, {nm->mkConst(false), lit}); |
328 |
|
} |
329 |
|
|
330 |
38705 |
std::shared_ptr<ProofNode> ProofCircuitPropagator::mkNot( |
331 |
|
const std::shared_ptr<ProofNode>& n) |
332 |
|
{ |
333 |
77410 |
Node m = n->getResult(); |
334 |
38705 |
if (m.getKind() == Kind::NOT && m[0].getKind() == Kind::NOT) |
335 |
|
{ |
336 |
873 |
return mkProof(PfRule::NOT_NOT_ELIM, {n}); |
337 |
|
} |
338 |
37832 |
return n; |
339 |
|
} |
340 |
|
|
341 |
180039 |
ProofCircuitPropagatorBackward::ProofCircuitPropagatorBackward( |
342 |
180039 |
ProofNodeManager* pnm, TNode parent, bool parentAssignment) |
343 |
|
: ProofCircuitPropagator(pnm), |
344 |
|
d_parent(parent), |
345 |
180039 |
d_parentAssignment(parentAssignment) |
346 |
|
{ |
347 |
180039 |
} |
348 |
|
|
349 |
145417 |
std::shared_ptr<ProofNode> ProofCircuitPropagatorBackward::andTrue( |
350 |
|
TNode::iterator i) |
351 |
|
{ |
352 |
145417 |
if (disabled()) |
353 |
|
{ |
354 |
103232 |
return nullptr; |
355 |
|
} |
356 |
|
return mkProof( |
357 |
42185 |
PfRule::AND_ELIM, {assume(d_parent)}, {mkRat(i - d_parent.begin())}); |
358 |
|
} |
359 |
|
|
360 |
4645 |
std::shared_ptr<ProofNode> ProofCircuitPropagatorBackward::orFalse( |
361 |
|
TNode::iterator i) |
362 |
|
{ |
363 |
4645 |
if (disabled()) |
364 |
|
{ |
365 |
2199 |
return nullptr; |
366 |
|
} |
367 |
14676 |
return mkNot(mkProof(PfRule::NOT_OR_ELIM, |
368 |
4892 |
{assume(d_parent.notNode())}, |
369 |
9784 |
{mkRat(i - d_parent.begin())})); |
370 |
|
} |
371 |
|
|
372 |
1272 |
std::shared_ptr<ProofNode> ProofCircuitPropagatorBackward::iteC(bool c) |
373 |
|
{ |
374 |
1272 |
if (disabled()) |
375 |
|
{ |
376 |
8 |
return nullptr; |
377 |
|
} |
378 |
1264 |
if (d_parentAssignment) |
379 |
|
{ |
380 |
|
return mkResolution( |
381 |
2052 |
mkProof(c ? PfRule::ITE_ELIM1 : PfRule::ITE_ELIM2, {assume(d_parent)}), |
382 |
|
d_parent[0], |
383 |
3078 |
!c); |
384 |
|
} |
385 |
|
return mkNot( |
386 |
1428 |
mkResolution(mkProof(c ? PfRule::NOT_ITE_ELIM1 : PfRule::NOT_ITE_ELIM2, |
387 |
714 |
{assume(d_parent.notNode())}), |
388 |
|
d_parent[0], |
389 |
714 |
!c)); |
390 |
|
} |
391 |
|
|
392 |
28 |
std::shared_ptr<ProofNode> ProofCircuitPropagatorBackward::iteIsCase(unsigned c) |
393 |
|
{ |
394 |
28 |
if (disabled()) |
395 |
|
{ |
396 |
|
return nullptr; |
397 |
|
} |
398 |
28 |
if (d_parentAssignment) |
399 |
|
{ |
400 |
60 |
return mkResolution(mkProof(c == 0 ? PfRule::ITE_ELIM1 : PfRule::ITE_ELIM2, |
401 |
20 |
{assume(d_parent)}), |
402 |
20 |
d_parent[c + 1], |
403 |
80 |
true); |
404 |
|
} |
405 |
|
return mkResolution( |
406 |
40 |
mkProof(c == 0 ? PfRule::NOT_ITE_ELIM1 : PfRule::NOT_ITE_ELIM2, |
407 |
24 |
{assume(d_parent.notNode())}), |
408 |
8 |
d_parent[c + 1], |
409 |
32 |
false); |
410 |
|
} |
411 |
|
|
412 |
602 |
std::shared_ptr<ProofNode> ProofCircuitPropagatorBackward::impliesNegX() |
413 |
|
{ |
414 |
602 |
if (disabled()) |
415 |
|
{ |
416 |
397 |
return nullptr; |
417 |
|
} |
418 |
|
return mkNot( |
419 |
205 |
mkProof(PfRule::NOT_IMPLIES_ELIM1, {assume(d_parent.notNode())})); |
420 |
|
} |
421 |
|
|
422 |
602 |
std::shared_ptr<ProofNode> ProofCircuitPropagatorBackward::impliesNegY() |
423 |
|
{ |
424 |
602 |
if (disabled()) |
425 |
|
{ |
426 |
397 |
return nullptr; |
427 |
|
} |
428 |
|
return mkNot( |
429 |
205 |
mkProof(PfRule::NOT_IMPLIES_ELIM2, {assume(d_parent.notNode())})); |
430 |
|
} |
431 |
|
|
432 |
197494 |
ProofCircuitPropagatorForward::ProofCircuitPropagatorForward( |
433 |
197494 |
ProofNodeManager* pnm, Node child, bool childAssignment, Node parent) |
434 |
|
: ProofCircuitPropagator{pnm}, |
435 |
|
d_child(child), |
436 |
|
d_childAssignment(childAssignment), |
437 |
197494 |
d_parent(parent) |
438 |
|
{ |
439 |
197494 |
} |
440 |
|
|
441 |
17820 |
std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::andAllTrue() |
442 |
|
{ |
443 |
17820 |
if (disabled()) |
444 |
|
{ |
445 |
10994 |
return nullptr; |
446 |
|
} |
447 |
13652 |
std::vector<std::shared_ptr<ProofNode>> children; |
448 |
8715948 |
for (const auto& child : d_parent) |
449 |
|
{ |
450 |
8709122 |
children.emplace_back(assume(child)); |
451 |
|
} |
452 |
6826 |
return mkProof(PfRule::AND_INTRO, children); |
453 |
|
} |
454 |
|
|
455 |
4468 |
std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::andOneFalse() |
456 |
|
{ |
457 |
4468 |
if (disabled()) |
458 |
|
{ |
459 |
2872 |
return nullptr; |
460 |
|
} |
461 |
1596 |
auto it = std::find(d_parent.begin(), d_parent.end(), d_child); |
462 |
|
return mkResolution( |
463 |
6384 |
mkProof( |
464 |
3192 |
PfRule::CNF_AND_POS, {}, {d_parent, mkRat(it - d_parent.begin())}), |
465 |
|
d_child, |
466 |
3192 |
true); |
467 |
|
} |
468 |
|
|
469 |
59200 |
std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::orOneTrue() |
470 |
|
{ |
471 |
59200 |
if (disabled()) |
472 |
|
{ |
473 |
57034 |
return nullptr; |
474 |
|
} |
475 |
2166 |
auto it = std::find(d_parent.begin(), d_parent.end(), d_child); |
476 |
6498 |
return mkNot(mkResolution( |
477 |
4332 |
mkProof(PfRule::CNF_OR_NEG, {}, {d_parent, mkRat(it - d_parent.begin())}), |
478 |
|
d_child, |
479 |
4332 |
false)); |
480 |
|
} |
481 |
|
|
482 |
4265 |
std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::orFalse() |
483 |
|
{ |
484 |
4265 |
if (disabled()) |
485 |
|
{ |
486 |
2157 |
return nullptr; |
487 |
|
} |
488 |
4216 |
std::vector<Node> children(d_parent.begin(), d_parent.end()); |
489 |
|
return mkCResolution( |
490 |
2108 |
mkProof(PfRule::CNF_OR_POS, {}, {d_parent}), children, true); |
491 |
|
} |
492 |
|
|
493 |
1345 |
std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::iteEvalThen(bool x) |
494 |
|
{ |
495 |
1345 |
if (disabled()) |
496 |
|
{ |
497 |
10 |
return nullptr; |
498 |
|
} |
499 |
|
return mkCResolution( |
500 |
2670 |
mkProof(x ? PfRule::CNF_ITE_NEG1 : PfRule::CNF_ITE_POS1, {}, {d_parent}), |
501 |
|
{d_parent[0], d_parent[1]}, |
502 |
4005 |
{false, !x}); |
503 |
|
} |
504 |
|
|
505 |
863 |
std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::iteEvalElse(bool y) |
506 |
|
{ |
507 |
863 |
if (disabled()) |
508 |
|
{ |
509 |
7 |
return nullptr; |
510 |
|
} |
511 |
|
return mkCResolution( |
512 |
1712 |
mkProof(y ? PfRule::CNF_ITE_NEG2 : PfRule::CNF_ITE_POS2, {}, {d_parent}), |
513 |
|
{d_parent[0], d_parent[2]}, |
514 |
2568 |
{true, !y}); |
515 |
|
} |
516 |
|
|
517 |
2048 |
std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::eqEval(bool x, bool y) |
518 |
|
{ |
519 |
2048 |
if (disabled()) |
520 |
|
{ |
521 |
213 |
return nullptr; |
522 |
|
} |
523 |
1835 |
if (x == y) |
524 |
|
{ |
525 |
|
return mkCResolution( |
526 |
4785 |
mkProof(x ? PfRule::CNF_EQUIV_NEG2 : PfRule::CNF_EQUIV_NEG1, |
527 |
|
{}, |
528 |
1595 |
{d_parent}), |
529 |
|
{d_parent[0], d_parent[1]}, |
530 |
4785 |
{!x, !y}); |
531 |
|
} |
532 |
|
return mkCResolution( |
533 |
720 |
mkProof( |
534 |
240 |
x ? PfRule::CNF_EQUIV_POS1 : PfRule::CNF_EQUIV_POS2, {}, {d_parent}), |
535 |
|
{d_parent[0], d_parent[1]}, |
536 |
720 |
{!x, !y}); |
537 |
|
} |
538 |
|
|
539 |
1918 |
std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::impliesEval( |
540 |
|
bool premise, bool conclusion) |
541 |
|
{ |
542 |
1918 |
if (disabled()) |
543 |
|
{ |
544 |
1292 |
return nullptr; |
545 |
|
} |
546 |
626 |
if (!premise) |
547 |
|
{ |
548 |
|
return mkResolution( |
549 |
31 |
mkProof(PfRule::CNF_IMPLIES_NEG1, {}, {d_parent}), d_parent[0], true); |
550 |
|
} |
551 |
595 |
if (conclusion) |
552 |
|
{ |
553 |
|
return mkResolution( |
554 |
201 |
mkProof(PfRule::CNF_IMPLIES_NEG2, {}, {d_parent}), d_parent[1], false); |
555 |
|
} |
556 |
788 |
return mkCResolution(mkProof(PfRule::CNF_IMPLIES_POS, {}, {d_parent}), |
557 |
|
{d_parent[0], d_parent[1]}, |
558 |
1182 |
{false, true}); |
559 |
|
} |
560 |
|
|
561 |
49 |
std::shared_ptr<ProofNode> ProofCircuitPropagatorForward::xorEval(bool x, |
562 |
|
bool y) |
563 |
|
{ |
564 |
49 |
if (disabled()) |
565 |
|
{ |
566 |
28 |
return nullptr; |
567 |
|
} |
568 |
21 |
if (x && y) |
569 |
|
{ |
570 |
8 |
return mkCResolution(mkProof(PfRule::CNF_XOR_POS2, {}, {d_parent}), |
571 |
|
{d_parent[0], d_parent[1]}, |
572 |
12 |
{false, false}); |
573 |
|
} |
574 |
17 |
else if (x && !y) |
575 |
|
{ |
576 |
10 |
return mkCResolution(mkProof(PfRule::CNF_XOR_NEG1, {}, {d_parent}), |
577 |
|
{d_parent[0], d_parent[1]}, |
578 |
15 |
{false, true}); |
579 |
|
} |
580 |
12 |
else if (!x && y) |
581 |
|
{ |
582 |
12 |
return mkCResolution(mkProof(PfRule::CNF_XOR_NEG2, {}, {d_parent}), |
583 |
|
{d_parent[0], d_parent[1]}, |
584 |
18 |
{true, false}); |
585 |
|
} |
586 |
6 |
Assert(!x && !y); |
587 |
12 |
return mkCResolution(mkProof(PfRule::CNF_XOR_POS1, {}, {d_parent}), |
588 |
|
{d_parent[0], d_parent[1]}, |
589 |
18 |
{true, true}); |
590 |
|
} |
591 |
|
|
592 |
|
} // namespace booleans |
593 |
|
} // namespace theory |
594 |
31137 |
} // namespace cvc5 |