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 : 51247 : BoolProofRuleChecker::BoolProofRuleChecker(NodeManager* nm)
23 : 51247 : : ProofRuleChecker(nm)
24 : : {
25 : 51247 : }
26 : :
27 : 19962 : void BoolProofRuleChecker::registerTo(ProofChecker* pc)
28 : : {
29 : 19962 : pc->registerChecker(ProofRule::SPLIT, this);
30 : 19962 : pc->registerChecker(ProofRule::RESOLUTION, this);
31 : 19962 : pc->registerChecker(ProofRule::CHAIN_RESOLUTION, this);
32 : 19962 : pc->registerChecker(ProofRule::CHAIN_M_RESOLUTION, this);
33 : 19962 : pc->registerChecker(ProofRule::FACTORING, this);
34 : 19962 : pc->registerChecker(ProofRule::REORDERING, this);
35 : 19962 : pc->registerChecker(ProofRule::EQ_RESOLVE, this);
36 : 19962 : pc->registerChecker(ProofRule::MODUS_PONENS, this);
37 : 19962 : pc->registerChecker(ProofRule::NOT_NOT_ELIM, this);
38 : 19962 : pc->registerChecker(ProofRule::CONTRA, this);
39 : 19962 : pc->registerChecker(ProofRule::AND_ELIM, this);
40 : 19962 : pc->registerChecker(ProofRule::AND_INTRO, this);
41 : 19962 : pc->registerChecker(ProofRule::NOT_OR_ELIM, this);
42 : 19962 : pc->registerChecker(ProofRule::IMPLIES_ELIM, this);
43 : 19962 : pc->registerChecker(ProofRule::NOT_IMPLIES_ELIM1, this);
44 : 19962 : pc->registerChecker(ProofRule::NOT_IMPLIES_ELIM2, this);
45 : 19962 : pc->registerChecker(ProofRule::EQUIV_ELIM1, this);
46 : 19962 : pc->registerChecker(ProofRule::EQUIV_ELIM2, this);
47 : 19962 : pc->registerChecker(ProofRule::NOT_EQUIV_ELIM1, this);
48 : 19962 : pc->registerChecker(ProofRule::NOT_EQUIV_ELIM2, this);
49 : 19962 : pc->registerChecker(ProofRule::XOR_ELIM1, this);
50 : 19962 : pc->registerChecker(ProofRule::XOR_ELIM2, this);
51 : 19962 : pc->registerChecker(ProofRule::NOT_XOR_ELIM1, this);
52 : 19962 : pc->registerChecker(ProofRule::NOT_XOR_ELIM2, this);
53 : 19962 : pc->registerChecker(ProofRule::ITE_ELIM1, this);
54 : 19962 : pc->registerChecker(ProofRule::ITE_ELIM2, this);
55 : 19962 : pc->registerChecker(ProofRule::NOT_ITE_ELIM1, this);
56 : 19962 : pc->registerChecker(ProofRule::NOT_ITE_ELIM2, this);
57 : 19962 : pc->registerChecker(ProofRule::NOT_AND, this);
58 : 19962 : pc->registerChecker(ProofRule::CNF_AND_POS, this);
59 : 19962 : pc->registerChecker(ProofRule::CNF_AND_NEG, this);
60 : 19962 : pc->registerChecker(ProofRule::CNF_OR_POS, this);
61 : 19962 : pc->registerChecker(ProofRule::CNF_OR_NEG, this);
62 : 19962 : pc->registerChecker(ProofRule::CNF_IMPLIES_POS, this);
63 : 19962 : pc->registerChecker(ProofRule::CNF_IMPLIES_NEG1, this);
64 : 19962 : pc->registerChecker(ProofRule::CNF_IMPLIES_NEG2, this);
65 : 19962 : pc->registerChecker(ProofRule::CNF_EQUIV_POS1, this);
66 : 19962 : pc->registerChecker(ProofRule::CNF_EQUIV_POS2, this);
67 : 19962 : pc->registerChecker(ProofRule::CNF_EQUIV_NEG1, this);
68 : 19962 : pc->registerChecker(ProofRule::CNF_EQUIV_NEG2, this);
69 : 19962 : pc->registerChecker(ProofRule::CNF_XOR_POS1, this);
70 : 19962 : pc->registerChecker(ProofRule::CNF_XOR_POS2, this);
71 : 19962 : pc->registerChecker(ProofRule::CNF_XOR_NEG1, this);
72 : 19962 : pc->registerChecker(ProofRule::CNF_XOR_NEG2, this);
73 : 19962 : pc->registerChecker(ProofRule::CNF_ITE_POS1, this);
74 : 19962 : pc->registerChecker(ProofRule::CNF_ITE_POS2, this);
75 : 19962 : pc->registerChecker(ProofRule::CNF_ITE_POS3, this);
76 : 19962 : pc->registerChecker(ProofRule::CNF_ITE_NEG1, this);
77 : 19962 : pc->registerChecker(ProofRule::CNF_ITE_NEG2, this);
78 : 19962 : pc->registerChecker(ProofRule::CNF_ITE_NEG3, this);
79 : 19962 : pc->registerTrustedChecker(ProofRule::SAT_REFUTATION, this, 1);
80 : 19962 : pc->registerTrustedChecker(ProofRule::DRAT_REFUTATION, this, 1);
81 : 19962 : pc->registerTrustedChecker(ProofRule::SAT_EXTERNAL_PROVE, this, 1);
82 : 19962 : }
83 : :
84 : 4945412 : Node BoolProofRuleChecker::checkInternal(ProofRule id,
85 : : const std::vector<Node>& children,
86 : : const std::vector<Node>& args)
87 : : {
88 [ + + ]: 4945412 : if (id == ProofRule::RESOLUTION)
89 : : {
90 [ - + ][ - + ]: 961816 : Assert(children.size() == 2);
[ - - ]
91 [ - + ][ - + ]: 961816 : Assert(args.size() == 2);
[ - - ]
92 : 961816 : NodeManager* nm = nodeManager();
93 : 961816 : std::vector<Node> disjuncts;
94 [ + + ]: 4809080 : Node pivots[2];
95 [ + + ]: 961816 : if (args[0] == nm->mkConst(true))
96 : : {
97 : 520129 : pivots[0] = args[1];
98 : 520129 : pivots[1] = args[1].notNode();
99 : : }
100 : : else
101 : : {
102 [ - + ][ - + ]: 441687 : Assert(args[0] == nm->mkConst(false));
[ - - ]
103 : 441687 : pivots[0] = args[1].notNode();
104 : 441687 : pivots[1] = args[1];
105 : : }
106 [ + + ]: 2885448 : 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 : 1923632 : std::vector<Node> lits;
112 [ + + ][ + + ]: 1923632 : if (children[i].getKind() == Kind::OR && pivots[i] != children[i])
[ + + ]
113 : : {
114 : 1607662 : lits.insert(lits.end(), children[i].begin(), children[i].end());
115 : : }
116 : : else
117 : : {
118 : 315970 : lits.push_back(children[i]);
119 : : }
120 [ + + ]: 21826047 : for (unsigned j = 0, size = lits.size(); j < size; ++j)
121 : : {
122 [ + + ]: 19902415 : if (pivots[i] != lits[j])
123 : : {
124 : 17978783 : disjuncts.push_back(lits[j]);
125 : : }
126 : : else
127 : : {
128 : : // just eliminate first occurrence
129 : 1923632 : pivots[i] = Node::null();
130 : : }
131 : : }
132 : 1923632 : }
133 : 1923632 : return disjuncts.empty() ? nm->mkConst(false)
134 : 1058285 : : disjuncts.size() == 1 ? disjuncts[0]
135 [ + + ][ + + ]: 2020101 : : nm->mkNode(Kind::OR, disjuncts);
136 [ + + ][ - - ]: 3847264 : }
137 [ + + ]: 3983596 : if (id == ProofRule::FACTORING)
138 : : {
139 [ - + ][ - + ]: 364247 : Assert(children.size() == 1);
[ - - ]
140 [ - + ][ - + ]: 364247 : Assert(args.empty());
[ - - ]
141 [ - + ]: 364247 : if (children[0].getKind() != Kind::OR)
142 : : {
143 : 0 : return Node::null();
144 : : }
145 : : // remove duplicates while keeping the order of children
146 : 364247 : std::unordered_set<TNode> clauseSet;
147 : 364247 : std::vector<Node> disjuncts;
148 : 364247 : unsigned size = children[0].getNumChildren();
149 [ + + ]: 9257771 : for (unsigned i = 0; i < size; ++i)
150 : : {
151 [ + + ]: 8893524 : if (clauseSet.count(children[0][i]))
152 : : {
153 : 2765289 : continue;
154 : : }
155 : 6128235 : disjuncts.push_back(children[0][i]);
156 : 6128235 : clauseSet.insert(children[0][i]);
157 : : }
158 [ - + ]: 364247 : if (disjuncts.size() == size)
159 : : {
160 : 0 : return Node::null();
161 : : }
162 : 364247 : NodeManager* nm = nodeManager();
163 : 364247 : return nm->mkOr(disjuncts);
164 : 364247 : }
165 [ + + ]: 3619349 : if (id == ProofRule::REORDERING)
166 : : {
167 [ - + ][ - + ]: 1224128 : Assert(children.size() == 1);
[ - - ]
168 [ - + ][ - + ]: 1224128 : Assert(args.size() == 1);
[ - - ]
169 : 1224128 : std::unordered_set<Node> clauseSet1, clauseSet2;
170 [ + - ]: 1224128 : if (children[0].getKind() == Kind::OR)
171 : : {
172 : 1224128 : clauseSet1.insert(children[0].begin(), children[0].end());
173 : : }
174 : : else
175 : : {
176 : 0 : clauseSet1.insert(children[0]);
177 : : }
178 [ + - ]: 1224128 : if (args[0].getKind() == Kind::OR)
179 : : {
180 : 1224128 : clauseSet2.insert(args[0].begin(), args[0].end());
181 : : }
182 : : else
183 : : {
184 : 0 : clauseSet2.insert(args[0]);
185 : : }
186 [ - + ]: 1224128 : 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 : 1224128 : return args[0];
193 : 1224128 : }
194 [ + + ]: 2395221 : if (id == ProofRule::CHAIN_RESOLUTION)
195 : : {
196 [ - + ][ - + ]: 372695 : Assert(children.size() > 1);
[ - - ]
197 [ - + ][ - + ]: 372695 : Assert(args.size() == 2);
[ - - ]
198 [ - + ][ - + ]: 372695 : Assert(args[0].getNumChildren() == (children.size() - 1));
[ - - ]
199 [ - + ][ - + ]: 372695 : Assert(args[1].getNumChildren() == (children.size() - 1));
[ - - ]
200 [ + - ]: 372695 : Trace("bool-pfcheck") << "chain_res:\n" << push;
201 : 372695 : NodeManager* nm = nodeManager();
202 : 372695 : Node trueNode = nm->mkConst(true);
203 : 372695 : 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 : 372695 : 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 : 372695 : 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 : 372695 : Node pols = args[0];
226 : 372695 : Node lits = args[1];
227 : 372695 : if (children[0].getKind() != Kind::OR
228 : 745127 : || (pols[0] == trueNode && children[0] == lits[0])
229 : 1117822 : || (pols[0] == falseNode && children[0] == lits[0].notNode()))
230 : : {
231 : 263 : lhsClause.push_back(children[0]);
232 : : }
233 : : else
234 : : {
235 : 372432 : 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 [ + + ]: 3389810 : for (size_t i = 0, argsSize = pols.getNumChildren(); i < argsSize; i++)
240 : : {
241 : : // Polarity determines how the pivot occurs in lhs and rhs
242 [ + + ]: 3017115 : if (pols[i] == trueNode)
243 : : {
244 : 1164101 : lhsElim = lits[i];
245 : 1164101 : rhsElim = lits[i].notNode();
246 : : }
247 : : else
248 : : {
249 [ - + ][ - + ]: 1853014 : Assert(pols[i] == falseNode);
[ - - ]
250 : 1853014 : lhsElim = lits[i].notNode();
251 : 1853014 : rhsElim = lits[i];
252 : : }
253 : : // The index of the child corresponding to the current rhs clause
254 : 3017115 : 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 : 3017115 : if (children[childIndex].getKind() != Kind::OR
258 [ + + ][ + + ]: 3017115 : || children[childIndex] == rhsElim)
[ + + ]
259 : : {
260 : 1553253 : rhsClause.push_back(children[childIndex]);
261 : : }
262 : : else
263 : : {
264 : 1463862 : rhsClause = {children[childIndex].begin(), children[childIndex].end()};
265 : : }
266 [ + - ]: 3017115 : Trace("bool-pfcheck") << i << "-th res link:\n";
267 [ + - ]: 3017115 : Trace("bool-pfcheck") << "\t - lhsClause: " << lhsClause << "\n";
268 [ + - ]: 3017115 : Trace("bool-pfcheck") << "\t\t - lhsElim: " << lhsElim << "\n";
269 [ + - ]: 3017115 : Trace("bool-pfcheck") << "\t - rhsClause: " << rhsClause << "\n";
270 [ + - ]: 3017115 : 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 : 3017115 : auto itlhs = std::find(lhsClause.begin(), lhsClause.end(), lhsElim);
276 [ - + ][ - + ]: 3017115 : AlwaysAssert(itlhs != lhsClause.end());
[ - - ]
277 : 3017115 : lhsClause.erase(itlhs);
278 [ + - ]: 3017115 : Trace("bool-pfcheck") << "\t.. after lhsClause: " << lhsClause << "\n";
279 : 3017115 : auto itrhs = std::find(rhsClause.begin(), rhsClause.end(), rhsElim);
280 [ - + ][ - + ]: 3017115 : AlwaysAssert(itrhs != rhsClause.end());
[ - - ]
281 : 3017115 : lhsClause.insert(lhsClause.end(), rhsClause.begin(), itrhs);
282 : 3017115 : lhsClause.insert(lhsClause.end(), itrhs + 1, rhsClause.end());
283 [ - + ]: 3017115 : 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 : 3017115 : rhsClause.clear();
292 : : }
293 [ + - ]: 745390 : Trace("bool-pfcheck") << "\n resulting clause: " << lhsClause << "\n"
294 : 372695 : << pop;
295 : 372695 : return nm->mkOr(lhsClause);
296 : 372695 : }
297 [ + + ]: 2022526 : if (id == ProofRule::CHAIN_M_RESOLUTION)
298 : : {
299 [ - + ][ - + ]: 277275 : Assert(children.size() > 1);
[ - - ]
300 [ + - ]: 277275 : Trace("bool-pfcheck") << "macro_res: " << args[0] << "\n" << push;
301 : 277275 : NodeManager* nm = nodeManager();
302 : 277275 : Node trueNode = nm->mkConst(true);
303 : 277275 : Node falseNode = nm->mkConst(false);
304 : 277275 : std::vector<Node> lhsClause, rhsClause;
305 : 277275 : Node lhsElim, rhsElim;
306 : 277275 : std::vector<Node> pols, lits;
307 [ - + ][ - + ]: 277275 : Assert(args.size() == 3);
[ - - ]
308 : 277275 : pols.insert(pols.end(), args[1].begin(), args[1].end());
309 : 277275 : lits.insert(lits.end(), args[2].begin(), args[2].end());
310 [ - + ]: 277275 : if (pols.size() != lits.size())
311 : : {
312 : 0 : return Node::null();
313 : : }
314 : 277275 : if (children[0].getKind() != Kind::OR
315 [ + + ][ + - ]: 277058 : || (pols[0] == trueNode && children[0] == lits[0])
316 [ + + ][ + + ]: 831608 : || (pols[0] == falseNode && children[0] == lits[0].notNode()))
[ - + ][ + + ]
[ + + ][ - - ]
317 : : {
318 : 217 : lhsClause.push_back(children[0]);
319 : : }
320 : : else
321 : : {
322 : 277058 : 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 [ + + ]: 4922196 : for (size_t i = 0, argsSize = pols.size(); i < argsSize; i++)
327 : : {
328 : : // Polarity determines how the pivot occurs in lhs and rhs
329 [ + + ]: 4644921 : if (pols[i] == trueNode)
330 : : {
331 : 2781553 : lhsElim = lits[i];
332 : 2781553 : rhsElim = lits[i].notNode();
333 : : }
334 : : else
335 : : {
336 [ - + ][ - + ]: 1863368 : Assert(pols[i] == falseNode);
[ - - ]
337 : 1863368 : lhsElim = lits[i].notNode();
338 : 1863368 : rhsElim = lits[i];
339 : : }
340 : : // The index of the child corresponding to the current rhs clause
341 : 4644921 : 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 : 4644921 : if (children[childIndex].getKind() != Kind::OR
345 [ + + ][ + + ]: 4644921 : || children[childIndex] == rhsElim)
[ + + ]
346 : : {
347 : 637962 : rhsClause.push_back(children[childIndex]);
348 : : }
349 : : else
350 : : {
351 : 4006959 : rhsClause = {children[childIndex].begin(), children[childIndex].end()};
352 : : }
353 [ + - ]: 4644921 : Trace("bool-pfcheck") << i << "-th res link:\n";
354 [ + - ]: 4644921 : Trace("bool-pfcheck") << "\t - lhsClause: " << lhsClause << "\n";
355 [ + - ]: 4644921 : Trace("bool-pfcheck") << "\t\t - lhsElim: " << lhsElim << "\n";
356 [ + - ]: 4644921 : Trace("bool-pfcheck") << "\t - rhsClause: " << rhsClause << "\n";
357 [ + - ]: 4644921 : 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 : 4644921 : lhsClause.erase(std::remove(lhsClause.begin(), lhsClause.end(), lhsElim),
371 : 4644921 : lhsClause.end());
372 [ + + ]: 21316688 : for (const Node& l : rhsClause)
373 : : {
374 : : // only add if literal does not occur in elimination set
375 [ + + ]: 16671767 : if (rhsElim != l)
376 : : {
377 : 12026846 : lhsClause.push_back(l);
378 : : }
379 : : }
380 : 4644921 : rhsClause.clear();
381 : : }
382 : :
383 [ + - ]: 277275 : Trace("bool-pfcheck") << "clause: " << lhsClause << "\n";
384 : : // check that set representation is the same as of the given conclusion
385 : 277275 : std::unordered_set<Node> clauseComputed{lhsClause.begin(), lhsClause.end()};
386 [ + - ]: 277275 : Trace("bool-pfcheck") << "clauseSet: " << clauseComputed << "\n" << pop;
387 [ + + ]: 277275 : if (clauseComputed.empty())
388 : : {
389 : : // conclusion differ
390 [ - + ]: 1923 : if (args[0] != falseNode)
391 : : {
392 : 0 : return Node::null();
393 : : }
394 : 1923 : return args[0];
395 : : }
396 [ + + ]: 275352 : if (clauseComputed.size() == 1)
397 : : {
398 : : // conclusion differ
399 [ - + ]: 87105 : if (args[0] != *clauseComputed.begin())
400 : : {
401 : 0 : return Node::null();
402 : : }
403 : 87105 : 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 [ - + ]: 188247 : if (args[0].getKind() != Kind::OR)
408 : : {
409 : 0 : return Node::null();
410 : : }
411 : 188247 : std::unordered_set<Node> clauseGiven{args[0].begin(), args[0].end()};
412 [ + - ]: 188247 : return clauseComputed == clauseGiven ? args[0] : Node::null();
413 : 277275 : }
414 [ + + ]: 1745251 : 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 [ + + ]: 1706401 : if (id == ProofRule::CONTRA)
421 : : {
422 [ - + ][ - + ]: 68422 : Assert(children.size() == 2);
[ - - ]
423 [ + - ][ + - ]: 68422 : if (children[1].getKind() == Kind::NOT && children[0] == children[1][0])
[ + - ][ + - ]
[ - - ]
424 : : {
425 : 136844 : return nodeManager()->mkConst(false);
426 : : }
427 : 0 : return Node::null();
428 : : }
429 [ + + ]: 1637979 : if (id == ProofRule::EQ_RESOLVE)
430 : : {
431 [ - + ][ - + ]: 418363 : Assert(children.size() == 2);
[ - - ]
432 [ - + ][ - + ]: 418363 : Assert(args.empty());
[ - - ]
433 [ + - ][ - + ]: 418363 : if (children[1].getKind() != Kind::EQUAL || children[0] != children[1][0])
[ + - ][ - + ]
[ - - ]
434 : : {
435 : 0 : return Node::null();
436 : : }
437 : 418363 : return children[1][1];
438 : : }
439 [ + + ]: 1219616 : if (id == ProofRule::MODUS_PONENS)
440 : : {
441 [ - + ][ - + ]: 223795 : Assert(children.size() == 2);
[ - - ]
442 [ - + ][ - + ]: 223795 : Assert(args.empty());
[ - - ]
443 [ + - ][ - + ]: 223795 : if (children[1].getKind() != Kind::IMPLIES || children[0] != children[1][0])
[ + - ][ - + ]
[ - - ]
444 : : {
445 : 0 : return Node::null();
446 : : }
447 : 223795 : return children[1][1];
448 : : }
449 [ + + ]: 995821 : if (id == ProofRule::NOT_NOT_ELIM)
450 : : {
451 [ - + ][ - + ]: 5679 : Assert(children.size() == 1);
[ - - ]
452 [ - + ][ - + ]: 5679 : Assert(args.empty());
[ - - ]
453 : 5679 : if (children[0].getKind() != Kind::NOT
454 [ + - ][ - + ]: 11358 : || children[0][0].getKind() != Kind::NOT)
[ + - ][ - + ]
[ - - ]
455 : : {
456 : 0 : return Node::null();
457 : : }
458 : 5679 : return children[0][0][0];
459 : : }
460 : : // natural deduction rules
461 [ + + ]: 990142 : if (id == ProofRule::AND_ELIM)
462 : : {
463 [ - + ][ - + ]: 201283 : Assert(children.size() == 1);
[ - - ]
464 [ - + ][ - + ]: 201283 : Assert(args.size() == 1);
[ - - ]
465 : : uint32_t i;
466 [ + - ][ - + ]: 201283 : if (children[0].getKind() != Kind::AND || !getUInt32(args[0], i))
[ + - ][ - + ]
[ - - ]
467 : : {
468 : 0 : return Node::null();
469 : : }
470 [ - + ]: 201283 : if (i >= children[0].getNumChildren())
471 : : {
472 : 0 : return Node::null();
473 : : }
474 : 201283 : return children[0][i];
475 : : }
476 [ + + ]: 788859 : if (id == ProofRule::AND_INTRO)
477 : : {
478 [ - + ][ - + ]: 247756 : Assert(children.size() >= 1);
[ - - ]
479 : 247756 : return children.size() == 1 ? children[0]
480 [ - + ]: 247756 : : nodeManager()->mkNode(Kind::AND, children);
481 : : }
482 [ + + ]: 541103 : if (id == ProofRule::NOT_OR_ELIM)
483 : : {
484 [ - + ][ - + ]: 7219 : Assert(children.size() == 1);
[ - - ]
485 [ - + ][ - + ]: 7219 : Assert(args.size() == 1);
[ - - ]
486 : : uint32_t i;
487 : 7219 : if (children[0].getKind() != Kind::NOT
488 : 14438 : || children[0][0].getKind() != Kind::OR || !getUInt32(args[0], i))
489 : : {
490 : 0 : return Node::null();
491 : : }
492 [ - + ]: 7219 : if (i >= children[0][0].getNumChildren())
493 : : {
494 : 0 : return Node::null();
495 : : }
496 : 7219 : return children[0][0][i].notNode();
497 : : }
498 [ + + ]: 533884 : if (id == ProofRule::IMPLIES_ELIM)
499 : : {
500 [ - + ][ - + ]: 60915 : Assert(children.size() == 1);
[ - - ]
501 [ - + ][ - + ]: 60915 : Assert(args.empty());
[ - - ]
502 [ - + ]: 60915 : if (children[0].getKind() != Kind::IMPLIES)
503 : : {
504 : 0 : return Node::null();
505 : : }
506 : 60915 : return nodeManager()->mkNode(
507 : 60915 : Kind::OR, children[0][0].notNode(), children[0][1]);
508 : : }
509 [ + + ]: 472969 : if (id == ProofRule::NOT_IMPLIES_ELIM1)
510 : : {
511 [ - + ][ - + ]: 4063 : Assert(children.size() == 1);
[ - - ]
512 [ - + ][ - + ]: 4063 : Assert(args.empty());
[ - - ]
513 : 4063 : if (children[0].getKind() != Kind::NOT
514 [ + - ][ - + ]: 8126 : || children[0][0].getKind() != Kind::IMPLIES)
[ + - ][ - + ]
[ - - ]
515 : : {
516 : 0 : return Node::null();
517 : : }
518 : 4063 : return children[0][0][0];
519 : : }
520 [ + + ]: 468906 : if (id == ProofRule::NOT_IMPLIES_ELIM2)
521 : : {
522 [ - + ][ - + ]: 1868 : Assert(children.size() == 1);
[ - - ]
523 [ - + ][ - + ]: 1868 : Assert(args.empty());
[ - - ]
524 : 1868 : if (children[0].getKind() != Kind::NOT
525 [ + - ][ - + ]: 3736 : || children[0][0].getKind() != Kind::IMPLIES)
[ + - ][ - + ]
[ - - ]
526 : : {
527 : 0 : return Node::null();
528 : : }
529 : 1868 : return children[0][0][1].notNode();
530 : : }
531 [ + + ]: 467038 : if (id == ProofRule::EQUIV_ELIM1)
532 : : {
533 [ - + ][ - + ]: 33920 : Assert(children.size() == 1);
[ - - ]
534 [ - + ][ - + ]: 33920 : Assert(args.empty());
[ - - ]
535 [ - + ]: 33920 : if (children[0].getKind() != Kind::EQUAL)
536 : : {
537 : 0 : return Node::null();
538 : : }
539 : 33920 : return nodeManager()->mkNode(
540 : 33920 : Kind::OR, children[0][0].notNode(), children[0][1]);
541 : : }
542 [ + + ]: 433118 : if (id == ProofRule::EQUIV_ELIM2)
543 : : {
544 [ - + ][ - + ]: 15384 : Assert(children.size() == 1);
[ - - ]
545 [ - + ][ - + ]: 15384 : Assert(args.empty());
[ - - ]
546 [ - + ]: 15384 : if (children[0].getKind() != Kind::EQUAL)
547 : : {
548 : 0 : return Node::null();
549 : : }
550 : 15384 : return nodeManager()->mkNode(
551 : 15384 : Kind::OR, children[0][0], children[0][1].notNode());
552 : : }
553 [ + + ]: 417734 : if (id == ProofRule::NOT_EQUIV_ELIM1)
554 : : {
555 [ - + ][ - + ]: 615 : Assert(children.size() == 1);
[ - - ]
556 [ - + ][ - + ]: 615 : Assert(args.empty());
[ - - ]
557 : 615 : if (children[0].getKind() != Kind::NOT
558 [ + - ][ - + ]: 1230 : || children[0][0].getKind() != Kind::EQUAL)
[ + - ][ - + ]
[ - - ]
559 : : {
560 : 0 : return Node::null();
561 : : }
562 : 615 : return nodeManager()->mkNode(
563 : 615 : Kind::OR, children[0][0][0], children[0][0][1]);
564 : : }
565 [ + + ]: 417119 : if (id == ProofRule::NOT_EQUIV_ELIM2)
566 : : {
567 [ - + ][ - + ]: 408 : Assert(children.size() == 1);
[ - - ]
568 [ - + ][ - + ]: 408 : Assert(args.empty());
[ - - ]
569 : 408 : if (children[0].getKind() != Kind::NOT
570 [ + - ][ - + ]: 816 : || children[0][0].getKind() != Kind::EQUAL)
[ + - ][ - + ]
[ - - ]
571 : : {
572 : 0 : return Node::null();
573 : : }
574 : 1224 : return nodeManager()->mkNode(
575 [ + + ][ - - ]: 1224 : Kind::OR, {children[0][0][0].notNode(), children[0][0][1].notNode()});
576 : : }
577 [ + + ]: 416711 : 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 [ + + ]: 416627 : 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 [ + + ]: 416525 : 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 [ + + ]: 416462 : 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 [ + + ]: 416391 : if (id == ProofRule::ITE_ELIM1)
623 : : {
624 [ - + ][ - + ]: 5273 : Assert(children.size() == 1);
[ - - ]
625 [ - + ][ - + ]: 5273 : Assert(args.empty());
[ - - ]
626 [ - + ]: 5273 : if (children[0].getKind() != Kind::ITE)
627 : : {
628 : 0 : return Node::null();
629 : : }
630 : 5273 : return nodeManager()->mkNode(
631 : 5273 : Kind::OR, children[0][0].notNode(), children[0][1]);
632 : : }
633 [ + + ]: 411118 : if (id == ProofRule::ITE_ELIM2)
634 : : {
635 [ - + ][ - + ]: 13482 : Assert(children.size() == 1);
[ - - ]
636 [ - + ][ - + ]: 13482 : Assert(args.empty());
[ - - ]
637 [ - + ]: 13482 : if (children[0].getKind() != Kind::ITE)
638 : : {
639 : 0 : return Node::null();
640 : : }
641 : 13482 : return nodeManager()->mkNode(Kind::OR, children[0][0], children[0][2]);
642 : : }
643 [ + + ]: 397636 : 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 [ + + ]: 397602 : 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 [ + + ]: 397568 : if (id == ProofRule::NOT_AND)
669 : : {
670 [ - + ][ - + ]: 178954 : Assert(children.size() == 1);
[ - - ]
671 [ - + ][ - + ]: 178954 : Assert(args.empty());
[ - - ]
672 : 178954 : if (children[0].getKind() != Kind::NOT
673 [ + - ][ - + ]: 357908 : || children[0][0].getKind() != Kind::AND)
[ + - ][ - + ]
[ - - ]
674 : : {
675 : 0 : return Node::null();
676 : : }
677 : 178954 : std::vector<Node> disjuncts;
678 [ + + ]: 900023 : for (std::size_t i = 0, size = children[0][0].getNumChildren(); i < size;
679 : : ++i)
680 : : {
681 : 721069 : disjuncts.push_back(children[0][0][i].notNode());
682 : : }
683 : 178954 : return nodeManager()->mkNode(Kind::OR, disjuncts);
684 : 178954 : }
685 : : // valid clauses rules for Tseitin CNF transformation
686 [ + + ]: 218614 : if (id == ProofRule::CNF_AND_POS)
687 : : {
688 [ - + ][ - + ]: 70920 : Assert(children.empty());
[ - - ]
689 [ - + ][ - + ]: 70920 : Assert(args.size() == 2);
[ - - ]
690 : : uint32_t i;
691 [ + - ][ - + ]: 70920 : if (args[0].getKind() != Kind::AND || !getUInt32(args[1], i))
[ + - ][ - + ]
[ - - ]
692 : : {
693 : 0 : return Node::null();
694 : : }
695 [ - + ]: 70920 : if (i >= args[0].getNumChildren())
696 : : {
697 : 0 : return Node::null();
698 : : }
699 : 70920 : return nodeManager()->mkNode(Kind::OR, args[0].notNode(), args[0][i]);
700 : : }
701 [ + + ]: 147694 : if (id == ProofRule::CNF_AND_NEG)
702 : : {
703 [ - + ][ - + ]: 50664 : Assert(children.empty());
[ - - ]
704 [ - + ][ - + ]: 50664 : Assert(args.size() == 1);
[ - - ]
705 [ - + ]: 50664 : if (args[0].getKind() != Kind::AND)
706 : : {
707 : 0 : return Node::null();
708 : : }
709 : 151992 : std::vector<Node> disjuncts{args[0]};
710 [ + + ]: 297821 : for (unsigned i = 0, size = args[0].getNumChildren(); i < size; ++i)
711 : : {
712 : 247157 : disjuncts.push_back(args[0][i].notNode());
713 : : }
714 : 50664 : return nodeManager()->mkNode(Kind::OR, disjuncts);
715 : 50664 : }
716 [ + + ]: 97030 : if (id == ProofRule::CNF_OR_POS)
717 : : {
718 [ - + ][ - + ]: 15511 : Assert(children.empty());
[ - - ]
719 [ - + ][ - + ]: 15511 : Assert(args.size() == 1);
[ - - ]
720 [ - + ]: 15511 : if (args[0].getKind() != Kind::OR)
721 : : {
722 : 0 : return Node::null();
723 : : }
724 : 46533 : std::vector<Node> disjuncts{args[0].notNode()};
725 [ + + ]: 1132643 : for (unsigned i = 0, size = args[0].getNumChildren(); i < size; ++i)
726 : : {
727 : 1117132 : disjuncts.push_back(args[0][i]);
728 : : }
729 : 15511 : return nodeManager()->mkNode(Kind::OR, disjuncts);
730 : 15511 : }
731 [ + + ]: 81519 : if (id == ProofRule::CNF_OR_NEG)
732 : : {
733 [ - + ][ - + ]: 43206 : Assert(children.empty());
[ - - ]
734 [ - + ][ - + ]: 43206 : Assert(args.size() == 2);
[ - - ]
735 : : uint32_t i;
736 [ + - ][ - + ]: 43206 : if (args[0].getKind() != Kind::OR || !getUInt32(args[1], i))
[ + - ][ - + ]
[ - - ]
737 : : {
738 : 0 : return Node::null();
739 : : }
740 [ - + ]: 43206 : if (i >= args[0].getNumChildren())
741 : : {
742 : 0 : return Node::null();
743 : : }
744 : 43206 : return nodeManager()->mkNode(Kind::OR, args[0], args[0][i].notNode());
745 : : }
746 [ + + ]: 38313 : if (id == ProofRule::CNF_IMPLIES_POS)
747 : : {
748 [ - + ][ - + ]: 2598 : Assert(children.empty());
[ - - ]
749 [ - + ][ - + ]: 2598 : Assert(args.size() == 1);
[ - - ]
750 [ - + ]: 2598 : if (args[0].getKind() != Kind::IMPLIES)
751 : : {
752 : 0 : return Node::null();
753 : : }
754 : : std::vector<Node> disjuncts{
755 : 15588 : args[0].notNode(), args[0][0].notNode(), args[0][1]};
756 : 2598 : return nodeManager()->mkNode(Kind::OR, disjuncts);
757 : 2598 : }
758 [ + + ]: 35715 : if (id == ProofRule::CNF_IMPLIES_NEG1)
759 : : {
760 [ - + ][ - + ]: 421 : Assert(children.empty());
[ - - ]
761 [ - + ][ - + ]: 421 : Assert(args.size() == 1);
[ - - ]
762 [ - + ]: 421 : if (args[0].getKind() != Kind::IMPLIES)
763 : : {
764 : 0 : return Node::null();
765 : : }
766 : 1684 : std::vector<Node> disjuncts{args[0], args[0][0]};
767 : 421 : return nodeManager()->mkNode(Kind::OR, disjuncts);
768 : 421 : }
769 [ + + ]: 35294 : if (id == ProofRule::CNF_IMPLIES_NEG2)
770 : : {
771 [ - + ][ - + ]: 2134 : Assert(children.empty());
[ - - ]
772 [ - + ][ - + ]: 2134 : Assert(args.size() == 1);
[ - - ]
773 [ - + ]: 2134 : if (args[0].getKind() != Kind::IMPLIES)
774 : : {
775 : 0 : return Node::null();
776 : : }
777 : 10670 : std::vector<Node> disjuncts{args[0], args[0][1].notNode()};
778 : 2134 : return nodeManager()->mkNode(Kind::OR, disjuncts);
779 : 2134 : }
780 [ + + ]: 33160 : if (id == ProofRule::CNF_EQUIV_POS1)
781 : : {
782 [ - + ][ - + ]: 2325 : Assert(children.empty());
[ - - ]
783 [ - + ][ - + ]: 2325 : Assert(args.size() == 1);
[ - - ]
784 [ - + ]: 2325 : if (args[0].getKind() != Kind::EQUAL)
785 : : {
786 : 0 : return Node::null();
787 : : }
788 : : std::vector<Node> disjuncts{
789 : 13950 : args[0].notNode(), args[0][0].notNode(), args[0][1]};
790 : 2325 : return nodeManager()->mkNode(Kind::OR, disjuncts);
791 : 2325 : }
792 [ + + ]: 30835 : if (id == ProofRule::CNF_EQUIV_POS2)
793 : : {
794 [ - + ][ - + ]: 2269 : Assert(children.empty());
[ - - ]
795 [ - + ][ - + ]: 2269 : Assert(args.size() == 1);
[ - - ]
796 [ - + ]: 2269 : if (args[0].getKind() != Kind::EQUAL)
797 : : {
798 : 0 : return Node::null();
799 : : }
800 : : std::vector<Node> disjuncts{
801 : 13614 : args[0].notNode(), args[0][0], args[0][1].notNode()};
802 : 2269 : return nodeManager()->mkNode(Kind::OR, disjuncts);
803 : 2269 : }
804 [ + + ]: 28566 : 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 [ + + ]: 26240 : if (id == ProofRule::CNF_EQUIV_NEG2)
816 : : {
817 [ - + ][ - + ]: 4468 : Assert(children.empty());
[ - - ]
818 [ - + ][ - + ]: 4468 : Assert(args.size() == 1);
[ - - ]
819 [ - + ]: 4468 : if (args[0].getKind() != Kind::EQUAL)
820 : : {
821 : 0 : return Node::null();
822 : : }
823 : : std::vector<Node> disjuncts{
824 : 26808 : args[0], args[0][0].notNode(), args[0][1].notNode()};
825 : 4468 : return nodeManager()->mkNode(Kind::OR, disjuncts);
826 : 4468 : }
827 [ + + ]: 21772 : if (id == ProofRule::CNF_XOR_POS1)
828 : : {
829 [ - + ][ - + ]: 2773 : Assert(children.empty());
[ - - ]
830 [ - + ][ - + ]: 2773 : Assert(args.size() == 1);
[ - - ]
831 [ - + ]: 2773 : if (args[0].getKind() != Kind::XOR)
832 : : {
833 : 0 : return Node::null();
834 : : }
835 : 13865 : std::vector<Node> disjuncts{args[0].notNode(), args[0][0], args[0][1]};
836 : 2773 : return nodeManager()->mkNode(Kind::OR, disjuncts);
837 : 2773 : }
838 [ + + ]: 18999 : 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 [ + + ]: 17439 : 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 [ + + ]: 15475 : 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 [ + + ]: 13761 : if (id == ProofRule::CNF_ITE_POS1)
873 : : {
874 [ - + ][ - + ]: 2488 : Assert(children.empty());
[ - - ]
875 [ - + ][ - + ]: 2488 : Assert(args.size() == 1);
[ - - ]
876 [ - + ]: 2488 : if (args[0].getKind() != Kind::ITE)
877 : : {
878 : 0 : return Node::null();
879 : : }
880 : : std::vector<Node> disjuncts{
881 : 14928 : args[0].notNode(), args[0][0].notNode(), args[0][1]};
882 : 2488 : return nodeManager()->mkNode(Kind::OR, disjuncts);
883 : 2488 : }
884 [ + + ]: 11273 : if (id == ProofRule::CNF_ITE_POS2)
885 : : {
886 [ - + ][ - + ]: 2189 : Assert(children.empty());
[ - - ]
887 [ - + ][ - + ]: 2189 : Assert(args.size() == 1);
[ - - ]
888 [ - + ]: 2189 : if (args[0].getKind() != Kind::ITE)
889 : : {
890 : 0 : return Node::null();
891 : : }
892 : 10945 : std::vector<Node> disjuncts{args[0].notNode(), args[0][0], args[0][2]};
893 : 2189 : return nodeManager()->mkNode(Kind::OR, disjuncts);
894 : 2189 : }
895 [ + + ]: 9084 : if (id == ProofRule::CNF_ITE_POS3)
896 : : {
897 [ - + ][ - + ]: 2670 : Assert(children.empty());
[ - - ]
898 [ - + ][ - + ]: 2670 : Assert(args.size() == 1);
[ - - ]
899 [ - + ]: 2670 : if (args[0].getKind() != Kind::ITE)
900 : : {
901 : 0 : return Node::null();
902 : : }
903 : 13350 : std::vector<Node> disjuncts{args[0].notNode(), args[0][1], args[0][2]};
904 : 2670 : return nodeManager()->mkNode(Kind::OR, disjuncts);
905 : 2670 : }
906 [ + + ]: 6414 : if (id == ProofRule::CNF_ITE_NEG1)
907 : : {
908 [ - + ][ - + ]: 3108 : Assert(children.empty());
[ - - ]
909 [ - + ][ - + ]: 3108 : Assert(args.size() == 1);
[ - - ]
910 [ - + ]: 3108 : if (args[0].getKind() != Kind::ITE)
911 : : {
912 : 0 : return Node::null();
913 : : }
914 : : std::vector<Node> disjuncts{
915 : 18648 : args[0], args[0][0].notNode(), args[0][1].notNode()};
916 : 3108 : return nodeManager()->mkNode(Kind::OR, disjuncts);
917 : 3108 : }
918 [ + + ]: 3306 : if (id == ProofRule::CNF_ITE_NEG2)
919 : : {
920 [ - + ][ - + ]: 1609 : Assert(children.empty());
[ - - ]
921 [ - + ][ - + ]: 1609 : Assert(args.size() == 1);
[ - - ]
922 [ - + ]: 1609 : if (args[0].getKind() != Kind::ITE)
923 : : {
924 : 0 : return Node::null();
925 : : }
926 : 9654 : std::vector<Node> disjuncts{args[0], args[0][0], args[0][2].notNode()};
927 : 1609 : return nodeManager()->mkNode(Kind::OR, disjuncts);
928 : 1609 : }
929 [ + + ]: 1697 : if (id == ProofRule::CNF_ITE_NEG3)
930 : : {
931 [ - + ][ - + ]: 1524 : Assert(children.empty());
[ - - ]
932 [ - + ][ - + ]: 1524 : Assert(args.size() == 1);
[ - - ]
933 [ - + ]: 1524 : if (args[0].getKind() != Kind::ITE)
934 : : {
935 : 0 : return Node::null();
936 : : }
937 : : std::vector<Node> disjuncts{
938 : 9144 : args[0], args[0][1].notNode(), args[0][2].notNode()};
939 : 1524 : return nodeManager()->mkNode(Kind::OR, disjuncts);
940 : 1524 : }
941 [ - + ][ - - ]: 173 : if (id == ProofRule::SAT_REFUTATION || id == ProofRule::DRAT_REFUTATION
942 [ - - ]: 0 : || id == ProofRule::SAT_EXTERNAL_PROVE)
943 : : {
944 [ - + ][ - - ]: 173 : Assert(args.size()
[ - + ][ - + ]
[ - - ]
945 : : == (id == ProofRule::SAT_REFUTATION
946 : : ? 0
947 : : : (id == ProofRule::SAT_EXTERNAL_PROVE ? 1 : 2)));
948 : 346 : 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
|
