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 |
7989 |
void BoolProofRuleChecker::registerTo(ProofChecker* pc) |
25 |
|
{ |
26 |
7989 |
pc->registerChecker(PfRule::SPLIT, this); |
27 |
7989 |
pc->registerChecker(PfRule::RESOLUTION, this); |
28 |
7989 |
pc->registerChecker(PfRule::CHAIN_RESOLUTION, this); |
29 |
7989 |
pc->registerTrustedChecker(PfRule::MACRO_RESOLUTION_TRUST, this, 3); |
30 |
7989 |
pc->registerChecker(PfRule::MACRO_RESOLUTION, this); |
31 |
7989 |
pc->registerChecker(PfRule::FACTORING, this); |
32 |
7989 |
pc->registerChecker(PfRule::REORDERING, this); |
33 |
7989 |
pc->registerChecker(PfRule::EQ_RESOLVE, this); |
34 |
7989 |
pc->registerChecker(PfRule::MODUS_PONENS, this); |
35 |
7989 |
pc->registerChecker(PfRule::NOT_NOT_ELIM, this); |
36 |
7989 |
pc->registerChecker(PfRule::CONTRA, this); |
37 |
7989 |
pc->registerChecker(PfRule::AND_ELIM, this); |
38 |
7989 |
pc->registerChecker(PfRule::AND_INTRO, this); |
39 |
7989 |
pc->registerChecker(PfRule::NOT_OR_ELIM, this); |
40 |
7989 |
pc->registerChecker(PfRule::IMPLIES_ELIM, this); |
41 |
7989 |
pc->registerChecker(PfRule::NOT_IMPLIES_ELIM1, this); |
42 |
7989 |
pc->registerChecker(PfRule::NOT_IMPLIES_ELIM2, this); |
43 |
7989 |
pc->registerChecker(PfRule::EQUIV_ELIM1, this); |
44 |
7989 |
pc->registerChecker(PfRule::EQUIV_ELIM2, this); |
45 |
7989 |
pc->registerChecker(PfRule::NOT_EQUIV_ELIM1, this); |
46 |
7989 |
pc->registerChecker(PfRule::NOT_EQUIV_ELIM2, this); |
47 |
7989 |
pc->registerChecker(PfRule::XOR_ELIM1, this); |
48 |
7989 |
pc->registerChecker(PfRule::XOR_ELIM2, this); |
49 |
7989 |
pc->registerChecker(PfRule::NOT_XOR_ELIM1, this); |
50 |
7989 |
pc->registerChecker(PfRule::NOT_XOR_ELIM2, this); |
51 |
7989 |
pc->registerChecker(PfRule::ITE_ELIM1, this); |
52 |
7989 |
pc->registerChecker(PfRule::ITE_ELIM2, this); |
53 |
7989 |
pc->registerChecker(PfRule::NOT_ITE_ELIM1, this); |
54 |
7989 |
pc->registerChecker(PfRule::NOT_ITE_ELIM2, this); |
55 |
7989 |
pc->registerChecker(PfRule::NOT_AND, this); |
56 |
7989 |
pc->registerChecker(PfRule::CNF_AND_POS, this); |
57 |
7989 |
pc->registerChecker(PfRule::CNF_AND_NEG, this); |
58 |
7989 |
pc->registerChecker(PfRule::CNF_OR_POS, this); |
59 |
7989 |
pc->registerChecker(PfRule::CNF_OR_NEG, this); |
60 |
7989 |
pc->registerChecker(PfRule::CNF_IMPLIES_POS, this); |
61 |
7989 |
pc->registerChecker(PfRule::CNF_IMPLIES_NEG1, this); |
62 |
7989 |
pc->registerChecker(PfRule::CNF_IMPLIES_NEG2, this); |
63 |
7989 |
pc->registerChecker(PfRule::CNF_EQUIV_POS1, this); |
64 |
7989 |
pc->registerChecker(PfRule::CNF_EQUIV_POS2, this); |
65 |
7989 |
pc->registerChecker(PfRule::CNF_EQUIV_NEG1, this); |
66 |
7989 |
pc->registerChecker(PfRule::CNF_EQUIV_NEG2, this); |
67 |
7989 |
pc->registerChecker(PfRule::CNF_XOR_POS1, this); |
68 |
7989 |
pc->registerChecker(PfRule::CNF_XOR_POS2, this); |
69 |
7989 |
pc->registerChecker(PfRule::CNF_XOR_NEG1, this); |
70 |
7989 |
pc->registerChecker(PfRule::CNF_XOR_NEG2, this); |
71 |
7989 |
pc->registerChecker(PfRule::CNF_ITE_POS1, this); |
72 |
7989 |
pc->registerChecker(PfRule::CNF_ITE_POS2, this); |
73 |
7989 |
pc->registerChecker(PfRule::CNF_ITE_POS3, this); |
74 |
7989 |
pc->registerChecker(PfRule::CNF_ITE_NEG1, this); |
75 |
7989 |
pc->registerChecker(PfRule::CNF_ITE_NEG2, this); |
76 |
7989 |
pc->registerChecker(PfRule::CNF_ITE_NEG3, this); |
77 |
7989 |
pc->registerTrustedChecker(PfRule::SAT_REFUTATION, this, 1); |
78 |
7989 |
} |
79 |
|
|
80 |
3576580 |
Node BoolProofRuleChecker::checkInternal(PfRule id, |
81 |
|
const std::vector<Node>& children, |
82 |
|
const std::vector<Node>& args) |
83 |
|
{ |
84 |
3576580 |
if (id == PfRule::RESOLUTION) |
85 |
|
{ |
86 |
19839 |
Assert(children.size() == 2); |
87 |
19839 |
Assert(args.size() == 2); |
88 |
19839 |
NodeManager* nm = NodeManager::currentNM(); |
89 |
39678 |
std::vector<Node> disjuncts; |
90 |
39678 |
Node pivots[2]; |
91 |
19839 |
if (args[0] == nm->mkConst(true)) |
92 |
|
{ |
93 |
15762 |
pivots[0] = args[1]; |
94 |
15762 |
pivots[1] = args[1].notNode(); |
95 |
|
} |
96 |
|
else |
97 |
|
{ |
98 |
4077 |
Assert(args[0] == nm->mkConst(false)); |
99 |
4077 |
pivots[0] = args[1].notNode(); |
100 |
4077 |
pivots[1] = args[1]; |
101 |
|
} |
102 |
59517 |
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 |
79356 |
std::vector<Node> lits; |
108 |
39678 |
if (children[i].getKind() == kind::OR && pivots[i] != children[i]) |
109 |
|
{ |
110 |
33449 |
lits.insert(lits.end(), children[i].begin(), children[i].end()); |
111 |
|
} |
112 |
|
else |
113 |
|
{ |
114 |
6229 |
lits.push_back(children[i]); |
115 |
|
} |
116 |
189815 |
for (unsigned j = 0, size = lits.size(); j < size; ++j) |
117 |
|
{ |
118 |
150137 |
if (pivots[i] != lits[j]) |
119 |
|
{ |
120 |
110459 |
disjuncts.push_back(lits[j]); |
121 |
|
} |
122 |
|
else |
123 |
|
{ |
124 |
|
// just eliminate first occurrence |
125 |
39678 |
pivots[i] = Node::null(); |
126 |
|
} |
127 |
|
} |
128 |
|
} |
129 |
19839 |
return disjuncts.empty() |
130 |
|
? nm->mkConst(false) |
131 |
26068 |
: disjuncts.size() == 1 ? disjuncts[0] |
132 |
45907 |
: nm->mkNode(kind::OR, disjuncts); |
133 |
|
} |
134 |
3556741 |
if (id == PfRule::FACTORING) |
135 |
|
{ |
136 |
409934 |
Assert(children.size() == 1); |
137 |
409934 |
Assert(args.empty()); |
138 |
409934 |
if (children[0].getKind() != kind::OR) |
139 |
|
{ |
140 |
|
return Node::null(); |
141 |
|
} |
142 |
|
// remove duplicates while keeping the order of children |
143 |
819868 |
std::unordered_set<TNode> clauseSet; |
144 |
819868 |
std::vector<Node> disjuncts; |
145 |
409934 |
unsigned size = children[0].getNumChildren(); |
146 |
8006832 |
for (unsigned i = 0; i < size; ++i) |
147 |
|
{ |
148 |
7596898 |
if (clauseSet.count(children[0][i])) |
149 |
|
{ |
150 |
2458155 |
continue; |
151 |
|
} |
152 |
5138743 |
disjuncts.push_back(children[0][i]); |
153 |
5138743 |
clauseSet.insert(children[0][i]); |
154 |
|
} |
155 |
409934 |
if (disjuncts.size() == size) |
156 |
|
{ |
157 |
|
return Node::null(); |
158 |
|
} |
159 |
409934 |
NodeManager* nm = NodeManager::currentNM(); |
160 |
409934 |
return nm->mkOr(disjuncts); |
161 |
|
} |
162 |
3146807 |
if (id == PfRule::REORDERING) |
163 |
|
{ |
164 |
998584 |
Assert(children.size() == 1); |
165 |
998584 |
Assert(args.size() == 1); |
166 |
1997168 |
std::unordered_set<Node> clauseSet1, clauseSet2; |
167 |
998584 |
if (children[0].getKind() == kind::OR) |
168 |
|
{ |
169 |
998584 |
clauseSet1.insert(children[0].begin(), children[0].end()); |
170 |
|
} |
171 |
|
else |
172 |
|
{ |
173 |
|
clauseSet1.insert(children[0]); |
174 |
|
} |
175 |
998584 |
if (args[0].getKind() == kind::OR) |
176 |
|
{ |
177 |
998584 |
clauseSet2.insert(args[0].begin(), args[0].end()); |
178 |
|
} |
179 |
|
else |
180 |
|
{ |
181 |
|
clauseSet2.insert(args[0]); |
182 |
|
} |
183 |
998584 |
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 |
998584 |
return args[0]; |
190 |
|
} |
191 |
2148223 |
if (id == PfRule::CHAIN_RESOLUTION) |
192 |
|
{ |
193 |
588100 |
Assert(children.size() > 1); |
194 |
588100 |
Assert(args.size() == 2 * (children.size() - 1)); |
195 |
588100 |
Trace("bool-pfcheck") << "chain_res:\n" << push; |
196 |
588100 |
NodeManager* nm = NodeManager::currentNM(); |
197 |
1176200 |
Node trueNode = nm->mkConst(true); |
198 |
1176200 |
Node falseNode = nm->mkConst(false); |
199 |
|
// The lhs and rhs clauses in a binary resolution step, respectively. Since |
200 |
|
// children correspond to the premises in the resolution chain, the first |
201 |
|
// lhs clause is the first premise, the first rhs clause is the second |
202 |
|
// premise. Each subsequent lhs clause will be the result of the previous |
203 |
|
// binary resolution step in the chain, while each subsequent rhs clause |
204 |
|
// will be respectively the second, third etc premises. |
205 |
1176200 |
std::vector<Node> lhsClause, rhsClause; |
206 |
|
// The pivots to be eliminated to the lhs clause and rhs clause in a binary |
207 |
|
// resolution step, respectively |
208 |
1176200 |
Node lhsElim, rhsElim; |
209 |
|
// Get lhsClause of first resolution. |
210 |
|
// |
211 |
|
// Since a Node cannot hold an OR with a single child we need to |
212 |
|
// disambiguate singleton clauses that are OR nodes from non-singleton |
213 |
|
// clauses (i.e. unit clauses in the SAT solver). |
214 |
|
// |
215 |
|
// If the child is not an OR, it is a singleton clause and we take the |
216 |
|
// child itself as the clause. Otherwise the child can only be a singleton |
217 |
|
// clause if the child itself is used as a resolution literal, i.e. if the |
218 |
|
// first child equal to the first pivot (which is args[1] or |
219 |
|
// args[1].notNote() depending on the polarity). |
220 |
1176200 |
if (children[0].getKind() != kind::OR |
221 |
587320 |
|| (args[0] == trueNode && children[0] == args[1]) |
222 |
1763520 |
|| (args[0] == falseNode && children[0] == args[1].notNode())) |
223 |
|
{ |
224 |
780 |
lhsClause.push_back(children[0]); |
225 |
|
} |
226 |
|
else |
227 |
|
{ |
228 |
587320 |
lhsClause.insert(lhsClause.end(), children[0].begin(), children[0].end()); |
229 |
|
} |
230 |
|
// Traverse the links, which amounts to for each pair of args removing a |
231 |
|
// literal from the lhs and a literal from the lhs. |
232 |
3984479 |
for (size_t i = 0, argsSize = args.size(); i < argsSize; i = i + 2) |
233 |
|
{ |
234 |
|
// Polarity determines how the pivot occurs in lhs and rhs |
235 |
3396379 |
if (args[i] == trueNode) |
236 |
|
{ |
237 |
1652655 |
lhsElim = args[i + 1]; |
238 |
1652655 |
rhsElim = args[i + 1].notNode(); |
239 |
|
} |
240 |
|
else |
241 |
|
{ |
242 |
1743724 |
Assert(args[i] == falseNode); |
243 |
1743724 |
lhsElim = args[i + 1].notNode(); |
244 |
1743724 |
rhsElim = args[i + 1]; |
245 |
|
} |
246 |
|
// The index of the child corresponding to the current rhs clause |
247 |
3396379 |
size_t childIndex = i / 2 + 1; |
248 |
|
// Get rhs clause. It's a singleton if not an OR node or if equal to |
249 |
|
// rhsElim |
250 |
6792758 |
if (children[childIndex].getKind() != kind::OR |
251 |
3396379 |
|| children[childIndex] == rhsElim) |
252 |
|
{ |
253 |
1235017 |
rhsClause.push_back(children[childIndex]); |
254 |
|
} |
255 |
|
else |
256 |
|
{ |
257 |
2161362 |
rhsClause = {children[childIndex].begin(), children[childIndex].end()}; |
258 |
|
} |
259 |
3396379 |
Trace("bool-pfcheck") << i / 2 << "-th res link:\n"; |
260 |
3396379 |
Trace("bool-pfcheck") << "\t - lhsClause: " << lhsClause << "\n"; |
261 |
3396379 |
Trace("bool-pfcheck") << "\t\t - lhsElim: " << lhsElim << "\n"; |
262 |
3396379 |
Trace("bool-pfcheck") << "\t - rhsClause: " << rhsClause << "\n"; |
263 |
3396379 |
Trace("bool-pfcheck") << "\t\t - rhsElim: " << rhsElim << "\n"; |
264 |
|
// Compute the resulting clause, which will be the next lhsClause, as |
265 |
|
// follows: |
266 |
|
// - remove lhsElim from lhsClause |
267 |
|
// - remove rhsElim from rhsClause and add the lits to lhsClause |
268 |
3396379 |
auto itlhs = std::find(lhsClause.begin(), lhsClause.end(), lhsElim); |
269 |
3396379 |
AlwaysAssert(itlhs != lhsClause.end()); |
270 |
3396379 |
lhsClause.erase(itlhs); |
271 |
3396379 |
Trace("bool-pfcheck") << "\t.. after lhsClause: " << lhsClause << "\n"; |
272 |
3396379 |
auto itrhs = std::find(rhsClause.begin(), rhsClause.end(), rhsElim); |
273 |
3396379 |
AlwaysAssert(itrhs != rhsClause.end()); |
274 |
3396379 |
lhsClause.insert(lhsClause.end(), rhsClause.begin(), itrhs); |
275 |
3396379 |
lhsClause.insert(lhsClause.end(), itrhs + 1, rhsClause.end()); |
276 |
3396379 |
Trace("bool-pfcheck") << "\t.. after rhsClause: " << lhsClause << "\n"; |
277 |
3396379 |
rhsClause.clear(); |
278 |
|
} |
279 |
1176200 |
Trace("bool-pfcheck") << "\n resulting clause: " << lhsClause << "\n" |
280 |
588100 |
<< pop; |
281 |
588100 |
return nm->mkOr(lhsClause); |
282 |
|
} |
283 |
1560123 |
if (id == PfRule::MACRO_RESOLUTION_TRUST) |
284 |
|
{ |
285 |
92187 |
Assert(children.size() > 1); |
286 |
92187 |
Assert(args.size() == 2 * (children.size() - 1) + 1); |
287 |
92187 |
return args[0]; |
288 |
|
} |
289 |
1467936 |
if (id == PfRule::MACRO_RESOLUTION) |
290 |
|
{ |
291 |
|
Assert(children.size() > 1); |
292 |
|
Assert(args.size() == 2 * (children.size() - 1) + 1); |
293 |
|
Trace("bool-pfcheck") << "macro_res: " << args[0] << "\n" << push; |
294 |
|
NodeManager* nm = NodeManager::currentNM(); |
295 |
|
Node trueNode = nm->mkConst(true); |
296 |
|
Node falseNode = nm->mkConst(false); |
297 |
|
std::vector<Node> clauseNodes; |
298 |
|
for (std::size_t i = 0, childrenSize = children.size(); i < childrenSize; |
299 |
|
++i) |
300 |
|
{ |
301 |
|
std::unordered_set<Node> elim; |
302 |
|
// literals to be removed from "first" clause |
303 |
|
if (i < childrenSize - 1) |
304 |
|
{ |
305 |
|
for (std::size_t j = (2 * i) + 1, argsSize = args.size(); j < argsSize; |
306 |
|
j = j + 2) |
307 |
|
{ |
308 |
|
// whether pivot should occur as is or negated depends on the polarity |
309 |
|
// of each step in the macro |
310 |
|
if (args[j] == trueNode) |
311 |
|
{ |
312 |
|
elim.insert(args[j + 1]); |
313 |
|
} |
314 |
|
else |
315 |
|
{ |
316 |
|
Assert(args[j] == falseNode); |
317 |
|
elim.insert(args[j + 1].notNode()); |
318 |
|
} |
319 |
|
} |
320 |
|
} |
321 |
|
// literal to be removed from "second" clause. They will be negated |
322 |
|
if (i > 0) |
323 |
|
{ |
324 |
|
std::size_t index = 2 * (i - 1) + 1; |
325 |
|
Node pivot = args[index] == trueNode ? args[index + 1].notNode() |
326 |
|
: args[index + 1]; |
327 |
|
elim.insert(pivot); |
328 |
|
} |
329 |
|
Trace("bool-pfcheck") << i << ": elimination set: " << elim << "\n"; |
330 |
|
// only add to conclusion nodes that are not in elimination set. First get |
331 |
|
// the nodes. |
332 |
|
// |
333 |
|
// Since a Node cannot hold an OR with a single child we need to |
334 |
|
// disambiguate singleton clauses that are OR nodes from non-singleton |
335 |
|
// clauses (i.e. unit clauses in the SAT solver). |
336 |
|
// |
337 |
|
// If the child is not an OR, it is a singleton clause and we take the |
338 |
|
// child itself as the clause. Otherwise the child can only be a singleton |
339 |
|
// clause if the child itself is used as a resolution literal, i.e. if the |
340 |
|
// child is in lhsElim or is equal to rhsElim (which means that the |
341 |
|
// negation of the child is in lhsElim). |
342 |
|
std::vector<Node> lits; |
343 |
|
if (children[i].getKind() == kind::OR && !elim.count(children[i])) |
344 |
|
{ |
345 |
|
lits.insert(lits.end(), children[i].begin(), children[i].end()); |
346 |
|
} |
347 |
|
else |
348 |
|
{ |
349 |
|
lits.push_back(children[i]); |
350 |
|
} |
351 |
|
Trace("bool-pfcheck") << i << ": clause lits: " << lits << "\n"; |
352 |
|
std::vector<Node> added; |
353 |
|
for (std::size_t j = 0, size = lits.size(); j < size; ++j) |
354 |
|
{ |
355 |
|
// only add if literal does not occur in elimination set |
356 |
|
if (elim.count(lits[j]) == 0) |
357 |
|
{ |
358 |
|
clauseNodes.push_back(lits[j]); |
359 |
|
added.push_back(lits[j]); |
360 |
|
// eliminate duplicates |
361 |
|
elim.insert(lits[j]); |
362 |
|
} |
363 |
|
} |
364 |
|
Trace("bool-pfcheck") << i << ": added lits: " << added << "\n\n"; |
365 |
|
} |
366 |
|
Trace("bool-pfcheck") << "clause: " << clauseNodes << "\n"; |
367 |
|
// check that set representation is the same as of the given conclusion |
368 |
|
std::unordered_set<Node> clauseComputed{clauseNodes.begin(), |
369 |
|
clauseNodes.end()}; |
370 |
|
Trace("bool-pfcheck") << "clauseSet: " << clauseComputed << "\n" << pop; |
371 |
|
if (clauseComputed.empty()) |
372 |
|
{ |
373 |
|
// conclusion differ |
374 |
|
if (args[0] != falseNode) |
375 |
|
{ |
376 |
|
return Node::null(); |
377 |
|
} |
378 |
|
return args[0]; |
379 |
|
} |
380 |
|
if (clauseComputed.size() == 1) |
381 |
|
{ |
382 |
|
// conclusion differ |
383 |
|
if (args[0] != *clauseComputed.begin()) |
384 |
|
{ |
385 |
|
return Node::null(); |
386 |
|
} |
387 |
|
return args[0]; |
388 |
|
} |
389 |
|
// At this point, should amount to them differing only on order. So the |
390 |
|
// original result can't be a singleton clause |
391 |
|
if (args[0].getKind() != kind::OR |
392 |
|
|| clauseComputed.size() != args[0].getNumChildren()) |
393 |
|
{ |
394 |
|
return Node::null(); |
395 |
|
} |
396 |
|
std::unordered_set<Node> clauseGiven{args[0].begin(), args[0].end()}; |
397 |
|
return clauseComputed == clauseGiven ? args[0] : Node::null(); |
398 |
|
} |
399 |
1467936 |
if (id == PfRule::SPLIT) |
400 |
|
{ |
401 |
20 |
Assert(children.empty()); |
402 |
20 |
Assert(args.size() == 1); |
403 |
|
return NodeManager::currentNM()->mkNode( |
404 |
20 |
kind::OR, args[0], args[0].notNode()); |
405 |
|
} |
406 |
1467916 |
if (id == PfRule::CONTRA) |
407 |
|
{ |
408 |
21020 |
Assert(children.size() == 2); |
409 |
21020 |
if (children[1].getKind() == Kind::NOT && children[0] == children[1][0]) |
410 |
|
{ |
411 |
21020 |
return NodeManager::currentNM()->mkConst(false); |
412 |
|
} |
413 |
|
return Node::null(); |
414 |
|
} |
415 |
1446896 |
if (id == PfRule::EQ_RESOLVE) |
416 |
|
{ |
417 |
379274 |
Assert(children.size() == 2); |
418 |
379274 |
Assert(args.empty()); |
419 |
379274 |
if (children[1].getKind() != kind::EQUAL || children[0] != children[1][0]) |
420 |
|
{ |
421 |
|
return Node::null(); |
422 |
|
} |
423 |
379274 |
return children[1][1]; |
424 |
|
} |
425 |
1067622 |
if (id == PfRule::MODUS_PONENS) |
426 |
|
{ |
427 |
75751 |
Assert(children.size() == 2); |
428 |
75751 |
Assert(args.empty()); |
429 |
75751 |
if (children[1].getKind() != kind::IMPLIES || children[0] != children[1][0]) |
430 |
|
{ |
431 |
|
return Node::null(); |
432 |
|
} |
433 |
75751 |
return children[1][1]; |
434 |
|
} |
435 |
991871 |
if (id == PfRule::NOT_NOT_ELIM) |
436 |
|
{ |
437 |
3009 |
Assert(children.size() == 1); |
438 |
3009 |
Assert(args.empty()); |
439 |
3009 |
if (children[0].getKind() != kind::NOT || children[0][0].getKind() != kind::NOT) |
440 |
|
{ |
441 |
|
return Node::null(); |
442 |
|
} |
443 |
3009 |
return children[0][0][0]; |
444 |
|
} |
445 |
|
// natural deduction rules |
446 |
988862 |
if (id == PfRule::AND_ELIM) |
447 |
|
{ |
448 |
675613 |
Assert(children.size() == 1); |
449 |
675613 |
Assert(args.size() == 1); |
450 |
|
uint32_t i; |
451 |
675613 |
if (children[0].getKind() != kind::AND || !getUInt32(args[0], i)) |
452 |
|
{ |
453 |
|
return Node::null(); |
454 |
|
} |
455 |
675613 |
if (i >= children[0].getNumChildren()) |
456 |
|
{ |
457 |
|
return Node::null(); |
458 |
|
} |
459 |
675613 |
return children[0][i]; |
460 |
|
} |
461 |
313249 |
if (id == PfRule::AND_INTRO) |
462 |
|
{ |
463 |
80556 |
Assert(children.size() >= 1); |
464 |
80556 |
return children.size() == 1 |
465 |
|
? children[0] |
466 |
80556 |
: NodeManager::currentNM()->mkNode(kind::AND, children); |
467 |
|
} |
468 |
232693 |
if (id == PfRule::NOT_OR_ELIM) |
469 |
|
{ |
470 |
3401 |
Assert(children.size() == 1); |
471 |
3401 |
Assert(args.size() == 1); |
472 |
|
uint32_t i; |
473 |
6802 |
if (children[0].getKind() != kind::NOT |
474 |
6802 |
|| children[0][0].getKind() != kind::OR || !getUInt32(args[0], i)) |
475 |
|
{ |
476 |
|
return Node::null(); |
477 |
|
} |
478 |
3401 |
if (i >= children[0][0].getNumChildren()) |
479 |
|
{ |
480 |
|
return Node::null(); |
481 |
|
} |
482 |
3401 |
return children[0][0][i].notNode(); |
483 |
|
} |
484 |
229292 |
if (id == PfRule::IMPLIES_ELIM) |
485 |
|
{ |
486 |
35502 |
Assert(children.size() == 1); |
487 |
35502 |
Assert(args.empty()); |
488 |
35502 |
if (children[0].getKind() != kind::IMPLIES) |
489 |
|
{ |
490 |
|
return Node::null(); |
491 |
|
} |
492 |
|
return NodeManager::currentNM()->mkNode( |
493 |
35502 |
kind::OR, children[0][0].notNode(), children[0][1]); |
494 |
|
} |
495 |
193790 |
if (id == PfRule::NOT_IMPLIES_ELIM1) |
496 |
|
{ |
497 |
733 |
Assert(children.size() == 1); |
498 |
733 |
Assert(args.empty()); |
499 |
1466 |
if (children[0].getKind() != kind::NOT |
500 |
1466 |
|| children[0][0].getKind() != kind::IMPLIES) |
501 |
|
{ |
502 |
|
return Node::null(); |
503 |
|
} |
504 |
733 |
return children[0][0][0]; |
505 |
|
} |
506 |
193057 |
if (id == PfRule::NOT_IMPLIES_ELIM2) |
507 |
|
{ |
508 |
393 |
Assert(children.size() == 1); |
509 |
393 |
Assert(args.empty()); |
510 |
786 |
if (children[0].getKind() != kind::NOT |
511 |
786 |
|| children[0][0].getKind() != kind::IMPLIES) |
512 |
|
{ |
513 |
|
return Node::null(); |
514 |
|
} |
515 |
393 |
return children[0][0][1].notNode(); |
516 |
|
} |
517 |
192664 |
if (id == PfRule::EQUIV_ELIM1) |
518 |
|
{ |
519 |
20524 |
Assert(children.size() == 1); |
520 |
20524 |
Assert(args.empty()); |
521 |
20524 |
if (children[0].getKind() != kind::EQUAL) |
522 |
|
{ |
523 |
|
return Node::null(); |
524 |
|
} |
525 |
|
return NodeManager::currentNM()->mkNode( |
526 |
20524 |
kind::OR, children[0][0].notNode(), children[0][1]); |
527 |
|
} |
528 |
172140 |
if (id == PfRule::EQUIV_ELIM2) |
529 |
|
{ |
530 |
16199 |
Assert(children.size() == 1); |
531 |
16199 |
Assert(args.empty()); |
532 |
16199 |
if (children[0].getKind() != kind::EQUAL) |
533 |
|
{ |
534 |
|
return Node::null(); |
535 |
|
} |
536 |
|
return NodeManager::currentNM()->mkNode( |
537 |
16199 |
kind::OR, children[0][0], children[0][1].notNode()); |
538 |
|
} |
539 |
155941 |
if (id == PfRule::NOT_EQUIV_ELIM1) |
540 |
|
{ |
541 |
364 |
Assert(children.size() == 1); |
542 |
364 |
Assert(args.empty()); |
543 |
728 |
if (children[0].getKind() != kind::NOT |
544 |
728 |
|| children[0][0].getKind() != kind::EQUAL) |
545 |
|
{ |
546 |
|
return Node::null(); |
547 |
|
} |
548 |
|
return NodeManager::currentNM()->mkNode( |
549 |
364 |
kind::OR, children[0][0][0], children[0][0][1]); |
550 |
|
} |
551 |
155577 |
if (id == PfRule::NOT_EQUIV_ELIM2) |
552 |
|
{ |
553 |
328 |
Assert(children.size() == 1); |
554 |
328 |
Assert(args.empty()); |
555 |
656 |
if (children[0].getKind() != kind::NOT |
556 |
656 |
|| children[0][0].getKind() != kind::EQUAL) |
557 |
|
{ |
558 |
|
return Node::null(); |
559 |
|
} |
560 |
|
return NodeManager::currentNM()->mkNode( |
561 |
328 |
kind::OR, children[0][0][0].notNode(), children[0][0][1].notNode()); |
562 |
|
} |
563 |
155249 |
if (id == PfRule::XOR_ELIM1) |
564 |
|
{ |
565 |
24 |
Assert(children.size() == 1); |
566 |
24 |
Assert(args.empty()); |
567 |
24 |
if (children[0].getKind() != kind::XOR) |
568 |
|
{ |
569 |
|
return Node::null(); |
570 |
|
} |
571 |
|
return NodeManager::currentNM()->mkNode( |
572 |
24 |
kind::OR, children[0][0], children[0][1]); |
573 |
|
} |
574 |
155225 |
if (id == PfRule::XOR_ELIM2) |
575 |
|
{ |
576 |
38 |
Assert(children.size() == 1); |
577 |
38 |
Assert(args.empty()); |
578 |
38 |
if (children[0].getKind() != kind::XOR) |
579 |
|
{ |
580 |
|
return Node::null(); |
581 |
|
} |
582 |
|
return NodeManager::currentNM()->mkNode( |
583 |
38 |
kind::OR, children[0][0].notNode(), children[0][1].notNode()); |
584 |
|
} |
585 |
155187 |
if (id == PfRule::NOT_XOR_ELIM1) |
586 |
|
{ |
587 |
10 |
Assert(children.size() == 1); |
588 |
10 |
Assert(args.empty()); |
589 |
20 |
if (children[0].getKind() != kind::NOT |
590 |
20 |
|| children[0][0].getKind() != kind::XOR) |
591 |
|
{ |
592 |
|
return Node::null(); |
593 |
|
} |
594 |
|
return NodeManager::currentNM()->mkNode( |
595 |
10 |
kind::OR, children[0][0][0], children[0][0][1].notNode()); |
596 |
|
} |
597 |
155177 |
if (id == PfRule::NOT_XOR_ELIM2) |
598 |
|
{ |
599 |
5 |
Assert(children.size() == 1); |
600 |
5 |
Assert(args.empty()); |
601 |
10 |
if (children[0].getKind() != kind::NOT |
602 |
10 |
|| children[0][0].getKind() != kind::XOR) |
603 |
|
{ |
604 |
|
return Node::null(); |
605 |
|
} |
606 |
|
return NodeManager::currentNM()->mkNode( |
607 |
5 |
kind::OR, children[0][0][0].notNode(), children[0][0][1]); |
608 |
|
} |
609 |
155172 |
if (id == PfRule::ITE_ELIM1) |
610 |
|
{ |
611 |
10170 |
Assert(children.size() == 1); |
612 |
10170 |
Assert(args.empty()); |
613 |
10170 |
if (children[0].getKind() != kind::ITE) |
614 |
|
{ |
615 |
|
return Node::null(); |
616 |
|
} |
617 |
|
return NodeManager::currentNM()->mkNode( |
618 |
10170 |
kind::OR, children[0][0].notNode(), children[0][1]); |
619 |
|
} |
620 |
145002 |
if (id == PfRule::ITE_ELIM2) |
621 |
|
{ |
622 |
21404 |
Assert(children.size() == 1); |
623 |
21404 |
Assert(args.empty()); |
624 |
21404 |
if (children[0].getKind() != kind::ITE) |
625 |
|
{ |
626 |
|
return Node::null(); |
627 |
|
} |
628 |
|
return NodeManager::currentNM()->mkNode( |
629 |
21404 |
kind::OR, children[0][0], children[0][2]); |
630 |
|
} |
631 |
123598 |
if (id == PfRule::NOT_ITE_ELIM1) |
632 |
|
{ |
633 |
1062 |
Assert(children.size() == 1); |
634 |
1062 |
Assert(args.empty()); |
635 |
2124 |
if (children[0].getKind() != kind::NOT |
636 |
2124 |
|| children[0][0].getKind() != kind::ITE) |
637 |
|
{ |
638 |
|
return Node::null(); |
639 |
|
} |
640 |
|
return NodeManager::currentNM()->mkNode( |
641 |
1062 |
kind::OR, children[0][0][0].notNode(), children[0][0][1].notNode()); |
642 |
|
} |
643 |
122536 |
if (id == PfRule::NOT_ITE_ELIM2) |
644 |
|
{ |
645 |
1597 |
Assert(children.size() == 1); |
646 |
1597 |
Assert(args.empty()); |
647 |
3194 |
if (children[0].getKind() != kind::NOT |
648 |
3194 |
|| children[0][0].getKind() != kind::ITE) |
649 |
|
{ |
650 |
|
return Node::null(); |
651 |
|
} |
652 |
|
return NodeManager::currentNM()->mkNode( |
653 |
1597 |
kind::OR, children[0][0][0], children[0][0][2].notNode()); |
654 |
|
} |
655 |
|
// De Morgan |
656 |
120939 |
if (id == PfRule::NOT_AND) |
657 |
|
{ |
658 |
39824 |
Assert(children.size() == 1); |
659 |
39824 |
Assert(args.empty()); |
660 |
79648 |
if (children[0].getKind() != kind::NOT |
661 |
79648 |
|| children[0][0].getKind() != kind::AND) |
662 |
|
{ |
663 |
|
return Node::null(); |
664 |
|
} |
665 |
79648 |
std::vector<Node> disjuncts; |
666 |
210868 |
for (std::size_t i = 0, size = children[0][0].getNumChildren(); i < size; |
667 |
|
++i) |
668 |
|
{ |
669 |
171044 |
disjuncts.push_back(children[0][0][i].notNode()); |
670 |
|
} |
671 |
39824 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
672 |
|
} |
673 |
|
// valid clauses rules for Tseitin CNF transformation |
674 |
81115 |
if (id == PfRule::CNF_AND_POS) |
675 |
|
{ |
676 |
14138 |
Assert(children.empty()); |
677 |
14138 |
Assert(args.size() == 2); |
678 |
|
uint32_t i; |
679 |
14138 |
if (args[0].getKind() != kind::AND || !getUInt32(args[1], i)) |
680 |
|
{ |
681 |
|
return Node::null(); |
682 |
|
} |
683 |
14138 |
if (i >= args[0].getNumChildren()) |
684 |
|
{ |
685 |
|
return Node::null(); |
686 |
|
} |
687 |
|
return NodeManager::currentNM()->mkNode( |
688 |
14138 |
kind::OR, args[0].notNode(), args[0][i]); |
689 |
|
} |
690 |
66977 |
if (id == PfRule::CNF_AND_NEG) |
691 |
|
{ |
692 |
22294 |
Assert(children.empty()); |
693 |
22294 |
Assert(args.size() == 1); |
694 |
22294 |
if (args[0].getKind() != kind::AND) |
695 |
|
{ |
696 |
|
return Node::null(); |
697 |
|
} |
698 |
44588 |
std::vector<Node> disjuncts{args[0]}; |
699 |
133612 |
for (unsigned i = 0, size = args[0].getNumChildren(); i < size; ++i) |
700 |
|
{ |
701 |
111318 |
disjuncts.push_back(args[0][i].notNode()); |
702 |
|
} |
703 |
22294 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
704 |
|
} |
705 |
44683 |
if (id == PfRule::CNF_OR_POS) |
706 |
|
{ |
707 |
5101 |
Assert(children.empty()); |
708 |
5101 |
Assert(args.size() == 1); |
709 |
5101 |
if (args[0].getKind() != kind::OR) |
710 |
|
{ |
711 |
|
return Node::null(); |
712 |
|
} |
713 |
10202 |
std::vector<Node> disjuncts{args[0].notNode()}; |
714 |
197640 |
for (unsigned i = 0, size = args[0].getNumChildren(); i < size; ++i) |
715 |
|
{ |
716 |
192539 |
disjuncts.push_back(args[0][i]); |
717 |
|
} |
718 |
5101 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
719 |
|
} |
720 |
39582 |
if (id == PfRule::CNF_OR_NEG) |
721 |
|
{ |
722 |
25191 |
Assert(children.empty()); |
723 |
25191 |
Assert(args.size() == 2); |
724 |
|
uint32_t i; |
725 |
25191 |
if (args[0].getKind() != kind::OR || !getUInt32(args[1], i)) |
726 |
|
{ |
727 |
|
return Node::null(); |
728 |
|
} |
729 |
25191 |
if (i >= args[0].getNumChildren()) |
730 |
|
{ |
731 |
|
return Node::null(); |
732 |
|
} |
733 |
|
return NodeManager::currentNM()->mkNode( |
734 |
25191 |
kind::OR, args[0], args[0][i].notNode()); |
735 |
|
} |
736 |
14391 |
if (id == PfRule::CNF_IMPLIES_POS) |
737 |
|
{ |
738 |
449 |
Assert(children.empty()); |
739 |
449 |
Assert(args.size() == 1); |
740 |
449 |
if (args[0].getKind() != kind::IMPLIES) |
741 |
|
{ |
742 |
|
return Node::null(); |
743 |
|
} |
744 |
|
std::vector<Node> disjuncts{ |
745 |
898 |
args[0].notNode(), args[0][0].notNode(), args[0][1]}; |
746 |
449 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
747 |
|
} |
748 |
13942 |
if (id == PfRule::CNF_IMPLIES_NEG1) |
749 |
|
{ |
750 |
122 |
Assert(children.empty()); |
751 |
122 |
Assert(args.size() == 1); |
752 |
122 |
if (args[0].getKind() != kind::IMPLIES) |
753 |
|
{ |
754 |
|
return Node::null(); |
755 |
|
} |
756 |
244 |
std::vector<Node> disjuncts{args[0], args[0][0]}; |
757 |
122 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
758 |
|
} |
759 |
13820 |
if (id == PfRule::CNF_IMPLIES_NEG2) |
760 |
|
{ |
761 |
1139 |
Assert(children.empty()); |
762 |
1139 |
Assert(args.size() == 1); |
763 |
1139 |
if (args[0].getKind() != kind::IMPLIES) |
764 |
|
{ |
765 |
|
return Node::null(); |
766 |
|
} |
767 |
2278 |
std::vector<Node> disjuncts{args[0], args[0][1].notNode()}; |
768 |
1139 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
769 |
|
} |
770 |
12681 |
if (id == PfRule::CNF_EQUIV_POS1) |
771 |
|
{ |
772 |
846 |
Assert(children.empty()); |
773 |
846 |
Assert(args.size() == 1); |
774 |
846 |
if (args[0].getKind() != kind::EQUAL) |
775 |
|
{ |
776 |
|
return Node::null(); |
777 |
|
} |
778 |
|
std::vector<Node> disjuncts{ |
779 |
1692 |
args[0].notNode(), args[0][0].notNode(), args[0][1]}; |
780 |
846 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
781 |
|
} |
782 |
11835 |
if (id == PfRule::CNF_EQUIV_POS2) |
783 |
|
{ |
784 |
821 |
Assert(children.empty()); |
785 |
821 |
Assert(args.size() == 1); |
786 |
821 |
if (args[0].getKind() != kind::EQUAL) |
787 |
|
{ |
788 |
|
return Node::null(); |
789 |
|
} |
790 |
|
std::vector<Node> disjuncts{ |
791 |
1642 |
args[0].notNode(), args[0][0], args[0][1].notNode()}; |
792 |
821 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
793 |
|
} |
794 |
11014 |
if (id == PfRule::CNF_EQUIV_NEG1) |
795 |
|
{ |
796 |
1211 |
Assert(children.empty()); |
797 |
1211 |
Assert(args.size() == 1); |
798 |
1211 |
if (args[0].getKind() != kind::EQUAL) |
799 |
|
{ |
800 |
|
return Node::null(); |
801 |
|
} |
802 |
2422 |
std::vector<Node> disjuncts{args[0], args[0][0], args[0][1]}; |
803 |
1211 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
804 |
|
} |
805 |
9803 |
if (id == PfRule::CNF_EQUIV_NEG2) |
806 |
|
{ |
807 |
2221 |
Assert(children.empty()); |
808 |
2221 |
Assert(args.size() == 1); |
809 |
2221 |
if (args[0].getKind() != kind::EQUAL) |
810 |
|
{ |
811 |
|
return Node::null(); |
812 |
|
} |
813 |
|
std::vector<Node> disjuncts{ |
814 |
4442 |
args[0], args[0][0].notNode(), args[0][1].notNode()}; |
815 |
2221 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
816 |
|
} |
817 |
7582 |
if (id == PfRule::CNF_XOR_POS1) |
818 |
|
{ |
819 |
1427 |
Assert(children.empty()); |
820 |
1427 |
Assert(args.size() == 1); |
821 |
1427 |
if (args[0].getKind() != kind::XOR) |
822 |
|
{ |
823 |
|
return Node::null(); |
824 |
|
} |
825 |
2854 |
std::vector<Node> disjuncts{args[0].notNode(), args[0][0], args[0][1]}; |
826 |
1427 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
827 |
|
} |
828 |
6155 |
if (id == PfRule::CNF_XOR_POS2) |
829 |
|
{ |
830 |
670 |
Assert(children.empty()); |
831 |
670 |
Assert(args.size() == 1); |
832 |
670 |
if (args[0].getKind() != kind::XOR) |
833 |
|
{ |
834 |
|
return Node::null(); |
835 |
|
} |
836 |
|
std::vector<Node> disjuncts{ |
837 |
1340 |
args[0].notNode(), args[0][0].notNode(), args[0][1].notNode()}; |
838 |
670 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
839 |
|
} |
840 |
5485 |
if (id == PfRule::CNF_XOR_NEG1) |
841 |
|
{ |
842 |
313 |
Assert(children.empty()); |
843 |
313 |
Assert(args.size() == 1); |
844 |
313 |
if (args[0].getKind() != kind::XOR) |
845 |
|
{ |
846 |
|
return Node::null(); |
847 |
|
} |
848 |
626 |
std::vector<Node> disjuncts{args[0], args[0][0].notNode(), args[0][1]}; |
849 |
313 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
850 |
|
} |
851 |
5172 |
if (id == PfRule::CNF_XOR_NEG2) |
852 |
|
{ |
853 |
263 |
Assert(children.empty()); |
854 |
263 |
Assert(args.size() == 1); |
855 |
263 |
if (args[0].getKind() != kind::XOR) |
856 |
|
{ |
857 |
|
return Node::null(); |
858 |
|
} |
859 |
526 |
std::vector<Node> disjuncts{args[0], args[0][0], args[0][1].notNode()}; |
860 |
263 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
861 |
|
} |
862 |
4909 |
if (id == PfRule::CNF_ITE_POS1) |
863 |
|
{ |
864 |
487 |
Assert(children.empty()); |
865 |
487 |
Assert(args.size() == 1); |
866 |
487 |
if (args[0].getKind() != kind::ITE) |
867 |
|
{ |
868 |
|
return Node::null(); |
869 |
|
} |
870 |
|
std::vector<Node> disjuncts{ |
871 |
974 |
args[0].notNode(), args[0][0].notNode(), args[0][1]}; |
872 |
487 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
873 |
|
} |
874 |
4422 |
if (id == PfRule::CNF_ITE_POS2) |
875 |
|
{ |
876 |
693 |
Assert(children.empty()); |
877 |
693 |
Assert(args.size() == 1); |
878 |
693 |
if (args[0].getKind() != kind::ITE) |
879 |
|
{ |
880 |
|
return Node::null(); |
881 |
|
} |
882 |
1386 |
std::vector<Node> disjuncts{args[0].notNode(), args[0][0], args[0][2]}; |
883 |
693 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
884 |
|
} |
885 |
3729 |
if (id == PfRule::CNF_ITE_POS3) |
886 |
|
{ |
887 |
236 |
Assert(children.empty()); |
888 |
236 |
Assert(args.size() == 1); |
889 |
236 |
if (args[0].getKind() != kind::ITE) |
890 |
|
{ |
891 |
|
return Node::null(); |
892 |
|
} |
893 |
472 |
std::vector<Node> disjuncts{args[0].notNode(), args[0][1], args[0][2]}; |
894 |
236 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
895 |
|
} |
896 |
3493 |
if (id == PfRule::CNF_ITE_NEG1) |
897 |
|
{ |
898 |
1508 |
Assert(children.empty()); |
899 |
1508 |
Assert(args.size() == 1); |
900 |
1508 |
if (args[0].getKind() != kind::ITE) |
901 |
|
{ |
902 |
|
return Node::null(); |
903 |
|
} |
904 |
|
std::vector<Node> disjuncts{ |
905 |
3016 |
args[0], args[0][0].notNode(), args[0][1].notNode()}; |
906 |
1508 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
907 |
|
} |
908 |
1985 |
if (id == PfRule::CNF_ITE_NEG2) |
909 |
|
{ |
910 |
483 |
Assert(children.empty()); |
911 |
483 |
Assert(args.size() == 1); |
912 |
483 |
if (args[0].getKind() != kind::ITE) |
913 |
|
{ |
914 |
|
return Node::null(); |
915 |
|
} |
916 |
966 |
std::vector<Node> disjuncts{args[0], args[0][0], args[0][2].notNode()}; |
917 |
483 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
918 |
|
} |
919 |
1502 |
if (id == PfRule::CNF_ITE_NEG3) |
920 |
|
{ |
921 |
92 |
Assert(children.empty()); |
922 |
92 |
Assert(args.size() == 1); |
923 |
92 |
if (args[0].getKind() != kind::ITE) |
924 |
|
{ |
925 |
|
return Node::null(); |
926 |
|
} |
927 |
|
std::vector<Node> disjuncts{ |
928 |
184 |
args[0], args[0][1].notNode(), args[0][2].notNode()}; |
929 |
92 |
return NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
930 |
|
} |
931 |
1410 |
if (id == PfRule::SAT_REFUTATION) |
932 |
|
{ |
933 |
1410 |
Assert(args.empty()); |
934 |
1410 |
return NodeManager::currentNM()->mkConst(false); |
935 |
|
} |
936 |
|
// no rule |
937 |
|
return Node::null(); |
938 |
|
} |
939 |
|
|
940 |
|
} // namespace booleans |
941 |
|
} // namespace theory |
942 |
31137 |
} // namespace cvc5 |