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 : :
15 : : #include "expr/skolem_manager.h"
16 : : #include "theory/rewriter.h"
17 : :
18 : : namespace cvc5::internal {
19 : : namespace theory {
20 : : namespace booleans {
21 : :
22 : 51310 : BoolProofRuleChecker::BoolProofRuleChecker(NodeManager* nm)
23 : 51310 : : ProofRuleChecker(nm)
24 : : {
25 : 51310 : }
26 : :
27 : 20018 : void BoolProofRuleChecker::registerTo(ProofChecker* pc)
28 : : {
29 : 20018 : pc->registerChecker(ProofRule::SPLIT, this);
30 : 20018 : pc->registerChecker(ProofRule::RESOLUTION, this);
31 : 20018 : pc->registerChecker(ProofRule::CHAIN_RESOLUTION, this);
32 : 20018 : pc->registerChecker(ProofRule::CHAIN_M_RESOLUTION, this);
33 : 20018 : pc->registerChecker(ProofRule::FACTORING, this);
34 : 20018 : pc->registerChecker(ProofRule::REORDERING, this);
35 : 20018 : pc->registerChecker(ProofRule::EQ_RESOLVE, this);
36 : 20018 : pc->registerChecker(ProofRule::MODUS_PONENS, this);
37 : 20018 : pc->registerChecker(ProofRule::NOT_NOT_ELIM, this);
38 : 20018 : pc->registerChecker(ProofRule::CONTRA, this);
39 : 20018 : pc->registerChecker(ProofRule::AND_ELIM, this);
40 : 20018 : pc->registerChecker(ProofRule::AND_INTRO, this);
41 : 20018 : pc->registerChecker(ProofRule::NOT_OR_ELIM, this);
42 : 20018 : pc->registerChecker(ProofRule::IMPLIES_ELIM, this);
43 : 20018 : pc->registerChecker(ProofRule::NOT_IMPLIES_ELIM1, this);
44 : 20018 : pc->registerChecker(ProofRule::NOT_IMPLIES_ELIM2, this);
45 : 20018 : pc->registerChecker(ProofRule::EQUIV_ELIM1, this);
46 : 20018 : pc->registerChecker(ProofRule::EQUIV_ELIM2, this);
47 : 20018 : pc->registerChecker(ProofRule::NOT_EQUIV_ELIM1, this);
48 : 20018 : pc->registerChecker(ProofRule::NOT_EQUIV_ELIM2, this);
49 : 20018 : pc->registerChecker(ProofRule::XOR_ELIM1, this);
50 : 20018 : pc->registerChecker(ProofRule::XOR_ELIM2, this);
51 : 20018 : pc->registerChecker(ProofRule::NOT_XOR_ELIM1, this);
52 : 20018 : pc->registerChecker(ProofRule::NOT_XOR_ELIM2, this);
53 : 20018 : pc->registerChecker(ProofRule::ITE_ELIM1, this);
54 : 20018 : pc->registerChecker(ProofRule::ITE_ELIM2, this);
55 : 20018 : pc->registerChecker(ProofRule::NOT_ITE_ELIM1, this);
56 : 20018 : pc->registerChecker(ProofRule::NOT_ITE_ELIM2, this);
57 : 20018 : pc->registerChecker(ProofRule::NOT_AND, this);
58 : 20018 : pc->registerChecker(ProofRule::CNF_AND_POS, this);
59 : 20018 : pc->registerChecker(ProofRule::CNF_AND_NEG, this);
60 : 20018 : pc->registerChecker(ProofRule::CNF_OR_POS, this);
61 : 20018 : pc->registerChecker(ProofRule::CNF_OR_NEG, this);
62 : 20018 : pc->registerChecker(ProofRule::CNF_IMPLIES_POS, this);
63 : 20018 : pc->registerChecker(ProofRule::CNF_IMPLIES_NEG1, this);
64 : 20018 : pc->registerChecker(ProofRule::CNF_IMPLIES_NEG2, this);
65 : 20018 : pc->registerChecker(ProofRule::CNF_EQUIV_POS1, this);
66 : 20018 : pc->registerChecker(ProofRule::CNF_EQUIV_POS2, this);
67 : 20018 : pc->registerChecker(ProofRule::CNF_EQUIV_NEG1, this);
68 : 20018 : pc->registerChecker(ProofRule::CNF_EQUIV_NEG2, this);
69 : 20018 : pc->registerChecker(ProofRule::CNF_XOR_POS1, this);
70 : 20018 : pc->registerChecker(ProofRule::CNF_XOR_POS2, this);
71 : 20018 : pc->registerChecker(ProofRule::CNF_XOR_NEG1, this);
72 : 20018 : pc->registerChecker(ProofRule::CNF_XOR_NEG2, this);
73 : 20018 : pc->registerChecker(ProofRule::CNF_ITE_POS1, this);
74 : 20018 : pc->registerChecker(ProofRule::CNF_ITE_POS2, this);
75 : 20018 : pc->registerChecker(ProofRule::CNF_ITE_POS3, this);
76 : 20018 : pc->registerChecker(ProofRule::CNF_ITE_NEG1, this);
77 : 20018 : pc->registerChecker(ProofRule::CNF_ITE_NEG2, this);
78 : 20018 : pc->registerChecker(ProofRule::CNF_ITE_NEG3, this);
79 : 20018 : pc->registerTrustedChecker(ProofRule::SAT_REFUTATION, this, 1);
80 : 20018 : pc->registerTrustedChecker(ProofRule::DRAT_REFUTATION, this, 1);
81 : 20018 : pc->registerTrustedChecker(ProofRule::SAT_EXTERNAL_PROVE, this, 1);
82 : 20018 : }
83 : :
84 : 4952847 : Node BoolProofRuleChecker::checkInternal(ProofRule id,
85 : : const std::vector<Node>& children,
86 : : const std::vector<Node>& args)
87 : : {
88 [ + + ]: 4952847 : if (id == ProofRule::RESOLUTION)
89 : : {
90 [ - + ][ - + ]: 962184 : Assert(children.size() == 2);
[ - - ]
91 [ - + ][ - + ]: 962184 : Assert(args.size() == 2);
[ - - ]
92 : 962184 : NodeManager* nm = nodeManager();
93 : 962184 : std::vector<Node> disjuncts;
94 [ + + ]: 4810920 : Node pivots[2];
95 [ + + ]: 962184 : if (args[0] == nm->mkConst(true))
96 : : {
97 : 520313 : pivots[0] = args[1];
98 : 520313 : pivots[1] = args[1].notNode();
99 : : }
100 : : else
101 : : {
102 [ - + ][ - + ]: 441871 : Assert(args[0] == nm->mkConst(false));
[ - - ]
103 : 441871 : pivots[0] = args[1].notNode();
104 : 441871 : pivots[1] = args[1];
105 : : }
106 [ + + ]: 2886552 : for (unsigned i = 0; i < 2; ++i)
107 : : {
108 : : // determine whether the clause is a singleton for effects of resolution,
109 : : // which is the case if it's not an OR node or it is an OR node but it is
110 : : // equal to the pivot
111 : 1924368 : std::vector<Node> lits;
112 [ + + ][ + + ]: 1924368 : if (children[i].getKind() == Kind::OR && pivots[i] != children[i])
[ + + ]
113 : : {
114 : 1608165 : lits.insert(lits.end(), children[i].begin(), children[i].end());
115 : : }
116 : : else
117 : : {
118 : 316203 : lits.push_back(children[i]);
119 : : }
120 [ + + ]: 21828370 : for (unsigned j = 0, size = lits.size(); j < size; ++j)
121 : : {
122 [ + + ]: 19904002 : if (pivots[i] != lits[j])
123 : : {
124 : 17979634 : disjuncts.push_back(lits[j]);
125 : : }
126 : : else
127 : : {
128 : : // just eliminate first occurrence
129 : 1924368 : pivots[i] = Node::null();
130 : : }
131 : : }
132 : 1924368 : }
133 : 1924368 : return disjuncts.empty() ? nm->mkConst(false)
134 : 1058797 : : disjuncts.size() == 1 ? disjuncts[0]
135 [ + + ][ + + ]: 2020981 : : nm->mkNode(Kind::OR, disjuncts);
136 [ + + ][ - - ]: 3848736 : }
137 [ + + ]: 3990663 : if (id == ProofRule::FACTORING)
138 : : {
139 [ - + ][ - + ]: 364312 : Assert(children.size() == 1);
[ - - ]
140 [ - + ][ - + ]: 364312 : Assert(args.empty());
[ - - ]
141 [ - + ]: 364312 : if (children[0].getKind() != Kind::OR)
142 : : {
143 : 0 : return Node::null();
144 : : }
145 : : // remove duplicates while keeping the order of children
146 : 364312 : std::unordered_set<TNode> clauseSet;
147 : 364312 : std::vector<Node> disjuncts;
148 : 364312 : unsigned size = children[0].getNumChildren();
149 [ + + ]: 9258187 : for (unsigned i = 0; i < size; ++i)
150 : : {
151 [ + + ]: 8893875 : if (clauseSet.count(children[0][i]))
152 : : {
153 : 2765445 : continue;
154 : : }
155 : 6128430 : disjuncts.push_back(children[0][i]);
156 : 6128430 : clauseSet.insert(children[0][i]);
157 : : }
158 [ - + ]: 364312 : if (disjuncts.size() == size)
159 : : {
160 : 0 : return Node::null();
161 : : }
162 : 364312 : NodeManager* nm = nodeManager();
163 : 364312 : return nm->mkOr(disjuncts);
164 : 364312 : }
165 [ + + ]: 3626351 : if (id == ProofRule::REORDERING)
166 : : {
167 [ - + ][ - + ]: 1225153 : Assert(children.size() == 1);
[ - - ]
168 [ - + ][ - + ]: 1225153 : Assert(args.size() == 1);
[ - - ]
169 : 1225153 : std::unordered_set<Node> clauseSet1, clauseSet2;
170 [ + - ]: 1225153 : if (children[0].getKind() == Kind::OR)
171 : : {
172 : 1225153 : clauseSet1.insert(children[0].begin(), children[0].end());
173 : : }
174 : : else
175 : : {
176 : 0 : clauseSet1.insert(children[0]);
177 : : }
178 [ + - ]: 1225153 : if (args[0].getKind() == Kind::OR)
179 : : {
180 : 1225153 : clauseSet2.insert(args[0].begin(), args[0].end());
181 : : }
182 : : else
183 : : {
184 : 0 : clauseSet2.insert(args[0]);
185 : : }
186 [ - + ]: 1225153 : if (clauseSet1 != clauseSet2)
187 : : {
188 [ - - ]: 0 : Trace("bool-pfcheck") << id << ": clause set1: " << clauseSet1 << "\n"
189 : 0 : << id << ": clause set2: " << clauseSet2 << "\n";
190 : 0 : return Node::null();
191 : : }
192 : 1225153 : return args[0];
193 : 1225153 : }
194 [ + + ]: 2401198 : if (id == ProofRule::CHAIN_RESOLUTION)
195 : : {
196 [ - + ][ - + ]: 372777 : Assert(children.size() > 1);
[ - - ]
197 [ - + ][ - + ]: 372777 : Assert(args.size() == 2);
[ - - ]
198 [ - + ][ - + ]: 372777 : Assert(args[0].getNumChildren() == (children.size() - 1));
[ - - ]
199 [ - + ][ - + ]: 372777 : Assert(args[1].getNumChildren() == (children.size() - 1));
[ - - ]
200 [ + - ]: 372777 : Trace("bool-pfcheck") << "chain_res:\n" << push;
201 : 372777 : NodeManager* nm = nodeManager();
202 : 372777 : Node trueNode = nm->mkConst(true);
203 : 372777 : Node falseNode = nm->mkConst(false);
204 : : // The lhs and rhs clauses in a binary resolution step, respectively. Since
205 : : // children correspond to the premises in the resolution chain, the first
206 : : // lhs clause is the first premise, the first rhs clause is the second
207 : : // premise. Each subsequent lhs clause will be the result of the previous
208 : : // binary resolution step in the chain, while each subsequent rhs clause
209 : : // will be respectively the second, third etc premises.
210 : 372777 : std::vector<Node> lhsClause, rhsClause;
211 : : // The pivots to be eliminated to the lhs clause and rhs clause in a binary
212 : : // resolution step, respectively
213 : 372777 : Node lhsElim, rhsElim;
214 : : // Get lhsClause of first resolution.
215 : : //
216 : : // Since a Node cannot hold an OR with a single child we need to
217 : : // disambiguate singleton clauses that are OR nodes from non-singleton
218 : : // clauses (i.e. unit clauses in the SAT solver).
219 : : //
220 : : // If the child is not an OR, it is a singleton clause and we take the
221 : : // child itself as the clause. Otherwise the child can only be a singleton
222 : : // clause if the child itself is used as a resolution literal, i.e. if the
223 : : // first child equal to the first pivot (which is args[1][0] or
224 : : // args[1][0].notNode() depending on the polarity).
225 : 372777 : Node pols = args[0];
226 : 372777 : Node lits = args[1];
227 : 372777 : if (children[0].getKind() != Kind::OR
228 : 745286 : || (pols[0] == trueNode && children[0] == lits[0])
229 : 1118063 : || (pols[0] == falseNode && children[0] == lits[0].notNode()))
230 : : {
231 : 268 : lhsClause.push_back(children[0]);
232 : : }
233 : : else
234 : : {
235 : 372509 : lhsClause.insert(lhsClause.end(), children[0].begin(), children[0].end());
236 : : }
237 : : // Traverse the links, which amounts to for each pair of args removing a
238 : : // literal from the lhs and a literal from the lhs.
239 [ + + ]: 3390603 : for (size_t i = 0, argsSize = pols.getNumChildren(); i < argsSize; i++)
240 : : {
241 : : // Polarity determines how the pivot occurs in lhs and rhs
242 [ + + ]: 3017826 : if (pols[i] == trueNode)
243 : : {
244 : 1164236 : lhsElim = lits[i];
245 : 1164236 : rhsElim = lits[i].notNode();
246 : : }
247 : : else
248 : : {
249 [ - + ][ - + ]: 1853590 : Assert(pols[i] == falseNode);
[ - - ]
250 : 1853590 : lhsElim = lits[i].notNode();
251 : 1853590 : rhsElim = lits[i];
252 : : }
253 : : // The index of the child corresponding to the current rhs clause
254 : 3017826 : size_t childIndex = i + 1;
255 : : // Get rhs clause. It's a singleton if not an OR node or if equal to
256 : : // rhsElim
257 : 3017826 : if (children[childIndex].getKind() != Kind::OR
258 [ + + ][ + + ]: 3017826 : || children[childIndex] == rhsElim)
[ + + ]
259 : : {
260 : 1553638 : rhsClause.push_back(children[childIndex]);
261 : : }
262 : : else
263 : : {
264 : 1464188 : rhsClause = {children[childIndex].begin(), children[childIndex].end()};
265 : : }
266 [ + - ]: 3017826 : Trace("bool-pfcheck") << i << "-th res link:\n";
267 [ + - ]: 3017826 : Trace("bool-pfcheck") << "\t - lhsClause: " << lhsClause << "\n";
268 [ + - ]: 3017826 : Trace("bool-pfcheck") << "\t\t - lhsElim: " << lhsElim << "\n";
269 [ + - ]: 3017826 : Trace("bool-pfcheck") << "\t - rhsClause: " << rhsClause << "\n";
270 [ + - ]: 3017826 : Trace("bool-pfcheck") << "\t\t - rhsElim: " << rhsElim << "\n";
271 : : // Compute the resulting clause, which will be the next lhsClause, as
272 : : // follows:
273 : : // - remove lhsElim from lhsClause
274 : : // - remove rhsElim from rhsClause and add the lits to lhsClause
275 : 3017826 : auto itlhs = std::find(lhsClause.begin(), lhsClause.end(), lhsElim);
276 [ - + ][ - + ]: 3017826 : AlwaysAssert(itlhs != lhsClause.end());
[ - - ]
277 : 3017826 : lhsClause.erase(itlhs);
278 [ + - ]: 3017826 : Trace("bool-pfcheck") << "\t.. after lhsClause: " << lhsClause << "\n";
279 : 3017826 : auto itrhs = std::find(rhsClause.begin(), rhsClause.end(), rhsElim);
280 [ - + ][ - + ]: 3017826 : AlwaysAssert(itrhs != rhsClause.end());
[ - - ]
281 : 3017826 : lhsClause.insert(lhsClause.end(), rhsClause.begin(), itrhs);
282 : 3017826 : lhsClause.insert(lhsClause.end(), itrhs + 1, rhsClause.end());
283 [ - + ]: 3017826 : if (TraceIsOn("bool-pfcheck"))
284 : : {
285 : 0 : std::vector<Node> updatedRhsClause{rhsClause.begin(), itrhs};
286 : 0 : updatedRhsClause.insert(
287 : 0 : updatedRhsClause.end(), itrhs + 1, rhsClause.end());
288 [ - - ]: 0 : Trace("bool-pfcheck")
289 : 0 : << "\t.. after rhsClause: " << updatedRhsClause << "\n";
290 : 0 : }
291 : 3017826 : rhsClause.clear();
292 : : }
293 [ + - ]: 745554 : Trace("bool-pfcheck") << "\n resulting clause: " << lhsClause << "\n"
294 : 372777 : << pop;
295 : 372777 : return nm->mkOr(lhsClause);
296 : 372777 : }
297 [ + + ]: 2028421 : if (id == ProofRule::CHAIN_M_RESOLUTION)
298 : : {
299 [ - + ][ - + ]: 277308 : Assert(children.size() > 1);
[ - - ]
300 [ + - ]: 277308 : Trace("bool-pfcheck") << "macro_res: " << args[0] << "\n" << push;
301 : 277308 : NodeManager* nm = nodeManager();
302 : 277308 : Node trueNode = nm->mkConst(true);
303 : 277308 : Node falseNode = nm->mkConst(false);
304 : 277308 : std::vector<Node> lhsClause, rhsClause;
305 : 277308 : Node lhsElim, rhsElim;
306 : 277308 : std::vector<Node> pols, lits;
307 [ - + ][ - + ]: 277308 : Assert(args.size() == 3);
[ - - ]
308 : 277308 : pols.insert(pols.end(), args[1].begin(), args[1].end());
309 : 277308 : lits.insert(lits.end(), args[2].begin(), args[2].end());
310 [ - + ]: 277308 : if (pols.size() != lits.size())
311 : : {
312 : 0 : return Node::null();
313 : : }
314 : 277308 : if (children[0].getKind() != Kind::OR
315 [ + + ][ + - ]: 277087 : || (pols[0] == trueNode && children[0] == lits[0])
316 [ + + ][ + + ]: 831703 : || (pols[0] == falseNode && children[0] == lits[0].notNode()))
[ - + ][ + + ]
[ + + ][ - - ]
317 : : {
318 : 221 : lhsClause.push_back(children[0]);
319 : : }
320 : : else
321 : : {
322 : 277087 : lhsClause.insert(lhsClause.end(), children[0].begin(), children[0].end());
323 : : }
324 : : // Traverse the links, which amounts to for each pair of args removing a
325 : : // literal from the lhs and a literal from the lhs.
326 [ + + ]: 4922971 : for (size_t i = 0, argsSize = pols.size(); i < argsSize; i++)
327 : : {
328 : : // Polarity determines how the pivot occurs in lhs and rhs
329 [ + + ]: 4645663 : if (pols[i] == trueNode)
330 : : {
331 : 2781708 : lhsElim = lits[i];
332 : 2781708 : rhsElim = lits[i].notNode();
333 : : }
334 : : else
335 : : {
336 [ - + ][ - + ]: 1863955 : Assert(pols[i] == falseNode);
[ - - ]
337 : 1863955 : lhsElim = lits[i].notNode();
338 : 1863955 : rhsElim = lits[i];
339 : : }
340 : : // The index of the child corresponding to the current rhs clause
341 : 4645663 : size_t childIndex = i + 1;
342 : : // Get rhs clause. It's a singleton if not an OR node or if equal to
343 : : // rhsElim
344 : 4645663 : if (children[childIndex].getKind() != Kind::OR
345 [ + + ][ + + ]: 4645663 : || children[childIndex] == rhsElim)
[ + + ]
346 : : {
347 : 638235 : rhsClause.push_back(children[childIndex]);
348 : : }
349 : : else
350 : : {
351 : 4007428 : rhsClause = {children[childIndex].begin(), children[childIndex].end()};
352 : : }
353 [ + - ]: 4645663 : Trace("bool-pfcheck") << i << "-th res link:\n";
354 [ + - ]: 4645663 : Trace("bool-pfcheck") << "\t - lhsClause: " << lhsClause << "\n";
355 [ + - ]: 4645663 : Trace("bool-pfcheck") << "\t\t - lhsElim: " << lhsElim << "\n";
356 [ + - ]: 4645663 : Trace("bool-pfcheck") << "\t - rhsClause: " << rhsClause << "\n";
357 [ + - ]: 4645663 : Trace("bool-pfcheck") << "\t\t - rhsElim: " << rhsElim << "\n";
358 : : // Compute the resulting clause, which will be the next lhsClause, as
359 : : // follows:
360 : : // - remove all lhsElim from lhsClause
361 : : // - remove all rhsElim from rhsClause and add the lits to lhsClause
362 : : //
363 : : // Note that to remove the elements from lhsClaus we use the
364 : : // "erase-remove" idiom in C++: the std::remove call shuffles the elements
365 : : // different from lhsElim to the beginning of the container, returning an
366 : : // iterator to the beginning of the "rest" of the container (with
367 : : // occurrences of lhsElim). Then the call to erase removes the range from
368 : : // there to the end. Once C++ 20 is allowed in the cvc5 code base, this
369 : : // could be done with a single call to std::erase.
370 : 4645663 : lhsClause.erase(std::remove(lhsClause.begin(), lhsClause.end(), lhsElim),
371 : 4645663 : lhsClause.end());
372 [ + + ]: 21319032 : for (const Node& l : rhsClause)
373 : : {
374 : : // only add if literal does not occur in elimination set
375 [ + + ]: 16673369 : if (rhsElim != l)
376 : : {
377 : 12027706 : lhsClause.push_back(l);
378 : : }
379 : : }
380 : 4645663 : rhsClause.clear();
381 : : }
382 : :
383 [ + - ]: 277308 : Trace("bool-pfcheck") << "clause: " << lhsClause << "\n";
384 : : // check that set representation is the same as of the given conclusion
385 : 277308 : std::unordered_set<Node> clauseComputed{lhsClause.begin(), lhsClause.end()};
386 [ + - ]: 277308 : Trace("bool-pfcheck") << "clauseSet: " << clauseComputed << "\n" << pop;
387 [ + + ]: 277308 : if (clauseComputed.empty())
388 : : {
389 : : // conclusion differ
390 [ - + ]: 1935 : if (args[0] != falseNode)
391 : : {
392 : 0 : return Node::null();
393 : : }
394 : 1935 : return args[0];
395 : : }
396 [ + + ]: 275373 : if (clauseComputed.size() == 1)
397 : : {
398 : : // conclusion differ
399 [ - + ]: 87109 : if (args[0] != *clauseComputed.begin())
400 : : {
401 : 0 : return Node::null();
402 : : }
403 : 87109 : return args[0];
404 : : }
405 : : // At this point, should amount to them differing only on order or in
406 : : // repetitions. So the original result can't be a singleton clause.
407 [ - + ]: 188264 : if (args[0].getKind() != Kind::OR)
408 : : {
409 : 0 : return Node::null();
410 : : }
411 : 188264 : std::unordered_set<Node> clauseGiven{args[0].begin(), args[0].end()};
412 [ + - ]: 188264 : return clauseComputed == clauseGiven ? args[0] : Node::null();
413 : 277308 : }
414 [ + + ]: 1751113 : if (id == ProofRule::SPLIT)
415 : : {
416 [ - + ][ - + ]: 38850 : Assert(children.empty());
[ - - ]
417 [ - + ][ - + ]: 38850 : Assert(args.size() == 1);
[ - - ]
418 : 38850 : return nodeManager()->mkNode(Kind::OR, args[0], args[0].notNode());
419 : : }
420 [ + + ]: 1712263 : if (id == ProofRule::CONTRA)
421 : : {
422 [ - + ][ - + ]: 69056 : Assert(children.size() == 2);
[ - - ]
423 [ + - ][ + - ]: 69056 : if (children[1].getKind() == Kind::NOT && children[0] == children[1][0])
[ + - ][ + - ]
[ - - ]
424 : : {
425 : 138112 : return nodeManager()->mkConst(false);
426 : : }
427 : 0 : return Node::null();
428 : : }
429 [ + + ]: 1643207 : if (id == ProofRule::EQ_RESOLVE)
430 : : {
431 [ - + ][ - + ]: 420250 : Assert(children.size() == 2);
[ - - ]
432 [ - + ][ - + ]: 420250 : Assert(args.empty());
[ - - ]
433 [ + - ][ - + ]: 420250 : if (children[1].getKind() != Kind::EQUAL || children[0] != children[1][0])
[ + - ][ - + ]
[ - - ]
434 : : {
435 : 0 : return Node::null();
436 : : }
437 : 420250 : return children[1][1];
438 : : }
439 [ + + ]: 1222957 : if (id == ProofRule::MODUS_PONENS)
440 : : {
441 [ - + ][ - + ]: 224753 : Assert(children.size() == 2);
[ - - ]
442 [ - + ][ - + ]: 224753 : Assert(args.empty());
[ - - ]
443 [ + - ][ - + ]: 224753 : if (children[1].getKind() != Kind::IMPLIES || children[0] != children[1][0])
[ + - ][ - + ]
[ - - ]
444 : : {
445 : 0 : return Node::null();
446 : : }
447 : 224753 : return children[1][1];
448 : : }
449 [ + + ]: 998204 : if (id == ProofRule::NOT_NOT_ELIM)
450 : : {
451 [ - + ][ - + ]: 5703 : Assert(children.size() == 1);
[ - - ]
452 [ - + ][ - + ]: 5703 : Assert(args.empty());
[ - - ]
453 : 5703 : if (children[0].getKind() != Kind::NOT
454 [ + - ][ - + ]: 11406 : || children[0][0].getKind() != Kind::NOT)
[ + - ][ - + ]
[ - - ]
455 : : {
456 : 0 : return Node::null();
457 : : }
458 : 5703 : return children[0][0][0];
459 : : }
460 : : // natural deduction rules
461 [ + + ]: 992501 : if (id == ProofRule::AND_ELIM)
462 : : {
463 [ - + ][ - + ]: 201587 : Assert(children.size() == 1);
[ - - ]
464 [ - + ][ - + ]: 201587 : Assert(args.size() == 1);
[ - - ]
465 : : uint32_t i;
466 [ + - ][ - + ]: 201587 : if (children[0].getKind() != Kind::AND || !getUInt32(args[0], i))
[ + - ][ - + ]
[ - - ]
467 : : {
468 : 0 : return Node::null();
469 : : }
470 [ - + ]: 201587 : if (i >= children[0].getNumChildren())
471 : : {
472 : 0 : return Node::null();
473 : : }
474 : 201587 : return children[0][i];
475 : : }
476 [ + + ]: 790914 : if (id == ProofRule::AND_INTRO)
477 : : {
478 [ - + ][ - + ]: 248709 : Assert(children.size() >= 1);
[ - - ]
479 : 248709 : return children.size() == 1 ? children[0]
480 [ - + ]: 248709 : : nodeManager()->mkNode(Kind::AND, children);
481 : : }
482 [ + + ]: 542205 : if (id == ProofRule::NOT_OR_ELIM)
483 : : {
484 [ - + ][ - + ]: 7230 : Assert(children.size() == 1);
[ - - ]
485 [ - + ][ - + ]: 7230 : Assert(args.size() == 1);
[ - - ]
486 : : uint32_t i;
487 : 7230 : if (children[0].getKind() != Kind::NOT
488 : 14460 : || children[0][0].getKind() != Kind::OR || !getUInt32(args[0], i))
489 : : {
490 : 0 : return Node::null();
491 : : }
492 [ - + ]: 7230 : if (i >= children[0][0].getNumChildren())
493 : : {
494 : 0 : return Node::null();
495 : : }
496 : 7230 : return children[0][0][i].notNode();
497 : : }
498 [ + + ]: 534975 : if (id == ProofRule::IMPLIES_ELIM)
499 : : {
500 [ - + ][ - + ]: 61154 : Assert(children.size() == 1);
[ - - ]
501 [ - + ][ - + ]: 61154 : Assert(args.empty());
[ - - ]
502 [ - + ]: 61154 : if (children[0].getKind() != Kind::IMPLIES)
503 : : {
504 : 0 : return Node::null();
505 : : }
506 : 61154 : return nodeManager()->mkNode(
507 : 61154 : Kind::OR, children[0][0].notNode(), children[0][1]);
508 : : }
509 [ + + ]: 473821 : if (id == ProofRule::NOT_IMPLIES_ELIM1)
510 : : {
511 [ - + ][ - + ]: 4102 : Assert(children.size() == 1);
[ - - ]
512 [ - + ][ - + ]: 4102 : Assert(args.empty());
[ - - ]
513 : 4102 : if (children[0].getKind() != Kind::NOT
514 [ + - ][ - + ]: 8204 : || children[0][0].getKind() != Kind::IMPLIES)
[ + - ][ - + ]
[ - - ]
515 : : {
516 : 0 : return Node::null();
517 : : }
518 : 4102 : return children[0][0][0];
519 : : }
520 [ + + ]: 469719 : if (id == ProofRule::NOT_IMPLIES_ELIM2)
521 : : {
522 [ - + ][ - + ]: 1917 : Assert(children.size() == 1);
[ - - ]
523 [ - + ][ - + ]: 1917 : Assert(args.empty());
[ - - ]
524 : 1917 : if (children[0].getKind() != Kind::NOT
525 [ + - ][ - + ]: 3834 : || children[0][0].getKind() != Kind::IMPLIES)
[ + - ][ - + ]
[ - - ]
526 : : {
527 : 0 : return Node::null();
528 : : }
529 : 1917 : return children[0][0][1].notNode();
530 : : }
531 [ + + ]: 467802 : if (id == ProofRule::EQUIV_ELIM1)
532 : : {
533 [ - + ][ - + ]: 33962 : Assert(children.size() == 1);
[ - - ]
534 [ - + ][ - + ]: 33962 : Assert(args.empty());
[ - - ]
535 [ - + ]: 33962 : if (children[0].getKind() != Kind::EQUAL)
536 : : {
537 : 0 : return Node::null();
538 : : }
539 : 33962 : return nodeManager()->mkNode(
540 : 33962 : Kind::OR, children[0][0].notNode(), children[0][1]);
541 : : }
542 [ + + ]: 433840 : if (id == ProofRule::EQUIV_ELIM2)
543 : : {
544 [ - + ][ - + ]: 15382 : Assert(children.size() == 1);
[ - - ]
545 [ - + ][ - + ]: 15382 : Assert(args.empty());
[ - - ]
546 [ - + ]: 15382 : if (children[0].getKind() != Kind::EQUAL)
547 : : {
548 : 0 : return Node::null();
549 : : }
550 : 15382 : return nodeManager()->mkNode(
551 : 15382 : Kind::OR, children[0][0], children[0][1].notNode());
552 : : }
553 [ + + ]: 418458 : if (id == ProofRule::NOT_EQUIV_ELIM1)
554 : : {
555 [ - + ][ - + ]: 617 : Assert(children.size() == 1);
[ - - ]
556 [ - + ][ - + ]: 617 : Assert(args.empty());
[ - - ]
557 : 617 : if (children[0].getKind() != Kind::NOT
558 [ + - ][ - + ]: 1234 : || children[0][0].getKind() != Kind::EQUAL)
[ + - ][ - + ]
[ - - ]
559 : : {
560 : 0 : return Node::null();
561 : : }
562 : 617 : return nodeManager()->mkNode(
563 : 617 : Kind::OR, children[0][0][0], children[0][0][1]);
564 : : }
565 [ + + ]: 417841 : if (id == ProofRule::NOT_EQUIV_ELIM2)
566 : : {
567 [ - + ][ - + ]: 403 : Assert(children.size() == 1);
[ - - ]
568 [ - + ][ - + ]: 403 : Assert(args.empty());
[ - - ]
569 : 403 : if (children[0].getKind() != Kind::NOT
570 [ + - ][ - + ]: 806 : || children[0][0].getKind() != Kind::EQUAL)
[ + - ][ - + ]
[ - - ]
571 : : {
572 : 0 : return Node::null();
573 : : }
574 : 1209 : return nodeManager()->mkNode(
575 [ + + ][ - - ]: 1209 : Kind::OR, {children[0][0][0].notNode(), children[0][0][1].notNode()});
576 : : }
577 [ + + ]: 417438 : if (id == ProofRule::XOR_ELIM1)
578 : : {
579 [ - + ][ - + ]: 84 : Assert(children.size() == 1);
[ - - ]
580 [ - + ][ - + ]: 84 : Assert(args.empty());
[ - - ]
581 [ - + ]: 84 : if (children[0].getKind() != Kind::XOR)
582 : : {
583 : 0 : return Node::null();
584 : : }
585 : 84 : return nodeManager()->mkNode(Kind::OR, children[0][0], children[0][1]);
586 : : }
587 [ + + ]: 417354 : if (id == ProofRule::XOR_ELIM2)
588 : : {
589 [ - + ][ - + ]: 102 : Assert(children.size() == 1);
[ - - ]
590 [ - + ][ - + ]: 102 : Assert(args.empty());
[ - - ]
591 [ - + ]: 102 : if (children[0].getKind() != Kind::XOR)
592 : : {
593 : 0 : return Node::null();
594 : : }
595 : 306 : return nodeManager()->mkNode(
596 [ + + ][ - - ]: 306 : Kind::OR, {children[0][0].notNode(), children[0][1].notNode()});
597 : : }
598 [ + + ]: 417252 : if (id == ProofRule::NOT_XOR_ELIM1)
599 : : {
600 [ - + ][ - + ]: 63 : Assert(children.size() == 1);
[ - - ]
601 [ - + ][ - + ]: 63 : Assert(args.empty());
[ - - ]
602 : 63 : if (children[0].getKind() != Kind::NOT
603 [ + - ][ - + ]: 126 : || children[0][0].getKind() != Kind::XOR)
[ + - ][ - + ]
[ - - ]
604 : : {
605 : 0 : return Node::null();
606 : : }
607 : 63 : return nodeManager()->mkNode(
608 : 63 : Kind::OR, children[0][0][0], children[0][0][1].notNode());
609 : : }
610 [ + + ]: 417189 : if (id == ProofRule::NOT_XOR_ELIM2)
611 : : {
612 [ - + ][ - + ]: 71 : Assert(children.size() == 1);
[ - - ]
613 [ - + ][ - + ]: 71 : Assert(args.empty());
[ - - ]
614 : 71 : if (children[0].getKind() != Kind::NOT
615 [ + - ][ - + ]: 142 : || children[0][0].getKind() != Kind::XOR)
[ + - ][ - + ]
[ - - ]
616 : : {
617 : 0 : return Node::null();
618 : : }
619 : 71 : return nodeManager()->mkNode(
620 : 71 : Kind::OR, children[0][0][0].notNode(), children[0][0][1]);
621 : : }
622 [ + + ]: 417118 : if (id == ProofRule::ITE_ELIM1)
623 : : {
624 [ - + ][ - + ]: 5293 : Assert(children.size() == 1);
[ - - ]
625 [ - + ][ - + ]: 5293 : Assert(args.empty());
[ - - ]
626 [ - + ]: 5293 : if (children[0].getKind() != Kind::ITE)
627 : : {
628 : 0 : return Node::null();
629 : : }
630 : 5293 : return nodeManager()->mkNode(
631 : 5293 : Kind::OR, children[0][0].notNode(), children[0][1]);
632 : : }
633 [ + + ]: 411825 : if (id == ProofRule::ITE_ELIM2)
634 : : {
635 [ - + ][ - + ]: 13536 : Assert(children.size() == 1);
[ - - ]
636 [ - + ][ - + ]: 13536 : Assert(args.empty());
[ - - ]
637 [ - + ]: 13536 : if (children[0].getKind() != Kind::ITE)
638 : : {
639 : 0 : return Node::null();
640 : : }
641 : 13536 : return nodeManager()->mkNode(Kind::OR, children[0][0], children[0][2]);
642 : : }
643 [ + + ]: 398289 : if (id == ProofRule::NOT_ITE_ELIM1)
644 : : {
645 [ - + ][ - + ]: 34 : Assert(children.size() == 1);
[ - - ]
646 [ - + ][ - + ]: 34 : Assert(args.empty());
[ - - ]
647 : 34 : if (children[0].getKind() != Kind::NOT
648 [ + - ][ - + ]: 68 : || children[0][0].getKind() != Kind::ITE)
[ + - ][ - + ]
[ - - ]
649 : : {
650 : 0 : return Node::null();
651 : : }
652 : 102 : return nodeManager()->mkNode(
653 [ + + ][ - - ]: 102 : Kind::OR, {children[0][0][0].notNode(), children[0][0][1].notNode()});
654 : : }
655 [ + + ]: 398255 : if (id == ProofRule::NOT_ITE_ELIM2)
656 : : {
657 [ - + ][ - + ]: 34 : Assert(children.size() == 1);
[ - - ]
658 [ - + ][ - + ]: 34 : Assert(args.empty());
[ - - ]
659 : 34 : if (children[0].getKind() != Kind::NOT
660 [ + - ][ - + ]: 68 : || children[0][0].getKind() != Kind::ITE)
[ + - ][ - + ]
[ - - ]
661 : : {
662 : 0 : return Node::null();
663 : : }
664 : 34 : return nodeManager()->mkNode(
665 : 34 : Kind::OR, children[0][0][0], children[0][0][2].notNode());
666 : : }
667 : : // De Morgan
668 [ + + ]: 398221 : if (id == ProofRule::NOT_AND)
669 : : {
670 [ - + ][ - + ]: 178862 : Assert(children.size() == 1);
[ - - ]
671 [ - + ][ - + ]: 178862 : Assert(args.empty());
[ - - ]
672 : 178862 : if (children[0].getKind() != Kind::NOT
673 [ + - ][ - + ]: 357724 : || children[0][0].getKind() != Kind::AND)
[ + - ][ - + ]
[ - - ]
674 : : {
675 : 0 : return Node::null();
676 : : }
677 : 178862 : std::vector<Node> disjuncts;
678 [ + + ]: 899597 : for (std::size_t i = 0, size = children[0][0].getNumChildren(); i < size;
679 : : ++i)
680 : : {
681 : 720735 : disjuncts.push_back(children[0][0][i].notNode());
682 : : }
683 : 178862 : return nodeManager()->mkNode(Kind::OR, disjuncts);
684 : 178862 : }
685 : : // valid clauses rules for Tseitin CNF transformation
686 [ + + ]: 219359 : if (id == ProofRule::CNF_AND_POS)
687 : : {
688 [ - + ][ - + ]: 71332 : Assert(children.empty());
[ - - ]
689 [ - + ][ - + ]: 71332 : Assert(args.size() == 2);
[ - - ]
690 : : uint32_t i;
691 [ + - ][ - + ]: 71332 : if (args[0].getKind() != Kind::AND || !getUInt32(args[1], i))
[ + - ][ - + ]
[ - - ]
692 : : {
693 : 0 : return Node::null();
694 : : }
695 [ - + ]: 71332 : if (i >= args[0].getNumChildren())
696 : : {
697 : 0 : return Node::null();
698 : : }
699 : 71332 : return nodeManager()->mkNode(Kind::OR, args[0].notNode(), args[0][i]);
700 : : }
701 [ + + ]: 148027 : if (id == ProofRule::CNF_AND_NEG)
702 : : {
703 [ - + ][ - + ]: 50797 : Assert(children.empty());
[ - - ]
704 [ - + ][ - + ]: 50797 : Assert(args.size() == 1);
[ - - ]
705 [ - + ]: 50797 : if (args[0].getKind() != Kind::AND)
706 : : {
707 : 0 : return Node::null();
708 : : }
709 : 152391 : std::vector<Node> disjuncts{args[0]};
710 [ + + ]: 298218 : for (unsigned i = 0, size = args[0].getNumChildren(); i < size; ++i)
711 : : {
712 : 247421 : disjuncts.push_back(args[0][i].notNode());
713 : : }
714 : 50797 : return nodeManager()->mkNode(Kind::OR, disjuncts);
715 : 50797 : }
716 [ + + ]: 97230 : if (id == ProofRule::CNF_OR_POS)
717 : : {
718 [ - + ][ - + ]: 15522 : Assert(children.empty());
[ - - ]
719 [ - + ][ - + ]: 15522 : Assert(args.size() == 1);
[ - - ]
720 [ - + ]: 15522 : if (args[0].getKind() != Kind::OR)
721 : : {
722 : 0 : return Node::null();
723 : : }
724 : 46566 : std::vector<Node> disjuncts{args[0].notNode()};
725 [ + + ]: 1132676 : for (unsigned i = 0, size = args[0].getNumChildren(); i < size; ++i)
726 : : {
727 : 1117154 : disjuncts.push_back(args[0][i]);
728 : : }
729 : 15522 : return nodeManager()->mkNode(Kind::OR, disjuncts);
730 : 15522 : }
731 [ + + ]: 81708 : if (id == ProofRule::CNF_OR_NEG)
732 : : {
733 [ - + ][ - + ]: 43227 : Assert(children.empty());
[ - - ]
734 [ - + ][ - + ]: 43227 : Assert(args.size() == 2);
[ - - ]
735 : : uint32_t i;
736 [ + - ][ - + ]: 43227 : if (args[0].getKind() != Kind::OR || !getUInt32(args[1], i))
[ + - ][ - + ]
[ - - ]
737 : : {
738 : 0 : return Node::null();
739 : : }
740 [ - + ]: 43227 : if (i >= args[0].getNumChildren())
741 : : {
742 : 0 : return Node::null();
743 : : }
744 : 43227 : return nodeManager()->mkNode(Kind::OR, args[0], args[0][i].notNode());
745 : : }
746 [ + + ]: 38481 : if (id == ProofRule::CNF_IMPLIES_POS)
747 : : {
748 [ - + ][ - + ]: 2592 : Assert(children.empty());
[ - - ]
749 [ - + ][ - + ]: 2592 : Assert(args.size() == 1);
[ - - ]
750 [ - + ]: 2592 : if (args[0].getKind() != Kind::IMPLIES)
751 : : {
752 : 0 : return Node::null();
753 : : }
754 : : std::vector<Node> disjuncts{
755 : 15552 : args[0].notNode(), args[0][0].notNode(), args[0][1]};
756 : 2592 : return nodeManager()->mkNode(Kind::OR, disjuncts);
757 : 2592 : }
758 [ + + ]: 35889 : if (id == ProofRule::CNF_IMPLIES_NEG1)
759 : : {
760 [ - + ][ - + ]: 393 : Assert(children.empty());
[ - - ]
761 [ - + ][ - + ]: 393 : Assert(args.size() == 1);
[ - - ]
762 [ - + ]: 393 : if (args[0].getKind() != Kind::IMPLIES)
763 : : {
764 : 0 : return Node::null();
765 : : }
766 : 1572 : std::vector<Node> disjuncts{args[0], args[0][0]};
767 : 393 : return nodeManager()->mkNode(Kind::OR, disjuncts);
768 : 393 : }
769 [ + + ]: 35496 : if (id == ProofRule::CNF_IMPLIES_NEG2)
770 : : {
771 [ - + ][ - + ]: 2116 : Assert(children.empty());
[ - - ]
772 [ - + ][ - + ]: 2116 : Assert(args.size() == 1);
[ - - ]
773 [ - + ]: 2116 : if (args[0].getKind() != Kind::IMPLIES)
774 : : {
775 : 0 : return Node::null();
776 : : }
777 : 10580 : std::vector<Node> disjuncts{args[0], args[0][1].notNode()};
778 : 2116 : return nodeManager()->mkNode(Kind::OR, disjuncts);
779 : 2116 : }
780 [ + + ]: 33380 : if (id == ProofRule::CNF_EQUIV_POS1)
781 : : {
782 [ - + ][ - + ]: 2336 : Assert(children.empty());
[ - - ]
783 [ - + ][ - + ]: 2336 : Assert(args.size() == 1);
[ - - ]
784 [ - + ]: 2336 : if (args[0].getKind() != Kind::EQUAL)
785 : : {
786 : 0 : return Node::null();
787 : : }
788 : : std::vector<Node> disjuncts{
789 : 14016 : args[0].notNode(), args[0][0].notNode(), args[0][1]};
790 : 2336 : return nodeManager()->mkNode(Kind::OR, disjuncts);
791 : 2336 : }
792 [ + + ]: 31044 : if (id == ProofRule::CNF_EQUIV_POS2)
793 : : {
794 [ - + ][ - + ]: 2274 : Assert(children.empty());
[ - - ]
795 [ - + ][ - + ]: 2274 : Assert(args.size() == 1);
[ - - ]
796 [ - + ]: 2274 : if (args[0].getKind() != Kind::EQUAL)
797 : : {
798 : 0 : return Node::null();
799 : : }
800 : : std::vector<Node> disjuncts{
801 : 13644 : args[0].notNode(), args[0][0], args[0][1].notNode()};
802 : 2274 : return nodeManager()->mkNode(Kind::OR, disjuncts);
803 : 2274 : }
804 [ + + ]: 28770 : if (id == ProofRule::CNF_EQUIV_NEG1)
805 : : {
806 [ - + ][ - + ]: 2326 : Assert(children.empty());
[ - - ]
807 [ - + ][ - + ]: 2326 : Assert(args.size() == 1);
[ - - ]
808 [ - + ]: 2326 : if (args[0].getKind() != Kind::EQUAL)
809 : : {
810 : 0 : return Node::null();
811 : : }
812 : 11630 : std::vector<Node> disjuncts{args[0], args[0][0], args[0][1]};
813 : 2326 : return nodeManager()->mkNode(Kind::OR, disjuncts);
814 : 2326 : }
815 [ + + ]: 26444 : if (id == ProofRule::CNF_EQUIV_NEG2)
816 : : {
817 [ - + ][ - + ]: 4470 : Assert(children.empty());
[ - - ]
818 [ - + ][ - + ]: 4470 : Assert(args.size() == 1);
[ - - ]
819 [ - + ]: 4470 : if (args[0].getKind() != Kind::EQUAL)
820 : : {
821 : 0 : return Node::null();
822 : : }
823 : : std::vector<Node> disjuncts{
824 : 26820 : args[0], args[0][0].notNode(), args[0][1].notNode()};
825 : 4470 : return nodeManager()->mkNode(Kind::OR, disjuncts);
826 : 4470 : }
827 [ + + ]: 21974 : if (id == ProofRule::CNF_XOR_POS1)
828 : : {
829 [ - + ][ - + ]: 2788 : Assert(children.empty());
[ - - ]
830 [ - + ][ - + ]: 2788 : Assert(args.size() == 1);
[ - - ]
831 [ - + ]: 2788 : if (args[0].getKind() != Kind::XOR)
832 : : {
833 : 0 : return Node::null();
834 : : }
835 : 13940 : std::vector<Node> disjuncts{args[0].notNode(), args[0][0], args[0][1]};
836 : 2788 : return nodeManager()->mkNode(Kind::OR, disjuncts);
837 : 2788 : }
838 [ + + ]: 19186 : if (id == ProofRule::CNF_XOR_POS2)
839 : : {
840 [ - + ][ - + ]: 1560 : Assert(children.empty());
[ - - ]
841 [ - + ][ - + ]: 1560 : Assert(args.size() == 1);
[ - - ]
842 [ - + ]: 1560 : if (args[0].getKind() != Kind::XOR)
843 : : {
844 : 0 : return Node::null();
845 : : }
846 : : std::vector<Node> disjuncts{
847 : 9360 : args[0].notNode(), args[0][0].notNode(), args[0][1].notNode()};
848 : 1560 : return nodeManager()->mkNode(Kind::OR, disjuncts);
849 : 1560 : }
850 [ + + ]: 17626 : if (id == ProofRule::CNF_XOR_NEG1)
851 : : {
852 [ - + ][ - + ]: 1964 : Assert(children.empty());
[ - - ]
853 [ - + ][ - + ]: 1964 : Assert(args.size() == 1);
[ - - ]
854 [ - + ]: 1964 : if (args[0].getKind() != Kind::XOR)
855 : : {
856 : 0 : return Node::null();
857 : : }
858 : 11784 : std::vector<Node> disjuncts{args[0], args[0][0].notNode(), args[0][1]};
859 : 1964 : return nodeManager()->mkNode(Kind::OR, disjuncts);
860 : 1964 : }
861 [ + + ]: 15662 : if (id == ProofRule::CNF_XOR_NEG2)
862 : : {
863 [ - + ][ - + ]: 1714 : Assert(children.empty());
[ - - ]
864 [ - + ][ - + ]: 1714 : Assert(args.size() == 1);
[ - - ]
865 [ - + ]: 1714 : if (args[0].getKind() != Kind::XOR)
866 : : {
867 : 0 : return Node::null();
868 : : }
869 : 10284 : std::vector<Node> disjuncts{args[0], args[0][0], args[0][1].notNode()};
870 : 1714 : return nodeManager()->mkNode(Kind::OR, disjuncts);
871 : 1714 : }
872 [ + + ]: 13948 : if (id == ProofRule::CNF_ITE_POS1)
873 : : {
874 [ - + ][ - + ]: 2504 : Assert(children.empty());
[ - - ]
875 [ - + ][ - + ]: 2504 : Assert(args.size() == 1);
[ - - ]
876 [ - + ]: 2504 : if (args[0].getKind() != Kind::ITE)
877 : : {
878 : 0 : return Node::null();
879 : : }
880 : : std::vector<Node> disjuncts{
881 : 15024 : args[0].notNode(), args[0][0].notNode(), args[0][1]};
882 : 2504 : return nodeManager()->mkNode(Kind::OR, disjuncts);
883 : 2504 : }
884 [ + + ]: 11444 : if (id == ProofRule::CNF_ITE_POS2)
885 : : {
886 [ - + ][ - + ]: 2281 : Assert(children.empty());
[ - - ]
887 [ - + ][ - + ]: 2281 : Assert(args.size() == 1);
[ - - ]
888 [ - + ]: 2281 : if (args[0].getKind() != Kind::ITE)
889 : : {
890 : 0 : return Node::null();
891 : : }
892 : 11405 : std::vector<Node> disjuncts{args[0].notNode(), args[0][0], args[0][2]};
893 : 2281 : return nodeManager()->mkNode(Kind::OR, disjuncts);
894 : 2281 : }
895 [ + + ]: 9163 : if (id == ProofRule::CNF_ITE_POS3)
896 : : {
897 [ - + ][ - + ]: 2656 : Assert(children.empty());
[ - - ]
898 [ - + ][ - + ]: 2656 : Assert(args.size() == 1);
[ - - ]
899 [ - + ]: 2656 : if (args[0].getKind() != Kind::ITE)
900 : : {
901 : 0 : return Node::null();
902 : : }
903 : 13280 : std::vector<Node> disjuncts{args[0].notNode(), args[0][1], args[0][2]};
904 : 2656 : return nodeManager()->mkNode(Kind::OR, disjuncts);
905 : 2656 : }
906 [ + + ]: 6507 : if (id == ProofRule::CNF_ITE_NEG1)
907 : : {
908 [ - + ][ - + ]: 3124 : Assert(children.empty());
[ - - ]
909 [ - + ][ - + ]: 3124 : Assert(args.size() == 1);
[ - - ]
910 [ - + ]: 3124 : if (args[0].getKind() != Kind::ITE)
911 : : {
912 : 0 : return Node::null();
913 : : }
914 : : std::vector<Node> disjuncts{
915 : 18744 : args[0], args[0][0].notNode(), args[0][1].notNode()};
916 : 3124 : return nodeManager()->mkNode(Kind::OR, disjuncts);
917 : 3124 : }
918 [ + + ]: 3383 : if (id == ProofRule::CNF_ITE_NEG2)
919 : : {
920 [ - + ][ - + ]: 1701 : Assert(children.empty());
[ - - ]
921 [ - + ][ - + ]: 1701 : Assert(args.size() == 1);
[ - - ]
922 [ - + ]: 1701 : if (args[0].getKind() != Kind::ITE)
923 : : {
924 : 0 : return Node::null();
925 : : }
926 : 10206 : std::vector<Node> disjuncts{args[0], args[0][0], args[0][2].notNode()};
927 : 1701 : return nodeManager()->mkNode(Kind::OR, disjuncts);
928 : 1701 : }
929 [ + + ]: 1682 : if (id == ProofRule::CNF_ITE_NEG3)
930 : : {
931 [ - + ][ - + ]: 1508 : Assert(children.empty());
[ - - ]
932 [ - + ][ - + ]: 1508 : Assert(args.size() == 1);
[ - - ]
933 [ - + ]: 1508 : if (args[0].getKind() != Kind::ITE)
934 : : {
935 : 0 : return Node::null();
936 : : }
937 : : std::vector<Node> disjuncts{
938 : 9048 : args[0], args[0][1].notNode(), args[0][2].notNode()};
939 : 1508 : return nodeManager()->mkNode(Kind::OR, disjuncts);
940 : 1508 : }
941 [ - + ][ - - ]: 174 : if (id == ProofRule::SAT_REFUTATION || id == ProofRule::DRAT_REFUTATION
942 [ - - ]: 0 : || id == ProofRule::SAT_EXTERNAL_PROVE)
943 : : {
944 [ - + ][ - - ]: 174 : Assert(args.size()
[ - + ][ - + ]
[ - - ]
945 : : == (id == ProofRule::SAT_REFUTATION
946 : : ? 0
947 : : : (id == ProofRule::SAT_EXTERNAL_PROVE ? 1 : 2)));
948 : 348 : return nodeManager()->mkConst(false);
949 : : }
950 : : // no rule
951 : 0 : return Node::null();
952 : : }
953 : :
954 : : } // namespace booleans
955 : : } // namespace theory
956 : : } // namespace cvc5::internal
|
