Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Haniel Barbosa, Hans-Joerg Schurr, Aina Niemetz
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
8 : : * in the top-level source directory and their institutional affiliations.
9 : : * All rights reserved. See the file COPYING in the top-level source
10 : : * directory for licensing information.
11 : : * ****************************************************************************
12 : : *
13 : : * Implementation of equality proof checker.
14 : : */
15 : :
16 : : #include "theory/booleans/proof_checker.h"
17 : : #include "expr/skolem_manager.h"
18 : : #include "theory/rewriter.h"
19 : :
20 : : namespace cvc5::internal {
21 : : namespace theory {
22 : : namespace booleans {
23 : :
24 : 49837 : BoolProofRuleChecker::BoolProofRuleChecker(NodeManager* nm)
25 : 49837 : : ProofRuleChecker(nm)
26 : : {
27 : 49837 : }
28 : :
29 : 19203 : void BoolProofRuleChecker::registerTo(ProofChecker* pc)
30 : : {
31 : 19203 : pc->registerChecker(ProofRule::SPLIT, this);
32 : 19203 : pc->registerChecker(ProofRule::RESOLUTION, this);
33 : 19203 : pc->registerChecker(ProofRule::CHAIN_RESOLUTION, this);
34 : 19203 : pc->registerTrustedChecker(ProofRule::MACRO_RESOLUTION_TRUST, this, 3);
35 : 19203 : pc->registerChecker(ProofRule::MACRO_RESOLUTION, this);
36 : 19203 : pc->registerChecker(ProofRule::FACTORING, this);
37 : 19203 : pc->registerChecker(ProofRule::REORDERING, this);
38 : 19203 : pc->registerChecker(ProofRule::EQ_RESOLVE, this);
39 : 19203 : pc->registerChecker(ProofRule::MODUS_PONENS, this);
40 : 19203 : pc->registerChecker(ProofRule::NOT_NOT_ELIM, this);
41 : 19203 : pc->registerChecker(ProofRule::CONTRA, this);
42 : 19203 : pc->registerChecker(ProofRule::AND_ELIM, this);
43 : 19203 : pc->registerChecker(ProofRule::AND_INTRO, this);
44 : 19203 : pc->registerChecker(ProofRule::NOT_OR_ELIM, this);
45 : 19203 : pc->registerChecker(ProofRule::IMPLIES_ELIM, this);
46 : 19203 : pc->registerChecker(ProofRule::NOT_IMPLIES_ELIM1, this);
47 : 19203 : pc->registerChecker(ProofRule::NOT_IMPLIES_ELIM2, this);
48 : 19203 : pc->registerChecker(ProofRule::EQUIV_ELIM1, this);
49 : 19203 : pc->registerChecker(ProofRule::EQUIV_ELIM2, this);
50 : 19203 : pc->registerChecker(ProofRule::NOT_EQUIV_ELIM1, this);
51 : 19203 : pc->registerChecker(ProofRule::NOT_EQUIV_ELIM2, this);
52 : 19203 : pc->registerChecker(ProofRule::XOR_ELIM1, this);
53 : 19203 : pc->registerChecker(ProofRule::XOR_ELIM2, this);
54 : 19203 : pc->registerChecker(ProofRule::NOT_XOR_ELIM1, this);
55 : 19203 : pc->registerChecker(ProofRule::NOT_XOR_ELIM2, this);
56 : 19203 : pc->registerChecker(ProofRule::ITE_ELIM1, this);
57 : 19203 : pc->registerChecker(ProofRule::ITE_ELIM2, this);
58 : 19203 : pc->registerChecker(ProofRule::NOT_ITE_ELIM1, this);
59 : 19203 : pc->registerChecker(ProofRule::NOT_ITE_ELIM2, this);
60 : 19203 : pc->registerChecker(ProofRule::NOT_AND, this);
61 : 19203 : pc->registerChecker(ProofRule::CNF_AND_POS, this);
62 : 19203 : pc->registerChecker(ProofRule::CNF_AND_NEG, this);
63 : 19203 : pc->registerChecker(ProofRule::CNF_OR_POS, this);
64 : 19203 : pc->registerChecker(ProofRule::CNF_OR_NEG, this);
65 : 19203 : pc->registerChecker(ProofRule::CNF_IMPLIES_POS, this);
66 : 19203 : pc->registerChecker(ProofRule::CNF_IMPLIES_NEG1, this);
67 : 19203 : pc->registerChecker(ProofRule::CNF_IMPLIES_NEG2, this);
68 : 19203 : pc->registerChecker(ProofRule::CNF_EQUIV_POS1, this);
69 : 19203 : pc->registerChecker(ProofRule::CNF_EQUIV_POS2, this);
70 : 19203 : pc->registerChecker(ProofRule::CNF_EQUIV_NEG1, this);
71 : 19203 : pc->registerChecker(ProofRule::CNF_EQUIV_NEG2, this);
72 : 19203 : pc->registerChecker(ProofRule::CNF_XOR_POS1, this);
73 : 19203 : pc->registerChecker(ProofRule::CNF_XOR_POS2, this);
74 : 19203 : pc->registerChecker(ProofRule::CNF_XOR_NEG1, this);
75 : 19203 : pc->registerChecker(ProofRule::CNF_XOR_NEG2, this);
76 : 19203 : pc->registerChecker(ProofRule::CNF_ITE_POS1, this);
77 : 19203 : pc->registerChecker(ProofRule::CNF_ITE_POS2, this);
78 : 19203 : pc->registerChecker(ProofRule::CNF_ITE_POS3, this);
79 : 19203 : pc->registerChecker(ProofRule::CNF_ITE_NEG1, this);
80 : 19203 : pc->registerChecker(ProofRule::CNF_ITE_NEG2, this);
81 : 19203 : pc->registerChecker(ProofRule::CNF_ITE_NEG3, this);
82 : 19203 : pc->registerTrustedChecker(ProofRule::SAT_REFUTATION, this, 1);
83 : 19203 : pc->registerTrustedChecker(ProofRule::DRAT_REFUTATION, this, 1);
84 : 19203 : pc->registerTrustedChecker(ProofRule::SAT_EXTERNAL_PROVE, this, 1);
85 : 19203 : }
86 : :
87 : 8967660 : Node BoolProofRuleChecker::checkInternal(ProofRule id,
88 : : const std::vector<Node>& children,
89 : : const std::vector<Node>& args)
90 : : {
91 [ + + ]: 8967660 : if (id == ProofRule::RESOLUTION)
92 : : {
93 [ - + ][ - + ]: 770158 : Assert(children.size() == 2);
[ - - ]
94 [ - + ][ - + ]: 770158 : Assert(args.size() == 2);
[ - - ]
95 : 770158 : NodeManager* nm = nodeManager();
96 : 1540320 : std::vector<Node> disjuncts;
97 [ + + ][ + + ]: 4620950 : Node pivots[2];
[ - - ]
98 [ + + ]: 770158 : if (args[0] == nm->mkConst(true))
99 : : {
100 : 405103 : pivots[0] = args[1];
101 : 405103 : pivots[1] = args[1].notNode();
102 : : }
103 : : else
104 : : {
105 [ - + ][ - + ]: 365055 : Assert(args[0] == nm->mkConst(false));
[ - - ]
106 : 365055 : pivots[0] = args[1].notNode();
107 : 365055 : pivots[1] = args[1];
108 : : }
109 [ + + ]: 2310470 : for (unsigned i = 0; i < 2; ++i)
110 : : {
111 : : // determine whether the clause is a singleton for effects of resolution,
112 : : // which is the case if it's not an OR node or it is an OR node but it is
113 : : // equal to the pivot
114 : 3080630 : std::vector<Node> lits;
115 [ + + ][ + + ]: 1540320 : if (children[i].getKind() == Kind::OR && pivots[i] != children[i])
[ + + ]
116 : : {
117 : 1258880 : lits.insert(lits.end(), children[i].begin(), children[i].end());
118 : : }
119 : : else
120 : : {
121 : 281441 : lits.push_back(children[i]);
122 : : }
123 [ + + ]: 15083600 : for (unsigned j = 0, size = lits.size(); j < size; ++j)
124 : : {
125 [ + + ]: 13543300 : if (pivots[i] != lits[j])
126 : : {
127 : 12003000 : disjuncts.push_back(lits[j]);
128 : : }
129 : : else
130 : : {
131 : : // just eliminate first occurrence
132 : 1540320 : pivots[i] = Node::null();
133 : : }
134 : : }
135 : : }
136 : 1540320 : return disjuncts.empty() ? nm->mkConst(false)
137 : 860999 : : disjuncts.size() == 1 ? disjuncts[0]
138 [ + + ][ + + ]: 1631160 : : nm->mkNode(Kind::OR, disjuncts);
139 : : }
140 [ + + ]: 8197500 : if (id == ProofRule::FACTORING)
141 : : {
142 [ - + ][ - + ]: 1639300 : Assert(children.size() == 1);
[ - - ]
143 [ - + ][ - + ]: 1639300 : Assert(args.empty());
[ - - ]
144 [ - + ]: 1639300 : if (children[0].getKind() != Kind::OR)
145 : : {
146 : 0 : return Node::null();
147 : : }
148 : : // remove duplicates while keeping the order of children
149 : 3278600 : std::unordered_set<TNode> clauseSet;
150 : 3278600 : std::vector<Node> disjuncts;
151 : 1639300 : unsigned size = children[0].getNumChildren();
152 [ + + ]: 56350600 : for (unsigned i = 0; i < size; ++i)
153 : : {
154 [ + + ]: 54711300 : if (clauseSet.count(children[0][i]))
155 : : {
156 : 10908200 : continue;
157 : : }
158 : 43803100 : disjuncts.push_back(children[0][i]);
159 : 43803100 : clauseSet.insert(children[0][i]);
160 : : }
161 [ - + ]: 1639300 : if (disjuncts.size() == size)
162 : : {
163 : 0 : return Node::null();
164 : : }
165 : 1639300 : NodeManager* nm = nodeManager();
166 : 1639300 : return nm->mkOr(disjuncts);
167 : : }
168 [ + + ]: 6558200 : if (id == ProofRule::REORDERING)
169 : : {
170 [ - + ][ - + ]: 2341460 : Assert(children.size() == 1);
[ - - ]
171 [ - + ][ - + ]: 2341460 : Assert(args.size() == 1);
[ - - ]
172 : 4682920 : std::unordered_set<Node> clauseSet1, clauseSet2;
173 [ + - ]: 2341460 : if (children[0].getKind() == Kind::OR)
174 : : {
175 : 2341460 : clauseSet1.insert(children[0].begin(), children[0].end());
176 : : }
177 : : else
178 : : {
179 : 0 : clauseSet1.insert(children[0]);
180 : : }
181 [ + - ]: 2341460 : if (args[0].getKind() == Kind::OR)
182 : : {
183 : 2341460 : clauseSet2.insert(args[0].begin(), args[0].end());
184 : : }
185 : : else
186 : : {
187 : 0 : clauseSet2.insert(args[0]);
188 : : }
189 [ - + ]: 2341460 : if (clauseSet1 != clauseSet2)
190 : : {
191 [ - - ]: 0 : Trace("bool-pfcheck") << id << ": clause set1: " << clauseSet1 << "\n"
192 : 0 : << id << ": clause set2: " << clauseSet2 << "\n";
193 : 0 : return Node::null();
194 : : }
195 : 2341460 : return args[0];
196 : : }
197 [ + + ]: 4216750 : if (id == ProofRule::CHAIN_RESOLUTION)
198 : : {
199 [ - + ][ - + ]: 1865000 : Assert(children.size() > 1);
[ - - ]
200 [ - + ][ - + ]: 1865000 : Assert(args.size() == 2);
[ - - ]
201 [ - + ][ - + ]: 1865000 : Assert(args[0].getNumChildren() == (children.size() - 1));
[ - - ]
202 [ - + ][ - + ]: 1865000 : Assert(args[1].getNumChildren() == (children.size() - 1));
[ - - ]
203 [ + - ]: 1865000 : Trace("bool-pfcheck") << "chain_res:\n" << push;
204 : 1865000 : NodeManager* nm = nodeManager();
205 : 3730000 : Node trueNode = nm->mkConst(true);
206 : 3730000 : Node falseNode = nm->mkConst(false);
207 : : // The lhs and rhs clauses in a binary resolution step, respectively. Since
208 : : // children correspond to the premises in the resolution chain, the first
209 : : // lhs clause is the first premise, the first rhs clause is the second
210 : : // premise. Each subsequent lhs clause will be the result of the previous
211 : : // binary resolution step in the chain, while each subsequent rhs clause
212 : : // will be respectively the second, third etc premises.
213 : 3730000 : std::vector<Node> lhsClause, rhsClause;
214 : : // The pivots to be eliminated to the lhs clause and rhs clause in a binary
215 : : // resolution step, respectively
216 : 3730000 : Node lhsElim, rhsElim;
217 : : // Get lhsClause of first resolution.
218 : : //
219 : : // Since a Node cannot hold an OR with a single child we need to
220 : : // disambiguate singleton clauses that are OR nodes from non-singleton
221 : : // clauses (i.e. unit clauses in the SAT solver).
222 : : //
223 : : // If the child is not an OR, it is a singleton clause and we take the
224 : : // child itself as the clause. Otherwise the child can only be a singleton
225 : : // clause if the child itself is used as a resolution literal, i.e. if the
226 : : // first child equal to the first pivot (which is args[1][0] or
227 : : // args[1][0].notNode() depending on the polarity).
228 : 3730000 : Node pols = args[0];
229 : 3730000 : Node lits = args[1];
230 : 1865000 : if (children[0].getKind() != Kind::OR
231 : 3729030 : || (pols[0] == trueNode && children[0] == lits[0])
232 : 5594030 : || (pols[0] == falseNode && children[0] == lits[0].notNode()))
233 : : {
234 : 972 : lhsClause.push_back(children[0]);
235 : : }
236 : : else
237 : : {
238 : 1864030 : lhsClause.insert(lhsClause.end(), children[0].begin(), children[0].end());
239 : : }
240 : : // Traverse the links, which amounts to for each pair of args removing a
241 : : // literal from the lhs and a literal from the lhs.
242 [ + + ]: 13813800 : for (size_t i = 0, argsSize = pols.getNumChildren(); i < argsSize; i++)
243 : : {
244 : : // Polarity determines how the pivot occurs in lhs and rhs
245 [ + + ]: 11948800 : if (pols[i] == trueNode)
246 : : {
247 : 6301420 : lhsElim = lits[i];
248 : 6301420 : rhsElim = lits[i].notNode();
249 : : }
250 : : else
251 : : {
252 [ - + ][ - + ]: 5647420 : Assert(pols[i] == falseNode);
[ - - ]
253 : 5647420 : lhsElim = lits[i].notNode();
254 : 5647420 : rhsElim = lits[i];
255 : : }
256 : : // The index of the child corresponding to the current rhs clause
257 : 11948800 : size_t childIndex = i + 1;
258 : : // Get rhs clause. It's a singleton if not an OR node or if equal to
259 : : // rhsElim
260 : 11948800 : if (children[childIndex].getKind() != Kind::OR
261 [ + + ][ + + ]: 11948800 : || children[childIndex] == rhsElim)
[ + + ]
262 : : {
263 : 3069040 : rhsClause.push_back(children[childIndex]);
264 : : }
265 : : else
266 : : {
267 : 8879800 : rhsClause = {children[childIndex].begin(), children[childIndex].end()};
268 : : }
269 [ + - ]: 11948800 : Trace("bool-pfcheck") << i << "-th res link:\n";
270 [ + - ]: 11948800 : Trace("bool-pfcheck") << "\t - lhsClause: " << lhsClause << "\n";
271 [ + - ]: 11948800 : Trace("bool-pfcheck") << "\t\t - lhsElim: " << lhsElim << "\n";
272 [ + - ]: 11948800 : Trace("bool-pfcheck") << "\t - rhsClause: " << rhsClause << "\n";
273 [ + - ]: 11948800 : Trace("bool-pfcheck") << "\t\t - rhsElim: " << rhsElim << "\n";
274 : : // Compute the resulting clause, which will be the next lhsClause, as
275 : : // follows:
276 : : // - remove lhsElim from lhsClause
277 : : // - remove rhsElim from rhsClause and add the lits to lhsClause
278 : 11948800 : auto itlhs = std::find(lhsClause.begin(), lhsClause.end(), lhsElim);
279 [ - + ][ - + ]: 11948800 : AlwaysAssert(itlhs != lhsClause.end());
[ - - ]
280 : 11948800 : lhsClause.erase(itlhs);
281 [ + - ]: 11948800 : Trace("bool-pfcheck") << "\t.. after lhsClause: " << lhsClause << "\n";
282 : 11948800 : auto itrhs = std::find(rhsClause.begin(), rhsClause.end(), rhsElim);
283 [ - + ][ - + ]: 11948800 : AlwaysAssert(itrhs != rhsClause.end());
[ - - ]
284 : 11948800 : lhsClause.insert(lhsClause.end(), rhsClause.begin(), itrhs);
285 : 11948800 : lhsClause.insert(lhsClause.end(), itrhs + 1, rhsClause.end());
286 [ - + ]: 11948800 : if (TraceIsOn("bool-pfcheck"))
287 : : {
288 : 0 : std::vector<Node> updatedRhsClause{rhsClause.begin(), itrhs};
289 : : updatedRhsClause.insert(
290 : 0 : updatedRhsClause.end(), itrhs + 1, rhsClause.end());
291 [ - - ]: 0 : Trace("bool-pfcheck")
292 : 0 : << "\t.. after rhsClause: " << updatedRhsClause << "\n";
293 : : }
294 : 11948800 : rhsClause.clear();
295 : : }
296 [ + - ]: 3730000 : Trace("bool-pfcheck") << "\n resulting clause: " << lhsClause << "\n"
297 : 1865000 : << pop;
298 : 1865000 : return nm->mkOr(lhsClause);
299 : : }
300 [ + + ]: 2351740 : if (id == ProofRule::MACRO_RESOLUTION_TRUST)
301 : : {
302 [ - + ][ - + ]: 209769 : Assert(children.size() > 1);
[ - - ]
303 [ - + ][ - + ]: 209769 : Assert(args.size() == 2 * (children.size() - 1) + 1);
[ - - ]
304 : 209769 : return args[0];
305 : : }
306 [ - + ]: 2141980 : if (id == ProofRule::MACRO_RESOLUTION)
307 : : {
308 : 0 : Assert(children.size() > 1);
309 : 0 : Assert(args.size() == 2 * (children.size() - 1) + 1);
310 [ - - ]: 0 : Trace("bool-pfcheck") << "macro_res: " << args[0] << "\n" << push;
311 : 0 : NodeManager* nm = nodeManager();
312 : 0 : Node trueNode = nm->mkConst(true);
313 : 0 : Node falseNode = nm->mkConst(false);
314 : 0 : std::vector<Node> lhsClause, rhsClause;
315 : 0 : Node lhsElim, rhsElim;
316 : 0 : std::vector<Node> pols, lits;
317 [ - - ]: 0 : for (size_t i = 1, nargs = args.size(); i < nargs; i = i + 2)
318 : : {
319 : 0 : pols.push_back(args[i]);
320 : 0 : lits.push_back(args[i + 1]);
321 : : }
322 : :
323 : 0 : if (children[0].getKind() != Kind::OR
324 : 0 : || (pols[0] == trueNode && children[0] == lits[0])
325 : 0 : || (pols[0] == falseNode && children[0] == lits[0].notNode()))
326 : : {
327 : 0 : lhsClause.push_back(children[0]);
328 : : }
329 : : else
330 : : {
331 : 0 : lhsClause.insert(lhsClause.end(), children[0].begin(), children[0].end());
332 : : }
333 : : // Traverse the links, which amounts to for each pair of args removing a
334 : : // literal from the lhs and a literal from the lhs.
335 [ - - ]: 0 : for (size_t i = 0, argsSize = pols.size(); i < argsSize; i++)
336 : : {
337 : : // Polarity determines how the pivot occurs in lhs and rhs
338 [ - - ]: 0 : if (pols[i] == trueNode)
339 : : {
340 : 0 : lhsElim = lits[i];
341 : 0 : rhsElim = lits[i].notNode();
342 : : }
343 : : else
344 : : {
345 : 0 : Assert(pols[i] == falseNode);
346 : 0 : lhsElim = lits[i].notNode();
347 : 0 : rhsElim = lits[i];
348 : : }
349 : : // The index of the child corresponding to the current rhs clause
350 : 0 : size_t childIndex = i + 1;
351 : : // Get rhs clause. It's a singleton if not an OR node or if equal to
352 : : // rhsElim
353 : 0 : if (children[childIndex].getKind() != Kind::OR
354 : 0 : || children[childIndex] == rhsElim)
355 : : {
356 : 0 : rhsClause.push_back(children[childIndex]);
357 : : }
358 : : else
359 : : {
360 : 0 : rhsClause = {children[childIndex].begin(), children[childIndex].end()};
361 : : }
362 [ - - ]: 0 : Trace("bool-pfcheck") << i << "-th res link:\n";
363 [ - - ]: 0 : Trace("bool-pfcheck") << "\t - lhsClause: " << lhsClause << "\n";
364 [ - - ]: 0 : Trace("bool-pfcheck") << "\t\t - lhsElim: " << lhsElim << "\n";
365 [ - - ]: 0 : Trace("bool-pfcheck") << "\t - rhsClause: " << rhsClause << "\n";
366 [ - - ]: 0 : Trace("bool-pfcheck") << "\t\t - rhsElim: " << rhsElim << "\n";
367 : : // Compute the resulting clause, which will be the next lhsClause, as
368 : : // follows:
369 : : // - remove all lhsElim from lhsClause
370 : : // - remove all rhsElim from rhsClause and add the lits to lhsClause
371 : : //
372 : : // Note that to remove the elements from lhsClaus we use the
373 : : // "erase-remove" idiom in C++: the std::remove call shuffles the elements
374 : : // different from lhsElim to the beginning of the container, returning an
375 : : // iterator to the beginning of the "rest" of the container (with
376 : : // occurrences of lhsElim). Then the call to erase removes the range from
377 : : // there to the end. Once C++ 20 is allowed in the cvc5 code base, this
378 : : // could be done with a single call to std::erase.
379 : 0 : lhsClause.erase(std::remove(lhsClause.begin(), lhsClause.end(), lhsElim),
380 : 0 : lhsClause.end());
381 [ - - ]: 0 : for (const Node& l : rhsClause)
382 : : {
383 : : // only add if literal does not occur in elimination set
384 [ - - ]: 0 : if (rhsElim != l)
385 : : {
386 : 0 : lhsClause.push_back(l);
387 : : }
388 : : }
389 : 0 : rhsClause.clear();
390 : : }
391 : :
392 [ - - ]: 0 : Trace("bool-pfcheck") << "clause: " << lhsClause << "\n";
393 : : // check that set representation is the same as of the given conclusion
394 : 0 : std::unordered_set<Node> clauseComputed{lhsClause.begin(), lhsClause.end()};
395 [ - - ]: 0 : Trace("bool-pfcheck") << "clauseSet: " << clauseComputed << "\n" << pop;
396 [ - - ]: 0 : if (clauseComputed.empty())
397 : : {
398 : : // conclusion differ
399 [ - - ]: 0 : if (args[0] != falseNode)
400 : : {
401 : 0 : return Node::null();
402 : : }
403 : 0 : return args[0];
404 : : }
405 [ - - ]: 0 : if (clauseComputed.size() == 1)
406 : : {
407 : : // conclusion differ
408 [ - - ]: 0 : if (args[0] != *clauseComputed.begin())
409 : : {
410 : 0 : return Node::null();
411 : : }
412 : 0 : return args[0];
413 : : }
414 : : // At this point, should amount to them differing only on order or in
415 : : // repetitions. So the original result can't be a singleton clause.
416 [ - - ]: 0 : if (args[0].getKind() != Kind::OR)
417 : : {
418 : 0 : return Node::null();
419 : : }
420 : 0 : std::unordered_set<Node> clauseGiven{args[0].begin(), args[0].end()};
421 [ - - ]: 0 : return clauseComputed == clauseGiven ? args[0] : Node::null();
422 : : }
423 [ + + ]: 2141980 : if (id == ProofRule::SPLIT)
424 : : {
425 [ - + ][ - + ]: 49814 : Assert(children.empty());
[ - - ]
426 [ - + ][ - + ]: 49814 : Assert(args.size() == 1);
[ - - ]
427 : 49814 : return nodeManager()->mkNode(Kind::OR, args[0], args[0].notNode());
428 : : }
429 [ + + ]: 2092160 : if (id == ProofRule::CONTRA)
430 : : {
431 [ - + ][ - + ]: 100501 : Assert(children.size() == 2);
[ - - ]
432 [ + - ][ + - ]: 100501 : if (children[1].getKind() == Kind::NOT && children[0] == children[1][0])
[ + - ][ + - ]
[ - - ]
433 : : {
434 : 201002 : return nodeManager()->mkConst(false);
435 : : }
436 : 0 : return Node::null();
437 : : }
438 [ + + ]: 1991660 : if (id == ProofRule::EQ_RESOLVE)
439 : : {
440 [ - + ][ - + ]: 465041 : Assert(children.size() == 2);
[ - - ]
441 [ - + ][ - + ]: 465041 : Assert(args.empty());
[ - - ]
442 [ + - ][ - + ]: 465041 : if (children[1].getKind() != Kind::EQUAL || children[0] != children[1][0])
[ + - ][ - + ]
[ - - ]
443 : : {
444 : 0 : return Node::null();
445 : : }
446 : 465041 : return children[1][1];
447 : : }
448 [ + + ]: 1526620 : if (id == ProofRule::MODUS_PONENS)
449 : : {
450 [ - + ][ - + ]: 210188 : Assert(children.size() == 2);
[ - - ]
451 [ - + ][ - + ]: 210188 : Assert(args.empty());
[ - - ]
452 [ + - ][ - + ]: 210188 : if (children[1].getKind() != Kind::IMPLIES || children[0] != children[1][0])
[ + - ][ - + ]
[ - - ]
453 : : {
454 : 0 : return Node::null();
455 : : }
456 : 210188 : return children[1][1];
457 : : }
458 [ + + ]: 1316430 : if (id == ProofRule::NOT_NOT_ELIM)
459 : : {
460 [ - + ][ - + ]: 7580 : Assert(children.size() == 1);
[ - - ]
461 [ - + ][ - + ]: 7580 : Assert(args.empty());
[ - - ]
462 : 7580 : if (children[0].getKind() != Kind::NOT
463 [ + - ][ - + ]: 15160 : || children[0][0].getKind() != Kind::NOT)
[ + - ][ - + ]
[ - - ]
464 : : {
465 : 0 : return Node::null();
466 : : }
467 : 7580 : return children[0][0][0];
468 : : }
469 : : // natural deduction rules
470 [ + + ]: 1308850 : if (id == ProofRule::AND_ELIM)
471 : : {
472 [ - + ][ - + ]: 350788 : Assert(children.size() == 1);
[ - - ]
473 [ - + ][ - + ]: 350788 : Assert(args.size() == 1);
[ - - ]
474 : : uint32_t i;
475 [ + - ][ - + ]: 350788 : if (children[0].getKind() != Kind::AND || !getUInt32(args[0], i))
[ + - ][ - + ]
[ - - ]
476 : : {
477 : 0 : return Node::null();
478 : : }
479 [ - + ]: 350788 : if (i >= children[0].getNumChildren())
480 : : {
481 : 0 : return Node::null();
482 : : }
483 : 350788 : return children[0][i];
484 : : }
485 [ + + ]: 958064 : if (id == ProofRule::AND_INTRO)
486 : : {
487 [ - + ][ - + ]: 264815 : Assert(children.size() >= 1);
[ - - ]
488 : 264815 : return children.size() == 1 ? children[0]
489 [ - + ]: 264815 : : nodeManager()->mkNode(Kind::AND, children);
490 : : }
491 [ + + ]: 693249 : if (id == ProofRule::NOT_OR_ELIM)
492 : : {
493 [ - + ][ - + ]: 8930 : Assert(children.size() == 1);
[ - - ]
494 [ - + ][ - + ]: 8930 : Assert(args.size() == 1);
[ - - ]
495 : : uint32_t i;
496 : 8930 : if (children[0].getKind() != Kind::NOT
497 : 17860 : || children[0][0].getKind() != Kind::OR || !getUInt32(args[0], i))
498 : : {
499 : 0 : return Node::null();
500 : : }
501 [ - + ]: 8930 : if (i >= children[0][0].getNumChildren())
502 : : {
503 : 0 : return Node::null();
504 : : }
505 : 8930 : return children[0][0][i].notNode();
506 : : }
507 [ + + ]: 684319 : if (id == ProofRule::IMPLIES_ELIM)
508 : : {
509 [ - + ][ - + ]: 84013 : Assert(children.size() == 1);
[ - - ]
510 [ - + ][ - + ]: 84013 : Assert(args.empty());
[ - - ]
511 [ - + ]: 84013 : if (children[0].getKind() != Kind::IMPLIES)
512 : : {
513 : 0 : return Node::null();
514 : : }
515 : : return nodeManager()->mkNode(
516 : 84013 : Kind::OR, children[0][0].notNode(), children[0][1]);
517 : : }
518 [ + + ]: 600306 : if (id == ProofRule::NOT_IMPLIES_ELIM1)
519 : : {
520 [ - + ][ - + ]: 4534 : Assert(children.size() == 1);
[ - - ]
521 [ - + ][ - + ]: 4534 : Assert(args.empty());
[ - - ]
522 : 4534 : if (children[0].getKind() != Kind::NOT
523 [ + - ][ - + ]: 9068 : || children[0][0].getKind() != Kind::IMPLIES)
[ + - ][ - + ]
[ - - ]
524 : : {
525 : 0 : return Node::null();
526 : : }
527 : 4534 : return children[0][0][0];
528 : : }
529 [ + + ]: 595772 : if (id == ProofRule::NOT_IMPLIES_ELIM2)
530 : : {
531 [ - + ][ - + ]: 2371 : Assert(children.size() == 1);
[ - - ]
532 [ - + ][ - + ]: 2371 : Assert(args.empty());
[ - - ]
533 : 2371 : if (children[0].getKind() != Kind::NOT
534 [ + - ][ - + ]: 4742 : || children[0][0].getKind() != Kind::IMPLIES)
[ + - ][ - + ]
[ - - ]
535 : : {
536 : 0 : return Node::null();
537 : : }
538 : 2371 : return children[0][0][1].notNode();
539 : : }
540 [ + + ]: 593401 : if (id == ProofRule::EQUIV_ELIM1)
541 : : {
542 [ - + ][ - + ]: 35640 : Assert(children.size() == 1);
[ - - ]
543 [ - + ][ - + ]: 35640 : Assert(args.empty());
[ - - ]
544 [ - + ]: 35640 : if (children[0].getKind() != Kind::EQUAL)
545 : : {
546 : 0 : return Node::null();
547 : : }
548 : : return nodeManager()->mkNode(
549 : 35640 : Kind::OR, children[0][0].notNode(), children[0][1]);
550 : : }
551 [ + + ]: 557761 : if (id == ProofRule::EQUIV_ELIM2)
552 : : {
553 [ - + ][ - + ]: 20583 : Assert(children.size() == 1);
[ - - ]
554 [ - + ][ - + ]: 20583 : Assert(args.empty());
[ - - ]
555 [ - + ]: 20583 : if (children[0].getKind() != Kind::EQUAL)
556 : : {
557 : 0 : return Node::null();
558 : : }
559 : : return nodeManager()->mkNode(
560 : 20583 : Kind::OR, children[0][0], children[0][1].notNode());
561 : : }
562 [ + + ]: 537178 : if (id == ProofRule::NOT_EQUIV_ELIM1)
563 : : {
564 [ - + ][ - + ]: 994 : Assert(children.size() == 1);
[ - - ]
565 [ - + ][ - + ]: 994 : Assert(args.empty());
[ - - ]
566 : 994 : if (children[0].getKind() != Kind::NOT
567 [ + - ][ - + ]: 1988 : || children[0][0].getKind() != Kind::EQUAL)
[ + - ][ - + ]
[ - - ]
568 : : {
569 : 0 : return Node::null();
570 : : }
571 : : return nodeManager()->mkNode(
572 : 994 : Kind::OR, children[0][0][0], children[0][0][1]);
573 : : }
574 [ + + ]: 536184 : if (id == ProofRule::NOT_EQUIV_ELIM2)
575 : : {
576 [ - + ][ - + ]: 569 : Assert(children.size() == 1);
[ - - ]
577 [ - + ][ - + ]: 569 : Assert(args.empty());
[ - - ]
578 : 569 : if (children[0].getKind() != Kind::NOT
579 [ + - ][ - + ]: 1138 : || children[0][0].getKind() != Kind::EQUAL)
[ + - ][ - + ]
[ - - ]
580 : : {
581 : 0 : return Node::null();
582 : : }
583 : : return nodeManager()->mkNode(
584 : 569 : Kind::OR, children[0][0][0].notNode(), children[0][0][1].notNode());
585 : : }
586 [ + + ]: 535615 : if (id == ProofRule::XOR_ELIM1)
587 : : {
588 [ - + ][ - + ]: 106 : Assert(children.size() == 1);
[ - - ]
589 [ - + ][ - + ]: 106 : Assert(args.empty());
[ - - ]
590 [ - + ]: 106 : if (children[0].getKind() != Kind::XOR)
591 : : {
592 : 0 : return Node::null();
593 : : }
594 : 106 : return nodeManager()->mkNode(Kind::OR, children[0][0], children[0][1]);
595 : : }
596 [ + + ]: 535509 : if (id == ProofRule::XOR_ELIM2)
597 : : {
598 [ - + ][ - + ]: 131 : Assert(children.size() == 1);
[ - - ]
599 [ - + ][ - + ]: 131 : Assert(args.empty());
[ - - ]
600 [ - + ]: 131 : if (children[0].getKind() != Kind::XOR)
601 : : {
602 : 0 : return Node::null();
603 : : }
604 : : return nodeManager()->mkNode(
605 : 131 : Kind::OR, children[0][0].notNode(), children[0][1].notNode());
606 : : }
607 [ + + ]: 535378 : if (id == ProofRule::NOT_XOR_ELIM1)
608 : : {
609 [ - + ][ - + ]: 74 : Assert(children.size() == 1);
[ - - ]
610 [ - + ][ - + ]: 74 : Assert(args.empty());
[ - - ]
611 : 74 : if (children[0].getKind() != Kind::NOT
612 [ + - ][ - + ]: 148 : || children[0][0].getKind() != Kind::XOR)
[ + - ][ - + ]
[ - - ]
613 : : {
614 : 0 : return Node::null();
615 : : }
616 : : return nodeManager()->mkNode(
617 : 74 : Kind::OR, children[0][0][0], children[0][0][1].notNode());
618 : : }
619 [ + + ]: 535304 : if (id == ProofRule::NOT_XOR_ELIM2)
620 : : {
621 [ - + ][ - + ]: 76 : Assert(children.size() == 1);
[ - - ]
622 [ - + ][ - + ]: 76 : Assert(args.empty());
[ - - ]
623 : 76 : if (children[0].getKind() != Kind::NOT
624 [ + - ][ - + ]: 152 : || children[0][0].getKind() != Kind::XOR)
[ + - ][ - + ]
[ - - ]
625 : : {
626 : 0 : return Node::null();
627 : : }
628 : : return nodeManager()->mkNode(
629 : 76 : Kind::OR, children[0][0][0].notNode(), children[0][0][1]);
630 : : }
631 [ + + ]: 535228 : if (id == ProofRule::ITE_ELIM1)
632 : : {
633 [ - + ][ - + ]: 9437 : Assert(children.size() == 1);
[ - - ]
634 [ - + ][ - + ]: 9437 : Assert(args.empty());
[ - - ]
635 [ - + ]: 9437 : if (children[0].getKind() != Kind::ITE)
636 : : {
637 : 0 : return Node::null();
638 : : }
639 : : return nodeManager()->mkNode(
640 : 9437 : Kind::OR, children[0][0].notNode(), children[0][1]);
641 : : }
642 [ + + ]: 525791 : if (id == ProofRule::ITE_ELIM2)
643 : : {
644 [ - + ][ - + ]: 22498 : Assert(children.size() == 1);
[ - - ]
645 [ - + ][ - + ]: 22498 : Assert(args.empty());
[ - - ]
646 [ - + ]: 22498 : if (children[0].getKind() != Kind::ITE)
647 : : {
648 : 0 : return Node::null();
649 : : }
650 : 22498 : return nodeManager()->mkNode(Kind::OR, children[0][0], children[0][2]);
651 : : }
652 [ + + ]: 503293 : if (id == ProofRule::NOT_ITE_ELIM1)
653 : : {
654 [ - + ][ - + ]: 30 : Assert(children.size() == 1);
[ - - ]
655 [ - + ][ - + ]: 30 : Assert(args.empty());
[ - - ]
656 : 30 : if (children[0].getKind() != Kind::NOT
657 [ + - ][ - + ]: 60 : || children[0][0].getKind() != Kind::ITE)
[ + - ][ - + ]
[ - - ]
658 : : {
659 : 0 : return Node::null();
660 : : }
661 : : return nodeManager()->mkNode(
662 : 30 : Kind::OR, children[0][0][0].notNode(), children[0][0][1].notNode());
663 : : }
664 [ + + ]: 503263 : if (id == ProofRule::NOT_ITE_ELIM2)
665 : : {
666 [ - + ][ - + ]: 58 : Assert(children.size() == 1);
[ - - ]
667 [ - + ][ - + ]: 58 : Assert(args.empty());
[ - - ]
668 : 58 : if (children[0].getKind() != Kind::NOT
669 [ + - ][ - + ]: 116 : || children[0][0].getKind() != Kind::ITE)
[ + - ][ - + ]
[ - - ]
670 : : {
671 : 0 : return Node::null();
672 : : }
673 : : return nodeManager()->mkNode(
674 : 58 : Kind::OR, children[0][0][0], children[0][0][2].notNode());
675 : : }
676 : : // De Morgan
677 [ + + ]: 503205 : if (id == ProofRule::NOT_AND)
678 : : {
679 [ - + ][ - + ]: 203434 : Assert(children.size() == 1);
[ - - ]
680 [ - + ][ - + ]: 203434 : Assert(args.empty());
[ - - ]
681 : 203434 : if (children[0].getKind() != Kind::NOT
682 [ + - ][ - + ]: 406868 : || children[0][0].getKind() != Kind::AND)
[ + - ][ - + ]
[ - - ]
683 : : {
684 : 0 : return Node::null();
685 : : }
686 : 406868 : std::vector<Node> disjuncts;
687 [ + + ]: 1039220 : for (std::size_t i = 0, size = children[0][0].getNumChildren(); i < size;
688 : : ++i)
689 : : {
690 : 835788 : disjuncts.push_back(children[0][0][i].notNode());
691 : : }
692 : 203434 : return nodeManager()->mkNode(Kind::OR, disjuncts);
693 : : }
694 : : // valid clauses rules for Tseitin CNF transformation
695 [ + + ]: 299771 : if (id == ProofRule::CNF_AND_POS)
696 : : {
697 [ - + ][ - + ]: 68566 : Assert(children.empty());
[ - - ]
698 [ - + ][ - + ]: 68566 : Assert(args.size() == 2);
[ - - ]
699 : : uint32_t i;
700 [ + - ][ - + ]: 68566 : if (args[0].getKind() != Kind::AND || !getUInt32(args[1], i))
[ + - ][ - + ]
[ - - ]
701 : : {
702 : 0 : return Node::null();
703 : : }
704 [ - + ]: 68566 : if (i >= args[0].getNumChildren())
705 : : {
706 : 0 : return Node::null();
707 : : }
708 : 68566 : return nodeManager()->mkNode(Kind::OR, args[0].notNode(), args[0][i]);
709 : : }
710 [ + + ]: 231205 : if (id == ProofRule::CNF_AND_NEG)
711 : : {
712 [ - + ][ - + ]: 80540 : Assert(children.empty());
[ - - ]
713 [ - + ][ - + ]: 80540 : Assert(args.size() == 1);
[ - - ]
714 [ - + ]: 80540 : if (args[0].getKind() != Kind::AND)
715 : : {
716 : 0 : return Node::null();
717 : : }
718 : 322160 : std::vector<Node> disjuncts{args[0]};
719 [ + + ]: 484675 : for (unsigned i = 0, size = args[0].getNumChildren(); i < size; ++i)
720 : : {
721 : 404135 : disjuncts.push_back(args[0][i].notNode());
722 : : }
723 : 80540 : return nodeManager()->mkNode(Kind::OR, disjuncts);
724 : : }
725 [ + + ]: 150665 : if (id == ProofRule::CNF_OR_POS)
726 : : {
727 [ - + ][ - + ]: 18396 : Assert(children.empty());
[ - - ]
728 [ - + ][ - + ]: 18396 : Assert(args.size() == 1);
[ - - ]
729 [ - + ]: 18396 : if (args[0].getKind() != Kind::OR)
730 : : {
731 : 0 : return Node::null();
732 : : }
733 : 73584 : std::vector<Node> disjuncts{args[0].notNode()};
734 [ + + ]: 1305020 : for (unsigned i = 0, size = args[0].getNumChildren(); i < size; ++i)
735 : : {
736 : 1286630 : disjuncts.push_back(args[0][i]);
737 : : }
738 : 18396 : return nodeManager()->mkNode(Kind::OR, disjuncts);
739 : : }
740 [ + + ]: 132269 : if (id == ProofRule::CNF_OR_NEG)
741 : : {
742 [ - + ][ - + ]: 69638 : Assert(children.empty());
[ - - ]
743 [ - + ][ - + ]: 69638 : Assert(args.size() == 2);
[ - - ]
744 : : uint32_t i;
745 [ + - ][ - + ]: 69638 : if (args[0].getKind() != Kind::OR || !getUInt32(args[1], i))
[ + - ][ - + ]
[ - - ]
746 : : {
747 : 0 : return Node::null();
748 : : }
749 [ - + ]: 69638 : if (i >= args[0].getNumChildren())
750 : : {
751 : 0 : return Node::null();
752 : : }
753 : 69638 : return nodeManager()->mkNode(Kind::OR, args[0], args[0][i].notNode());
754 : : }
755 [ + + ]: 62631 : if (id == ProofRule::CNF_IMPLIES_POS)
756 : : {
757 [ - + ][ - + ]: 3059 : Assert(children.empty());
[ - - ]
758 [ - + ][ - + ]: 3059 : Assert(args.size() == 1);
[ - - ]
759 [ - + ]: 3059 : if (args[0].getKind() != Kind::IMPLIES)
760 : : {
761 : 0 : return Node::null();
762 : : }
763 : : std::vector<Node> disjuncts{
764 : 21413 : args[0].notNode(), args[0][0].notNode(), args[0][1]};
765 : 3059 : return nodeManager()->mkNode(Kind::OR, disjuncts);
766 : : }
767 [ + + ]: 59572 : if (id == ProofRule::CNF_IMPLIES_NEG1)
768 : : {
769 [ - + ][ - + ]: 628 : Assert(children.empty());
[ - - ]
770 [ - + ][ - + ]: 628 : Assert(args.size() == 1);
[ - - ]
771 [ - + ]: 628 : if (args[0].getKind() != Kind::IMPLIES)
772 : : {
773 : 0 : return Node::null();
774 : : }
775 : 3140 : std::vector<Node> disjuncts{args[0], args[0][0]};
776 : 628 : return nodeManager()->mkNode(Kind::OR, disjuncts);
777 : : }
778 [ + + ]: 58944 : if (id == ProofRule::CNF_IMPLIES_NEG2)
779 : : {
780 [ - + ][ - + ]: 3434 : Assert(children.empty());
[ - - ]
781 [ - + ][ - + ]: 3434 : Assert(args.size() == 1);
[ - - ]
782 [ - + ]: 3434 : if (args[0].getKind() != Kind::IMPLIES)
783 : : {
784 : 0 : return Node::null();
785 : : }
786 : 20604 : std::vector<Node> disjuncts{args[0], args[0][1].notNode()};
787 : 3434 : return nodeManager()->mkNode(Kind::OR, disjuncts);
788 : : }
789 [ + + ]: 55510 : if (id == ProofRule::CNF_EQUIV_POS1)
790 : : {
791 [ - + ][ - + ]: 8272 : Assert(children.empty());
[ - - ]
792 [ - + ][ - + ]: 8272 : Assert(args.size() == 1);
[ - - ]
793 [ - + ]: 8272 : if (args[0].getKind() != Kind::EQUAL)
794 : : {
795 : 0 : return Node::null();
796 : : }
797 : : std::vector<Node> disjuncts{
798 : 57904 : args[0].notNode(), args[0][0].notNode(), args[0][1]};
799 : 8272 : return nodeManager()->mkNode(Kind::OR, disjuncts);
800 : : }
801 [ + + ]: 47238 : if (id == ProofRule::CNF_EQUIV_POS2)
802 : : {
803 [ - + ][ - + ]: 8300 : Assert(children.empty());
[ - - ]
804 [ - + ][ - + ]: 8300 : Assert(args.size() == 1);
[ - - ]
805 [ - + ]: 8300 : if (args[0].getKind() != Kind::EQUAL)
806 : : {
807 : 0 : return Node::null();
808 : : }
809 : : std::vector<Node> disjuncts{
810 : 58100 : args[0].notNode(), args[0][0], args[0][1].notNode()};
811 : 8300 : return nodeManager()->mkNode(Kind::OR, disjuncts);
812 : : }
813 [ + + ]: 38938 : if (id == ProofRule::CNF_EQUIV_NEG1)
814 : : {
815 [ - + ][ - + ]: 4760 : Assert(children.empty());
[ - - ]
816 [ - + ][ - + ]: 4760 : Assert(args.size() == 1);
[ - - ]
817 [ - + ]: 4760 : if (args[0].getKind() != Kind::EQUAL)
818 : : {
819 : 0 : return Node::null();
820 : : }
821 : 28560 : std::vector<Node> disjuncts{args[0], args[0][0], args[0][1]};
822 : 4760 : return nodeManager()->mkNode(Kind::OR, disjuncts);
823 : : }
824 [ + + ]: 34178 : if (id == ProofRule::CNF_EQUIV_NEG2)
825 : : {
826 [ - + ][ - + ]: 11850 : Assert(children.empty());
[ - - ]
827 [ - + ][ - + ]: 11850 : Assert(args.size() == 1);
[ - - ]
828 [ - + ]: 11850 : if (args[0].getKind() != Kind::EQUAL)
829 : : {
830 : 0 : return Node::null();
831 : : }
832 : : std::vector<Node> disjuncts{
833 : 82950 : args[0], args[0][0].notNode(), args[0][1].notNode()};
834 : 11850 : return nodeManager()->mkNode(Kind::OR, disjuncts);
835 : : }
836 [ + + ]: 22328 : if (id == ProofRule::CNF_XOR_POS1)
837 : : {
838 [ - + ][ - + ]: 4275 : Assert(children.empty());
[ - - ]
839 [ - + ][ - + ]: 4275 : Assert(args.size() == 1);
[ - - ]
840 [ - + ]: 4275 : if (args[0].getKind() != Kind::XOR)
841 : : {
842 : 0 : return Node::null();
843 : : }
844 : 25650 : std::vector<Node> disjuncts{args[0].notNode(), args[0][0], args[0][1]};
845 : 4275 : return nodeManager()->mkNode(Kind::OR, disjuncts);
846 : : }
847 [ + + ]: 18053 : if (id == ProofRule::CNF_XOR_POS2)
848 : : {
849 [ - + ][ - + ]: 1780 : Assert(children.empty());
[ - - ]
850 [ - + ][ - + ]: 1780 : Assert(args.size() == 1);
[ - - ]
851 [ - + ]: 1780 : if (args[0].getKind() != Kind::XOR)
852 : : {
853 : 0 : return Node::null();
854 : : }
855 : : std::vector<Node> disjuncts{
856 : 12460 : args[0].notNode(), args[0][0].notNode(), args[0][1].notNode()};
857 : 1780 : return nodeManager()->mkNode(Kind::OR, disjuncts);
858 : : }
859 [ + + ]: 16273 : if (id == ProofRule::CNF_XOR_NEG1)
860 : : {
861 [ - + ][ - + ]: 1680 : Assert(children.empty());
[ - - ]
862 [ - + ][ - + ]: 1680 : Assert(args.size() == 1);
[ - - ]
863 [ - + ]: 1680 : if (args[0].getKind() != Kind::XOR)
864 : : {
865 : 0 : return Node::null();
866 : : }
867 : 11760 : std::vector<Node> disjuncts{args[0], args[0][0].notNode(), args[0][1]};
868 : 1680 : return nodeManager()->mkNode(Kind::OR, disjuncts);
869 : : }
870 [ + + ]: 14593 : if (id == ProofRule::CNF_XOR_NEG2)
871 : : {
872 [ - + ][ - + ]: 1766 : Assert(children.empty());
[ - - ]
873 [ - + ][ - + ]: 1766 : Assert(args.size() == 1);
[ - - ]
874 [ - + ]: 1766 : if (args[0].getKind() != Kind::XOR)
875 : : {
876 : 0 : return Node::null();
877 : : }
878 : 12362 : std::vector<Node> disjuncts{args[0], args[0][0], args[0][1].notNode()};
879 : 1766 : return nodeManager()->mkNode(Kind::OR, disjuncts);
880 : : }
881 [ + + ]: 12827 : if (id == ProofRule::CNF_ITE_POS1)
882 : : {
883 [ - + ][ - + ]: 1524 : Assert(children.empty());
[ - - ]
884 [ - + ][ - + ]: 1524 : Assert(args.size() == 1);
[ - - ]
885 [ - + ]: 1524 : if (args[0].getKind() != Kind::ITE)
886 : : {
887 : 0 : return Node::null();
888 : : }
889 : : std::vector<Node> disjuncts{
890 : 10668 : args[0].notNode(), args[0][0].notNode(), args[0][1]};
891 : 1524 : return nodeManager()->mkNode(Kind::OR, disjuncts);
892 : : }
893 [ + + ]: 11303 : if (id == ProofRule::CNF_ITE_POS2)
894 : : {
895 [ - + ][ - + ]: 1651 : Assert(children.empty());
[ - - ]
896 [ - + ][ - + ]: 1651 : Assert(args.size() == 1);
[ - - ]
897 [ - + ]: 1651 : if (args[0].getKind() != Kind::ITE)
898 : : {
899 : 0 : return Node::null();
900 : : }
901 : 9906 : std::vector<Node> disjuncts{args[0].notNode(), args[0][0], args[0][2]};
902 : 1651 : return nodeManager()->mkNode(Kind::OR, disjuncts);
903 : : }
904 [ + + ]: 9652 : if (id == ProofRule::CNF_ITE_POS3)
905 : : {
906 [ - + ][ - + ]: 1571 : Assert(children.empty());
[ - - ]
907 [ - + ][ - + ]: 1571 : Assert(args.size() == 1);
[ - - ]
908 [ - + ]: 1571 : if (args[0].getKind() != Kind::ITE)
909 : : {
910 : 0 : return Node::null();
911 : : }
912 : 9426 : std::vector<Node> disjuncts{args[0].notNode(), args[0][1], args[0][2]};
913 : 1571 : return nodeManager()->mkNode(Kind::OR, disjuncts);
914 : : }
915 [ + + ]: 8081 : if (id == ProofRule::CNF_ITE_NEG1)
916 : : {
917 [ - + ][ - + ]: 5662 : Assert(children.empty());
[ - - ]
918 [ - + ][ - + ]: 5662 : Assert(args.size() == 1);
[ - - ]
919 [ - + ]: 5662 : if (args[0].getKind() != Kind::ITE)
920 : : {
921 : 0 : return Node::null();
922 : : }
923 : : std::vector<Node> disjuncts{
924 : 39634 : args[0], args[0][0].notNode(), args[0][1].notNode()};
925 : 5662 : return nodeManager()->mkNode(Kind::OR, disjuncts);
926 : : }
927 [ + + ]: 2419 : if (id == ProofRule::CNF_ITE_NEG2)
928 : : {
929 [ - + ][ - + ]: 1096 : Assert(children.empty());
[ - - ]
930 [ - + ][ - + ]: 1096 : Assert(args.size() == 1);
[ - - ]
931 [ - + ]: 1096 : if (args[0].getKind() != Kind::ITE)
932 : : {
933 : 0 : return Node::null();
934 : : }
935 : 7672 : std::vector<Node> disjuncts{args[0], args[0][0], args[0][2].notNode()};
936 : 1096 : return nodeManager()->mkNode(Kind::OR, disjuncts);
937 : : }
938 [ + + ]: 1323 : if (id == ProofRule::CNF_ITE_NEG3)
939 : : {
940 [ - + ][ - + ]: 1255 : Assert(children.empty());
[ - - ]
941 [ - + ][ - + ]: 1255 : Assert(args.size() == 1);
[ - - ]
942 [ - + ]: 1255 : if (args[0].getKind() != Kind::ITE)
943 : : {
944 : 0 : return Node::null();
945 : : }
946 : : std::vector<Node> disjuncts{
947 : 8785 : args[0], args[0][1].notNode(), args[0][2].notNode()};
948 : 1255 : return nodeManager()->mkNode(Kind::OR, disjuncts);
949 : : }
950 [ - + ][ - - ]: 68 : if (id == ProofRule::SAT_REFUTATION || id == ProofRule::DRAT_REFUTATION
951 [ - - ]: 0 : || id == ProofRule::SAT_EXTERNAL_PROVE)
952 : : {
953 [ - + ][ - - ]: 68 : Assert(args.size()
[ - + ][ - + ]
[ - - ]
954 : : == (id == ProofRule::SAT_REFUTATION
955 : : ? 0
956 : : : (id == ProofRule::SAT_EXTERNAL_PROVE ? 1 : 2)));
957 : 136 : return nodeManager()->mkConst(false);
958 : : }
959 : : // no rule
960 : 0 : return Node::null();
961 : : }
962 : :
963 : : } // namespace booleans
964 : : } // namespace theory
965 : : } // namespace cvc5::internal
|
