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 |
3756 |
void BoolProofRuleChecker::registerTo(ProofChecker* pc) |
25 |
|
{ |
26 |
3756 |
pc->registerChecker(PfRule::SPLIT, this); |
27 |
3756 |
pc->registerChecker(PfRule::RESOLUTION, this); |
28 |
3756 |
pc->registerChecker(PfRule::CHAIN_RESOLUTION, this); |
29 |
3756 |
pc->registerTrustedChecker(PfRule::MACRO_RESOLUTION_TRUST, this, 3); |
30 |
3756 |
pc->registerChecker(PfRule::MACRO_RESOLUTION, this); |
31 |
3756 |
pc->registerChecker(PfRule::FACTORING, this); |
32 |
3756 |
pc->registerChecker(PfRule::REORDERING, this); |
33 |
3756 |
pc->registerChecker(PfRule::EQ_RESOLVE, this); |
34 |
3756 |
pc->registerChecker(PfRule::MODUS_PONENS, this); |
35 |
3756 |
pc->registerChecker(PfRule::NOT_NOT_ELIM, this); |
36 |
3756 |
pc->registerChecker(PfRule::CONTRA, this); |
37 |
3756 |
pc->registerChecker(PfRule::AND_ELIM, this); |
38 |
3756 |
pc->registerChecker(PfRule::AND_INTRO, this); |
39 |
3756 |
pc->registerChecker(PfRule::NOT_OR_ELIM, this); |
40 |
3756 |
pc->registerChecker(PfRule::IMPLIES_ELIM, this); |
41 |
3756 |
pc->registerChecker(PfRule::NOT_IMPLIES_ELIM1, this); |
42 |
3756 |
pc->registerChecker(PfRule::NOT_IMPLIES_ELIM2, this); |
43 |
3756 |
pc->registerChecker(PfRule::EQUIV_ELIM1, this); |
44 |
3756 |
pc->registerChecker(PfRule::EQUIV_ELIM2, this); |
45 |
3756 |
pc->registerChecker(PfRule::NOT_EQUIV_ELIM1, this); |
46 |
3756 |
pc->registerChecker(PfRule::NOT_EQUIV_ELIM2, this); |
47 |
3756 |
pc->registerChecker(PfRule::XOR_ELIM1, this); |
48 |
3756 |
pc->registerChecker(PfRule::XOR_ELIM2, this); |
49 |
3756 |
pc->registerChecker(PfRule::NOT_XOR_ELIM1, this); |
50 |
3756 |
pc->registerChecker(PfRule::NOT_XOR_ELIM2, this); |
51 |
3756 |
pc->registerChecker(PfRule::ITE_ELIM1, this); |
52 |
3756 |
pc->registerChecker(PfRule::ITE_ELIM2, this); |
53 |
3756 |
pc->registerChecker(PfRule::NOT_ITE_ELIM1, this); |
54 |
3756 |
pc->registerChecker(PfRule::NOT_ITE_ELIM2, this); |
55 |
3756 |
pc->registerChecker(PfRule::NOT_AND, this); |
56 |
3756 |
pc->registerChecker(PfRule::CNF_AND_POS, this); |
57 |
3756 |
pc->registerChecker(PfRule::CNF_AND_NEG, this); |
58 |
3756 |
pc->registerChecker(PfRule::CNF_OR_POS, this); |
59 |
3756 |
pc->registerChecker(PfRule::CNF_OR_NEG, this); |
60 |
3756 |
pc->registerChecker(PfRule::CNF_IMPLIES_POS, this); |
61 |
3756 |
pc->registerChecker(PfRule::CNF_IMPLIES_NEG1, this); |
62 |
3756 |
pc->registerChecker(PfRule::CNF_IMPLIES_NEG2, this); |
63 |
3756 |
pc->registerChecker(PfRule::CNF_EQUIV_POS1, this); |
64 |
3756 |
pc->registerChecker(PfRule::CNF_EQUIV_POS2, this); |
65 |
3756 |
pc->registerChecker(PfRule::CNF_EQUIV_NEG1, this); |
66 |
3756 |
pc->registerChecker(PfRule::CNF_EQUIV_NEG2, this); |
67 |
3756 |
pc->registerChecker(PfRule::CNF_XOR_POS1, this); |
68 |
3756 |
pc->registerChecker(PfRule::CNF_XOR_POS2, this); |
69 |
3756 |
pc->registerChecker(PfRule::CNF_XOR_NEG1, this); |
70 |
3756 |
pc->registerChecker(PfRule::CNF_XOR_NEG2, this); |
71 |
3756 |
pc->registerChecker(PfRule::CNF_ITE_POS1, this); |
72 |
3756 |
pc->registerChecker(PfRule::CNF_ITE_POS2, this); |
73 |
3756 |
pc->registerChecker(PfRule::CNF_ITE_POS3, this); |
74 |
3756 |
pc->registerChecker(PfRule::CNF_ITE_NEG1, this); |
75 |
3756 |
pc->registerChecker(PfRule::CNF_ITE_NEG2, this); |
76 |
3756 |
pc->registerChecker(PfRule::CNF_ITE_NEG3, this); |
77 |
3756 |
pc->registerTrustedChecker(PfRule::SAT_REFUTATION, this, 1); |
78 |
3756 |
} |
79 |
|
|
80 |
4295527 |
Node BoolProofRuleChecker::checkInternal(PfRule id, |
81 |
|
const std::vector<Node>& children, |
82 |
|
const std::vector<Node>& args) |
83 |
|
{ |
84 |
4295527 |
if (id == PfRule::RESOLUTION) |
85 |
|
{ |
86 |
20419 |
Assert(children.size() == 2); |
87 |
20419 |
Assert(args.size() == 2); |
88 |
20419 |
NodeManager* nm = NodeManager::currentNM(); |
89 |
40838 |
std::vector<Node> disjuncts; |
90 |
40838 |
Node pivots[2]; |
91 |
20419 |
if (args[0] == nm->mkConst(true)) |
92 |
|
{ |
93 |
18160 |
pivots[0] = args[1]; |
94 |
18160 |
pivots[1] = args[1].notNode(); |
95 |
|
} |
96 |
|
else |
97 |
|
{ |
98 |
2259 |
Assert(args[0] == nm->mkConst(false)); |
99 |
2259 |
pivots[0] = args[1].notNode(); |
100 |
2259 |
pivots[1] = args[1]; |
101 |
|
} |
102 |
61257 |
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 |
81676 |
std::vector<Node> lits; |
108 |
40838 |
if (children[i].getKind() == kind::OR && pivots[i] != children[i]) |
109 |
|
{ |
110 |
37585 |
lits.insert(lits.end(), children[i].begin(), children[i].end()); |
111 |
|
} |
112 |
|
else |
113 |
|
{ |
114 |
3253 |
lits.push_back(children[i]); |
115 |
|
} |
116 |
239830 |
for (unsigned j = 0, size = lits.size(); j < size; ++j) |
117 |
|
{ |
118 |
198992 |
if (pivots[i] != lits[j]) |
119 |
|
{ |
120 |
158154 |
disjuncts.push_back(lits[j]); |
121 |
|
} |
122 |
|
else |
123 |
|
{ |
124 |
|
// just eliminate first occurrence |
125 |
40838 |
pivots[i] = Node::null(); |
126 |
|
} |
127 |
|
} |
128 |
|
} |
129 |
20419 |
return disjuncts.empty() |
130 |
|
? nm->mkConst(false) |
131 |
23672 |
: disjuncts.size() == 1 ? disjuncts[0] |
132 |
44091 |
: nm->mkNode(kind::OR, disjuncts); |
133 |
|
} |
134 |
4275108 |
if (id == PfRule::FACTORING) |
135 |
|
{ |
136 |
311485 |
Assert(children.size() == 1); |
137 |
311485 |
Assert(args.empty()); |
138 |
311485 |
if (children[0].getKind() != kind::OR) |
139 |
|
{ |
140 |
|
return Node::null(); |
141 |
|
} |
142 |
|
// remove duplicates while keeping the order of children |
143 |
622970 |
std::unordered_set<TNode> clauseSet; |
144 |
622970 |
std::vector<Node> disjuncts; |
145 |
311485 |
unsigned size = children[0].getNumChildren(); |
146 |
9758464 |
for (unsigned i = 0; i < size; ++i) |
147 |
|
{ |
148 |
9446979 |
if (clauseSet.count(children[0][i])) |
149 |
|
{ |
150 |
2598886 |
continue; |
151 |
|
} |
152 |
6848093 |
disjuncts.push_back(children[0][i]); |
153 |
6848093 |
clauseSet.insert(children[0][i]); |
154 |
|
} |
155 |
311485 |
if (disjuncts.size() == size) |
156 |
|
{ |
157 |
|
return Node::null(); |
158 |
|
} |
159 |
311485 |
NodeManager* nm = NodeManager::currentNM(); |
160 |
311485 |
return nm->mkOr(disjuncts); |
161 |
|
} |
162 |
3963623 |
if (id == PfRule::REORDERING) |
163 |
|
{ |
164 |
1452909 |
Assert(children.size() == 1); |
165 |
1452909 |
Assert(args.size() == 1); |
166 |
2905818 |
std::unordered_set<Node> clauseSet1, clauseSet2; |
167 |
1452909 |
if (children[0].getKind() == kind::OR) |
168 |
|
{ |
169 |
1452909 |
clauseSet1.insert(children[0].begin(), children[0].end()); |
170 |
|
} |
171 |
|
else |
172 |
|
{ |
173 |
|
clauseSet1.insert(children[0]); |
174 |
|
} |
175 |
1452909 |
if (args[0].getKind() == kind::OR) |
176 |
|
{ |
177 |
1452909 |
clauseSet2.insert(args[0].begin(), args[0].end()); |
178 |
|
} |
179 |
|
else |
180 |
|
{ |
181 |
|
clauseSet2.insert(args[0]); |
182 |
|
} |
183 |
1452909 |
if (clauseSet1 != clauseSet2) |
184 |
|
{ |
185 |
|
Trace("bool-pfcheck") << id << ": clause set1: " << clauseSet1 << "\n" |
186 |
|
<< id << ": clause set2: " << clauseSet2 << "\n"; |
187 |
|
return Node::null(); |
188 |
|
} |
189 |
1452909 |
return args[0]; |
190 |
|
} |
191 |
2510714 |
if (id == PfRule::CHAIN_RESOLUTION) |
192 |
|
{ |
193 |
408318 |
Assert(children.size() > 1); |
194 |
408318 |
Assert(args.size() == 2 * (children.size() - 1)); |
195 |
408318 |
Trace("bool-pfcheck") << "chain_res:\n" << push; |
196 |
408318 |
NodeManager* nm = NodeManager::currentNM(); |
197 |
816636 |
Node trueNode = nm->mkConst(true); |
198 |
816636 |
Node falseNode = nm->mkConst(false); |
199 |
816636 |
std::vector<Node> clauseNodes; |
200 |
|
// literals to be removed from the virtual lhs clause of the resolution |
201 |
816636 |
std::unordered_map<Node, unsigned> lhsElim; |
202 |
2672006 |
for (std::size_t i = 0, argsSize = args.size(); i < argsSize; i = i + 2) |
203 |
|
{ |
204 |
|
// whether pivot should occur as is or negated depends on the polarity of |
205 |
|
// each step in the chain |
206 |
2263688 |
if (args[i] == trueNode) |
207 |
|
{ |
208 |
1193935 |
lhsElim[args[i + 1]]++; |
209 |
|
} |
210 |
|
else |
211 |
|
{ |
212 |
1069753 |
Assert(args[i] == falseNode); |
213 |
1069753 |
lhsElim[args[i + 1].notNode()]++; |
214 |
|
} |
215 |
|
} |
216 |
408318 |
if (Trace.isOn("bool-pfcheck")) |
217 |
|
{ |
218 |
|
Trace("bool-pfcheck") |
219 |
|
<< "Original elimination multiset for lhs clause:\n"; |
220 |
|
for (const auto& pair : lhsElim) |
221 |
|
{ |
222 |
|
Trace("bool-pfcheck") |
223 |
|
<< "\t- " << pair.first << " {" << pair.second << "}\n"; |
224 |
|
} |
225 |
|
} |
226 |
3080324 |
for (std::size_t i = 0, childrenSize = children.size(); i < childrenSize; |
227 |
|
++i) |
228 |
|
{ |
229 |
|
// literal to be removed from rhs clause. They will be negated |
230 |
5344012 |
Node rhsElim = Node::null(); |
231 |
2672006 |
if (Trace.isOn("bool-pfcheck")) |
232 |
|
{ |
233 |
|
Trace("bool-pfcheck") << i << ": current lhsElim:\n"; |
234 |
|
for (const auto& pair : lhsElim) |
235 |
|
{ |
236 |
|
Trace("bool-pfcheck") |
237 |
|
<< "\t- " << pair.first << " {" << pair.second << "}\n"; |
238 |
|
} |
239 |
|
} |
240 |
2672006 |
if (i > 0) |
241 |
|
{ |
242 |
2263688 |
std::size_t index = 2 * (i - 1); |
243 |
3333441 |
rhsElim = args[index] == trueNode ? args[index + 1].notNode() |
244 |
1069753 |
: args[index + 1]; |
245 |
2263688 |
Trace("bool-pfcheck") << i << ": rhs elim: " << rhsElim << "\n"; |
246 |
|
} |
247 |
|
// Only add to conclusion nodes that are not in elimination set. First get |
248 |
|
// the nodes. |
249 |
|
// |
250 |
|
// Since a Node cannot hold an OR with a single child we need to |
251 |
|
// disambiguate singleton clauses that are OR nodes from non-singleton |
252 |
|
// clauses (i.e. unit clauses in the SAT solver). |
253 |
|
// |
254 |
|
// If the child is not an OR, it is a singleton clause and we take the |
255 |
|
// child itself as the clause. Otherwise the child can only be a singleton |
256 |
|
// clause if the child itself is used as a resolution literal, i.e. if the |
257 |
|
// child is in lhsElim or is equal to rhsElim (which means that the |
258 |
|
// negation of the child is in lhsElim). |
259 |
5344012 |
std::vector<Node> lits; |
260 |
7403544 |
if (children[i].getKind() == kind::OR && lhsElim.count(children[i]) == 0 |
261 |
4731538 |
&& children[i] != rhsElim) |
262 |
|
{ |
263 |
2053296 |
lits.insert(lits.end(), children[i].begin(), children[i].end()); |
264 |
|
} |
265 |
|
else |
266 |
|
{ |
267 |
618710 |
lits.push_back(children[i]); |
268 |
|
} |
269 |
2672006 |
Trace("bool-pfcheck") << i << ": clause lits: " << lits << "\n"; |
270 |
5344012 |
std::vector<Node> added; |
271 |
19403456 |
for (std::size_t j = 0, size = lits.size(); j < size; ++j) |
272 |
|
{ |
273 |
18995138 |
if (lits[j] == rhsElim) |
274 |
|
{ |
275 |
2263688 |
rhsElim = Node::null(); |
276 |
2263688 |
continue; |
277 |
|
} |
278 |
14467762 |
auto it = lhsElim.find(lits[j]); |
279 |
14467762 |
if (it == lhsElim.end()) |
280 |
|
{ |
281 |
12204074 |
clauseNodes.push_back(lits[j]); |
282 |
12204074 |
added.push_back(lits[j]); |
283 |
|
} |
284 |
|
else |
285 |
|
{ |
286 |
|
// remove occurrence |
287 |
2263688 |
it->second--; |
288 |
2263688 |
if (it->second == 0) |
289 |
|
{ |
290 |
2174066 |
lhsElim.erase(it); |
291 |
|
} |
292 |
|
} |
293 |
|
} |
294 |
2672006 |
Trace("bool-pfcheck") << i << ": added lits: " << added << "\n\n"; |
295 |
|
} |
296 |
408318 |
Trace("bool-pfcheck") << "clause: " << clauseNodes << "\n" << pop; |
297 |
408318 |
return nm->mkOr(clauseNodes); |
298 |
|
} |
299 |
2102396 |
if (id == PfRule::MACRO_RESOLUTION_TRUST) |
300 |
|
{ |
301 |
326173 |
Assert(children.size() > 1); |
302 |
326173 |
Assert(args.size() == 2 * (children.size() - 1) + 1); |
303 |
326173 |
return args[0]; |
304 |
|
} |
305 |
1776223 |
if (id == PfRule::MACRO_RESOLUTION) |
306 |
|
{ |
307 |
|
Assert(children.size() > 1); |
308 |
|
Assert(args.size() == 2 * (children.size() - 1) + 1); |
309 |
|
Trace("bool-pfcheck") << "macro_res: " << args[0] << "\n" << push; |
310 |
|
NodeManager* nm = NodeManager::currentNM(); |
311 |
|
Node trueNode = nm->mkConst(true); |
312 |
|
Node falseNode = nm->mkConst(false); |
313 |
|
std::vector<Node> clauseNodes; |
314 |
|
for (std::size_t i = 0, childrenSize = children.size(); i < childrenSize; |
315 |
|
++i) |
316 |
|
{ |
317 |
|
std::unordered_set<Node> elim; |
318 |
|
// literals to be removed from "first" clause |
319 |
|
if (i < childrenSize - 1) |
320 |
|
{ |
321 |
|
for (std::size_t j = (2 * i) + 1, argsSize = args.size(); j < argsSize; |
322 |
|
j = j + 2) |
323 |
|
{ |
324 |
|
// whether pivot should occur as is or negated depends on the polarity |
325 |
|
// of each step in the macro |
326 |
|
if (args[j] == trueNode) |
327 |
|
{ |
328 |
|
elim.insert(args[j + 1]); |
329 |
|
} |
330 |
|
else |
331 |
|
{ |
332 |
|
Assert(args[j] == falseNode); |
333 |
|
elim.insert(args[j + 1].notNode()); |
334 |
|
} |
335 |
|
} |
336 |
|
} |
337 |
|
// literal to be removed from "second" clause. They will be negated |
338 |
|
if (i > 0) |
339 |
|
{ |
340 |
|
std::size_t index = 2 * (i - 1) + 1; |
341 |
|
Node pivot = args[index] == trueNode ? args[index + 1].notNode() |
342 |
|
: args[index + 1]; |
343 |
|
elim.insert(pivot); |
344 |
|
} |
345 |
|
Trace("bool-pfcheck") << i << ": elimination set: " << elim << "\n"; |
346 |
|
// only add to conclusion nodes that are not in elimination set. First get |
347 |
|
// the nodes. |
348 |
|
// |
349 |
|
// Since a Node cannot hold an OR with a single child we need to |
350 |
|
// disambiguate singleton clauses that are OR nodes from non-singleton |
351 |
|
// clauses (i.e. unit clauses in the SAT solver). |
352 |
|
// |
353 |
|
// If the child is not an OR, it is a singleton clause and we take the |
354 |
|
// child itself as the clause. Otherwise the child can only be a singleton |
355 |
|
// clause if the child itself is used as a resolution literal, i.e. if the |
356 |
|
// child is in lhsElim or is equal to rhsElim (which means that the |
357 |
|
// negation of the child is in lhsElim). |
358 |
|
std::vector<Node> lits; |
359 |
|
if (children[i].getKind() == kind::OR && !elim.count(children[i])) |
360 |
|
{ |
361 |
|
lits.insert(lits.end(), children[i].begin(), children[i].end()); |
362 |
|
} |
363 |
|
else |
364 |
|
{ |
365 |
|
lits.push_back(children[i]); |
366 |
|
} |
367 |
|
Trace("bool-pfcheck") << i << ": clause lits: " << lits << "\n"; |
368 |
|
std::vector<Node> added; |
369 |
|
for (std::size_t j = 0, size = lits.size(); j < size; ++j) |
370 |
|
{ |
371 |
|
// only add if literal does not occur in elimination set |
372 |
|
if (elim.count(lits[j]) == 0) |
373 |
|
{ |
374 |
|
clauseNodes.push_back(lits[j]); |
375 |
|
added.push_back(lits[j]); |
376 |
|
// eliminate duplicates |
377 |
|
elim.insert(lits[j]); |
378 |
|
} |
379 |
|
} |
380 |
|
Trace("bool-pfcheck") << i << ": added lits: " << added << "\n\n"; |
381 |
|
} |
382 |
|
Trace("bool-pfcheck") << "clause: " << clauseNodes << "\n"; |
383 |
|
// check that set representation is the same as of the given conclusion |
384 |
|
std::unordered_set<Node> clauseComputed{clauseNodes.begin(), |
385 |
|
clauseNodes.end()}; |
386 |
|
Trace("bool-pfcheck") << "clauseSet: " << clauseComputed << "\n" << pop; |
387 |
|
if (clauseComputed.empty()) |
388 |
|
{ |
389 |
|
// conclusion differ |
390 |
|
if (args[0] != falseNode) |
391 |
|
{ |
392 |
|
return Node::null(); |
393 |
|
} |
394 |
|
return args[0]; |
395 |
|
} |
396 |
|
if (clauseComputed.size() == 1) |
397 |
|
{ |
398 |
|
// conclusion differ |
399 |
|
if (args[0] != *clauseComputed.begin()) |
400 |
|
{ |
401 |
|
return Node::null(); |
402 |
|
} |
403 |
|
return args[0]; |
404 |
|
} |
405 |
|
// At this point, should amount to them differing only on order. So the |
406 |
|
// original result can't be a singleton clause |
407 |
|
if (args[0].getKind() != kind::OR |
408 |
|
|| clauseComputed.size() != args[0].getNumChildren()) |
409 |
|
{ |
410 |
|
return Node::null(); |
411 |
|
} |
412 |
|
std::unordered_set<Node> clauseGiven{args[0].begin(), args[0].end()}; |
413 |
|
return clauseComputed == clauseGiven ? args[0] : Node::null(); |
414 |
|
} |
415 |
1776223 |
if (id == PfRule::SPLIT) |
416 |
|
{ |
417 |
10305 |
Assert(children.empty()); |
418 |
10305 |
Assert(args.size() == 1); |
419 |
|
return NodeManager::currentNM()->mkNode( |
420 |
10305 |
kind::OR, args[0], args[0].notNode()); |
421 |
|
} |
422 |
1765918 |
if (id == PfRule::CONTRA) |
423 |
|
{ |
424 |
12034 |
Assert(children.size() == 2); |
425 |
12034 |
if (children[1].getKind() == Kind::NOT && children[0] == children[1][0]) |
426 |
|
{ |
427 |
12034 |
return NodeManager::currentNM()->mkConst(false); |
428 |
|
} |
429 |
|
return Node::null(); |
430 |
|
} |
431 |
1753884 |
if (id == PfRule::EQ_RESOLVE) |
432 |
|
{ |
433 |
302545 |
Assert(children.size() == 2); |
434 |
302545 |
Assert(args.empty()); |
435 |
302545 |
if (children[1].getKind() != kind::EQUAL || children[0] != children[1][0]) |
436 |
|
{ |
437 |
|
return Node::null(); |
438 |
|
} |
439 |
302545 |
return children[1][1]; |
440 |
|
} |
441 |
1451339 |
if (id == PfRule::MODUS_PONENS) |
442 |
|
{ |
443 |
85802 |
Assert(children.size() == 2); |
444 |
85802 |
Assert(args.empty()); |
445 |
85802 |
if (children[1].getKind() != kind::IMPLIES || children[0] != children[1][0]) |
446 |
|
{ |
447 |
|
return Node::null(); |
448 |
|
} |
449 |
85802 |
return children[1][1]; |
450 |
|
} |
451 |
1365537 |
if (id == PfRule::NOT_NOT_ELIM) |
452 |
|
{ |
453 |
2655 |
Assert(children.size() == 1); |
454 |
2655 |
Assert(args.empty()); |
455 |
2655 |
if (children[0].getKind() != kind::NOT || children[0][0].getKind() != kind::NOT) |
456 |
|
{ |
457 |
|
return Node::null(); |
458 |
|
} |
459 |
2655 |
return children[0][0][0]; |
460 |
|
} |
461 |
|
// natural deduction rules |
462 |
1362882 |
if (id == PfRule::AND_ELIM) |
463 |
|
{ |
464 |
475715 |
Assert(children.size() == 1); |
465 |
475715 |
Assert(args.size() == 1); |
466 |
|
uint32_t i; |
467 |
475715 |
if (children[0].getKind() != kind::AND || !getUInt32(args[0], i)) |
468 |
|
{ |
469 |
|
return Node::null(); |
470 |
|
} |
471 |
475715 |
if (i >= children[0].getNumChildren()) |
472 |
|
{ |
473 |
|
return Node::null(); |
474 |
|
} |
475 |
475715 |
return children[0][i]; |
476 |
|
} |
477 |
887167 |
if (id == PfRule::AND_INTRO) |
478 |
|
{ |
479 |
99672 |
Assert(children.size() >= 1); |
480 |
99672 |
return children.size() == 1 |
481 |
|
? children[0] |
482 |
99672 |
: NodeManager::currentNM()->mkNode(kind::AND, children); |
483 |
|
} |
484 |
787495 |
if (id == PfRule::NOT_OR_ELIM) |
485 |
|
{ |
486 |
2450 |
Assert(children.size() == 1); |
487 |
2450 |
Assert(args.size() == 1); |
488 |
|
uint32_t i; |
489 |
4900 |
if (children[0].getKind() != kind::NOT |
490 |
4900 |
|| children[0][0].getKind() != kind::OR || !getUInt32(args[0], i)) |
491 |
|
{ |
492 |
|
return Node::null(); |
493 |
|
} |
494 |
2450 |
if (i >= children[0][0].getNumChildren()) |
495 |
|
{ |
496 |
|
return Node::null(); |
497 |
|
} |
498 |
2450 |
return children[0][0][i].notNode(); |
499 |
|
} |
500 |
785045 |
if (id == PfRule::IMPLIES_ELIM) |
501 |
|
{ |
502 |
41563 |
Assert(children.size() == 1); |
503 |
41563 |
Assert(args.empty()); |
504 |
41563 |
if (children[0].getKind() != kind::IMPLIES) |
505 |
|
{ |
506 |
|
return Node::null(); |
507 |
|
} |
508 |
|
return NodeManager::currentNM()->mkNode( |
509 |
41563 |
kind::OR, children[0][0].notNode(), children[0][1]); |
510 |
|
} |
511 |
743482 |
if (id == PfRule::NOT_IMPLIES_ELIM1) |
512 |
|
{ |
513 |
633 |
Assert(children.size() == 1); |
514 |
633 |
Assert(args.empty()); |
515 |
1266 |
if (children[0].getKind() != kind::NOT |
516 |
1266 |
|| children[0][0].getKind() != kind::IMPLIES) |
517 |
|
{ |
518 |
|
return Node::null(); |
519 |
|
} |
520 |
633 |
return children[0][0][0]; |
521 |
|
} |
522 |
742849 |
if (id == PfRule::NOT_IMPLIES_ELIM2) |
523 |
|
{ |
524 |
386 |
Assert(children.size() == 1); |
525 |
386 |
Assert(args.empty()); |
526 |
772 |
if (children[0].getKind() != kind::NOT |
527 |
772 |
|| children[0][0].getKind() != kind::IMPLIES) |
528 |
|
{ |
529 |
|
return Node::null(); |
530 |
|
} |
531 |
386 |
return children[0][0][1].notNode(); |
532 |
|
} |
533 |
742463 |
if (id == PfRule::EQUIV_ELIM1) |
534 |
|
{ |
535 |
15506 |
Assert(children.size() == 1); |
536 |
15506 |
Assert(args.empty()); |
537 |
15506 |
if (children[0].getKind() != kind::EQUAL) |
538 |
|
{ |
539 |
|
return Node::null(); |
540 |
|
} |
541 |
|
return NodeManager::currentNM()->mkNode( |
542 |
15506 |
kind::OR, children[0][0].notNode(), children[0][1]); |
543 |
|
} |
544 |
726957 |
if (id == PfRule::EQUIV_ELIM2) |
545 |
|
{ |
546 |
13294 |
Assert(children.size() == 1); |
547 |
13294 |
Assert(args.empty()); |
548 |
13294 |
if (children[0].getKind() != kind::EQUAL) |
549 |
|
{ |
550 |
|
return Node::null(); |
551 |
|
} |
552 |
|
return NodeManager::currentNM()->mkNode( |
553 |
13294 |
kind::OR, children[0][0], children[0][1].notNode()); |
554 |
|
} |
555 |
713663 |
if (id == PfRule::NOT_EQUIV_ELIM1) |
556 |
|
{ |
557 |
216 |
Assert(children.size() == 1); |
558 |
216 |
Assert(args.empty()); |
559 |
432 |
if (children[0].getKind() != kind::NOT |
560 |
432 |
|| children[0][0].getKind() != kind::EQUAL) |
561 |
|
{ |
562 |
|
return Node::null(); |
563 |
|
} |
564 |
|
return NodeManager::currentNM()->mkNode( |
565 |
216 |
kind::OR, children[0][0][0], children[0][0][1]); |
566 |
|
} |
567 |
713447 |
if (id == PfRule::NOT_EQUIV_ELIM2) |
568 |
|
{ |
569 |
156 |
Assert(children.size() == 1); |
570 |
156 |
Assert(args.empty()); |
571 |
312 |
if (children[0].getKind() != kind::NOT |
572 |
312 |
|| children[0][0].getKind() != kind::EQUAL) |
573 |
|
{ |
574 |
|
return Node::null(); |
575 |
|
} |
576 |
|
return NodeManager::currentNM()->mkNode( |
577 |
156 |
kind::OR, children[0][0][0].notNode(), children[0][0][1].notNode()); |
578 |
|
} |
579 |
713291 |
if (id == PfRule::XOR_ELIM1) |
580 |
|
{ |
581 |
24 |
Assert(children.size() == 1); |
582 |
24 |
Assert(args.empty()); |
583 |
24 |
if (children[0].getKind() != kind::XOR) |
584 |
|
{ |
585 |
|
return Node::null(); |
586 |
|
} |
587 |
|
return NodeManager::currentNM()->mkNode( |
588 |
24 |
kind::OR, children[0][0], children[0][1]); |
589 |
|
} |
590 |
713267 |
if (id == PfRule::XOR_ELIM2) |
591 |
|
{ |
592 |
31 |
Assert(children.size() == 1); |
593 |
31 |
Assert(args.empty()); |
594 |
31 |
if (children[0].getKind() != kind::XOR) |
595 |
|
{ |
596 |
|
return Node::null(); |
597 |
|
} |
598 |
|
return NodeManager::currentNM()->mkNode( |
599 |
31 |
kind::OR, children[0][0].notNode(), children[0][1].notNode()); |
600 |
|
} |
601 |
713236 |
if (id == PfRule::NOT_XOR_ELIM1) |
602 |
|
{ |
603 |
5 |
Assert(children.size() == 1); |
604 |
5 |
Assert(args.empty()); |
605 |
10 |
if (children[0].getKind() != kind::NOT |
606 |
10 |
|| children[0][0].getKind() != kind::XOR) |
607 |
|
{ |
608 |
|
return Node::null(); |
609 |
|
} |
610 |
|
return NodeManager::currentNM()->mkNode( |
611 |
5 |
kind::OR, children[0][0][0], children[0][0][1].notNode()); |
612 |
|
} |
613 |
713231 |
if (id == PfRule::NOT_XOR_ELIM2) |
614 |
|
{ |
615 |
3 |
Assert(children.size() == 1); |
616 |
3 |
Assert(args.empty()); |
617 |
6 |
if (children[0].getKind() != kind::NOT |
618 |
6 |
|| children[0][0].getKind() != kind::XOR) |
619 |
|
{ |
620 |
|
return Node::null(); |
621 |
|
} |
622 |
|
return NodeManager::currentNM()->mkNode( |
623 |
3 |
kind::OR, children[0][0][0].notNode(), children[0][0][1]); |
624 |
|
} |
625 |
713228 |
if (id == PfRule::ITE_ELIM1) |
626 |
|
{ |
627 |
7872 |
Assert(children.size() == 1); |
628 |
7872 |
Assert(args.empty()); |
629 |
7872 |
if (children[0].getKind() != kind::ITE) |
630 |
|
{ |
631 |
|
return Node::null(); |
632 |
|
} |
633 |
|
return NodeManager::currentNM()->mkNode( |
634 |
7872 |
kind::OR, children[0][0].notNode(), children[0][1]); |
635 |
|
} |
636 |
705356 |
if (id == PfRule::ITE_ELIM2) |
637 |
|
{ |
638 |
15191 |
Assert(children.size() == 1); |
639 |
15191 |
Assert(args.empty()); |
640 |
15191 |
if (children[0].getKind() != kind::ITE) |
641 |
|
{ |
642 |
|
return Node::null(); |
643 |
|
} |
644 |
|
return NodeManager::currentNM()->mkNode( |
645 |
15191 |
kind::OR, children[0][0], children[0][2]); |
646 |
|
} |
647 |
690165 |
if (id == PfRule::NOT_ITE_ELIM1) |
648 |
|
{ |
649 |
71 |
Assert(children.size() == 1); |
650 |
71 |
Assert(args.empty()); |
651 |
142 |
if (children[0].getKind() != kind::NOT |
652 |
142 |
|| children[0][0].getKind() != kind::ITE) |
653 |
|
{ |
654 |
|
return Node::null(); |
655 |
|
} |
656 |
|
return NodeManager::currentNM()->mkNode( |
657 |
71 |
kind::OR, children[0][0][0].notNode(), children[0][0][1].notNode()); |
658 |
|
} |
659 |
690094 |
if (id == PfRule::NOT_ITE_ELIM2) |
660 |
|
{ |
661 |
107 |
Assert(children.size() == 1); |
662 |
107 |
Assert(args.empty()); |
663 |
214 |
if (children[0].getKind() != kind::NOT |
664 |
214 |
|| children[0][0].getKind() != kind::ITE) |
665 |
|
{ |
666 |
|
return Node::null(); |
667 |
|
} |
668 |
|
return NodeManager::currentNM()->mkNode( |
669 |
107 |
kind::OR, children[0][0][0], children[0][0][2].notNode()); |
670 |
|
} |
671 |
|
// De Morgan |
672 |
689987 |
if (id == PfRule::NOT_AND) |
673 |
|
{ |
674 |
41114 |
Assert(children.size() == 1); |
675 |
41114 |
Assert(args.empty()); |
676 |
82228 |
if (children[0].getKind() != kind::NOT |
677 |
82228 |
|| children[0][0].getKind() != kind::AND) |
678 |
|
{ |
679 |
|
return Node::null(); |
680 |
|
} |
681 |
82228 |
std::vector<Node> disjuncts; |
682 |
266344 |
for (std::size_t i = 0, size = children[0][0].getNumChildren(); i < size; |
683 |
|
++i) |
684 |
|
{ |
685 |
225230 |
disjuncts.push_back(children[0][0][i].notNode()); |
686 |
|
} |
687 |
41114 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
688 |
|
} |
689 |
|
// valid clauses rules for Tseitin CNF transformation |
690 |
648873 |
if (id == PfRule::CNF_AND_POS) |
691 |
|
{ |
692 |
271263 |
Assert(children.empty()); |
693 |
271263 |
Assert(args.size() == 2); |
694 |
|
uint32_t i; |
695 |
271263 |
if (args[0].getKind() != kind::AND || !getUInt32(args[1], i)) |
696 |
|
{ |
697 |
|
return Node::null(); |
698 |
|
} |
699 |
271263 |
if (i >= args[0].getNumChildren()) |
700 |
|
{ |
701 |
|
return Node::null(); |
702 |
|
} |
703 |
|
return NodeManager::currentNM()->mkNode( |
704 |
271263 |
kind::OR, args[0].notNode(), args[0][i]); |
705 |
|
} |
706 |
377610 |
if (id == PfRule::CNF_AND_NEG) |
707 |
|
{ |
708 |
68885 |
Assert(children.empty()); |
709 |
68885 |
Assert(args.size() == 1); |
710 |
68885 |
if (args[0].getKind() != kind::AND) |
711 |
|
{ |
712 |
|
return Node::null(); |
713 |
|
} |
714 |
137770 |
std::vector<Node> disjuncts{args[0]}; |
715 |
491865 |
for (unsigned i = 0, size = args[0].getNumChildren(); i < size; ++i) |
716 |
|
{ |
717 |
422980 |
disjuncts.push_back(args[0][i].notNode()); |
718 |
|
} |
719 |
68885 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
720 |
|
} |
721 |
308725 |
if (id == PfRule::CNF_OR_POS) |
722 |
|
{ |
723 |
30054 |
Assert(children.empty()); |
724 |
30054 |
Assert(args.size() == 1); |
725 |
30054 |
if (args[0].getKind() != kind::OR) |
726 |
|
{ |
727 |
|
return Node::null(); |
728 |
|
} |
729 |
60108 |
std::vector<Node> disjuncts{args[0].notNode()}; |
730 |
297598 |
for (unsigned i = 0, size = args[0].getNumChildren(); i < size; ++i) |
731 |
|
{ |
732 |
267544 |
disjuncts.push_back(args[0][i]); |
733 |
|
} |
734 |
30054 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
735 |
|
} |
736 |
278671 |
if (id == PfRule::CNF_OR_NEG) |
737 |
|
{ |
738 |
87088 |
Assert(children.empty()); |
739 |
87088 |
Assert(args.size() == 2); |
740 |
|
uint32_t i; |
741 |
87088 |
if (args[0].getKind() != kind::OR || !getUInt32(args[1], i)) |
742 |
|
{ |
743 |
|
return Node::null(); |
744 |
|
} |
745 |
87088 |
if (i >= args[0].getNumChildren()) |
746 |
|
{ |
747 |
|
return Node::null(); |
748 |
|
} |
749 |
|
return NodeManager::currentNM()->mkNode( |
750 |
87088 |
kind::OR, args[0], args[0][i].notNode()); |
751 |
|
} |
752 |
191583 |
if (id == PfRule::CNF_IMPLIES_POS) |
753 |
|
{ |
754 |
1378 |
Assert(children.empty()); |
755 |
1378 |
Assert(args.size() == 1); |
756 |
1378 |
if (args[0].getKind() != kind::IMPLIES) |
757 |
|
{ |
758 |
|
return Node::null(); |
759 |
|
} |
760 |
|
std::vector<Node> disjuncts{ |
761 |
2756 |
args[0].notNode(), args[0][0].notNode(), args[0][1]}; |
762 |
1378 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
763 |
|
} |
764 |
190205 |
if (id == PfRule::CNF_IMPLIES_NEG1) |
765 |
|
{ |
766 |
1019 |
Assert(children.empty()); |
767 |
1019 |
Assert(args.size() == 1); |
768 |
1019 |
if (args[0].getKind() != kind::IMPLIES) |
769 |
|
{ |
770 |
|
return Node::null(); |
771 |
|
} |
772 |
2038 |
std::vector<Node> disjuncts{args[0], args[0][0]}; |
773 |
1019 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
774 |
|
} |
775 |
189186 |
if (id == PfRule::CNF_IMPLIES_NEG2) |
776 |
|
{ |
777 |
1877 |
Assert(children.empty()); |
778 |
1877 |
Assert(args.size() == 1); |
779 |
1877 |
if (args[0].getKind() != kind::IMPLIES) |
780 |
|
{ |
781 |
|
return Node::null(); |
782 |
|
} |
783 |
3754 |
std::vector<Node> disjuncts{args[0], args[0][1].notNode()}; |
784 |
1877 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
785 |
|
} |
786 |
187309 |
if (id == PfRule::CNF_EQUIV_POS1) |
787 |
|
{ |
788 |
25080 |
Assert(children.empty()); |
789 |
25080 |
Assert(args.size() == 1); |
790 |
25080 |
if (args[0].getKind() != kind::EQUAL) |
791 |
|
{ |
792 |
|
return Node::null(); |
793 |
|
} |
794 |
|
std::vector<Node> disjuncts{ |
795 |
50160 |
args[0].notNode(), args[0][0].notNode(), args[0][1]}; |
796 |
25080 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
797 |
|
} |
798 |
162229 |
if (id == PfRule::CNF_EQUIV_POS2) |
799 |
|
{ |
800 |
24081 |
Assert(children.empty()); |
801 |
24081 |
Assert(args.size() == 1); |
802 |
24081 |
if (args[0].getKind() != kind::EQUAL) |
803 |
|
{ |
804 |
|
return Node::null(); |
805 |
|
} |
806 |
|
std::vector<Node> disjuncts{ |
807 |
48162 |
args[0].notNode(), args[0][0], args[0][1].notNode()}; |
808 |
24081 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
809 |
|
} |
810 |
138148 |
if (id == PfRule::CNF_EQUIV_NEG1) |
811 |
|
{ |
812 |
24276 |
Assert(children.empty()); |
813 |
24276 |
Assert(args.size() == 1); |
814 |
24276 |
if (args[0].getKind() != kind::EQUAL) |
815 |
|
{ |
816 |
|
return Node::null(); |
817 |
|
} |
818 |
48552 |
std::vector<Node> disjuncts{args[0], args[0][0], args[0][1]}; |
819 |
24276 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
820 |
|
} |
821 |
113872 |
if (id == PfRule::CNF_EQUIV_NEG2) |
822 |
|
{ |
823 |
27409 |
Assert(children.empty()); |
824 |
27409 |
Assert(args.size() == 1); |
825 |
27409 |
if (args[0].getKind() != kind::EQUAL) |
826 |
|
{ |
827 |
|
return Node::null(); |
828 |
|
} |
829 |
|
std::vector<Node> disjuncts{ |
830 |
54818 |
args[0], args[0][0].notNode(), args[0][1].notNode()}; |
831 |
27409 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
832 |
|
} |
833 |
86463 |
if (id == PfRule::CNF_XOR_POS1) |
834 |
|
{ |
835 |
10770 |
Assert(children.empty()); |
836 |
10770 |
Assert(args.size() == 1); |
837 |
10770 |
if (args[0].getKind() != kind::XOR) |
838 |
|
{ |
839 |
|
return Node::null(); |
840 |
|
} |
841 |
21540 |
std::vector<Node> disjuncts{args[0].notNode(), args[0][0], args[0][1]}; |
842 |
10770 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
843 |
|
} |
844 |
75693 |
if (id == PfRule::CNF_XOR_POS2) |
845 |
|
{ |
846 |
11036 |
Assert(children.empty()); |
847 |
11036 |
Assert(args.size() == 1); |
848 |
11036 |
if (args[0].getKind() != kind::XOR) |
849 |
|
{ |
850 |
|
return Node::null(); |
851 |
|
} |
852 |
|
std::vector<Node> disjuncts{ |
853 |
22072 |
args[0].notNode(), args[0][0].notNode(), args[0][1].notNode()}; |
854 |
11036 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
855 |
|
} |
856 |
64657 |
if (id == PfRule::CNF_XOR_NEG1) |
857 |
|
{ |
858 |
10772 |
Assert(children.empty()); |
859 |
10772 |
Assert(args.size() == 1); |
860 |
10772 |
if (args[0].getKind() != kind::XOR) |
861 |
|
{ |
862 |
|
return Node::null(); |
863 |
|
} |
864 |
21544 |
std::vector<Node> disjuncts{args[0], args[0][0].notNode(), args[0][1]}; |
865 |
10772 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
866 |
|
} |
867 |
53885 |
if (id == PfRule::CNF_XOR_NEG2) |
868 |
|
{ |
869 |
10733 |
Assert(children.empty()); |
870 |
10733 |
Assert(args.size() == 1); |
871 |
10733 |
if (args[0].getKind() != kind::XOR) |
872 |
|
{ |
873 |
|
return Node::null(); |
874 |
|
} |
875 |
21466 |
std::vector<Node> disjuncts{args[0], args[0][0], args[0][1].notNode()}; |
876 |
10733 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
877 |
|
} |
878 |
43152 |
if (id == PfRule::CNF_ITE_POS1) |
879 |
|
{ |
880 |
6989 |
Assert(children.empty()); |
881 |
6989 |
Assert(args.size() == 1); |
882 |
6989 |
if (args[0].getKind() != kind::ITE) |
883 |
|
{ |
884 |
|
return Node::null(); |
885 |
|
} |
886 |
|
std::vector<Node> disjuncts{ |
887 |
13978 |
args[0].notNode(), args[0][0].notNode(), args[0][1]}; |
888 |
6989 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
889 |
|
} |
890 |
36163 |
if (id == PfRule::CNF_ITE_POS2) |
891 |
|
{ |
892 |
6763 |
Assert(children.empty()); |
893 |
6763 |
Assert(args.size() == 1); |
894 |
6763 |
if (args[0].getKind() != kind::ITE) |
895 |
|
{ |
896 |
|
return Node::null(); |
897 |
|
} |
898 |
13526 |
std::vector<Node> disjuncts{args[0].notNode(), args[0][0], args[0][2]}; |
899 |
6763 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
900 |
|
} |
901 |
29400 |
if (id == PfRule::CNF_ITE_POS3) |
902 |
|
{ |
903 |
7062 |
Assert(children.empty()); |
904 |
7062 |
Assert(args.size() == 1); |
905 |
7062 |
if (args[0].getKind() != kind::ITE) |
906 |
|
{ |
907 |
|
return Node::null(); |
908 |
|
} |
909 |
14124 |
std::vector<Node> disjuncts{args[0].notNode(), args[0][1], args[0][2]}; |
910 |
7062 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
911 |
|
} |
912 |
22338 |
if (id == PfRule::CNF_ITE_NEG1) |
913 |
|
{ |
914 |
7114 |
Assert(children.empty()); |
915 |
7114 |
Assert(args.size() == 1); |
916 |
7114 |
if (args[0].getKind() != kind::ITE) |
917 |
|
{ |
918 |
|
return Node::null(); |
919 |
|
} |
920 |
|
std::vector<Node> disjuncts{ |
921 |
14228 |
args[0], args[0][0].notNode(), args[0][1].notNode()}; |
922 |
7114 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
923 |
|
} |
924 |
15224 |
if (id == PfRule::CNF_ITE_NEG2) |
925 |
|
{ |
926 |
6756 |
Assert(children.empty()); |
927 |
6756 |
Assert(args.size() == 1); |
928 |
6756 |
if (args[0].getKind() != kind::ITE) |
929 |
|
{ |
930 |
|
return Node::null(); |
931 |
|
} |
932 |
13512 |
std::vector<Node> disjuncts{args[0], args[0][0], args[0][2].notNode()}; |
933 |
6756 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
934 |
|
} |
935 |
8468 |
if (id == PfRule::CNF_ITE_NEG3) |
936 |
|
{ |
937 |
7100 |
Assert(children.empty()); |
938 |
7100 |
Assert(args.size() == 1); |
939 |
7100 |
if (args[0].getKind() != kind::ITE) |
940 |
|
{ |
941 |
|
return Node::null(); |
942 |
|
} |
943 |
|
std::vector<Node> disjuncts{ |
944 |
14200 |
args[0], args[0][1].notNode(), args[0][2].notNode()}; |
945 |
7100 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
946 |
|
} |
947 |
1368 |
if (id == PfRule::SAT_REFUTATION) |
948 |
|
{ |
949 |
1368 |
Assert(args.empty()); |
950 |
1368 |
return NodeManager::currentNM()->mkConst(false); |
951 |
|
} |
952 |
|
// no rule |
953 |
|
return Node::null(); |
954 |
|
} |
955 |
|
|
956 |
|
} // namespace booleans |
957 |
|
} // namespace theory |
958 |
29280 |
} // namespace cvc5 |