1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Haniel Barbosa, Andrew Reynolds, Mathias Preiner |
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 |
|
* Implementation of equality proof checker. |
14 |
|
*/ |
15 |
|
|
16 |
|
#include "theory/booleans/proof_checker.h" |
17 |
|
#include "expr/skolem_manager.h" |
18 |
|
#include "theory/rewriter.h" |
19 |
|
|
20 |
|
namespace cvc5 { |
21 |
|
namespace theory { |
22 |
|
namespace booleans { |
23 |
|
|
24 |
3117 |
void BoolProofRuleChecker::registerTo(ProofChecker* pc) |
25 |
|
{ |
26 |
3117 |
pc->registerChecker(PfRule::SPLIT, this); |
27 |
3117 |
pc->registerChecker(PfRule::RESOLUTION, this); |
28 |
3117 |
pc->registerChecker(PfRule::CHAIN_RESOLUTION, this); |
29 |
3117 |
pc->registerTrustedChecker(PfRule::MACRO_RESOLUTION_TRUST, this, 3); |
30 |
3117 |
pc->registerChecker(PfRule::MACRO_RESOLUTION, this); |
31 |
3117 |
pc->registerChecker(PfRule::FACTORING, this); |
32 |
3117 |
pc->registerChecker(PfRule::REORDERING, this); |
33 |
3117 |
pc->registerChecker(PfRule::EQ_RESOLVE, this); |
34 |
3117 |
pc->registerChecker(PfRule::MODUS_PONENS, this); |
35 |
3117 |
pc->registerChecker(PfRule::NOT_NOT_ELIM, this); |
36 |
3117 |
pc->registerChecker(PfRule::CONTRA, this); |
37 |
3117 |
pc->registerChecker(PfRule::AND_ELIM, this); |
38 |
3117 |
pc->registerChecker(PfRule::AND_INTRO, this); |
39 |
3117 |
pc->registerChecker(PfRule::NOT_OR_ELIM, this); |
40 |
3117 |
pc->registerChecker(PfRule::IMPLIES_ELIM, this); |
41 |
3117 |
pc->registerChecker(PfRule::NOT_IMPLIES_ELIM1, this); |
42 |
3117 |
pc->registerChecker(PfRule::NOT_IMPLIES_ELIM2, this); |
43 |
3117 |
pc->registerChecker(PfRule::EQUIV_ELIM1, this); |
44 |
3117 |
pc->registerChecker(PfRule::EQUIV_ELIM2, this); |
45 |
3117 |
pc->registerChecker(PfRule::NOT_EQUIV_ELIM1, this); |
46 |
3117 |
pc->registerChecker(PfRule::NOT_EQUIV_ELIM2, this); |
47 |
3117 |
pc->registerChecker(PfRule::XOR_ELIM1, this); |
48 |
3117 |
pc->registerChecker(PfRule::XOR_ELIM2, this); |
49 |
3117 |
pc->registerChecker(PfRule::NOT_XOR_ELIM1, this); |
50 |
3117 |
pc->registerChecker(PfRule::NOT_XOR_ELIM2, this); |
51 |
3117 |
pc->registerChecker(PfRule::ITE_ELIM1, this); |
52 |
3117 |
pc->registerChecker(PfRule::ITE_ELIM2, this); |
53 |
3117 |
pc->registerChecker(PfRule::NOT_ITE_ELIM1, this); |
54 |
3117 |
pc->registerChecker(PfRule::NOT_ITE_ELIM2, this); |
55 |
3117 |
pc->registerChecker(PfRule::NOT_AND, this); |
56 |
3117 |
pc->registerChecker(PfRule::CNF_AND_POS, this); |
57 |
3117 |
pc->registerChecker(PfRule::CNF_AND_NEG, this); |
58 |
3117 |
pc->registerChecker(PfRule::CNF_OR_POS, this); |
59 |
3117 |
pc->registerChecker(PfRule::CNF_OR_NEG, this); |
60 |
3117 |
pc->registerChecker(PfRule::CNF_IMPLIES_POS, this); |
61 |
3117 |
pc->registerChecker(PfRule::CNF_IMPLIES_NEG1, this); |
62 |
3117 |
pc->registerChecker(PfRule::CNF_IMPLIES_NEG2, this); |
63 |
3117 |
pc->registerChecker(PfRule::CNF_EQUIV_POS1, this); |
64 |
3117 |
pc->registerChecker(PfRule::CNF_EQUIV_POS2, this); |
65 |
3117 |
pc->registerChecker(PfRule::CNF_EQUIV_NEG1, this); |
66 |
3117 |
pc->registerChecker(PfRule::CNF_EQUIV_NEG2, this); |
67 |
3117 |
pc->registerChecker(PfRule::CNF_XOR_POS1, this); |
68 |
3117 |
pc->registerChecker(PfRule::CNF_XOR_POS2, this); |
69 |
3117 |
pc->registerChecker(PfRule::CNF_XOR_NEG1, this); |
70 |
3117 |
pc->registerChecker(PfRule::CNF_XOR_NEG2, this); |
71 |
3117 |
pc->registerChecker(PfRule::CNF_ITE_POS1, this); |
72 |
3117 |
pc->registerChecker(PfRule::CNF_ITE_POS2, this); |
73 |
3117 |
pc->registerChecker(PfRule::CNF_ITE_POS3, this); |
74 |
3117 |
pc->registerChecker(PfRule::CNF_ITE_NEG1, this); |
75 |
3117 |
pc->registerChecker(PfRule::CNF_ITE_NEG2, this); |
76 |
3117 |
pc->registerChecker(PfRule::CNF_ITE_NEG3, this); |
77 |
3117 |
pc->registerTrustedChecker(PfRule::SAT_REFUTATION, this, 1); |
78 |
3117 |
} |
79 |
|
|
80 |
3697394 |
Node BoolProofRuleChecker::checkInternal(PfRule id, |
81 |
|
const std::vector<Node>& children, |
82 |
|
const std::vector<Node>& args) |
83 |
|
{ |
84 |
3697394 |
if (id == PfRule::RESOLUTION) |
85 |
|
{ |
86 |
23995 |
Assert(children.size() == 2); |
87 |
23995 |
Assert(args.size() == 2); |
88 |
23995 |
NodeManager* nm = NodeManager::currentNM(); |
89 |
47990 |
std::vector<Node> disjuncts; |
90 |
47990 |
Node pivots[2]; |
91 |
23995 |
if (args[0] == nm->mkConst(true)) |
92 |
|
{ |
93 |
21696 |
pivots[0] = args[1]; |
94 |
21696 |
pivots[1] = args[1].notNode(); |
95 |
|
} |
96 |
|
else |
97 |
|
{ |
98 |
2299 |
Assert(args[0] == nm->mkConst(false)); |
99 |
2299 |
pivots[0] = args[1].notNode(); |
100 |
2299 |
pivots[1] = args[1]; |
101 |
|
} |
102 |
71985 |
for (unsigned i = 0; i < 2; ++i) |
103 |
|
{ |
104 |
|
// determine whether the clause is a singleton for effects of resolution, |
105 |
|
// which is the case if it's not an OR node or it is an OR node but it is |
106 |
|
// equal to the pivot |
107 |
95980 |
std::vector<Node> lits; |
108 |
47990 |
if (children[i].getKind() == kind::OR && pivots[i] != children[i]) |
109 |
|
{ |
110 |
44616 |
lits.insert(lits.end(), children[i].begin(), children[i].end()); |
111 |
|
} |
112 |
|
else |
113 |
|
{ |
114 |
3374 |
lits.push_back(children[i]); |
115 |
|
} |
116 |
276142 |
for (unsigned j = 0, size = lits.size(); j < size; ++j) |
117 |
|
{ |
118 |
228152 |
if (pivots[i] != lits[j]) |
119 |
|
{ |
120 |
180162 |
disjuncts.push_back(lits[j]); |
121 |
|
} |
122 |
|
else |
123 |
|
{ |
124 |
|
// just eliminate first occurrence |
125 |
47990 |
pivots[i] = Node::null(); |
126 |
|
} |
127 |
|
} |
128 |
|
} |
129 |
23995 |
return disjuncts.empty() |
130 |
|
? nm->mkConst(false) |
131 |
27369 |
: disjuncts.size() == 1 ? disjuncts[0] |
132 |
51364 |
: nm->mkNode(kind::OR, disjuncts); |
133 |
|
} |
134 |
3673399 |
if (id == PfRule::FACTORING) |
135 |
|
{ |
136 |
333102 |
Assert(children.size() == 1); |
137 |
333102 |
Assert(args.empty()); |
138 |
333102 |
if (children[0].getKind() != kind::OR) |
139 |
|
{ |
140 |
|
return Node::null(); |
141 |
|
} |
142 |
|
// remove duplicates while keeping the order of children |
143 |
666204 |
std::unordered_set<TNode> clauseSet; |
144 |
666204 |
std::vector<Node> disjuncts; |
145 |
333102 |
unsigned size = children[0].getNumChildren(); |
146 |
10528557 |
for (unsigned i = 0; i < size; ++i) |
147 |
|
{ |
148 |
10195455 |
if (clauseSet.count(children[0][i])) |
149 |
|
{ |
150 |
2776588 |
continue; |
151 |
|
} |
152 |
7418867 |
disjuncts.push_back(children[0][i]); |
153 |
7418867 |
clauseSet.insert(children[0][i]); |
154 |
|
} |
155 |
333102 |
if (disjuncts.size() == size) |
156 |
|
{ |
157 |
|
return Node::null(); |
158 |
|
} |
159 |
333102 |
NodeManager* nm = NodeManager::currentNM(); |
160 |
333102 |
return disjuncts.empty() |
161 |
|
? nm->mkConst<bool>(false) |
162 |
334133 |
: disjuncts.size() == 1 ? disjuncts[0] |
163 |
667235 |
: nm->mkNode(kind::OR, disjuncts); |
164 |
|
} |
165 |
3340297 |
if (id == PfRule::REORDERING) |
166 |
|
{ |
167 |
1176908 |
Assert(children.size() == 1); |
168 |
1176908 |
Assert(args.size() == 1); |
169 |
2353816 |
std::unordered_set<Node> clauseSet1, clauseSet2; |
170 |
1176908 |
if (children[0].getKind() == kind::OR) |
171 |
|
{ |
172 |
1176908 |
clauseSet1.insert(children[0].begin(), children[0].end()); |
173 |
|
} |
174 |
|
else |
175 |
|
{ |
176 |
|
clauseSet1.insert(children[0]); |
177 |
|
} |
178 |
1176908 |
if (args[0].getKind() == kind::OR) |
179 |
|
{ |
180 |
1176908 |
clauseSet2.insert(args[0].begin(), args[0].end()); |
181 |
|
} |
182 |
|
else |
183 |
|
{ |
184 |
|
clauseSet2.insert(args[0]); |
185 |
|
} |
186 |
1176908 |
if (clauseSet1 != clauseSet2) |
187 |
|
{ |
188 |
|
Trace("bool-pfcheck") << id << ": clause set1: " << clauseSet1 << "\n" |
189 |
|
<< id << ": clause set2: " << clauseSet2 << "\n"; |
190 |
|
return Node::null(); |
191 |
|
} |
192 |
1176908 |
return args[0]; |
193 |
|
} |
194 |
2163389 |
if (id == PfRule::CHAIN_RESOLUTION) |
195 |
|
{ |
196 |
414609 |
Assert(children.size() > 1); |
197 |
414609 |
Assert(args.size() == 2 * (children.size() - 1)); |
198 |
414609 |
Trace("bool-pfcheck") << "chain_res:\n" << push; |
199 |
414609 |
NodeManager* nm = NodeManager::currentNM(); |
200 |
829218 |
Node trueNode = nm->mkConst(true); |
201 |
829218 |
Node falseNode = nm->mkConst(false); |
202 |
829218 |
std::vector<Node> clauseNodes; |
203 |
|
// literals to be removed from the virtual lhs clause of the resolution |
204 |
829218 |
std::unordered_map<Node, unsigned> lhsElim; |
205 |
2903062 |
for (std::size_t i = 0, argsSize = args.size(); i < argsSize; i = i + 2) |
206 |
|
{ |
207 |
|
// whether pivot should occur as is or negated depends on the polarity of |
208 |
|
// each step in the chain |
209 |
2488453 |
if (args[i] == trueNode) |
210 |
|
{ |
211 |
1250404 |
lhsElim[args[i + 1]]++; |
212 |
|
} |
213 |
|
else |
214 |
|
{ |
215 |
1238049 |
Assert(args[i] == falseNode); |
216 |
1238049 |
lhsElim[args[i + 1].notNode()]++; |
217 |
|
} |
218 |
|
} |
219 |
414609 |
if (Trace.isOn("bool-pfcheck")) |
220 |
|
{ |
221 |
|
Trace("bool-pfcheck") |
222 |
|
<< "Original elimination multiset for lhs clause:\n"; |
223 |
|
for (const auto& pair : lhsElim) |
224 |
|
{ |
225 |
|
Trace("bool-pfcheck") |
226 |
|
<< "\t- " << pair.first << " {" << pair.second << "}\n"; |
227 |
|
} |
228 |
|
} |
229 |
3317671 |
for (std::size_t i = 0, childrenSize = children.size(); i < childrenSize; |
230 |
|
++i) |
231 |
|
{ |
232 |
|
// literal to be removed from rhs clause. They will be negated |
233 |
5806124 |
Node rhsElim = Node::null(); |
234 |
2903062 |
if (Trace.isOn("bool-pfcheck")) |
235 |
|
{ |
236 |
|
Trace("bool-pfcheck") << i << ": current lhsElim:\n"; |
237 |
|
for (const auto& pair : lhsElim) |
238 |
|
{ |
239 |
|
Trace("bool-pfcheck") |
240 |
|
<< "\t- " << pair.first << " {" << pair.second << "}\n"; |
241 |
|
} |
242 |
|
} |
243 |
2903062 |
if (i > 0) |
244 |
|
{ |
245 |
2488453 |
std::size_t index = 2 * (i - 1); |
246 |
3726502 |
rhsElim = args[index] == trueNode ? args[index + 1].notNode() |
247 |
1238049 |
: args[index + 1]; |
248 |
2488453 |
Trace("bool-pfcheck") << i << ": rhs elim: " << rhsElim << "\n"; |
249 |
|
} |
250 |
|
// Only add to conclusion nodes that are not in elimination set. First get |
251 |
|
// the nodes. |
252 |
|
// |
253 |
|
// Since a Node cannot hold an OR with a single child we need to |
254 |
|
// disambiguate singleton clauses that are OR nodes from non-singleton |
255 |
|
// clauses (i.e. unit clauses in the SAT solver). |
256 |
|
// |
257 |
|
// If the child is not an OR, it is a singleton clause and we take the |
258 |
|
// child itself as the clause. Otherwise the child can only be a singleton |
259 |
|
// clause if the child itself is used as a resolution literal, i.e. if the |
260 |
|
// child is in lhsElim or is equal to rhsElim (which means that the |
261 |
|
// negation of the child is in lhsElim). |
262 |
5806124 |
std::vector<Node> lits; |
263 |
8080006 |
if (children[i].getKind() == kind::OR && lhsElim.count(children[i]) == 0 |
264 |
5176944 |
&& children[i] != rhsElim) |
265 |
|
{ |
266 |
2269909 |
lits.insert(lits.end(), children[i].begin(), children[i].end()); |
267 |
|
} |
268 |
|
else |
269 |
|
{ |
270 |
633153 |
lits.push_back(children[i]); |
271 |
|
} |
272 |
2903062 |
Trace("bool-pfcheck") << i << ": clause lits: " << lits << "\n"; |
273 |
5806124 |
std::vector<Node> added; |
274 |
20938591 |
for (std::size_t j = 0, size = lits.size(); j < size; ++j) |
275 |
|
{ |
276 |
20523982 |
if (lits[j] == rhsElim) |
277 |
|
{ |
278 |
2488453 |
rhsElim = Node::null(); |
279 |
2488453 |
continue; |
280 |
|
} |
281 |
15547076 |
auto it = lhsElim.find(lits[j]); |
282 |
15547076 |
if (it == lhsElim.end()) |
283 |
|
{ |
284 |
13058623 |
clauseNodes.push_back(lits[j]); |
285 |
13058623 |
added.push_back(lits[j]); |
286 |
|
} |
287 |
|
else |
288 |
|
{ |
289 |
|
// remove occurrence |
290 |
2488453 |
it->second--; |
291 |
2488453 |
if (it->second == 0) |
292 |
|
{ |
293 |
2384264 |
lhsElim.erase(it); |
294 |
|
} |
295 |
|
} |
296 |
|
} |
297 |
2903062 |
Trace("bool-pfcheck") << i << ": added lits: " << added << "\n\n"; |
298 |
|
} |
299 |
414609 |
Trace("bool-pfcheck") << "clause: " << clauseNodes << "\n" << pop; |
300 |
414609 |
return clauseNodes.empty() |
301 |
|
? nm->mkConst(false) |
302 |
442262 |
: clauseNodes.size() == 1 ? clauseNodes[0] |
303 |
856871 |
: nm->mkNode(kind::OR, clauseNodes); |
304 |
|
} |
305 |
1748780 |
if (id == PfRule::MACRO_RESOLUTION_TRUST) |
306 |
|
{ |
307 |
300190 |
Assert(children.size() > 1); |
308 |
300190 |
Assert(args.size() == 2 * (children.size() - 1) + 1); |
309 |
300190 |
return args[0]; |
310 |
|
} |
311 |
1448590 |
if (id == PfRule::MACRO_RESOLUTION) |
312 |
|
{ |
313 |
|
Assert(children.size() > 1); |
314 |
|
Assert(args.size() == 2 * (children.size() - 1) + 1); |
315 |
|
Trace("bool-pfcheck") << "macro_res: " << args[0] << "\n" << push; |
316 |
|
NodeManager* nm = NodeManager::currentNM(); |
317 |
|
Node trueNode = nm->mkConst(true); |
318 |
|
Node falseNode = nm->mkConst(false); |
319 |
|
std::vector<Node> clauseNodes; |
320 |
|
for (std::size_t i = 0, childrenSize = children.size(); i < childrenSize; |
321 |
|
++i) |
322 |
|
{ |
323 |
|
std::unordered_set<Node> elim; |
324 |
|
// literals to be removed from "first" clause |
325 |
|
if (i < childrenSize - 1) |
326 |
|
{ |
327 |
|
for (std::size_t j = (2 * i) + 1, argsSize = args.size(); j < argsSize; |
328 |
|
j = j + 2) |
329 |
|
{ |
330 |
|
// whether pivot should occur as is or negated depends on the polarity |
331 |
|
// of each step in the macro |
332 |
|
if (args[j] == trueNode) |
333 |
|
{ |
334 |
|
elim.insert(args[j + 1]); |
335 |
|
} |
336 |
|
else |
337 |
|
{ |
338 |
|
Assert(args[j] == falseNode); |
339 |
|
elim.insert(args[j + 1].notNode()); |
340 |
|
} |
341 |
|
} |
342 |
|
} |
343 |
|
// literal to be removed from "second" clause. They will be negated |
344 |
|
if (i > 0) |
345 |
|
{ |
346 |
|
std::size_t index = 2 * (i - 1) + 1; |
347 |
|
Node pivot = args[index] == trueNode ? args[index + 1].notNode() |
348 |
|
: args[index + 1]; |
349 |
|
elim.insert(pivot); |
350 |
|
} |
351 |
|
Trace("bool-pfcheck") << i << ": elimination set: " << elim << "\n"; |
352 |
|
// only add to conclusion nodes that are not in elimination set. First get |
353 |
|
// the nodes. |
354 |
|
// |
355 |
|
// Since a Node cannot hold an OR with a single child we need to |
356 |
|
// disambiguate singleton clauses that are OR nodes from non-singleton |
357 |
|
// clauses (i.e. unit clauses in the SAT solver). |
358 |
|
// |
359 |
|
// If the child is not an OR, it is a singleton clause and we take the |
360 |
|
// child itself as the clause. Otherwise the child can only be a singleton |
361 |
|
// clause if the child itself is used as a resolution literal, i.e. if the |
362 |
|
// child is in lhsElim or is equal to rhsElim (which means that the |
363 |
|
// negation of the child is in lhsElim). |
364 |
|
std::vector<Node> lits; |
365 |
|
if (children[i].getKind() == kind::OR && !elim.count(children[i])) |
366 |
|
{ |
367 |
|
lits.insert(lits.end(), children[i].begin(), children[i].end()); |
368 |
|
} |
369 |
|
else |
370 |
|
{ |
371 |
|
lits.push_back(children[i]); |
372 |
|
} |
373 |
|
Trace("bool-pfcheck") << i << ": clause lits: " << lits << "\n"; |
374 |
|
std::vector<Node> added; |
375 |
|
for (std::size_t j = 0, size = lits.size(); j < size; ++j) |
376 |
|
{ |
377 |
|
// only add if literal does not occur in elimination set |
378 |
|
if (elim.count(lits[j]) == 0) |
379 |
|
{ |
380 |
|
clauseNodes.push_back(lits[j]); |
381 |
|
added.push_back(lits[j]); |
382 |
|
// eliminate duplicates |
383 |
|
elim.insert(lits[j]); |
384 |
|
} |
385 |
|
} |
386 |
|
Trace("bool-pfcheck") << i << ": added lits: " << added << "\n\n"; |
387 |
|
} |
388 |
|
Trace("bool-pfcheck") << "clause: " << clauseNodes << "\n"; |
389 |
|
// check that set representation is the same as of the given conclusion |
390 |
|
std::unordered_set<Node> clauseComputed{clauseNodes.begin(), |
391 |
|
clauseNodes.end()}; |
392 |
|
Trace("bool-pfcheck") << "clauseSet: " << clauseComputed << "\n" << pop; |
393 |
|
if (clauseComputed.empty()) |
394 |
|
{ |
395 |
|
// conclusion differ |
396 |
|
if (args[0] != falseNode) |
397 |
|
{ |
398 |
|
return Node::null(); |
399 |
|
} |
400 |
|
return args[0]; |
401 |
|
} |
402 |
|
if (clauseComputed.size() == 1) |
403 |
|
{ |
404 |
|
// conclusion differ |
405 |
|
if (args[0] != *clauseComputed.begin()) |
406 |
|
{ |
407 |
|
return Node::null(); |
408 |
|
} |
409 |
|
return args[0]; |
410 |
|
} |
411 |
|
// At this point, should amount to them differing only on order. So the |
412 |
|
// original result can't be a singleton clause |
413 |
|
if (args[0].getKind() != kind::OR |
414 |
|
|| clauseComputed.size() != args[0].getNumChildren()) |
415 |
|
{ |
416 |
|
return Node::null(); |
417 |
|
} |
418 |
|
std::unordered_set<Node> clauseGiven{args[0].begin(), args[0].end()}; |
419 |
|
return clauseComputed == clauseGiven ? args[0] : Node::null(); |
420 |
|
} |
421 |
1448590 |
if (id == PfRule::SPLIT) |
422 |
|
{ |
423 |
10025 |
Assert(children.empty()); |
424 |
10025 |
Assert(args.size() == 1); |
425 |
|
return NodeManager::currentNM()->mkNode( |
426 |
10025 |
kind::OR, args[0], args[0].notNode()); |
427 |
|
} |
428 |
1438565 |
if (id == PfRule::CONTRA) |
429 |
|
{ |
430 |
11593 |
Assert(children.size() == 2); |
431 |
11593 |
if (children[1].getKind() == Kind::NOT && children[0] == children[1][0]) |
432 |
|
{ |
433 |
11593 |
return NodeManager::currentNM()->mkConst(false); |
434 |
|
} |
435 |
|
return Node::null(); |
436 |
|
} |
437 |
1426972 |
if (id == PfRule::EQ_RESOLVE) |
438 |
|
{ |
439 |
292813 |
Assert(children.size() == 2); |
440 |
292813 |
Assert(args.empty()); |
441 |
292813 |
if (children[1].getKind() != kind::EQUAL || children[0] != children[1][0]) |
442 |
|
{ |
443 |
|
return Node::null(); |
444 |
|
} |
445 |
292813 |
return children[1][1]; |
446 |
|
} |
447 |
1134159 |
if (id == PfRule::MODUS_PONENS) |
448 |
|
{ |
449 |
51051 |
Assert(children.size() == 2); |
450 |
51051 |
Assert(args.empty()); |
451 |
51051 |
if (children[1].getKind() != kind::IMPLIES || children[0] != children[1][0]) |
452 |
|
{ |
453 |
|
return Node::null(); |
454 |
|
} |
455 |
51051 |
return children[1][1]; |
456 |
|
} |
457 |
1083108 |
if (id == PfRule::NOT_NOT_ELIM) |
458 |
|
{ |
459 |
2639 |
Assert(children.size() == 1); |
460 |
2639 |
Assert(args.empty()); |
461 |
2639 |
if (children[0].getKind() != kind::NOT || children[0][0].getKind() != kind::NOT) |
462 |
|
{ |
463 |
|
return Node::null(); |
464 |
|
} |
465 |
2639 |
return children[0][0][0]; |
466 |
|
} |
467 |
|
// natural deduction rules |
468 |
1080469 |
if (id == PfRule::AND_ELIM) |
469 |
|
{ |
470 |
472793 |
Assert(children.size() == 1); |
471 |
472793 |
Assert(args.size() == 1); |
472 |
|
uint32_t i; |
473 |
472793 |
if (children[0].getKind() != kind::AND || !getUInt32(args[0], i)) |
474 |
|
{ |
475 |
|
return Node::null(); |
476 |
|
} |
477 |
472793 |
if (i >= children[0].getNumChildren()) |
478 |
|
{ |
479 |
|
return Node::null(); |
480 |
|
} |
481 |
472793 |
return children[0][i]; |
482 |
|
} |
483 |
607676 |
if (id == PfRule::AND_INTRO) |
484 |
|
{ |
485 |
65520 |
Assert(children.size() >= 1); |
486 |
65520 |
return children.size() == 1 |
487 |
|
? children[0] |
488 |
65520 |
: NodeManager::currentNM()->mkNode(kind::AND, children); |
489 |
|
} |
490 |
542156 |
if (id == PfRule::NOT_OR_ELIM) |
491 |
|
{ |
492 |
6699 |
Assert(children.size() == 1); |
493 |
6699 |
Assert(args.size() == 1); |
494 |
|
uint32_t i; |
495 |
13398 |
if (children[0].getKind() != kind::NOT |
496 |
13398 |
|| children[0][0].getKind() != kind::OR || !getUInt32(args[0], i)) |
497 |
|
{ |
498 |
|
return Node::null(); |
499 |
|
} |
500 |
6699 |
if (i >= children[0][0].getNumChildren()) |
501 |
|
{ |
502 |
|
return Node::null(); |
503 |
|
} |
504 |
6699 |
return children[0][0][i].notNode(); |
505 |
|
} |
506 |
535457 |
if (id == PfRule::IMPLIES_ELIM) |
507 |
|
{ |
508 |
54119 |
Assert(children.size() == 1); |
509 |
54119 |
Assert(args.empty()); |
510 |
54119 |
if (children[0].getKind() != kind::IMPLIES) |
511 |
|
{ |
512 |
|
return Node::null(); |
513 |
|
} |
514 |
|
return NodeManager::currentNM()->mkNode( |
515 |
54119 |
kind::OR, children[0][0].notNode(), children[0][1]); |
516 |
|
} |
517 |
481338 |
if (id == PfRule::NOT_IMPLIES_ELIM1) |
518 |
|
{ |
519 |
665 |
Assert(children.size() == 1); |
520 |
665 |
Assert(args.empty()); |
521 |
1330 |
if (children[0].getKind() != kind::NOT |
522 |
1330 |
|| children[0][0].getKind() != kind::IMPLIES) |
523 |
|
{ |
524 |
|
return Node::null(); |
525 |
|
} |
526 |
665 |
return children[0][0][0]; |
527 |
|
} |
528 |
480673 |
if (id == PfRule::NOT_IMPLIES_ELIM2) |
529 |
|
{ |
530 |
462 |
Assert(children.size() == 1); |
531 |
462 |
Assert(args.empty()); |
532 |
924 |
if (children[0].getKind() != kind::NOT |
533 |
924 |
|| children[0][0].getKind() != kind::IMPLIES) |
534 |
|
{ |
535 |
|
return Node::null(); |
536 |
|
} |
537 |
462 |
return children[0][0][1].notNode(); |
538 |
|
} |
539 |
480211 |
if (id == PfRule::EQUIV_ELIM1) |
540 |
|
{ |
541 |
2241 |
Assert(children.size() == 1); |
542 |
2241 |
Assert(args.empty()); |
543 |
2241 |
if (children[0].getKind() != kind::EQUAL) |
544 |
|
{ |
545 |
|
return Node::null(); |
546 |
|
} |
547 |
|
return NodeManager::currentNM()->mkNode( |
548 |
2241 |
kind::OR, children[0][0].notNode(), children[0][1]); |
549 |
|
} |
550 |
477970 |
if (id == PfRule::EQUIV_ELIM2) |
551 |
|
{ |
552 |
2909 |
Assert(children.size() == 1); |
553 |
2909 |
Assert(args.empty()); |
554 |
2909 |
if (children[0].getKind() != kind::EQUAL) |
555 |
|
{ |
556 |
|
return Node::null(); |
557 |
|
} |
558 |
|
return NodeManager::currentNM()->mkNode( |
559 |
2909 |
kind::OR, children[0][0], children[0][1].notNode()); |
560 |
|
} |
561 |
475061 |
if (id == PfRule::NOT_EQUIV_ELIM1) |
562 |
|
{ |
563 |
107 |
Assert(children.size() == 1); |
564 |
107 |
Assert(args.empty()); |
565 |
214 |
if (children[0].getKind() != kind::NOT |
566 |
214 |
|| children[0][0].getKind() != kind::EQUAL) |
567 |
|
{ |
568 |
|
return Node::null(); |
569 |
|
} |
570 |
|
return NodeManager::currentNM()->mkNode( |
571 |
107 |
kind::OR, children[0][0][0], children[0][0][1]); |
572 |
|
} |
573 |
474954 |
if (id == PfRule::NOT_EQUIV_ELIM2) |
574 |
|
{ |
575 |
137 |
Assert(children.size() == 1); |
576 |
137 |
Assert(args.empty()); |
577 |
274 |
if (children[0].getKind() != kind::NOT |
578 |
274 |
|| children[0][0].getKind() != kind::EQUAL) |
579 |
|
{ |
580 |
|
return Node::null(); |
581 |
|
} |
582 |
|
return NodeManager::currentNM()->mkNode( |
583 |
137 |
kind::OR, children[0][0][0].notNode(), children[0][0][1].notNode()); |
584 |
|
} |
585 |
474817 |
if (id == PfRule::XOR_ELIM1) |
586 |
|
{ |
587 |
36 |
Assert(children.size() == 1); |
588 |
36 |
Assert(args.empty()); |
589 |
36 |
if (children[0].getKind() != kind::XOR) |
590 |
|
{ |
591 |
|
return Node::null(); |
592 |
|
} |
593 |
|
return NodeManager::currentNM()->mkNode( |
594 |
36 |
kind::OR, children[0][0], children[0][1]); |
595 |
|
} |
596 |
474781 |
if (id == PfRule::XOR_ELIM2) |
597 |
|
{ |
598 |
34 |
Assert(children.size() == 1); |
599 |
34 |
Assert(args.empty()); |
600 |
34 |
if (children[0].getKind() != kind::XOR) |
601 |
|
{ |
602 |
|
return Node::null(); |
603 |
|
} |
604 |
|
return NodeManager::currentNM()->mkNode( |
605 |
34 |
kind::OR, children[0][0].notNode(), children[0][1].notNode()); |
606 |
|
} |
607 |
474747 |
if (id == PfRule::NOT_XOR_ELIM1) |
608 |
|
{ |
609 |
5 |
Assert(children.size() == 1); |
610 |
5 |
Assert(args.empty()); |
611 |
10 |
if (children[0].getKind() != kind::NOT |
612 |
10 |
|| children[0][0].getKind() != kind::XOR) |
613 |
|
{ |
614 |
|
return Node::null(); |
615 |
|
} |
616 |
|
return NodeManager::currentNM()->mkNode( |
617 |
5 |
kind::OR, children[0][0][0], children[0][0][1].notNode()); |
618 |
|
} |
619 |
474742 |
if (id == PfRule::NOT_XOR_ELIM2) |
620 |
|
{ |
621 |
3 |
Assert(children.size() == 1); |
622 |
3 |
Assert(args.empty()); |
623 |
6 |
if (children[0].getKind() != kind::NOT |
624 |
6 |
|| children[0][0].getKind() != kind::XOR) |
625 |
|
{ |
626 |
|
return Node::null(); |
627 |
|
} |
628 |
|
return NodeManager::currentNM()->mkNode( |
629 |
3 |
kind::OR, children[0][0][0].notNode(), children[0][0][1]); |
630 |
|
} |
631 |
474739 |
if (id == PfRule::ITE_ELIM1) |
632 |
|
{ |
633 |
13413 |
Assert(children.size() == 1); |
634 |
13413 |
Assert(args.empty()); |
635 |
13413 |
if (children[0].getKind() != kind::ITE) |
636 |
|
{ |
637 |
|
return Node::null(); |
638 |
|
} |
639 |
|
return NodeManager::currentNM()->mkNode( |
640 |
13413 |
kind::OR, children[0][0].notNode(), children[0][1]); |
641 |
|
} |
642 |
461326 |
if (id == PfRule::ITE_ELIM2) |
643 |
|
{ |
644 |
41986 |
Assert(children.size() == 1); |
645 |
41986 |
Assert(args.empty()); |
646 |
41986 |
if (children[0].getKind() != kind::ITE) |
647 |
|
{ |
648 |
|
return Node::null(); |
649 |
|
} |
650 |
|
return NodeManager::currentNM()->mkNode( |
651 |
41986 |
kind::OR, children[0][0], children[0][2]); |
652 |
|
} |
653 |
419340 |
if (id == PfRule::NOT_ITE_ELIM1) |
654 |
|
{ |
655 |
71 |
Assert(children.size() == 1); |
656 |
71 |
Assert(args.empty()); |
657 |
142 |
if (children[0].getKind() != kind::NOT |
658 |
142 |
|| children[0][0].getKind() != kind::ITE) |
659 |
|
{ |
660 |
|
return Node::null(); |
661 |
|
} |
662 |
|
return NodeManager::currentNM()->mkNode( |
663 |
71 |
kind::OR, children[0][0][0].notNode(), children[0][0][1].notNode()); |
664 |
|
} |
665 |
419269 |
if (id == PfRule::NOT_ITE_ELIM2) |
666 |
|
{ |
667 |
107 |
Assert(children.size() == 1); |
668 |
107 |
Assert(args.empty()); |
669 |
214 |
if (children[0].getKind() != kind::NOT |
670 |
214 |
|| children[0][0].getKind() != kind::ITE) |
671 |
|
{ |
672 |
|
return Node::null(); |
673 |
|
} |
674 |
|
return NodeManager::currentNM()->mkNode( |
675 |
107 |
kind::OR, children[0][0][0], children[0][0][2].notNode()); |
676 |
|
} |
677 |
|
// De Morgan |
678 |
419162 |
if (id == PfRule::NOT_AND) |
679 |
|
{ |
680 |
43639 |
Assert(children.size() == 1); |
681 |
43639 |
Assert(args.empty()); |
682 |
87278 |
if (children[0].getKind() != kind::NOT |
683 |
87278 |
|| children[0][0].getKind() != kind::AND) |
684 |
|
{ |
685 |
|
return Node::null(); |
686 |
|
} |
687 |
87278 |
std::vector<Node> disjuncts; |
688 |
297459 |
for (std::size_t i = 0, size = children[0][0].getNumChildren(); i < size; |
689 |
|
++i) |
690 |
|
{ |
691 |
253820 |
disjuncts.push_back(children[0][0][i].notNode()); |
692 |
|
} |
693 |
43639 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
694 |
|
} |
695 |
|
// valid clauses rules for Tseitin CNF transformation |
696 |
375523 |
if (id == PfRule::CNF_AND_POS) |
697 |
|
{ |
698 |
153503 |
Assert(children.empty()); |
699 |
153503 |
Assert(args.size() == 2); |
700 |
|
uint32_t i; |
701 |
153503 |
if (args[0].getKind() != kind::AND || !getUInt32(args[1], i)) |
702 |
|
{ |
703 |
|
return Node::null(); |
704 |
|
} |
705 |
153503 |
if (i >= args[0].getNumChildren()) |
706 |
|
{ |
707 |
|
return Node::null(); |
708 |
|
} |
709 |
|
return NodeManager::currentNM()->mkNode( |
710 |
153503 |
kind::OR, args[0].notNode(), args[0][i]); |
711 |
|
} |
712 |
222020 |
if (id == PfRule::CNF_AND_NEG) |
713 |
|
{ |
714 |
46832 |
Assert(children.empty()); |
715 |
46832 |
Assert(args.size() == 1); |
716 |
46832 |
if (args[0].getKind() != kind::AND) |
717 |
|
{ |
718 |
|
return Node::null(); |
719 |
|
} |
720 |
93664 |
std::vector<Node> disjuncts{args[0]}; |
721 |
366104 |
for (unsigned i = 0, size = args[0].getNumChildren(); i < size; ++i) |
722 |
|
{ |
723 |
319272 |
disjuncts.push_back(args[0][i].notNode()); |
724 |
|
} |
725 |
46832 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
726 |
|
} |
727 |
175188 |
if (id == PfRule::CNF_OR_POS) |
728 |
|
{ |
729 |
14689 |
Assert(children.empty()); |
730 |
14689 |
Assert(args.size() == 1); |
731 |
14689 |
if (args[0].getKind() != kind::OR) |
732 |
|
{ |
733 |
|
return Node::null(); |
734 |
|
} |
735 |
29378 |
std::vector<Node> disjuncts{args[0].notNode()}; |
736 |
243053 |
for (unsigned i = 0, size = args[0].getNumChildren(); i < size; ++i) |
737 |
|
{ |
738 |
228364 |
disjuncts.push_back(args[0][i]); |
739 |
|
} |
740 |
14689 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
741 |
|
} |
742 |
160499 |
if (id == PfRule::CNF_OR_NEG) |
743 |
|
{ |
744 |
56494 |
Assert(children.empty()); |
745 |
56494 |
Assert(args.size() == 2); |
746 |
|
uint32_t i; |
747 |
56494 |
if (args[0].getKind() != kind::OR || !getUInt32(args[1], i)) |
748 |
|
{ |
749 |
|
return Node::null(); |
750 |
|
} |
751 |
56494 |
if (i >= args[0].getNumChildren()) |
752 |
|
{ |
753 |
|
return Node::null(); |
754 |
|
} |
755 |
|
return NodeManager::currentNM()->mkNode( |
756 |
56494 |
kind::OR, args[0], args[0][i].notNode()); |
757 |
|
} |
758 |
104005 |
if (id == PfRule::CNF_IMPLIES_POS) |
759 |
|
{ |
760 |
2391 |
Assert(children.empty()); |
761 |
2391 |
Assert(args.size() == 1); |
762 |
2391 |
if (args[0].getKind() != kind::IMPLIES) |
763 |
|
{ |
764 |
|
return Node::null(); |
765 |
|
} |
766 |
|
std::vector<Node> disjuncts{ |
767 |
4782 |
args[0].notNode(), args[0][0].notNode(), args[0][1]}; |
768 |
2391 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
769 |
|
} |
770 |
101614 |
if (id == PfRule::CNF_IMPLIES_NEG1) |
771 |
|
{ |
772 |
1968 |
Assert(children.empty()); |
773 |
1968 |
Assert(args.size() == 1); |
774 |
1968 |
if (args[0].getKind() != kind::IMPLIES) |
775 |
|
{ |
776 |
|
return Node::null(); |
777 |
|
} |
778 |
3936 |
std::vector<Node> disjuncts{args[0], args[0][0]}; |
779 |
1968 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
780 |
|
} |
781 |
99646 |
if (id == PfRule::CNF_IMPLIES_NEG2) |
782 |
|
{ |
783 |
67711 |
Assert(children.empty()); |
784 |
67711 |
Assert(args.size() == 1); |
785 |
67711 |
if (args[0].getKind() != kind::IMPLIES) |
786 |
|
{ |
787 |
|
return Node::null(); |
788 |
|
} |
789 |
135422 |
std::vector<Node> disjuncts{args[0], args[0][1].notNode()}; |
790 |
67711 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
791 |
|
} |
792 |
31935 |
if (id == PfRule::CNF_EQUIV_POS1) |
793 |
|
{ |
794 |
1580 |
Assert(children.empty()); |
795 |
1580 |
Assert(args.size() == 1); |
796 |
1580 |
if (args[0].getKind() != kind::EQUAL) |
797 |
|
{ |
798 |
|
return Node::null(); |
799 |
|
} |
800 |
|
std::vector<Node> disjuncts{ |
801 |
3160 |
args[0].notNode(), args[0][0].notNode(), args[0][1]}; |
802 |
1580 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
803 |
|
} |
804 |
30355 |
if (id == PfRule::CNF_EQUIV_POS2) |
805 |
|
{ |
806 |
1171 |
Assert(children.empty()); |
807 |
1171 |
Assert(args.size() == 1); |
808 |
1171 |
if (args[0].getKind() != kind::EQUAL) |
809 |
|
{ |
810 |
|
return Node::null(); |
811 |
|
} |
812 |
|
std::vector<Node> disjuncts{ |
813 |
2342 |
args[0].notNode(), args[0][0], args[0][1].notNode()}; |
814 |
1171 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
815 |
|
} |
816 |
29184 |
if (id == PfRule::CNF_EQUIV_NEG1) |
817 |
|
{ |
818 |
1274 |
Assert(children.empty()); |
819 |
1274 |
Assert(args.size() == 1); |
820 |
1274 |
if (args[0].getKind() != kind::EQUAL) |
821 |
|
{ |
822 |
|
return Node::null(); |
823 |
|
} |
824 |
2548 |
std::vector<Node> disjuncts{args[0], args[0][0], args[0][1]}; |
825 |
1274 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
826 |
|
} |
827 |
27910 |
if (id == PfRule::CNF_EQUIV_NEG2) |
828 |
|
{ |
829 |
3545 |
Assert(children.empty()); |
830 |
3545 |
Assert(args.size() == 1); |
831 |
3545 |
if (args[0].getKind() != kind::EQUAL) |
832 |
|
{ |
833 |
|
return Node::null(); |
834 |
|
} |
835 |
|
std::vector<Node> disjuncts{ |
836 |
7090 |
args[0], args[0][0].notNode(), args[0][1].notNode()}; |
837 |
3545 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
838 |
|
} |
839 |
24365 |
if (id == PfRule::CNF_XOR_POS1) |
840 |
|
{ |
841 |
158 |
Assert(children.empty()); |
842 |
158 |
Assert(args.size() == 1); |
843 |
158 |
if (args[0].getKind() != kind::XOR) |
844 |
|
{ |
845 |
|
return Node::null(); |
846 |
|
} |
847 |
316 |
std::vector<Node> disjuncts{args[0].notNode(), args[0][0], args[0][1]}; |
848 |
158 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
849 |
|
} |
850 |
24207 |
if (id == PfRule::CNF_XOR_POS2) |
851 |
|
{ |
852 |
163 |
Assert(children.empty()); |
853 |
163 |
Assert(args.size() == 1); |
854 |
163 |
if (args[0].getKind() != kind::XOR) |
855 |
|
{ |
856 |
|
return Node::null(); |
857 |
|
} |
858 |
|
std::vector<Node> disjuncts{ |
859 |
326 |
args[0].notNode(), args[0][0].notNode(), args[0][1].notNode()}; |
860 |
163 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
861 |
|
} |
862 |
24044 |
if (id == PfRule::CNF_XOR_NEG1) |
863 |
|
{ |
864 |
158 |
Assert(children.empty()); |
865 |
158 |
Assert(args.size() == 1); |
866 |
158 |
if (args[0].getKind() != kind::XOR) |
867 |
|
{ |
868 |
|
return Node::null(); |
869 |
|
} |
870 |
316 |
std::vector<Node> disjuncts{args[0], args[0][0].notNode(), args[0][1]}; |
871 |
158 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
872 |
|
} |
873 |
23886 |
if (id == PfRule::CNF_XOR_NEG2) |
874 |
|
{ |
875 |
164 |
Assert(children.empty()); |
876 |
164 |
Assert(args.size() == 1); |
877 |
164 |
if (args[0].getKind() != kind::XOR) |
878 |
|
{ |
879 |
|
return Node::null(); |
880 |
|
} |
881 |
328 |
std::vector<Node> disjuncts{args[0], args[0][0], args[0][1].notNode()}; |
882 |
164 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
883 |
|
} |
884 |
23722 |
if (id == PfRule::CNF_ITE_POS1) |
885 |
|
{ |
886 |
3795 |
Assert(children.empty()); |
887 |
3795 |
Assert(args.size() == 1); |
888 |
3795 |
if (args[0].getKind() != kind::ITE) |
889 |
|
{ |
890 |
|
return Node::null(); |
891 |
|
} |
892 |
|
std::vector<Node> disjuncts{ |
893 |
7590 |
args[0].notNode(), args[0][0].notNode(), args[0][1]}; |
894 |
3795 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
895 |
|
} |
896 |
19927 |
if (id == PfRule::CNF_ITE_POS2) |
897 |
|
{ |
898 |
3517 |
Assert(children.empty()); |
899 |
3517 |
Assert(args.size() == 1); |
900 |
3517 |
if (args[0].getKind() != kind::ITE) |
901 |
|
{ |
902 |
|
return Node::null(); |
903 |
|
} |
904 |
7034 |
std::vector<Node> disjuncts{args[0].notNode(), args[0][0], args[0][2]}; |
905 |
3517 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
906 |
|
} |
907 |
16410 |
if (id == PfRule::CNF_ITE_POS3) |
908 |
|
{ |
909 |
3835 |
Assert(children.empty()); |
910 |
3835 |
Assert(args.size() == 1); |
911 |
3835 |
if (args[0].getKind() != kind::ITE) |
912 |
|
{ |
913 |
|
return Node::null(); |
914 |
|
} |
915 |
7670 |
std::vector<Node> disjuncts{args[0].notNode(), args[0][1], args[0][2]}; |
916 |
3835 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
917 |
|
} |
918 |
12575 |
if (id == PfRule::CNF_ITE_NEG1) |
919 |
|
{ |
920 |
4246 |
Assert(children.empty()); |
921 |
4246 |
Assert(args.size() == 1); |
922 |
4246 |
if (args[0].getKind() != kind::ITE) |
923 |
|
{ |
924 |
|
return Node::null(); |
925 |
|
} |
926 |
|
std::vector<Node> disjuncts{ |
927 |
8492 |
args[0], args[0][0].notNode(), args[0][1].notNode()}; |
928 |
4246 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
929 |
|
} |
930 |
8329 |
if (id == PfRule::CNF_ITE_NEG2) |
931 |
|
{ |
932 |
3513 |
Assert(children.empty()); |
933 |
3513 |
Assert(args.size() == 1); |
934 |
3513 |
if (args[0].getKind() != kind::ITE) |
935 |
|
{ |
936 |
|
return Node::null(); |
937 |
|
} |
938 |
7026 |
std::vector<Node> disjuncts{args[0], args[0][0], args[0][2].notNode()}; |
939 |
3513 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
940 |
|
} |
941 |
4816 |
if (id == PfRule::CNF_ITE_NEG3) |
942 |
|
{ |
943 |
3853 |
Assert(children.empty()); |
944 |
3853 |
Assert(args.size() == 1); |
945 |
3853 |
if (args[0].getKind() != kind::ITE) |
946 |
|
{ |
947 |
|
return Node::null(); |
948 |
|
} |
949 |
|
std::vector<Node> disjuncts{ |
950 |
7706 |
args[0], args[0][1].notNode(), args[0][2].notNode()}; |
951 |
3853 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
952 |
|
} |
953 |
963 |
if (id == PfRule::SAT_REFUTATION) |
954 |
|
{ |
955 |
963 |
Assert(args.empty()); |
956 |
963 |
return NodeManager::currentNM()->mkConst(false); |
957 |
|
} |
958 |
|
// no rule |
959 |
|
return Node::null(); |
960 |
|
} |
961 |
|
|
962 |
|
} // namespace booleans |
963 |
|
} // namespace theory |
964 |
27735 |
} // namespace cvc5 |