Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Implementation of equality proof checker.
11 : : */
12 : :
13 : : #include "theory/booleans/proof_checker.h"
14 : : #include "expr/skolem_manager.h"
15 : : #include "theory/rewriter.h"
16 : :
17 : : namespace cvc5::internal {
18 : : namespace theory {
19 : : namespace booleans {
20 : :
21 : 49917 : BoolProofRuleChecker::BoolProofRuleChecker(NodeManager* nm)
22 : 49917 : : ProofRuleChecker(nm)
23 : : {
24 : 49917 : }
25 : :
26 : 18895 : void BoolProofRuleChecker::registerTo(ProofChecker* pc)
27 : : {
28 : 18895 : pc->registerChecker(ProofRule::SPLIT, this);
29 : 18895 : pc->registerChecker(ProofRule::RESOLUTION, this);
30 : 18895 : pc->registerChecker(ProofRule::CHAIN_RESOLUTION, this);
31 : 18895 : pc->registerChecker(ProofRule::CHAIN_M_RESOLUTION, this);
32 : 18895 : pc->registerChecker(ProofRule::FACTORING, this);
33 : 18895 : pc->registerChecker(ProofRule::REORDERING, this);
34 : 18895 : pc->registerChecker(ProofRule::EQ_RESOLVE, this);
35 : 18895 : pc->registerChecker(ProofRule::MODUS_PONENS, this);
36 : 18895 : pc->registerChecker(ProofRule::NOT_NOT_ELIM, this);
37 : 18895 : pc->registerChecker(ProofRule::CONTRA, this);
38 : 18895 : pc->registerChecker(ProofRule::AND_ELIM, this);
39 : 18895 : pc->registerChecker(ProofRule::AND_INTRO, this);
40 : 18895 : pc->registerChecker(ProofRule::NOT_OR_ELIM, this);
41 : 18895 : pc->registerChecker(ProofRule::IMPLIES_ELIM, this);
42 : 18895 : pc->registerChecker(ProofRule::NOT_IMPLIES_ELIM1, this);
43 : 18895 : pc->registerChecker(ProofRule::NOT_IMPLIES_ELIM2, this);
44 : 18895 : pc->registerChecker(ProofRule::EQUIV_ELIM1, this);
45 : 18895 : pc->registerChecker(ProofRule::EQUIV_ELIM2, this);
46 : 18895 : pc->registerChecker(ProofRule::NOT_EQUIV_ELIM1, this);
47 : 18895 : pc->registerChecker(ProofRule::NOT_EQUIV_ELIM2, this);
48 : 18895 : pc->registerChecker(ProofRule::XOR_ELIM1, this);
49 : 18895 : pc->registerChecker(ProofRule::XOR_ELIM2, this);
50 : 18895 : pc->registerChecker(ProofRule::NOT_XOR_ELIM1, this);
51 : 18895 : pc->registerChecker(ProofRule::NOT_XOR_ELIM2, this);
52 : 18895 : pc->registerChecker(ProofRule::ITE_ELIM1, this);
53 : 18895 : pc->registerChecker(ProofRule::ITE_ELIM2, this);
54 : 18895 : pc->registerChecker(ProofRule::NOT_ITE_ELIM1, this);
55 : 18895 : pc->registerChecker(ProofRule::NOT_ITE_ELIM2, this);
56 : 18895 : pc->registerChecker(ProofRule::NOT_AND, this);
57 : 18895 : pc->registerChecker(ProofRule::CNF_AND_POS, this);
58 : 18895 : pc->registerChecker(ProofRule::CNF_AND_NEG, this);
59 : 18895 : pc->registerChecker(ProofRule::CNF_OR_POS, this);
60 : 18895 : pc->registerChecker(ProofRule::CNF_OR_NEG, this);
61 : 18895 : pc->registerChecker(ProofRule::CNF_IMPLIES_POS, this);
62 : 18895 : pc->registerChecker(ProofRule::CNF_IMPLIES_NEG1, this);
63 : 18895 : pc->registerChecker(ProofRule::CNF_IMPLIES_NEG2, this);
64 : 18895 : pc->registerChecker(ProofRule::CNF_EQUIV_POS1, this);
65 : 18895 : pc->registerChecker(ProofRule::CNF_EQUIV_POS2, this);
66 : 18895 : pc->registerChecker(ProofRule::CNF_EQUIV_NEG1, this);
67 : 18895 : pc->registerChecker(ProofRule::CNF_EQUIV_NEG2, this);
68 : 18895 : pc->registerChecker(ProofRule::CNF_XOR_POS1, this);
69 : 18895 : pc->registerChecker(ProofRule::CNF_XOR_POS2, this);
70 : 18895 : pc->registerChecker(ProofRule::CNF_XOR_NEG1, this);
71 : 18895 : pc->registerChecker(ProofRule::CNF_XOR_NEG2, this);
72 : 18895 : pc->registerChecker(ProofRule::CNF_ITE_POS1, this);
73 : 18895 : pc->registerChecker(ProofRule::CNF_ITE_POS2, this);
74 : 18895 : pc->registerChecker(ProofRule::CNF_ITE_POS3, this);
75 : 18895 : pc->registerChecker(ProofRule::CNF_ITE_NEG1, this);
76 : 18895 : pc->registerChecker(ProofRule::CNF_ITE_NEG2, this);
77 : 18895 : pc->registerChecker(ProofRule::CNF_ITE_NEG3, this);
78 : 18895 : pc->registerTrustedChecker(ProofRule::SAT_REFUTATION, this, 1);
79 : 18895 : pc->registerTrustedChecker(ProofRule::DRAT_REFUTATION, this, 1);
80 : 18895 : pc->registerTrustedChecker(ProofRule::SAT_EXTERNAL_PROVE, this, 1);
81 : 18895 : }
82 : :
83 : 4465809 : Node BoolProofRuleChecker::checkInternal(ProofRule id,
84 : : const std::vector<Node>& children,
85 : : const std::vector<Node>& args)
86 : : {
87 [ + + ]: 4465809 : if (id == ProofRule::RESOLUTION)
88 : : {
89 [ - + ][ - + ]: 770383 : Assert(children.size() == 2);
[ - - ]
90 [ - + ][ - + ]: 770383 : Assert(args.size() == 2);
[ - - ]
91 : 770383 : NodeManager* nm = nodeManager();
92 : 770383 : std::vector<Node> disjuncts;
93 [ + + ]: 3851915 : Node pivots[2];
94 [ + + ]: 770383 : if (args[0] == nm->mkConst(true))
95 : : {
96 : 394019 : pivots[0] = args[1];
97 : 394019 : pivots[1] = args[1].notNode();
98 : : }
99 : : else
100 : : {
101 [ - + ][ - + ]: 376364 : Assert(args[0] == nm->mkConst(false));
[ - - ]
102 : 376364 : pivots[0] = args[1].notNode();
103 : 376364 : pivots[1] = args[1];
104 : : }
105 [ + + ]: 2311149 : for (unsigned i = 0; i < 2; ++i)
106 : : {
107 : : // determine whether the clause is a singleton for effects of resolution,
108 : : // which is the case if it's not an OR node or it is an OR node but it is
109 : : // equal to the pivot
110 : 1540766 : std::vector<Node> lits;
111 [ + + ][ + + ]: 1540766 : if (children[i].getKind() == Kind::OR && pivots[i] != children[i])
[ + + ]
112 : : {
113 : 1244128 : lits.insert(lits.end(), children[i].begin(), children[i].end());
114 : : }
115 : : else
116 : : {
117 : 296638 : lits.push_back(children[i]);
118 : : }
119 [ + + ]: 15066389 : for (unsigned j = 0, size = lits.size(); j < size; ++j)
120 : : {
121 [ + + ]: 13525623 : if (pivots[i] != lits[j])
122 : : {
123 : 11984857 : disjuncts.push_back(lits[j]);
124 : : }
125 : : else
126 : : {
127 : : // just eliminate first occurrence
128 : 1540766 : pivots[i] = Node::null();
129 : : }
130 : : }
131 : 1540766 : }
132 : 1540766 : return disjuncts.empty() ? nm->mkConst(false)
133 : 862311 : : disjuncts.size() == 1 ? disjuncts[0]
134 [ + + ][ + + ]: 1632694 : : nm->mkNode(Kind::OR, disjuncts);
135 [ + + ][ - - ]: 3081532 : }
136 [ + + ]: 3695426 : if (id == ProofRule::FACTORING)
137 : : {
138 [ - + ][ - + ]: 313398 : Assert(children.size() == 1);
[ - - ]
139 [ - + ][ - + ]: 313398 : Assert(args.empty());
[ - - ]
140 [ - + ]: 313398 : if (children[0].getKind() != Kind::OR)
141 : : {
142 : 0 : return Node::null();
143 : : }
144 : : // remove duplicates while keeping the order of children
145 : 313398 : std::unordered_set<TNode> clauseSet;
146 : 313398 : std::vector<Node> disjuncts;
147 : 313398 : unsigned size = children[0].getNumChildren();
148 [ + + ]: 8038359 : for (unsigned i = 0; i < size; ++i)
149 : : {
150 [ + + ]: 7724961 : if (clauseSet.count(children[0][i]))
151 : : {
152 : 2541992 : continue;
153 : : }
154 : 5182969 : disjuncts.push_back(children[0][i]);
155 : 5182969 : clauseSet.insert(children[0][i]);
156 : : }
157 [ - + ]: 313398 : if (disjuncts.size() == size)
158 : : {
159 : 0 : return Node::null();
160 : : }
161 : 313398 : NodeManager* nm = nodeManager();
162 : 313398 : return nm->mkOr(disjuncts);
163 : 313398 : }
164 [ + + ]: 3382028 : if (id == ProofRule::REORDERING)
165 : : {
166 [ - + ][ - + ]: 1032085 : Assert(children.size() == 1);
[ - - ]
167 [ - + ][ - + ]: 1032085 : Assert(args.size() == 1);
[ - - ]
168 : 1032085 : std::unordered_set<Node> clauseSet1, clauseSet2;
169 [ + - ]: 1032085 : if (children[0].getKind() == Kind::OR)
170 : : {
171 : 1032085 : clauseSet1.insert(children[0].begin(), children[0].end());
172 : : }
173 : : else
174 : : {
175 : 0 : clauseSet1.insert(children[0]);
176 : : }
177 [ + - ]: 1032085 : if (args[0].getKind() == Kind::OR)
178 : : {
179 : 1032085 : clauseSet2.insert(args[0].begin(), args[0].end());
180 : : }
181 : : else
182 : : {
183 : 0 : clauseSet2.insert(args[0]);
184 : : }
185 [ - + ]: 1032085 : if (clauseSet1 != clauseSet2)
186 : : {
187 [ - - ]: 0 : Trace("bool-pfcheck") << id << ": clause set1: " << clauseSet1 << "\n"
188 : 0 : << id << ": clause set2: " << clauseSet2 << "\n";
189 : 0 : return Node::null();
190 : : }
191 : 1032085 : return args[0];
192 : 1032085 : }
193 [ + + ]: 2349943 : if (id == ProofRule::CHAIN_RESOLUTION)
194 : : {
195 [ - + ][ - + ]: 334806 : Assert(children.size() > 1);
[ - - ]
196 [ - + ][ - + ]: 334806 : Assert(args.size() == 2);
[ - - ]
197 [ - + ][ - + ]: 334806 : Assert(args[0].getNumChildren() == (children.size() - 1));
[ - - ]
198 [ - + ][ - + ]: 334806 : Assert(args[1].getNumChildren() == (children.size() - 1));
[ - - ]
199 [ + - ]: 334806 : Trace("bool-pfcheck") << "chain_res:\n" << push;
200 : 334806 : NodeManager* nm = nodeManager();
201 : 334806 : Node trueNode = nm->mkConst(true);
202 : 334806 : Node falseNode = nm->mkConst(false);
203 : : // The lhs and rhs clauses in a binary resolution step, respectively. Since
204 : : // children correspond to the premises in the resolution chain, the first
205 : : // lhs clause is the first premise, the first rhs clause is the second
206 : : // premise. Each subsequent lhs clause will be the result of the previous
207 : : // binary resolution step in the chain, while each subsequent rhs clause
208 : : // will be respectively the second, third etc premises.
209 : 334806 : std::vector<Node> lhsClause, rhsClause;
210 : : // The pivots to be eliminated to the lhs clause and rhs clause in a binary
211 : : // resolution step, respectively
212 : 334806 : Node lhsElim, rhsElim;
213 : : // Get lhsClause of first resolution.
214 : : //
215 : : // Since a Node cannot hold an OR with a single child we need to
216 : : // disambiguate singleton clauses that are OR nodes from non-singleton
217 : : // clauses (i.e. unit clauses in the SAT solver).
218 : : //
219 : : // If the child is not an OR, it is a singleton clause and we take the
220 : : // child itself as the clause. Otherwise the child can only be a singleton
221 : : // clause if the child itself is used as a resolution literal, i.e. if the
222 : : // first child equal to the first pivot (which is args[1][0] or
223 : : // args[1][0].notNode() depending on the polarity).
224 : 334806 : Node pols = args[0];
225 : 334806 : Node lits = args[1];
226 : 334806 : if (children[0].getKind() != Kind::OR
227 : 669349 : || (pols[0] == trueNode && children[0] == lits[0])
228 : 1004155 : || (pols[0] == falseNode && children[0] == lits[0].notNode()))
229 : : {
230 : 263 : lhsClause.push_back(children[0]);
231 : : }
232 : : else
233 : : {
234 : 334543 : lhsClause.insert(lhsClause.end(), children[0].begin(), children[0].end());
235 : : }
236 : : // Traverse the links, which amounts to for each pair of args removing a
237 : : // literal from the lhs and a literal from the lhs.
238 [ + + ]: 3042264 : for (size_t i = 0, argsSize = pols.getNumChildren(); i < argsSize; i++)
239 : : {
240 : : // Polarity determines how the pivot occurs in lhs and rhs
241 [ + + ]: 2707458 : if (pols[i] == trueNode)
242 : : {
243 : 955839 : lhsElim = lits[i];
244 : 955839 : rhsElim = lits[i].notNode();
245 : : }
246 : : else
247 : : {
248 [ - + ][ - + ]: 1751619 : Assert(pols[i] == falseNode);
[ - - ]
249 : 1751619 : lhsElim = lits[i].notNode();
250 : 1751619 : rhsElim = lits[i];
251 : : }
252 : : // The index of the child corresponding to the current rhs clause
253 : 2707458 : size_t childIndex = i + 1;
254 : : // Get rhs clause. It's a singleton if not an OR node or if equal to
255 : : // rhsElim
256 : 2707458 : if (children[childIndex].getKind() != Kind::OR
257 [ + + ][ + + ]: 2707458 : || children[childIndex] == rhsElim)
[ + + ]
258 : : {
259 : 1531444 : rhsClause.push_back(children[childIndex]);
260 : : }
261 : : else
262 : : {
263 : 1176014 : rhsClause = {children[childIndex].begin(), children[childIndex].end()};
264 : : }
265 [ + - ]: 2707458 : Trace("bool-pfcheck") << i << "-th res link:\n";
266 [ + - ]: 2707458 : Trace("bool-pfcheck") << "\t - lhsClause: " << lhsClause << "\n";
267 [ + - ]: 2707458 : Trace("bool-pfcheck") << "\t\t - lhsElim: " << lhsElim << "\n";
268 [ + - ]: 2707458 : Trace("bool-pfcheck") << "\t - rhsClause: " << rhsClause << "\n";
269 [ + - ]: 2707458 : Trace("bool-pfcheck") << "\t\t - rhsElim: " << rhsElim << "\n";
270 : : // Compute the resulting clause, which will be the next lhsClause, as
271 : : // follows:
272 : : // - remove lhsElim from lhsClause
273 : : // - remove rhsElim from rhsClause and add the lits to lhsClause
274 : 2707458 : auto itlhs = std::find(lhsClause.begin(), lhsClause.end(), lhsElim);
275 [ - + ][ - + ]: 2707458 : AlwaysAssert(itlhs != lhsClause.end());
[ - - ]
276 : 2707458 : lhsClause.erase(itlhs);
277 [ + - ]: 2707458 : Trace("bool-pfcheck") << "\t.. after lhsClause: " << lhsClause << "\n";
278 : 2707458 : auto itrhs = std::find(rhsClause.begin(), rhsClause.end(), rhsElim);
279 [ - + ][ - + ]: 2707458 : AlwaysAssert(itrhs != rhsClause.end());
[ - - ]
280 : 2707458 : lhsClause.insert(lhsClause.end(), rhsClause.begin(), itrhs);
281 : 2707458 : lhsClause.insert(lhsClause.end(), itrhs + 1, rhsClause.end());
282 [ - + ]: 2707458 : if (TraceIsOn("bool-pfcheck"))
283 : : {
284 : 0 : std::vector<Node> updatedRhsClause{rhsClause.begin(), itrhs};
285 : 0 : updatedRhsClause.insert(
286 : 0 : updatedRhsClause.end(), itrhs + 1, rhsClause.end());
287 [ - - ]: 0 : Trace("bool-pfcheck")
288 : 0 : << "\t.. after rhsClause: " << updatedRhsClause << "\n";
289 : 0 : }
290 : 2707458 : rhsClause.clear();
291 : : }
292 [ + - ]: 669612 : Trace("bool-pfcheck") << "\n resulting clause: " << lhsClause << "\n"
293 : 334806 : << pop;
294 : 334806 : return nm->mkOr(lhsClause);
295 : 334806 : }
296 [ + + ]: 2015137 : if (id == ProofRule::CHAIN_M_RESOLUTION)
297 : : {
298 [ - + ][ - + ]: 304602 : Assert(children.size() > 1);
[ - - ]
299 [ + - ]: 304602 : Trace("bool-pfcheck") << "macro_res: " << args[0] << "\n" << push;
300 : 304602 : NodeManager* nm = nodeManager();
301 : 304602 : Node trueNode = nm->mkConst(true);
302 : 304602 : Node falseNode = nm->mkConst(false);
303 : 304602 : std::vector<Node> lhsClause, rhsClause;
304 : 304602 : Node lhsElim, rhsElim;
305 : 304602 : std::vector<Node> pols, lits;
306 [ - + ][ - + ]: 304602 : Assert(args.size() == 3);
[ - - ]
307 : 304602 : pols.insert(pols.end(), args[1].begin(), args[1].end());
308 : 304602 : lits.insert(lits.end(), args[2].begin(), args[2].end());
309 [ - + ]: 304602 : if (pols.size() != lits.size())
310 : : {
311 : 0 : return Node::null();
312 : : }
313 : 304602 : if (children[0].getKind() != Kind::OR
314 [ + + ][ + - ]: 304383 : || (pols[0] == trueNode && children[0] == lits[0])
315 [ + + ][ + + ]: 913587 : || (pols[0] == falseNode && children[0] == lits[0].notNode()))
[ - + ][ + + ]
[ + + ][ - - ]
316 : : {
317 : 219 : lhsClause.push_back(children[0]);
318 : : }
319 : : else
320 : : {
321 : 304383 : lhsClause.insert(lhsClause.end(), children[0].begin(), children[0].end());
322 : : }
323 : : // Traverse the links, which amounts to for each pair of args removing a
324 : : // literal from the lhs and a literal from the lhs.
325 [ + + ]: 5772659 : for (size_t i = 0, argsSize = pols.size(); i < argsSize; i++)
326 : : {
327 : : // Polarity determines how the pivot occurs in lhs and rhs
328 [ + + ]: 5468057 : if (pols[i] == trueNode)
329 : : {
330 : 3320245 : lhsElim = lits[i];
331 : 3320245 : rhsElim = lits[i].notNode();
332 : : }
333 : : else
334 : : {
335 [ - + ][ - + ]: 2147812 : Assert(pols[i] == falseNode);
[ - - ]
336 : 2147812 : lhsElim = lits[i].notNode();
337 : 2147812 : rhsElim = lits[i];
338 : : }
339 : : // The index of the child corresponding to the current rhs clause
340 : 5468057 : size_t childIndex = i + 1;
341 : : // Get rhs clause. It's a singleton if not an OR node or if equal to
342 : : // rhsElim
343 : 5468057 : if (children[childIndex].getKind() != Kind::OR
344 [ + + ][ + + ]: 5468057 : || children[childIndex] == rhsElim)
[ + + ]
345 : : {
346 : 675100 : rhsClause.push_back(children[childIndex]);
347 : : }
348 : : else
349 : : {
350 : 4792957 : rhsClause = {children[childIndex].begin(), children[childIndex].end()};
351 : : }
352 [ + - ]: 5468057 : Trace("bool-pfcheck") << i << "-th res link:\n";
353 [ + - ]: 5468057 : Trace("bool-pfcheck") << "\t - lhsClause: " << lhsClause << "\n";
354 [ + - ]: 5468057 : Trace("bool-pfcheck") << "\t\t - lhsElim: " << lhsElim << "\n";
355 [ + - ]: 5468057 : Trace("bool-pfcheck") << "\t - rhsClause: " << rhsClause << "\n";
356 [ + - ]: 5468057 : Trace("bool-pfcheck") << "\t\t - rhsElim: " << rhsElim << "\n";
357 : : // Compute the resulting clause, which will be the next lhsClause, as
358 : : // follows:
359 : : // - remove all lhsElim from lhsClause
360 : : // - remove all rhsElim from rhsClause and add the lits to lhsClause
361 : : //
362 : : // Note that to remove the elements from lhsClaus we use the
363 : : // "erase-remove" idiom in C++: the std::remove call shuffles the elements
364 : : // different from lhsElim to the beginning of the container, returning an
365 : : // iterator to the beginning of the "rest" of the container (with
366 : : // occurrences of lhsElim). Then the call to erase removes the range from
367 : : // there to the end. Once C++ 20 is allowed in the cvc5 code base, this
368 : : // could be done with a single call to std::erase.
369 : 5468057 : lhsClause.erase(std::remove(lhsClause.begin(), lhsClause.end(), lhsElim),
370 : 5468057 : lhsClause.end());
371 [ + + ]: 24949943 : for (const Node& l : rhsClause)
372 : : {
373 : : // only add if literal does not occur in elimination set
374 [ + + ]: 19481886 : if (rhsElim != l)
375 : : {
376 : 14013829 : lhsClause.push_back(l);
377 : : }
378 : : }
379 : 5468057 : rhsClause.clear();
380 : : }
381 : :
382 [ + - ]: 304602 : Trace("bool-pfcheck") << "clause: " << lhsClause << "\n";
383 : : // check that set representation is the same as of the given conclusion
384 : 304602 : std::unordered_set<Node> clauseComputed{lhsClause.begin(), lhsClause.end()};
385 [ + - ]: 304602 : Trace("bool-pfcheck") << "clauseSet: " << clauseComputed << "\n" << pop;
386 [ + + ]: 304602 : if (clauseComputed.empty())
387 : : {
388 : : // conclusion differ
389 [ - + ]: 1876 : if (args[0] != falseNode)
390 : : {
391 : 0 : return Node::null();
392 : : }
393 : 1876 : return args[0];
394 : : }
395 [ + + ]: 302726 : if (clauseComputed.size() == 1)
396 : : {
397 : : // conclusion differ
398 [ - + ]: 86042 : if (args[0] != *clauseComputed.begin())
399 : : {
400 : 0 : return Node::null();
401 : : }
402 : 86042 : return args[0];
403 : : }
404 : : // At this point, should amount to them differing only on order or in
405 : : // repetitions. So the original result can't be a singleton clause.
406 [ - + ]: 216684 : if (args[0].getKind() != Kind::OR)
407 : : {
408 : 0 : return Node::null();
409 : : }
410 : 216684 : std::unordered_set<Node> clauseGiven{args[0].begin(), args[0].end()};
411 [ + - ]: 216684 : return clauseComputed == clauseGiven ? args[0] : Node::null();
412 : 304602 : }
413 [ + + ]: 1710535 : if (id == ProofRule::SPLIT)
414 : : {
415 [ - + ][ - + ]: 38952 : Assert(children.empty());
[ - - ]
416 [ - + ][ - + ]: 38952 : Assert(args.size() == 1);
[ - - ]
417 : 38952 : return nodeManager()->mkNode(Kind::OR, args[0], args[0].notNode());
418 : : }
419 [ + + ]: 1671583 : if (id == ProofRule::CONTRA)
420 : : {
421 [ - + ][ - + ]: 66555 : Assert(children.size() == 2);
[ - - ]
422 [ + - ][ + - ]: 66555 : if (children[1].getKind() == Kind::NOT && children[0] == children[1][0])
[ + - ][ + - ]
[ - - ]
423 : : {
424 : 133110 : return nodeManager()->mkConst(false);
425 : : }
426 : 0 : return Node::null();
427 : : }
428 [ + + ]: 1605028 : if (id == ProofRule::EQ_RESOLVE)
429 : : {
430 [ - + ][ - + ]: 417385 : Assert(children.size() == 2);
[ - - ]
431 [ - + ][ - + ]: 417385 : Assert(args.empty());
[ - - ]
432 [ + - ][ - + ]: 417385 : if (children[1].getKind() != Kind::EQUAL || children[0] != children[1][0])
[ + - ][ - + ]
[ - - ]
433 : : {
434 : 0 : return Node::null();
435 : : }
436 : 417385 : return children[1][1];
437 : : }
438 [ + + ]: 1187643 : if (id == ProofRule::MODUS_PONENS)
439 : : {
440 [ - + ][ - + ]: 233163 : Assert(children.size() == 2);
[ - - ]
441 [ - + ][ - + ]: 233163 : Assert(args.empty());
[ - - ]
442 [ + - ][ - + ]: 233163 : if (children[1].getKind() != Kind::IMPLIES || children[0] != children[1][0])
[ + - ][ - + ]
[ - - ]
443 : : {
444 : 0 : return Node::null();
445 : : }
446 : 233163 : return children[1][1];
447 : : }
448 [ + + ]: 954480 : if (id == ProofRule::NOT_NOT_ELIM)
449 : : {
450 [ - + ][ - + ]: 5630 : Assert(children.size() == 1);
[ - - ]
451 [ - + ][ - + ]: 5630 : Assert(args.empty());
[ - - ]
452 : 5630 : if (children[0].getKind() != Kind::NOT
453 [ + - ][ - + ]: 11260 : || children[0][0].getKind() != Kind::NOT)
[ + - ][ - + ]
[ - - ]
454 : : {
455 : 0 : return Node::null();
456 : : }
457 : 5630 : return children[0][0][0];
458 : : }
459 : : // natural deduction rules
460 [ + + ]: 948850 : if (id == ProofRule::AND_ELIM)
461 : : {
462 [ - + ][ - + ]: 189531 : Assert(children.size() == 1);
[ - - ]
463 [ - + ][ - + ]: 189531 : Assert(args.size() == 1);
[ - - ]
464 : : uint32_t i;
465 [ + - ][ - + ]: 189531 : if (children[0].getKind() != Kind::AND || !getUInt32(args[0], i))
[ + - ][ - + ]
[ - - ]
466 : : {
467 : 0 : return Node::null();
468 : : }
469 [ - + ]: 189531 : if (i >= children[0].getNumChildren())
470 : : {
471 : 0 : return Node::null();
472 : : }
473 : 189531 : return children[0][i];
474 : : }
475 [ + + ]: 759319 : if (id == ProofRule::AND_INTRO)
476 : : {
477 [ - + ][ - + ]: 254467 : Assert(children.size() >= 1);
[ - - ]
478 : 254467 : return children.size() == 1 ? children[0]
479 [ - + ]: 254467 : : nodeManager()->mkNode(Kind::AND, children);
480 : : }
481 [ + + ]: 504852 : if (id == ProofRule::NOT_OR_ELIM)
482 : : {
483 [ - + ][ - + ]: 7338 : Assert(children.size() == 1);
[ - - ]
484 [ - + ][ - + ]: 7338 : Assert(args.size() == 1);
[ - - ]
485 : : uint32_t i;
486 : 7338 : if (children[0].getKind() != Kind::NOT
487 : 14676 : || children[0][0].getKind() != Kind::OR || !getUInt32(args[0], i))
488 : : {
489 : 0 : return Node::null();
490 : : }
491 [ - + ]: 7338 : if (i >= children[0][0].getNumChildren())
492 : : {
493 : 0 : return Node::null();
494 : : }
495 : 7338 : return children[0][0][i].notNode();
496 : : }
497 [ + + ]: 497514 : if (id == ProofRule::IMPLIES_ELIM)
498 : : {
499 [ - + ][ - + ]: 64695 : Assert(children.size() == 1);
[ - - ]
500 [ - + ][ - + ]: 64695 : Assert(args.empty());
[ - - ]
501 [ - + ]: 64695 : if (children[0].getKind() != Kind::IMPLIES)
502 : : {
503 : 0 : return Node::null();
504 : : }
505 : 64695 : return nodeManager()->mkNode(
506 : 64695 : Kind::OR, children[0][0].notNode(), children[0][1]);
507 : : }
508 [ + + ]: 432819 : if (id == ProofRule::NOT_IMPLIES_ELIM1)
509 : : {
510 [ - + ][ - + ]: 4041 : Assert(children.size() == 1);
[ - - ]
511 [ - + ][ - + ]: 4041 : Assert(args.empty());
[ - - ]
512 : 4041 : if (children[0].getKind() != Kind::NOT
513 [ + - ][ - + ]: 8082 : || children[0][0].getKind() != Kind::IMPLIES)
[ + - ][ - + ]
[ - - ]
514 : : {
515 : 0 : return Node::null();
516 : : }
517 : 4041 : return children[0][0][0];
518 : : }
519 [ + + ]: 428778 : if (id == ProofRule::NOT_IMPLIES_ELIM2)
520 : : {
521 [ - + ][ - + ]: 1853 : Assert(children.size() == 1);
[ - - ]
522 [ - + ][ - + ]: 1853 : Assert(args.empty());
[ - - ]
523 : 1853 : if (children[0].getKind() != Kind::NOT
524 [ + - ][ - + ]: 3706 : || children[0][0].getKind() != Kind::IMPLIES)
[ + - ][ - + ]
[ - - ]
525 : : {
526 : 0 : return Node::null();
527 : : }
528 : 1853 : return children[0][0][1].notNode();
529 : : }
530 [ + + ]: 426925 : if (id == ProofRule::EQUIV_ELIM1)
531 : : {
532 [ - + ][ - + ]: 16330 : Assert(children.size() == 1);
[ - - ]
533 [ - + ][ - + ]: 16330 : Assert(args.empty());
[ - - ]
534 [ - + ]: 16330 : if (children[0].getKind() != Kind::EQUAL)
535 : : {
536 : 0 : return Node::null();
537 : : }
538 : 16330 : return nodeManager()->mkNode(
539 : 16330 : Kind::OR, children[0][0].notNode(), children[0][1]);
540 : : }
541 [ + + ]: 410595 : if (id == ProofRule::EQUIV_ELIM2)
542 : : {
543 [ - + ][ - + ]: 9476 : Assert(children.size() == 1);
[ - - ]
544 [ - + ][ - + ]: 9476 : Assert(args.empty());
[ - - ]
545 [ - + ]: 9476 : if (children[0].getKind() != Kind::EQUAL)
546 : : {
547 : 0 : return Node::null();
548 : : }
549 : 9476 : return nodeManager()->mkNode(
550 : 9476 : Kind::OR, children[0][0], children[0][1].notNode());
551 : : }
552 [ + + ]: 401119 : if (id == ProofRule::NOT_EQUIV_ELIM1)
553 : : {
554 [ - + ][ - + ]: 641 : Assert(children.size() == 1);
[ - - ]
555 [ - + ][ - + ]: 641 : Assert(args.empty());
[ - - ]
556 : 641 : if (children[0].getKind() != Kind::NOT
557 [ + - ][ - + ]: 1282 : || children[0][0].getKind() != Kind::EQUAL)
[ + - ][ - + ]
[ - - ]
558 : : {
559 : 0 : return Node::null();
560 : : }
561 : 641 : return nodeManager()->mkNode(
562 : 641 : Kind::OR, children[0][0][0], children[0][0][1]);
563 : : }
564 [ + + ]: 400478 : if (id == ProofRule::NOT_EQUIV_ELIM2)
565 : : {
566 [ - + ][ - + ]: 402 : Assert(children.size() == 1);
[ - - ]
567 [ - + ][ - + ]: 402 : Assert(args.empty());
[ - - ]
568 : 402 : if (children[0].getKind() != Kind::NOT
569 [ + - ][ - + ]: 804 : || children[0][0].getKind() != Kind::EQUAL)
[ + - ][ - + ]
[ - - ]
570 : : {
571 : 0 : return Node::null();
572 : : }
573 : 402 : return nodeManager()->mkNode(
574 : 402 : Kind::OR, children[0][0][0].notNode(), children[0][0][1].notNode());
575 : : }
576 [ + + ]: 400076 : if (id == ProofRule::XOR_ELIM1)
577 : : {
578 [ - + ][ - + ]: 84 : Assert(children.size() == 1);
[ - - ]
579 [ - + ][ - + ]: 84 : Assert(args.empty());
[ - - ]
580 [ - + ]: 84 : if (children[0].getKind() != Kind::XOR)
581 : : {
582 : 0 : return Node::null();
583 : : }
584 : 84 : return nodeManager()->mkNode(Kind::OR, children[0][0], children[0][1]);
585 : : }
586 [ + + ]: 399992 : if (id == ProofRule::XOR_ELIM2)
587 : : {
588 [ - + ][ - + ]: 102 : Assert(children.size() == 1);
[ - - ]
589 [ - + ][ - + ]: 102 : Assert(args.empty());
[ - - ]
590 [ - + ]: 102 : if (children[0].getKind() != Kind::XOR)
591 : : {
592 : 0 : return Node::null();
593 : : }
594 : 102 : return nodeManager()->mkNode(
595 : 102 : Kind::OR, children[0][0].notNode(), children[0][1].notNode());
596 : : }
597 [ + + ]: 399890 : if (id == ProofRule::NOT_XOR_ELIM1)
598 : : {
599 [ - + ][ - + ]: 63 : Assert(children.size() == 1);
[ - - ]
600 [ - + ][ - + ]: 63 : Assert(args.empty());
[ - - ]
601 : 63 : if (children[0].getKind() != Kind::NOT
602 [ + - ][ - + ]: 126 : || children[0][0].getKind() != Kind::XOR)
[ + - ][ - + ]
[ - - ]
603 : : {
604 : 0 : return Node::null();
605 : : }
606 : 63 : return nodeManager()->mkNode(
607 : 63 : Kind::OR, children[0][0][0], children[0][0][1].notNode());
608 : : }
609 [ + + ]: 399827 : if (id == ProofRule::NOT_XOR_ELIM2)
610 : : {
611 [ - + ][ - + ]: 71 : Assert(children.size() == 1);
[ - - ]
612 [ - + ][ - + ]: 71 : Assert(args.empty());
[ - - ]
613 : 71 : if (children[0].getKind() != Kind::NOT
614 [ + - ][ - + ]: 142 : || children[0][0].getKind() != Kind::XOR)
[ + - ][ - + ]
[ - - ]
615 : : {
616 : 0 : return Node::null();
617 : : }
618 : 71 : return nodeManager()->mkNode(
619 : 71 : Kind::OR, children[0][0][0].notNode(), children[0][0][1]);
620 : : }
621 [ + + ]: 399756 : if (id == ProofRule::ITE_ELIM1)
622 : : {
623 [ - + ][ - + ]: 4912 : Assert(children.size() == 1);
[ - - ]
624 [ - + ][ - + ]: 4912 : Assert(args.empty());
[ - - ]
625 [ - + ]: 4912 : if (children[0].getKind() != Kind::ITE)
626 : : {
627 : 0 : return Node::null();
628 : : }
629 : 4912 : return nodeManager()->mkNode(
630 : 4912 : Kind::OR, children[0][0].notNode(), children[0][1]);
631 : : }
632 [ + + ]: 394844 : if (id == ProofRule::ITE_ELIM2)
633 : : {
634 [ - + ][ - + ]: 12232 : Assert(children.size() == 1);
[ - - ]
635 [ - + ][ - + ]: 12232 : Assert(args.empty());
[ - - ]
636 [ - + ]: 12232 : if (children[0].getKind() != Kind::ITE)
637 : : {
638 : 0 : return Node::null();
639 : : }
640 : 12232 : return nodeManager()->mkNode(Kind::OR, children[0][0], children[0][2]);
641 : : }
642 [ + + ]: 382612 : if (id == ProofRule::NOT_ITE_ELIM1)
643 : : {
644 [ - + ][ - + ]: 24 : Assert(children.size() == 1);
[ - - ]
645 [ - + ][ - + ]: 24 : Assert(args.empty());
[ - - ]
646 : 24 : if (children[0].getKind() != Kind::NOT
647 [ + - ][ - + ]: 48 : || children[0][0].getKind() != Kind::ITE)
[ + - ][ - + ]
[ - - ]
648 : : {
649 : 0 : return Node::null();
650 : : }
651 : 24 : return nodeManager()->mkNode(
652 : 24 : Kind::OR, children[0][0][0].notNode(), children[0][0][1].notNode());
653 : : }
654 [ + + ]: 382588 : if (id == ProofRule::NOT_ITE_ELIM2)
655 : : {
656 [ - + ][ - + ]: 52 : Assert(children.size() == 1);
[ - - ]
657 [ - + ][ - + ]: 52 : Assert(args.empty());
[ - - ]
658 : 52 : if (children[0].getKind() != Kind::NOT
659 [ + - ][ - + ]: 104 : || children[0][0].getKind() != Kind::ITE)
[ + - ][ - + ]
[ - - ]
660 : : {
661 : 0 : return Node::null();
662 : : }
663 : 52 : return nodeManager()->mkNode(
664 : 52 : Kind::OR, children[0][0][0], children[0][0][2].notNode());
665 : : }
666 : : // De Morgan
667 [ + + ]: 382536 : if (id == ProofRule::NOT_AND)
668 : : {
669 [ - + ][ - + ]: 185007 : Assert(children.size() == 1);
[ - - ]
670 [ - + ][ - + ]: 185007 : Assert(args.empty());
[ - - ]
671 : 185007 : if (children[0].getKind() != Kind::NOT
672 [ + - ][ - + ]: 370014 : || children[0][0].getKind() != Kind::AND)
[ + - ][ - + ]
[ - - ]
673 : : {
674 : 0 : return Node::null();
675 : : }
676 : 185007 : std::vector<Node> disjuncts;
677 [ + + ]: 924643 : for (std::size_t i = 0, size = children[0][0].getNumChildren(); i < size;
678 : : ++i)
679 : : {
680 : 739636 : disjuncts.push_back(children[0][0][i].notNode());
681 : : }
682 : 185007 : return nodeManager()->mkNode(Kind::OR, disjuncts);
683 : 185007 : }
684 : : // valid clauses rules for Tseitin CNF transformation
685 [ + + ]: 197529 : if (id == ProofRule::CNF_AND_POS)
686 : : {
687 [ - + ][ - + ]: 67802 : Assert(children.empty());
[ - - ]
688 [ - + ][ - + ]: 67802 : Assert(args.size() == 2);
[ - - ]
689 : : uint32_t i;
690 [ + - ][ - + ]: 67802 : if (args[0].getKind() != Kind::AND || !getUInt32(args[1], i))
[ + - ][ - + ]
[ - - ]
691 : : {
692 : 0 : return Node::null();
693 : : }
694 [ - + ]: 67802 : if (i >= args[0].getNumChildren())
695 : : {
696 : 0 : return Node::null();
697 : : }
698 : 67802 : return nodeManager()->mkNode(Kind::OR, args[0].notNode(), args[0][i]);
699 : : }
700 [ + + ]: 129727 : if (id == ProofRule::CNF_AND_NEG)
701 : : {
702 [ - + ][ - + ]: 50408 : Assert(children.empty());
[ - - ]
703 [ - + ][ - + ]: 50408 : Assert(args.size() == 1);
[ - - ]
704 [ - + ]: 50408 : if (args[0].getKind() != Kind::AND)
705 : : {
706 : 0 : return Node::null();
707 : : }
708 : 151224 : std::vector<Node> disjuncts{args[0]};
709 [ + + ]: 385817 : for (unsigned i = 0, size = args[0].getNumChildren(); i < size; ++i)
710 : : {
711 : 335409 : disjuncts.push_back(args[0][i].notNode());
712 : : }
713 : 50408 : return nodeManager()->mkNode(Kind::OR, disjuncts);
714 : 50408 : }
715 [ + + ]: 79319 : if (id == ProofRule::CNF_OR_POS)
716 : : {
717 [ - + ][ - + ]: 14602 : Assert(children.empty());
[ - - ]
718 [ - + ][ - + ]: 14602 : Assert(args.size() == 1);
[ - - ]
719 [ - + ]: 14602 : if (args[0].getKind() != Kind::OR)
720 : : {
721 : 0 : return Node::null();
722 : : }
723 : 43806 : std::vector<Node> disjuncts{args[0].notNode()};
724 [ + + ]: 1129910 : for (unsigned i = 0, size = args[0].getNumChildren(); i < size; ++i)
725 : : {
726 : 1115308 : disjuncts.push_back(args[0][i]);
727 : : }
728 : 14602 : return nodeManager()->mkNode(Kind::OR, disjuncts);
729 : 14602 : }
730 [ + + ]: 64717 : if (id == ProofRule::CNF_OR_NEG)
731 : : {
732 [ - + ][ - + ]: 32236 : Assert(children.empty());
[ - - ]
733 [ - + ][ - + ]: 32236 : Assert(args.size() == 2);
[ - - ]
734 : : uint32_t i;
735 [ + - ][ - + ]: 32236 : if (args[0].getKind() != Kind::OR || !getUInt32(args[1], i))
[ + - ][ - + ]
[ - - ]
736 : : {
737 : 0 : return Node::null();
738 : : }
739 [ - + ]: 32236 : if (i >= args[0].getNumChildren())
740 : : {
741 : 0 : return Node::null();
742 : : }
743 : 32236 : return nodeManager()->mkNode(Kind::OR, args[0], args[0][i].notNode());
744 : : }
745 [ + + ]: 32481 : if (id == ProofRule::CNF_IMPLIES_POS)
746 : : {
747 [ - + ][ - + ]: 2574 : Assert(children.empty());
[ - - ]
748 [ - + ][ - + ]: 2574 : Assert(args.size() == 1);
[ - - ]
749 [ - + ]: 2574 : if (args[0].getKind() != Kind::IMPLIES)
750 : : {
751 : 0 : return Node::null();
752 : : }
753 : : std::vector<Node> disjuncts{
754 : 15444 : args[0].notNode(), args[0][0].notNode(), args[0][1]};
755 : 2574 : return nodeManager()->mkNode(Kind::OR, disjuncts);
756 : 2574 : }
757 [ + + ]: 29907 : if (id == ProofRule::CNF_IMPLIES_NEG1)
758 : : {
759 [ - + ][ - + ]: 421 : Assert(children.empty());
[ - - ]
760 [ - + ][ - + ]: 421 : Assert(args.size() == 1);
[ - - ]
761 [ - + ]: 421 : if (args[0].getKind() != Kind::IMPLIES)
762 : : {
763 : 0 : return Node::null();
764 : : }
765 : 1684 : std::vector<Node> disjuncts{args[0], args[0][0]};
766 : 421 : return nodeManager()->mkNode(Kind::OR, disjuncts);
767 : 421 : }
768 [ + + ]: 29486 : if (id == ProofRule::CNF_IMPLIES_NEG2)
769 : : {
770 [ - + ][ - + ]: 2134 : Assert(children.empty());
[ - - ]
771 [ - + ][ - + ]: 2134 : Assert(args.size() == 1);
[ - - ]
772 [ - + ]: 2134 : if (args[0].getKind() != Kind::IMPLIES)
773 : : {
774 : 0 : return Node::null();
775 : : }
776 : 10670 : std::vector<Node> disjuncts{args[0], args[0][1].notNode()};
777 : 2134 : return nodeManager()->mkNode(Kind::OR, disjuncts);
778 : 2134 : }
779 [ + + ]: 27352 : if (id == ProofRule::CNF_EQUIV_POS1)
780 : : {
781 [ - + ][ - + ]: 2154 : Assert(children.empty());
[ - - ]
782 [ - + ][ - + ]: 2154 : Assert(args.size() == 1);
[ - - ]
783 [ - + ]: 2154 : if (args[0].getKind() != Kind::EQUAL)
784 : : {
785 : 0 : return Node::null();
786 : : }
787 : : std::vector<Node> disjuncts{
788 : 12924 : args[0].notNode(), args[0][0].notNode(), args[0][1]};
789 : 2154 : return nodeManager()->mkNode(Kind::OR, disjuncts);
790 : 2154 : }
791 [ + + ]: 25198 : if (id == ProofRule::CNF_EQUIV_POS2)
792 : : {
793 [ - + ][ - + ]: 2119 : Assert(children.empty());
[ - - ]
794 [ - + ][ - + ]: 2119 : Assert(args.size() == 1);
[ - - ]
795 [ - + ]: 2119 : if (args[0].getKind() != Kind::EQUAL)
796 : : {
797 : 0 : return Node::null();
798 : : }
799 : : std::vector<Node> disjuncts{
800 : 12714 : args[0].notNode(), args[0][0], args[0][1].notNode()};
801 : 2119 : return nodeManager()->mkNode(Kind::OR, disjuncts);
802 : 2119 : }
803 [ + + ]: 23079 : if (id == ProofRule::CNF_EQUIV_NEG1)
804 : : {
805 [ - + ][ - + ]: 2059 : Assert(children.empty());
[ - - ]
806 [ - + ][ - + ]: 2059 : Assert(args.size() == 1);
[ - - ]
807 [ - + ]: 2059 : if (args[0].getKind() != Kind::EQUAL)
808 : : {
809 : 0 : return Node::null();
810 : : }
811 : 10295 : std::vector<Node> disjuncts{args[0], args[0][0], args[0][1]};
812 : 2059 : return nodeManager()->mkNode(Kind::OR, disjuncts);
813 : 2059 : }
814 [ + + ]: 21020 : if (id == ProofRule::CNF_EQUIV_NEG2)
815 : : {
816 [ - + ][ - + ]: 3074 : Assert(children.empty());
[ - - ]
817 [ - + ][ - + ]: 3074 : Assert(args.size() == 1);
[ - - ]
818 [ - + ]: 3074 : if (args[0].getKind() != Kind::EQUAL)
819 : : {
820 : 0 : return Node::null();
821 : : }
822 : : std::vector<Node> disjuncts{
823 : 18444 : args[0], args[0][0].notNode(), args[0][1].notNode()};
824 : 3074 : return nodeManager()->mkNode(Kind::OR, disjuncts);
825 : 3074 : }
826 [ + + ]: 17946 : if (id == ProofRule::CNF_XOR_POS1)
827 : : {
828 [ - + ][ - + ]: 2222 : Assert(children.empty());
[ - - ]
829 [ - + ][ - + ]: 2222 : Assert(args.size() == 1);
[ - - ]
830 [ - + ]: 2222 : if (args[0].getKind() != Kind::XOR)
831 : : {
832 : 0 : return Node::null();
833 : : }
834 : 11110 : std::vector<Node> disjuncts{args[0].notNode(), args[0][0], args[0][1]};
835 : 2222 : return nodeManager()->mkNode(Kind::OR, disjuncts);
836 : 2222 : }
837 [ + + ]: 15724 : if (id == ProofRule::CNF_XOR_POS2)
838 : : {
839 [ - + ][ - + ]: 1164 : Assert(children.empty());
[ - - ]
840 [ - + ][ - + ]: 1164 : Assert(args.size() == 1);
[ - - ]
841 [ - + ]: 1164 : if (args[0].getKind() != Kind::XOR)
842 : : {
843 : 0 : return Node::null();
844 : : }
845 : : std::vector<Node> disjuncts{
846 : 6984 : args[0].notNode(), args[0][0].notNode(), args[0][1].notNode()};
847 : 1164 : return nodeManager()->mkNode(Kind::OR, disjuncts);
848 : 1164 : }
849 [ + + ]: 14560 : if (id == ProofRule::CNF_XOR_NEG1)
850 : : {
851 [ - + ][ - + ]: 1194 : Assert(children.empty());
[ - - ]
852 [ - + ][ - + ]: 1194 : Assert(args.size() == 1);
[ - - ]
853 [ - + ]: 1194 : if (args[0].getKind() != Kind::XOR)
854 : : {
855 : 0 : return Node::null();
856 : : }
857 : 7164 : std::vector<Node> disjuncts{args[0], args[0][0].notNode(), args[0][1]};
858 : 1194 : return nodeManager()->mkNode(Kind::OR, disjuncts);
859 : 1194 : }
860 [ + + ]: 13366 : if (id == ProofRule::CNF_XOR_NEG2)
861 : : {
862 [ - + ][ - + ]: 1218 : Assert(children.empty());
[ - - ]
863 [ - + ][ - + ]: 1218 : Assert(args.size() == 1);
[ - - ]
864 [ - + ]: 1218 : if (args[0].getKind() != Kind::XOR)
865 : : {
866 : 0 : return Node::null();
867 : : }
868 : 7308 : std::vector<Node> disjuncts{args[0], args[0][0], args[0][1].notNode()};
869 : 1218 : return nodeManager()->mkNode(Kind::OR, disjuncts);
870 : 1218 : }
871 [ + + ]: 12148 : if (id == ProofRule::CNF_ITE_POS1)
872 : : {
873 [ - + ][ - + ]: 2127 : Assert(children.empty());
[ - - ]
874 [ - + ][ - + ]: 2127 : Assert(args.size() == 1);
[ - - ]
875 [ - + ]: 2127 : if (args[0].getKind() != Kind::ITE)
876 : : {
877 : 0 : return Node::null();
878 : : }
879 : : std::vector<Node> disjuncts{
880 : 12762 : args[0].notNode(), args[0][0].notNode(), args[0][1]};
881 : 2127 : return nodeManager()->mkNode(Kind::OR, disjuncts);
882 : 2127 : }
883 [ + + ]: 10021 : if (id == ProofRule::CNF_ITE_POS2)
884 : : {
885 [ - + ][ - + ]: 2025 : Assert(children.empty());
[ - - ]
886 [ - + ][ - + ]: 2025 : Assert(args.size() == 1);
[ - - ]
887 [ - + ]: 2025 : if (args[0].getKind() != Kind::ITE)
888 : : {
889 : 0 : return Node::null();
890 : : }
891 : 10125 : std::vector<Node> disjuncts{args[0].notNode(), args[0][0], args[0][2]};
892 : 2025 : return nodeManager()->mkNode(Kind::OR, disjuncts);
893 : 2025 : }
894 [ + + ]: 7996 : if (id == ProofRule::CNF_ITE_POS3)
895 : : {
896 [ - + ][ - + ]: 2042 : Assert(children.empty());
[ - - ]
897 [ - + ][ - + ]: 2042 : Assert(args.size() == 1);
[ - - ]
898 [ - + ]: 2042 : if (args[0].getKind() != Kind::ITE)
899 : : {
900 : 0 : return Node::null();
901 : : }
902 : 10210 : std::vector<Node> disjuncts{args[0].notNode(), args[0][1], args[0][2]};
903 : 2042 : return nodeManager()->mkNode(Kind::OR, disjuncts);
904 : 2042 : }
905 [ + + ]: 5954 : if (id == ProofRule::CNF_ITE_NEG1)
906 : : {
907 [ - + ][ - + ]: 3048 : Assert(children.empty());
[ - - ]
908 [ - + ][ - + ]: 3048 : Assert(args.size() == 1);
[ - - ]
909 [ - + ]: 3048 : if (args[0].getKind() != Kind::ITE)
910 : : {
911 : 0 : return Node::null();
912 : : }
913 : : std::vector<Node> disjuncts{
914 : 18288 : args[0], args[0][0].notNode(), args[0][1].notNode()};
915 : 3048 : return nodeManager()->mkNode(Kind::OR, disjuncts);
916 : 3048 : }
917 [ + + ]: 2906 : if (id == ProofRule::CNF_ITE_NEG2)
918 : : {
919 [ - + ][ - + ]: 1378 : Assert(children.empty());
[ - - ]
920 [ - + ][ - + ]: 1378 : Assert(args.size() == 1);
[ - - ]
921 [ - + ]: 1378 : if (args[0].getKind() != Kind::ITE)
922 : : {
923 : 0 : return Node::null();
924 : : }
925 : 8268 : std::vector<Node> disjuncts{args[0], args[0][0], args[0][2].notNode()};
926 : 1378 : return nodeManager()->mkNode(Kind::OR, disjuncts);
927 : 1378 : }
928 [ + + ]: 1528 : if (id == ProofRule::CNF_ITE_NEG3)
929 : : {
930 [ - + ][ - + ]: 1353 : Assert(children.empty());
[ - - ]
931 [ - + ][ - + ]: 1353 : Assert(args.size() == 1);
[ - - ]
932 [ - + ]: 1353 : if (args[0].getKind() != Kind::ITE)
933 : : {
934 : 0 : return Node::null();
935 : : }
936 : : std::vector<Node> disjuncts{
937 : 8118 : args[0], args[0][1].notNode(), args[0][2].notNode()};
938 : 1353 : return nodeManager()->mkNode(Kind::OR, disjuncts);
939 : 1353 : }
940 [ - + ][ - - ]: 175 : if (id == ProofRule::SAT_REFUTATION || id == ProofRule::DRAT_REFUTATION
941 [ - - ]: 0 : || id == ProofRule::SAT_EXTERNAL_PROVE)
942 : : {
943 [ - + ][ - - ]: 175 : Assert(args.size()
[ - + ][ - + ]
[ - - ]
944 : : == (id == ProofRule::SAT_REFUTATION
945 : : ? 0
946 : : : (id == ProofRule::SAT_EXTERNAL_PROVE ? 1 : 2)));
947 : 350 : return nodeManager()->mkConst(false);
948 : : }
949 : : // no rule
950 : 0 : return Node::null();
951 : : }
952 : :
953 : : } // namespace booleans
954 : : } // namespace theory
955 : : } // namespace cvc5::internal
|
