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 the proof-producing CNF stream.
11 : : */
12 : :
13 : : #include "prop/proof_cnf_stream.h"
14 : :
15 : : #include "options/smt_options.h"
16 : : #include "prop/minisat/minisat.h"
17 : : #include "theory/builtin/proof_checker.h"
18 : : #include "util/rational.h"
19 : :
20 : : namespace cvc5::internal {
21 : : namespace prop {
22 : :
23 : 20037 : ProofCnfStream::ProofCnfStream(Env& env,
24 : : CnfStream& cnfStream,
25 : 20037 : PropPfManager* ppm)
26 : : : EnvObj(env),
27 : 20037 : d_cnfStream(cnfStream),
28 : 20037 : d_ppm(ppm),
29 : 20037 : d_proof(ppm->getCnfProof())
30 : : {
31 : 20037 : }
32 : :
33 : 766191 : void ProofCnfStream::convertAndAssert(TNode node,
34 : : bool negated,
35 : : bool removable,
36 : : bool input,
37 : : ProofGenerator* pg)
38 : : {
39 : : // this method is re-entrant due to lemmas sent during preregistration of new
40 : : // lemmas, thus we must remember and revert d_input below.
41 : 766191 : bool backupInput = d_input;
42 [ + - ]: 1532382 : Trace("cnf") << "ProofCnfStream::convertAndAssert(" << node
43 [ - - ]: 0 : << ", negated = " << (negated ? "true" : "false")
44 [ - - ]: 0 : << ", removable = " << (removable ? "true" : "false")
45 [ - - ]: 0 : << ", input = " << (input ? "true" : "false") << "), level "
46 : 766191 : << userContext()->getLevel() << "\n";
47 : 766191 : d_cnfStream.d_removable = removable;
48 : 766191 : d_input = input;
49 [ + + ]: 766191 : if (pg)
50 : : {
51 [ + - ][ - + ]: 905844 : Trace("cnf") << "ProofCnfStream::convertAndAssert: pg: " << pg->identify()
[ - - ]
52 : 452922 : << "\n";
53 [ + + ]: 452922 : Node toJustify = negated ? node.notNode() : static_cast<Node>(node);
54 : 452922 : d_proof->addLazyStep(toJustify,
55 : : pg,
56 : : TrustId::NONE,
57 : : true,
58 : : "ProofCnfStream::convertAndAssert:cnf");
59 : 452922 : }
60 : 766191 : convertAndAssert(node, negated);
61 : 766191 : d_input = backupInput;
62 : 766191 : }
63 : :
64 : 867262 : void ProofCnfStream::convertAndAssert(TNode node, bool negated)
65 : : {
66 [ + - ]: 1734524 : Trace("cnf") << "ProofCnfStream::convertAndAssert(" << node
67 [ - - ]: 867262 : << ", negated = " << (negated ? "true" : "false") << ")\n"
68 : 867262 : << push;
69 [ + + ][ + + ]: 867262 : switch (node.getKind())
[ + + ][ + + ]
70 : : {
71 : 139534 : case Kind::AND: convertAndAssertAnd(node, negated); break;
72 : 249872 : case Kind::OR: convertAndAssertOr(node, negated); break;
73 : 42 : case Kind::XOR: convertAndAssertXor(node, negated); break;
74 : 149722 : case Kind::IMPLIES: convertAndAssertImplies(node, negated); break;
75 : 26636 : case Kind::ITE: convertAndAssertIte(node, negated); break;
76 : 43413 : case Kind::NOT:
77 : : {
78 : : // track double negation elimination
79 [ + + ]: 43413 : if (negated)
80 : : {
81 : 4676 : d_proof->addStep(
82 : : node[0], ProofRule::NOT_NOT_ELIM, {node.notNode()}, {});
83 [ + - ]: 4676 : Trace("cnf")
84 : 0 : << "ProofCnfStream::convertAndAssert: NOT_NOT_ELIM added norm "
85 [ - + ][ - - ]: 2338 : << node[0] << "\n";
86 : : }
87 : 43413 : convertAndAssert(node[0], !negated);
88 : 43413 : break;
89 : : }
90 : 106945 : case Kind::EQUAL:
91 [ + + ]: 106945 : if (node[0].getType().isBoolean())
92 : : {
93 : 33525 : convertAndAssertIff(node, negated);
94 : 33525 : break;
95 : : }
96 : : CVC5_FALLTHROUGH;
97 : : default:
98 : : {
99 : : // negate
100 [ + + ]: 224518 : Node nnode = negated ? node.negate() : static_cast<Node>(node);
101 : : // Atoms
102 : 224518 : SatLiteral lit = toCNF(node, negated);
103 : 224518 : bool added = d_cnfStream.assertClause(nnode, lit);
104 [ + + ][ + + ]: 224518 : if (negated && added && nnode != node.notNode())
[ - + ][ + + ]
[ - + ][ - - ]
105 : : {
106 : : // track double negation elimination
107 : : // (not (not n))
108 : : // -------------- NOT_NOT_ELIM
109 : : // n
110 : 0 : d_proof->addStep(nnode, ProofRule::NOT_NOT_ELIM, {node.notNode()}, {});
111 [ - - ]: 0 : Trace("cnf")
112 : 0 : << "ProofCnfStream::convertAndAssert: NOT_NOT_ELIM added norm "
113 : 0 : << nnode << "\n";
114 : : }
115 [ + + ]: 224518 : if (added)
116 : : {
117 : : // note that we do not need to do the normalization here since this is
118 : : // not a clause and double negation is tracked in a dedicated manner
119 : : // above
120 : 140580 : d_ppm->normalizeAndRegister(nnode, d_input, false);
121 : : }
122 : 224518 : }
123 : : }
124 [ + - ]: 867262 : Trace("cnf") << pop;
125 : 867262 : }
126 : :
127 : 139534 : void ProofCnfStream::convertAndAssertAnd(TNode node, bool negated)
128 : : {
129 [ + - ]: 279068 : Trace("cnf") << "ProofCnfStream::convertAndAssertAnd(" << node
130 [ - - ]: 139534 : << ", negated = " << (negated ? "true" : "false") << ")\n"
131 : 139534 : << push;
132 [ - + ][ - + ]: 139534 : Assert(node.getKind() == Kind::AND);
[ - - ]
133 [ + + ]: 139534 : if (!negated)
134 : : {
135 : : // If the node is a conjunction, we handle each conjunct separately
136 : 21322 : NodeManager* nm = nodeManager();
137 [ + + ]: 75229 : for (unsigned i = 0, size = node.getNumChildren(); i < size; ++i)
138 : : {
139 : : // Create a proof step for each n_i
140 : 53907 : Node iNode = nm->mkConstInt(i);
141 : 161721 : d_proof->addStep(node[i], ProofRule::AND_ELIM, {node}, {iNode});
142 [ + - ]: 107814 : Trace("cnf") << "ProofCnfStream::convertAndAssertAnd: AND_ELIM " << i
143 [ - + ][ - - ]: 53907 : << " added norm " << node[i] << "\n";
144 : 53907 : convertAndAssert(node[i], false);
145 : 53907 : }
146 : : }
147 : : else
148 : : {
149 : : // If the node is a disjunction, we construct a clause and assert it
150 : 118212 : unsigned i, size = node.getNumChildren();
151 : 118212 : SatClause clause(size);
152 [ + + ]: 1184202 : for (i = 0; i < size; ++i)
153 : : {
154 : 1065990 : clause[i] = toCNF(node[i], true);
155 : : }
156 : 118212 : bool added = d_cnfStream.assertClause(node.negate(), clause);
157 : : // register proof step
158 [ + + ]: 118212 : if (added)
159 : : {
160 : 118178 : std::vector<Node> disjuncts;
161 [ + + ]: 1184043 : for (i = 0; i < size; ++i)
162 : : {
163 : 1065865 : disjuncts.push_back(node[i].notNode());
164 : : }
165 : 118178 : Node clauseNode = nodeManager()->mkNode(Kind::OR, disjuncts);
166 : 236356 : d_proof->addStep(clauseNode, ProofRule::NOT_AND, {node.notNode()}, {});
167 [ + - ]: 236356 : Trace("cnf") << "ProofCnfStream::convertAndAssertAnd: NOT_AND added "
168 : 118178 : << clauseNode << "\n";
169 : 118178 : d_ppm->normalizeAndRegister(clauseNode, d_input);
170 : 118178 : }
171 : 118212 : }
172 [ + - ]: 139534 : Trace("cnf") << pop;
173 : 139534 : }
174 : :
175 : 249872 : void ProofCnfStream::convertAndAssertOr(TNode node, bool negated)
176 : : {
177 [ + - ]: 499744 : Trace("cnf") << "ProofCnfStream::convertAndAssertOr(" << node
178 [ - - ]: 249872 : << ", negated = " << (negated ? "true" : "false") << ")\n"
179 : 249872 : << push;
180 [ - + ][ - + ]: 249872 : Assert(node.getKind() == Kind::OR);
[ - - ]
181 [ + + ]: 249872 : if (!negated)
182 : : {
183 : : // If the node is a disjunction, we construct a clause and assert it
184 : 249636 : unsigned size = node.getNumChildren();
185 : 249636 : SatClause clause(size);
186 [ + + ]: 1065087 : for (unsigned i = 0; i < size; ++i)
187 : : {
188 : 815451 : clause[i] = toCNF(node[i], false);
189 : : }
190 : 249636 : d_ppm->normalizeAndRegister(node, d_input);
191 : 249636 : d_cnfStream.assertClause(node, clause);
192 : 249636 : }
193 : : else
194 : : {
195 : : // If the node is a negated disjunction, we handle it as a conjunction of
196 : : // the negated arguments
197 : 236 : NodeManager* nm = nodeManager();
198 [ + + ]: 3079 : for (unsigned i = 0, size = node.getNumChildren(); i < size; ++i)
199 : : {
200 : : // Create a proof step for each (not n_i)
201 : 2843 : Node iNode = nm->mkConstInt(i);
202 : 14215 : d_proof->addStep(
203 : 5686 : node[i].notNode(), ProofRule::NOT_OR_ELIM, {node.notNode()}, {iNode});
204 [ + - ]: 5686 : Trace("cnf") << "ProofCnfStream::convertAndAssertOr: NOT_OR_ELIM " << i
205 : 2843 : << " added norm " << node[i].notNode() << "\n";
206 : 2843 : convertAndAssert(node[i], true);
207 : 2843 : }
208 : : }
209 [ + - ]: 249872 : Trace("cnf") << pop;
210 : 249872 : }
211 : :
212 : 42 : void ProofCnfStream::convertAndAssertXor(TNode node, bool negated)
213 : : {
214 [ + - ]: 84 : Trace("cnf") << "ProofCnfStream::convertAndAssertXor(" << node
215 [ - - ]: 42 : << ", negated = " << (negated ? "true" : "false") << ")\n"
216 : 42 : << push;
217 [ + + ]: 42 : if (!negated)
218 : : {
219 : : // p XOR q
220 : 33 : SatLiteral p = toCNF(node[0], false);
221 : 33 : SatLiteral q = toCNF(node[1], false);
222 : : bool added;
223 : 33 : NodeManager* nm = nodeManager();
224 : : // Construct the clause (~p v ~q)
225 : 33 : SatClause clause1(2);
226 : 33 : clause1[0] = ~p;
227 : 33 : clause1[1] = ~q;
228 : 33 : added = d_cnfStream.assertClause(node, clause1);
229 [ + - ]: 33 : if (added)
230 : : {
231 : : Node clauseNode =
232 : 66 : nm->mkNode(Kind::OR, node[0].notNode(), node[1].notNode());
233 : 66 : d_proof->addStep(clauseNode, ProofRule::XOR_ELIM2, {node}, {});
234 [ + - ]: 66 : Trace("cnf") << "ProofCnfStream::convertAndAssertXor: XOR_ELIM2 added "
235 : 33 : << clauseNode << "\n";
236 : 33 : d_ppm->normalizeAndRegister(clauseNode, d_input);
237 : 33 : }
238 : : // Construct the clause (p v q)
239 : 33 : SatClause clause2(2);
240 : 33 : clause2[0] = p;
241 : 33 : clause2[1] = q;
242 : 33 : added = d_cnfStream.assertClause(node, clause2);
243 [ + - ]: 33 : if (added)
244 : : {
245 : 66 : Node clauseNode = nm->mkNode(Kind::OR, node[0], node[1]);
246 : 66 : d_proof->addStep(clauseNode, ProofRule::XOR_ELIM1, {node}, {});
247 [ + - ]: 66 : Trace("cnf") << "ProofCnfStream::convertAndAssertXor: XOR_ELIM1 added "
248 : 33 : << clauseNode << "\n";
249 : 33 : d_ppm->normalizeAndRegister(clauseNode, d_input);
250 : 33 : }
251 : 33 : }
252 : : else
253 : : {
254 : : // ~(p XOR q) is the same as p <=> q
255 : 9 : SatLiteral p = toCNF(node[0], false);
256 : 9 : SatLiteral q = toCNF(node[1], false);
257 : : bool added;
258 : 9 : NodeManager* nm = nodeManager();
259 : : // Construct the clause ~p v q
260 : 9 : SatClause clause1(2);
261 : 9 : clause1[0] = ~p;
262 : 9 : clause1[1] = q;
263 : 9 : added = d_cnfStream.assertClause(node.negate(), clause1);
264 [ + - ]: 9 : if (added)
265 : : {
266 : 18 : Node clauseNode = nm->mkNode(Kind::OR, node[0].notNode(), node[1]);
267 : 18 : d_proof->addStep(
268 : : clauseNode, ProofRule::NOT_XOR_ELIM2, {node.notNode()}, {});
269 [ + - ]: 18 : Trace("cnf")
270 : 0 : << "ProofCnfStream::convertAndAssertXor: NOT_XOR_ELIM2 added "
271 : 9 : << clauseNode << "\n";
272 : 9 : d_ppm->normalizeAndRegister(clauseNode, d_input);
273 : 9 : }
274 : : // Construct the clause ~q v p
275 : 9 : SatClause clause2(2);
276 : 9 : clause2[0] = p;
277 : 9 : clause2[1] = ~q;
278 : 9 : added = d_cnfStream.assertClause(node.negate(), clause2);
279 [ + - ]: 9 : if (added)
280 : : {
281 : 18 : Node clauseNode = nm->mkNode(Kind::OR, node[0], node[1].notNode());
282 : 18 : d_proof->addStep(
283 : : clauseNode, ProofRule::NOT_XOR_ELIM1, {node.notNode()}, {});
284 [ + - ]: 18 : Trace("cnf")
285 : 0 : << "ProofCnfStream::convertAndAssertXor: NOT_XOR_ELIM1 added "
286 : 9 : << clauseNode << "\n";
287 : 9 : d_ppm->normalizeAndRegister(clauseNode, d_input);
288 : 9 : }
289 : 9 : }
290 [ + - ]: 42 : Trace("cnf") << pop;
291 : 42 : }
292 : :
293 : 33525 : void ProofCnfStream::convertAndAssertIff(TNode node, bool negated)
294 : : {
295 [ + - ]: 67050 : Trace("cnf") << "ProofCnfStream::convertAndAssertIff(" << node
296 [ - - ]: 33525 : << ", negated = " << (negated ? "true" : "false") << ")\n"
297 : 33525 : << push;
298 [ + + ]: 33525 : if (!negated)
299 : : {
300 : : // p <=> q
301 [ + - ]: 33283 : Trace("cnf") << push;
302 : 33283 : SatLiteral p = toCNF(node[0], false);
303 : 33283 : SatLiteral q = toCNF(node[1], false);
304 [ + - ]: 33283 : Trace("cnf") << pop;
305 : : bool added;
306 : 33283 : NodeManager* nm = nodeManager();
307 : : // Construct the clauses ~p v q
308 : 33283 : SatClause clause1(2);
309 : 33283 : clause1[0] = ~p;
310 : 33283 : clause1[1] = q;
311 : 33283 : added = d_cnfStream.assertClause(node, clause1);
312 [ + + ]: 33283 : if (added)
313 : : {
314 : 61762 : Node clauseNode = nm->mkNode(Kind::OR, node[0].notNode(), node[1]);
315 : 61762 : d_proof->addStep(clauseNode, ProofRule::EQUIV_ELIM1, {node}, {});
316 [ + - ]: 61762 : Trace("cnf") << "ProofCnfStream::convertAndAssertIff: EQUIV_ELIM1 added "
317 : 30881 : << clauseNode << "\n";
318 : 30881 : d_ppm->normalizeAndRegister(clauseNode, d_input);
319 : 30881 : }
320 : : // Construct the clauses ~q v p
321 : 33283 : SatClause clause2(2);
322 : 33283 : clause2[0] = p;
323 : 33283 : clause2[1] = ~q;
324 : 33283 : added = d_cnfStream.assertClause(node, clause2);
325 [ + + ]: 33283 : if (added)
326 : : {
327 : 59164 : Node clauseNode = nm->mkNode(Kind::OR, node[0], node[1].notNode());
328 : 59164 : d_proof->addStep(clauseNode, ProofRule::EQUIV_ELIM2, {node}, {});
329 [ + - ]: 59164 : Trace("cnf") << "ProofCnfStream::convertAndAssertIff: EQUIV_ELIM2 added "
330 : 29582 : << clauseNode << "\n";
331 : 29582 : d_ppm->normalizeAndRegister(clauseNode, d_input);
332 : 29582 : }
333 : 33283 : }
334 : : else
335 : : {
336 : : // ~(p <=> q) is the same as p XOR q
337 [ + - ]: 242 : Trace("cnf") << push;
338 : 242 : SatLiteral p = toCNF(node[0], false);
339 : 242 : SatLiteral q = toCNF(node[1], false);
340 [ + - ]: 242 : Trace("cnf") << pop;
341 : : bool added;
342 : 242 : NodeManager* nm = nodeManager();
343 : : // Construct the clauses ~p v ~q
344 : 242 : SatClause clause1(2);
345 : 242 : clause1[0] = ~p;
346 : 242 : clause1[1] = ~q;
347 : 242 : added = d_cnfStream.assertClause(node.negate(), clause1);
348 [ + + ]: 242 : if (added)
349 : : {
350 : : Node clauseNode =
351 : 482 : nm->mkNode(Kind::OR, node[0].notNode(), node[1].notNode());
352 : 482 : d_proof->addStep(
353 : : clauseNode, ProofRule::NOT_EQUIV_ELIM2, {node.notNode()}, {});
354 [ + - ]: 482 : Trace("cnf")
355 : 0 : << "ProofCnfStream::convertAndAssertIff: NOT_EQUIV_ELIM2 added "
356 : 241 : << clauseNode << "\n";
357 : 241 : d_ppm->normalizeAndRegister(clauseNode, d_input);
358 : 241 : }
359 : : // Construct the clauses q v p
360 : 242 : SatClause clause2(2);
361 : 242 : clause2[0] = p;
362 : 242 : clause2[1] = q;
363 : 242 : added = d_cnfStream.assertClause(node.negate(), clause2);
364 [ + + ]: 242 : if (added)
365 : : {
366 : 466 : Node clauseNode = nm->mkNode(Kind::OR, node[0], node[1]);
367 : 466 : d_proof->addStep(
368 : : clauseNode, ProofRule::NOT_EQUIV_ELIM1, {node.notNode()}, {});
369 [ + - ]: 466 : Trace("cnf")
370 : 0 : << "ProofCnfStream::convertAndAssertIff: NOT_EQUIV_ELIM1 added "
371 : 233 : << clauseNode << "\n";
372 : 233 : d_ppm->normalizeAndRegister(clauseNode, d_input);
373 : 233 : }
374 : 242 : }
375 [ + - ]: 33525 : Trace("cnf") << pop;
376 : 33525 : }
377 : :
378 : 149722 : void ProofCnfStream::convertAndAssertImplies(TNode node, bool negated)
379 : : {
380 [ + - ]: 299444 : Trace("cnf") << "ProofCnfStream::convertAndAssertImplies(" << node
381 [ - - ]: 149722 : << ", negated = " << (negated ? "true" : "false") << ")\n"
382 : 149722 : << push;
383 [ + + ]: 149722 : if (!negated)
384 : : {
385 : : // ~p v q
386 : 149268 : SatLiteral p = toCNF(node[0], false);
387 : 149268 : SatLiteral q = toCNF(node[1], false);
388 : : // Construct the clause ~p || q
389 : 149268 : SatClause clause(2);
390 : 149268 : clause[0] = ~p;
391 : 149268 : clause[1] = q;
392 : 149268 : bool added = d_cnfStream.assertClause(node, clause);
393 [ + + ]: 149268 : if (added)
394 : : {
395 : : Node clauseNode =
396 : 295638 : nodeManager()->mkNode(Kind::OR, node[0].notNode(), node[1]);
397 : 295638 : d_proof->addStep(clauseNode, ProofRule::IMPLIES_ELIM, {node}, {});
398 [ + - ]: 295638 : Trace("cnf")
399 : 0 : << "ProofCnfStream::convertAndAssertImplies: IMPLIES_ELIM added "
400 : 147819 : << clauseNode << "\n";
401 : 147819 : d_ppm->normalizeAndRegister(clauseNode, d_input);
402 : 147819 : }
403 : 149268 : }
404 : : else
405 : : {
406 : : // ~(p => q) is the same as p ^ ~q
407 : : // process p
408 : 454 : convertAndAssert(node[0], false);
409 : 908 : d_proof->addStep(
410 : : node[0], ProofRule::NOT_IMPLIES_ELIM1, {node.notNode()}, {});
411 [ + - ]: 908 : Trace("cnf")
412 : 0 : << "ProofCnfStream::convertAndAssertImplies: NOT_IMPLIES_ELIM1 added "
413 [ - + ][ - - ]: 454 : << node[0] << "\n";
414 : : // process ~q
415 : 454 : convertAndAssert(node[1], true);
416 : 1816 : d_proof->addStep(
417 : 908 : node[1].notNode(), ProofRule::NOT_IMPLIES_ELIM2, {node.notNode()}, {});
418 [ + - ]: 908 : Trace("cnf")
419 : 0 : << "ProofCnfStream::convertAndAssertImplies: NOT_IMPLIES_ELIM2 added "
420 : 454 : << node[1].notNode() << "\n";
421 : : }
422 [ + - ]: 149722 : Trace("cnf") << pop;
423 : 149722 : }
424 : :
425 : 26636 : void ProofCnfStream::convertAndAssertIte(TNode node, bool negated)
426 : : {
427 [ + - ]: 53272 : Trace("cnf") << "ProofCnfStream::convertAndAssertIte(" << node
428 [ - - ]: 26636 : << ", negated = " << (negated ? "true" : "false") << ")\n"
429 : 26636 : << push;
430 : : // ITE(p, q, r)
431 : 26636 : SatLiteral p = toCNF(node[0], false);
432 : 26636 : SatLiteral q = toCNF(node[1], negated);
433 : 26636 : SatLiteral r = toCNF(node[2], negated);
434 : : bool added;
435 : 26636 : NodeManager* nm = nodeManager();
436 : : // Construct the clauses:
437 : : // (~p v q) and (p v r)
438 : : //
439 : : // Note that below q and r can be used directly because whether they are
440 : : // negated has been push to the literal definitions above
441 [ + + ]: 26636 : Node nnode = negated ? node.negate() : static_cast<Node>(node);
442 : : // (~p v q)
443 : 26636 : SatClause clause1(2);
444 : 26636 : clause1[0] = ~p;
445 : 26636 : clause1[1] = q;
446 : 26636 : added = d_cnfStream.assertClause(nnode, clause1);
447 [ + + ]: 26636 : if (added)
448 : : {
449 : : // redo the negation here to avoid silent double negation elimination
450 [ + + ]: 26136 : if (!negated)
451 : : {
452 : 52236 : Node clauseNode = nm->mkNode(Kind::OR, node[0].notNode(), node[1]);
453 : 52236 : d_proof->addStep(clauseNode, ProofRule::ITE_ELIM1, {node}, {});
454 [ + - ]: 52236 : Trace("cnf") << "ProofCnfStream::convertAndAssertIte: ITE_ELIM1 added "
455 : 26118 : << clauseNode << "\n";
456 : 26118 : d_ppm->normalizeAndRegister(clauseNode, d_input);
457 : 26118 : }
458 : : else
459 : : {
460 : : Node clauseNode =
461 : 36 : nm->mkNode(Kind::OR, node[0].notNode(), node[1].notNode());
462 : 36 : d_proof->addStep(
463 : : clauseNode, ProofRule::NOT_ITE_ELIM1, {node.notNode()}, {});
464 [ + - ]: 36 : Trace("cnf")
465 : 0 : << "ProofCnfStream::convertAndAssertIte: NOT_ITE_ELIM1 added "
466 : 18 : << clauseNode << "\n";
467 : 18 : d_ppm->normalizeAndRegister(clauseNode, d_input);
468 : 18 : }
469 : : }
470 : : // (p v r)
471 : 26636 : SatClause clause2(2);
472 : 26636 : clause2[0] = p;
473 : 26636 : clause2[1] = r;
474 : 26636 : added = d_cnfStream.assertClause(nnode, clause2);
475 [ + + ]: 26636 : if (added)
476 : : {
477 : : // redo the negation here to avoid silent double negation elimination
478 [ + + ]: 25946 : if (!negated)
479 : : {
480 : 51856 : Node clauseNode = nm->mkNode(Kind::OR, node[0], node[2]);
481 : 51856 : d_proof->addStep(clauseNode, ProofRule::ITE_ELIM2, {node}, {});
482 [ + - ]: 51856 : Trace("cnf") << "ProofCnfStream::convertAndAssertIte: ITE_ELIM2 added "
483 : 25928 : << clauseNode << "\n";
484 : 25928 : d_ppm->normalizeAndRegister(clauseNode, d_input);
485 : 25928 : }
486 : : else
487 : : {
488 : 36 : Node clauseNode = nm->mkNode(Kind::OR, node[0], node[2].notNode());
489 : 36 : d_proof->addStep(
490 : : clauseNode, ProofRule::NOT_ITE_ELIM2, {node.notNode()}, {});
491 [ + - ]: 36 : Trace("cnf")
492 : 0 : << "ProofCnfStream::convertAndAssertIte: NOT_ITE_ELIM2 added "
493 : 18 : << clauseNode << "\n";
494 : 18 : d_ppm->normalizeAndRegister(clauseNode, d_input);
495 : 18 : }
496 : : }
497 [ + - ]: 26636 : Trace("cnf") << pop;
498 : 26636 : }
499 : :
500 : 345649 : void ProofCnfStream::ensureLiteral(TNode n)
501 : : {
502 [ + - ]: 345649 : Trace("cnf") << "ProofCnfStream::ensureLiteral(" << n << ")\n";
503 [ + + ]: 345649 : if (d_cnfStream.hasLiteral(n))
504 : : {
505 : 254129 : d_cnfStream.ensureMappingForLiteral(n);
506 : 254129 : return;
507 : : }
508 : : // remove top level negation. We don't need to track this because it's a
509 : : // literal.
510 [ + + ]: 91520 : n = n.getKind() == Kind::NOT ? n[0] : n;
511 [ + + ][ + + ]: 91520 : if (d_env.theoryOf(n) == theory::THEORY_BOOL && !n.isVar())
[ + - ][ + + ]
[ - - ]
512 : : {
513 : : // These are not removable
514 : 54099 : d_cnfStream.d_removable = false;
515 : 54099 : SatLiteral lit = toCNF(n, false);
516 : : // Store backward-mappings
517 : : // These may already exist
518 : 54099 : d_cnfStream.d_literalToNodeMap.insert_safe(lit, n);
519 : 54099 : d_cnfStream.d_literalToNodeMap.insert_safe(~lit, n.notNode());
520 : : }
521 : : else
522 : : {
523 : 37421 : d_cnfStream.convertAtom(n);
524 : : }
525 : : }
526 : :
527 : 0 : bool ProofCnfStream::hasLiteral(TNode n) const
528 : : {
529 : 0 : return d_cnfStream.hasLiteral(n);
530 : : }
531 : :
532 : 0 : SatLiteral ProofCnfStream::getLiteral(TNode node)
533 : : {
534 : 0 : return d_cnfStream.getLiteral(node);
535 : : }
536 : :
537 : 0 : void ProofCnfStream::getBooleanVariables(
538 : : std::vector<TNode>& outputVariables) const
539 : : {
540 : 0 : d_cnfStream.getBooleanVariables(outputVariables);
541 : 0 : }
542 : :
543 : 4883465 : SatLiteral ProofCnfStream::toCNF(TNode node, bool negated)
544 : : {
545 [ + - ]: 9766930 : Trace("cnf") << "toCNF(" << node
546 [ - - ]: 4883465 : << ", negated = " << (negated ? "true" : "false") << ")\n";
547 : 4883465 : SatLiteral lit;
548 : : // If the node has already has a literal, return it (maybe negated)
549 [ + + ]: 4883465 : if (d_cnfStream.hasLiteral(node))
550 : : {
551 [ + - ]: 3253187 : Trace("cnf") << "toCNF(): already translated\n";
552 : 3253187 : lit = d_cnfStream.getLiteral(node);
553 : : // Return the (maybe negated) literal
554 [ + + ]: 3253187 : return !negated ? lit : ~lit;
555 : : }
556 : :
557 : : // Handle each Boolean operator case
558 [ + + ][ + + ]: 1630278 : switch (node.getKind())
[ + + ][ + + ]
559 : : {
560 : 267660 : case Kind::AND: lit = handleAnd(node); break;
561 : 184022 : case Kind::OR: lit = handleOr(node); break;
562 : 40805 : case Kind::XOR: lit = handleXor(node); break;
563 : 5054 : case Kind::IMPLIES: lit = handleImplies(node); break;
564 : 42265 : case Kind::ITE: lit = handleIte(node); break;
565 : 162815 : case Kind::NOT: lit = ~toCNF(node[0]); break;
566 : 460211 : case Kind::EQUAL:
567 [ + + ][ - - ]: 920422 : lit = node[0].getType().isBoolean() ? handleIff(node)
568 [ + + ][ + + ]: 460211 : : d_cnfStream.convertAtom(node);
[ - - ]
569 : 460211 : break;
570 : 467446 : default:
571 : : {
572 : 467446 : lit = d_cnfStream.convertAtom(node);
573 : : }
574 : 467446 : break;
575 : : }
576 : : // Return the (maybe negated) literal
577 [ + + ]: 1630278 : return !negated ? lit : ~lit;
578 : : }
579 : :
580 : 267660 : SatLiteral ProofCnfStream::handleAnd(TNode node)
581 : : {
582 [ - + ][ - + ]: 267660 : Assert(!d_cnfStream.hasLiteral(node)) << "Atom already mapped!";
[ - - ]
583 [ - + ][ - + ]: 267660 : Assert(node.getKind() == Kind::AND) << "Expecting an AND expression!";
[ - - ]
584 [ - + ][ - + ]: 267660 : Assert(node.getNumChildren() > 1) << "Expecting more than 1 child!";
[ - - ]
585 [ - + ][ - + ]: 267660 : Assert(!d_cnfStream.d_removable)
[ - - ]
586 : 0 : << "Removable clauses cannot contain Boolean structure";
587 [ + - ]: 267660 : Trace("cnf") << "ProofCnfStream::handleAnd(" << node << ")\n";
588 : : // Number of children
589 : 267660 : unsigned size = node.getNumChildren();
590 : : // Transform all the children first (remembering the negation)
591 : 267660 : SatClause clause(size + 1);
592 [ + + ]: 1316784 : for (unsigned i = 0; i < size; ++i)
593 : : {
594 [ + - ]: 1049124 : Trace("cnf") << push;
595 : 1049124 : clause[i] = ~toCNF(node[i]);
596 [ + - ]: 1049124 : Trace("cnf") << pop;
597 : : }
598 : : // Create literal for the node
599 : 267660 : SatLiteral lit = d_cnfStream.newLiteral(node);
600 : : bool added;
601 : 267660 : NodeManager* nm = nodeManager();
602 : : // lit -> (a_1 & a_2 & a_3 & ... & a_n)
603 : : // ~lit | (a_1 & a_2 & a_3 & ... & a_n)
604 : : // (~lit | a_1) & (~lit | a_2) & ... & (~lit | a_n)
605 [ + + ]: 1316784 : for (unsigned i = 0; i < size; ++i)
606 : : {
607 [ + - ]: 1049124 : Trace("cnf") << push;
608 : 1049124 : added = d_cnfStream.assertClause(node.negate(), ~lit, ~clause[i]);
609 [ + - ]: 1049124 : Trace("cnf") << pop;
610 [ + + ]: 1049124 : if (added)
611 : : {
612 : 1980124 : Node clauseNode = nm->mkNode(Kind::OR, node.notNode(), node[i]);
613 : 990062 : Node iNode = nm->mkConstInt(i);
614 [ + + ][ - - ]: 2970186 : d_proof->addStep(clauseNode, ProofRule::CNF_AND_POS, {}, {node, iNode});
615 [ + - ]: 1980124 : Trace("cnf") << "ProofCnfStream::handleAnd: CNF_AND_POS " << i
616 : 990062 : << " added " << clauseNode << "\n";
617 : 990062 : d_ppm->normalizeAndRegister(clauseNode, d_input);
618 : 990062 : }
619 : : }
620 : : // lit <- (a_1 & a_2 & a_3 & ... a_n)
621 : : // lit | ~(a_1 & a_2 & a_3 & ... & a_n)
622 : : // lit | ~a_1 | ~a_2 | ~a_3 | ... | ~a_n
623 : 267660 : clause[size] = lit;
624 : : // This needs to go last, as the clause might get modified by the SAT solver
625 [ + - ]: 267660 : Trace("cnf") << push;
626 : 267660 : added = d_cnfStream.assertClause(node, clause);
627 [ + - ]: 267660 : Trace("cnf") << pop;
628 [ + + ]: 267660 : if (added)
629 : : {
630 : 789675 : std::vector<Node> disjuncts{node};
631 [ + + ]: 1294180 : for (unsigned i = 0; i < size; ++i)
632 : : {
633 : 1030955 : disjuncts.push_back(node[i].notNode());
634 : : }
635 : 263225 : Node clauseNode = nm->mkNode(Kind::OR, disjuncts);
636 : 526450 : d_proof->addStep(clauseNode, ProofRule::CNF_AND_NEG, {}, {node});
637 [ + - ]: 526450 : Trace("cnf") << "ProofCnfStream::handleAnd: CNF_AND_NEG added "
638 : 263225 : << clauseNode << "\n";
639 : 263225 : d_ppm->normalizeAndRegister(clauseNode, d_input);
640 : 263225 : }
641 : 267660 : return lit;
642 : 267660 : }
643 : :
644 : 184022 : SatLiteral ProofCnfStream::handleOr(TNode node)
645 : : {
646 [ - + ][ - + ]: 184022 : Assert(!d_cnfStream.hasLiteral(node)) << "Atom already mapped!";
[ - - ]
647 [ - + ][ - + ]: 184022 : Assert(node.getKind() == Kind::OR) << "Expecting an OR expression!";
[ - - ]
648 [ - + ][ - + ]: 184022 : Assert(node.getNumChildren() > 1) << "Expecting more then 1 child!";
[ - - ]
649 [ - + ][ - + ]: 184022 : Assert(!d_cnfStream.d_removable)
[ - - ]
650 : 0 : << "Removable clauses can not contain Boolean structure";
651 [ + - ]: 184022 : Trace("cnf") << "ProofCnfStream::handleOr(" << node << ")\n";
652 : : // Number of children
653 : 184022 : unsigned size = node.getNumChildren();
654 : : // Transform all the children first
655 : 184022 : SatClause clause(size + 1);
656 [ + + ]: 767731 : for (unsigned i = 0; i < size; ++i)
657 : : {
658 : 583709 : clause[i] = toCNF(node[i]);
659 : : }
660 : : // Create literal for the node
661 : 184022 : SatLiteral lit = d_cnfStream.newLiteral(node);
662 : : bool added;
663 : 184022 : NodeManager* nm = nodeManager();
664 : : // lit <- (a_1 | a_2 | a_3 | ... | a_n)
665 : : // lit | ~(a_1 | a_2 | a_3 | ... | a_n)
666 : : // (lit | ~a_1) & (lit | ~a_2) & (lit & ~a_3) & ... & (lit & ~a_n)
667 [ + + ]: 767731 : for (unsigned i = 0; i < size; ++i)
668 : : {
669 : 583709 : added = d_cnfStream.assertClause(node, lit, ~clause[i]);
670 [ + + ]: 583709 : if (added)
671 : : {
672 : 1130804 : Node clauseNode = nm->mkNode(Kind::OR, node, node[i].notNode());
673 : 565402 : Node iNode = nm->mkConstInt(i);
674 [ + + ][ - - ]: 1696206 : d_proof->addStep(clauseNode, ProofRule::CNF_OR_NEG, {}, {node, iNode});
675 [ + - ]: 1130804 : Trace("cnf") << "ProofCnfStream::handleOr: CNF_OR_NEG " << i << " added "
676 : 565402 : << clauseNode << "\n";
677 : 565402 : d_ppm->normalizeAndRegister(clauseNode, d_input);
678 : 565402 : }
679 : : }
680 : : // lit -> (a_1 | a_2 | a_3 | ... | a_n)
681 : : // ~lit | a_1 | a_2 | a_3 | ... | a_n
682 : 184022 : clause[size] = ~lit;
683 : : // This needs to go last, as the clause might get modified by the SAT solver
684 : 184022 : added = d_cnfStream.assertClause(node.negate(), clause);
685 [ + + ]: 184022 : if (added)
686 : : {
687 : 543555 : std::vector<Node> disjuncts{node.notNode()};
688 [ + + ]: 755876 : for (unsigned i = 0; i < size; ++i)
689 : : {
690 : 574691 : disjuncts.push_back(node[i]);
691 : : }
692 : 181185 : Node clauseNode = nm->mkNode(Kind::OR, disjuncts);
693 : 362370 : d_proof->addStep(clauseNode, ProofRule::CNF_OR_POS, {}, {node});
694 [ + - ]: 362370 : Trace("cnf") << "ProofCnfStream::handleOr: CNF_OR_POS added " << clauseNode
695 : 181185 : << "\n";
696 : 181185 : d_ppm->normalizeAndRegister(clauseNode, d_input);
697 : 181185 : }
698 : 184022 : return lit;
699 : 184022 : }
700 : :
701 : 40805 : SatLiteral ProofCnfStream::handleXor(TNode node)
702 : : {
703 [ - + ][ - + ]: 40805 : Assert(!d_cnfStream.hasLiteral(node)) << "Atom already mapped!";
[ - - ]
704 [ - + ][ - + ]: 40805 : Assert(node.getKind() == Kind::XOR) << "Expecting an XOR expression!";
[ - - ]
705 [ - + ][ - + ]: 40805 : Assert(node.getNumChildren() == 2) << "Expecting exactly 2 children!";
[ - - ]
706 [ - + ][ - + ]: 40805 : Assert(!d_cnfStream.d_removable)
[ - - ]
707 : 0 : << "Removable clauses can not contain Boolean structure";
708 [ + - ]: 40805 : Trace("cnf") << "ProofCnfStream::handleXor(" << node << ")\n";
709 : 40805 : SatLiteral a = toCNF(node[0]);
710 : 40805 : SatLiteral b = toCNF(node[1]);
711 : 40805 : SatLiteral lit = d_cnfStream.newLiteral(node);
712 : : bool added;
713 : 40805 : added = d_cnfStream.assertClause(node.negate(), a, b, ~lit);
714 [ + + ]: 40805 : if (added)
715 : : {
716 : : Node clauseNode =
717 : 81272 : nodeManager()->mkNode(Kind::OR, node.notNode(), node[0], node[1]);
718 : 81272 : d_proof->addStep(clauseNode, ProofRule::CNF_XOR_POS1, {}, {node});
719 [ + - ]: 81272 : Trace("cnf") << "ProofCnfStream::handleXor: CNF_XOR_POS1 added "
720 : 40636 : << clauseNode << "\n";
721 : 40636 : d_ppm->normalizeAndRegister(clauseNode, d_input);
722 : 40636 : }
723 : 40805 : added = d_cnfStream.assertClause(node.negate(), ~a, ~b, ~lit);
724 [ + + ]: 40805 : if (added)
725 : : {
726 : 40635 : Node clauseNode = nodeManager()->mkNode(
727 : 81270 : Kind::OR, node.notNode(), node[0].notNode(), node[1].notNode());
728 : 81270 : d_proof->addStep(clauseNode, ProofRule::CNF_XOR_POS2, {}, {node});
729 [ + - ]: 81270 : Trace("cnf") << "ProofCnfStream::handleXor: CNF_XOR_POS2 added "
730 : 40635 : << clauseNode << "\n";
731 : 40635 : d_ppm->normalizeAndRegister(clauseNode, d_input);
732 : 40635 : }
733 : 40805 : added = d_cnfStream.assertClause(node, a, ~b, lit);
734 [ + + ]: 40805 : if (added)
735 : : {
736 : : Node clauseNode =
737 : 81254 : nodeManager()->mkNode(Kind::OR, node, node[0], node[1].notNode());
738 : 81254 : d_proof->addStep(clauseNode, ProofRule::CNF_XOR_NEG2, {}, {node});
739 [ + - ]: 81254 : Trace("cnf") << "ProofCnfStream::handleXor: CNF_XOR_NEG2 added "
740 : 40627 : << clauseNode << "\n";
741 : 40627 : d_ppm->normalizeAndRegister(clauseNode, d_input);
742 : 40627 : }
743 : 40805 : added = d_cnfStream.assertClause(node, ~a, b, lit);
744 [ + + ]: 40805 : if (added)
745 : : {
746 : : Node clauseNode =
747 : 81328 : nodeManager()->mkNode(Kind::OR, node, node[0].notNode(), node[1]);
748 : 81328 : d_proof->addStep(clauseNode, ProofRule::CNF_XOR_NEG1, {}, {node});
749 [ + - ]: 81328 : Trace("cnf") << "ProofCnfStream::handleXor: CNF_XOR_NEG1 added "
750 : 40664 : << clauseNode << "\n";
751 : 40664 : d_ppm->normalizeAndRegister(clauseNode, d_input);
752 : 40664 : }
753 : 40805 : return lit;
754 : : }
755 : :
756 : 131834 : SatLiteral ProofCnfStream::handleIff(TNode node)
757 : : {
758 [ - + ][ - + ]: 131834 : Assert(!d_cnfStream.hasLiteral(node)) << "Atom already mapped!";
[ - - ]
759 [ - + ][ - + ]: 131834 : Assert(node.getKind() == Kind::EQUAL) << "Expecting an EQUAL expression!";
[ - - ]
760 [ - + ][ - + ]: 131834 : Assert(node.getNumChildren() == 2) << "Expecting exactly 2 children!";
[ - - ]
761 [ + - ]: 131834 : Trace("cnf") << "handleIff(" << node << ")\n";
762 : : // Convert the children to CNF
763 : 131834 : SatLiteral a = toCNF(node[0]);
764 : 131834 : SatLiteral b = toCNF(node[1]);
765 : : // Create literal for the node
766 : 131834 : SatLiteral lit = d_cnfStream.newLiteral(node);
767 : : bool added;
768 : 131834 : NodeManager* nm = nodeManager();
769 : : // lit -> ((a-> b) & (b->a))
770 : : // ~lit | ((~a | b) & (~b | a))
771 : : // (~a | b | ~lit) & (~b | a | ~lit)
772 : 131834 : added = d_cnfStream.assertClause(node.negate(), ~a, b, ~lit);
773 [ + + ]: 131834 : if (added)
774 : : {
775 : : Node clauseNode =
776 : 259346 : nm->mkNode(Kind::OR, node.notNode(), node[0].notNode(), node[1]);
777 : 259346 : d_proof->addStep(clauseNode, ProofRule::CNF_EQUIV_POS1, {}, {node});
778 [ + - ]: 259346 : Trace("cnf") << "ProofCnfStream::handleIff: CNF_EQUIV_POS1 added "
779 : 129673 : << clauseNode << "\n";
780 : 129673 : d_ppm->normalizeAndRegister(clauseNode, d_input);
781 : 129673 : }
782 : 131834 : added = d_cnfStream.assertClause(node.negate(), a, ~b, ~lit);
783 [ + + ]: 131834 : if (added)
784 : : {
785 : : Node clauseNode =
786 : 253362 : nm->mkNode(Kind::OR, node.notNode(), node[0], node[1].notNode());
787 : 253362 : d_proof->addStep(clauseNode, ProofRule::CNF_EQUIV_POS2, {}, {node});
788 [ + - ]: 253362 : Trace("cnf") << "ProofCnfStream::handleIff: CNF_EQUIV_POS2 added "
789 : 126681 : << clauseNode << "\n";
790 : 126681 : d_ppm->normalizeAndRegister(clauseNode, d_input);
791 : 126681 : }
792 : : // (a<->b) -> lit
793 : : // ~((a & b) | (~a & ~b)) | lit
794 : : // (~(a & b)) & (~(~a & ~b)) | lit
795 : : // ((~a | ~b) & (a | b)) | lit
796 : : // (~a | ~b | lit) & (a | b | lit)
797 : 131834 : added = d_cnfStream.assertClause(node, ~a, ~b, lit);
798 [ + + ]: 131834 : if (added)
799 : : {
800 : : Node clauseNode =
801 : 258822 : nm->mkNode(Kind::OR, node, node[0].notNode(), node[1].notNode());
802 : 258822 : d_proof->addStep(clauseNode, ProofRule::CNF_EQUIV_NEG2, {}, {node});
803 [ + - ]: 258822 : Trace("cnf") << "ProofCnfStream::handleIff: CNF_EQUIV_NEG2 added "
804 : 129411 : << clauseNode << "\n";
805 : 129411 : d_ppm->normalizeAndRegister(clauseNode, d_input);
806 : 129411 : }
807 : 131834 : added = d_cnfStream.assertClause(node, a, b, lit);
808 [ + + ]: 131834 : if (added)
809 : : {
810 : 253952 : Node clauseNode = nm->mkNode(Kind::OR, node, node[0], node[1]);
811 : 253952 : d_proof->addStep(clauseNode, ProofRule::CNF_EQUIV_NEG1, {}, {node});
812 [ + - ]: 253952 : Trace("cnf") << "ProofCnfStream::handleIff: CNF_EQUIV_NEG1 added "
813 : 126976 : << clauseNode << "\n";
814 : 126976 : d_ppm->normalizeAndRegister(clauseNode, d_input);
815 : 126976 : }
816 : 131834 : return lit;
817 : : }
818 : :
819 : 5054 : SatLiteral ProofCnfStream::handleImplies(TNode node)
820 : : {
821 [ - + ][ - + ]: 5054 : Assert(!d_cnfStream.hasLiteral(node)) << "Atom already mapped!";
[ - - ]
822 [ - + ][ - + ]: 5054 : Assert(node.getKind() == Kind::IMPLIES) << "Expecting an IMPLIES expression!";
[ - - ]
823 [ - + ][ - + ]: 5054 : Assert(node.getNumChildren() == 2) << "Expecting exactly 2 children!";
[ - - ]
824 [ - + ][ - + ]: 5054 : Assert(!d_cnfStream.d_removable)
[ - - ]
825 : 0 : << "Removable clauses can not contain Boolean structure";
826 [ + - ]: 5054 : Trace("cnf") << "ProofCnfStream::handleImplies(" << node << ")\n";
827 : : // Convert the children to cnf
828 : 5054 : SatLiteral a = toCNF(node[0]);
829 : 5054 : SatLiteral b = toCNF(node[1]);
830 : 5054 : SatLiteral lit = d_cnfStream.newLiteral(node);
831 : : bool added;
832 : 5054 : NodeManager* nm = nodeManager();
833 : : // lit -> (a->b)
834 : : // ~lit | ~ a | b
835 : 5054 : added = d_cnfStream.assertClause(node.negate(), ~lit, ~a, b);
836 [ + + ]: 5054 : if (added)
837 : : {
838 : : Node clauseNode =
839 : 10024 : nm->mkNode(Kind::OR, node.notNode(), node[0].notNode(), node[1]);
840 : 10024 : d_proof->addStep(clauseNode, ProofRule::CNF_IMPLIES_POS, {}, {node});
841 [ + - ]: 10024 : Trace("cnf") << "ProofCnfStream::handleImplies: CNF_IMPLIES_POS added "
842 : 5012 : << clauseNode << "\n";
843 : 5012 : d_ppm->normalizeAndRegister(clauseNode, d_input);
844 : 5012 : }
845 : : // (a->b) -> lit
846 : : // ~(~a | b) | lit
847 : : // (a | l) & (~b | l)
848 : 5054 : added = d_cnfStream.assertClause(node, a, lit);
849 [ + + ]: 5054 : if (added)
850 : : {
851 : 10074 : Node clauseNode = nm->mkNode(Kind::OR, node, node[0]);
852 : 10074 : d_proof->addStep(clauseNode, ProofRule::CNF_IMPLIES_NEG1, {}, {node});
853 [ + - ]: 10074 : Trace("cnf") << "ProofCnfStream::handleImplies: CNF_IMPLIES_NEG1 added "
854 : 5037 : << clauseNode << "\n";
855 : 5037 : d_ppm->normalizeAndRegister(clauseNode, d_input);
856 : 5037 : }
857 : 5054 : added = d_cnfStream.assertClause(node, ~b, lit);
858 [ + + ]: 5054 : if (added)
859 : : {
860 : 10098 : Node clauseNode = nm->mkNode(Kind::OR, node, node[1].notNode());
861 : 10098 : d_proof->addStep(clauseNode, ProofRule::CNF_IMPLIES_NEG2, {}, {node});
862 [ + - ]: 10098 : Trace("cnf") << "ProofCnfStream::handleImplies: CNF_IMPLIES_NEG2 added "
863 : 5049 : << clauseNode << "\n";
864 : 5049 : d_ppm->normalizeAndRegister(clauseNode, d_input);
865 : 5049 : }
866 : 5054 : return lit;
867 : : }
868 : :
869 : 42265 : SatLiteral ProofCnfStream::handleIte(TNode node)
870 : : {
871 [ - + ][ - + ]: 42265 : Assert(!d_cnfStream.hasLiteral(node)) << "Atom already mapped!";
[ - - ]
872 [ - + ][ - + ]: 42265 : Assert(node.getKind() == Kind::ITE);
[ - - ]
873 [ - + ][ - + ]: 42265 : Assert(node.getNumChildren() == 3);
[ - - ]
874 [ - + ][ - + ]: 42265 : Assert(!d_cnfStream.d_removable)
[ - - ]
875 : 0 : << "Removable clauses can not contain Boolean structure";
876 : 84530 : Trace("cnf") << "handleIte(" << node[0] << " " << node[1] << " " << node[2]
877 : 42265 : << ")\n";
878 : 42265 : SatLiteral condLit = toCNF(node[0]);
879 : 42265 : SatLiteral thenLit = toCNF(node[1]);
880 : 42265 : SatLiteral elseLit = toCNF(node[2]);
881 : : // create literal to the node
882 : 42265 : SatLiteral lit = d_cnfStream.newLiteral(node);
883 : : bool added;
884 : 42265 : NodeManager* nm = nodeManager();
885 : : // If ITE is true then one of the branches is true and the condition
886 : : // implies which one
887 : : // lit -> (ite b t e)
888 : : // lit -> (t | e) & (b -> t) & (!b -> e)
889 : : // lit -> (t | e) & (!b | t) & (b | e)
890 : : // (!lit | t | e) & (!lit | !b | t) & (!lit | b | e)
891 : 42265 : added = d_cnfStream.assertClause(node.negate(), ~lit, thenLit, elseLit);
892 [ + + ]: 42265 : if (added)
893 : : {
894 : 84266 : Node clauseNode = nm->mkNode(Kind::OR, node.notNode(), node[1], node[2]);
895 : 84266 : d_proof->addStep(clauseNode, ProofRule::CNF_ITE_POS3, {}, {node});
896 [ + - ]: 84266 : Trace("cnf") << "ProofCnfStream::handleIte: CNF_ITE_POS3 added "
897 : 42133 : << clauseNode << "\n";
898 : 42133 : d_ppm->normalizeAndRegister(clauseNode, d_input);
899 : 42133 : }
900 : 42265 : added = d_cnfStream.assertClause(node.negate(), ~lit, ~condLit, thenLit);
901 [ + + ]: 42265 : if (added)
902 : : {
903 : : Node clauseNode =
904 : 82056 : nm->mkNode(Kind::OR, node.notNode(), node[0].notNode(), node[1]);
905 : 82056 : d_proof->addStep(clauseNode, ProofRule::CNF_ITE_POS1, {}, {node});
906 [ + - ]: 82056 : Trace("cnf") << "ProofCnfStream::handleIte: CNF_ITE_POS1 added "
907 : 41028 : << clauseNode << "\n";
908 : 41028 : d_ppm->normalizeAndRegister(clauseNode, d_input);
909 : 41028 : }
910 : 42265 : added = d_cnfStream.assertClause(node.negate(), ~lit, condLit, elseLit);
911 [ + + ]: 42265 : if (added)
912 : : {
913 : 77368 : Node clauseNode = nm->mkNode(Kind::OR, node.notNode(), node[0], node[2]);
914 : 77368 : d_proof->addStep(clauseNode, ProofRule::CNF_ITE_POS2, {}, {node});
915 [ + - ]: 77368 : Trace("cnf") << "ProofCnfStream::handleIte: CNF_ITE_POS2 added "
916 : 38684 : << clauseNode << "\n";
917 : 38684 : d_ppm->normalizeAndRegister(clauseNode, d_input);
918 : 38684 : }
919 : : // If ITE is false then one of the branches is false and the condition
920 : : // implies which one
921 : : // !lit -> !(ite b t e)
922 : : // !lit -> (!t | !e) & (b -> !t) & (!b -> !e)
923 : : // !lit -> (!t | !e) & (!b | !t) & (b | !e)
924 : : // (lit | !t | !e) & (lit | !b | !t) & (lit | b | !e)
925 : 42265 : added = d_cnfStream.assertClause(node, lit, ~thenLit, ~elseLit);
926 [ + + ]: 42265 : if (added)
927 : : {
928 : : Node clauseNode =
929 : 84240 : nm->mkNode(Kind::OR, node, node[1].notNode(), node[2].notNode());
930 : 84240 : d_proof->addStep(clauseNode, ProofRule::CNF_ITE_NEG3, {}, {node});
931 [ + - ]: 84240 : Trace("cnf") << "ProofCnfStream::handleIte: CNF_ITE_NEG3 added "
932 : 42120 : << clauseNode << "\n";
933 : 42120 : d_ppm->normalizeAndRegister(clauseNode, d_input);
934 : 42120 : }
935 : 42265 : added = d_cnfStream.assertClause(node, lit, ~condLit, ~thenLit);
936 [ + + ]: 42265 : if (added)
937 : : {
938 : : Node clauseNode =
939 : 81992 : nm->mkNode(Kind::OR, node, node[0].notNode(), node[1].notNode());
940 : 81992 : d_proof->addStep(clauseNode, ProofRule::CNF_ITE_NEG1, {}, {node});
941 [ + - ]: 81992 : Trace("cnf") << "ProofCnfStream::handleIte: CNF_ITE_NEG1 added "
942 : 40996 : << clauseNode << "\n";
943 : 40996 : d_ppm->normalizeAndRegister(clauseNode, d_input);
944 : 40996 : }
945 : 42265 : added = d_cnfStream.assertClause(node, lit, condLit, ~elseLit);
946 [ + + ]: 42265 : if (added)
947 : : {
948 : 77326 : Node clauseNode = nm->mkNode(Kind::OR, node, node[0], node[2].notNode());
949 : 77326 : d_proof->addStep(clauseNode, ProofRule::CNF_ITE_NEG2, {}, {node});
950 [ + - ]: 77326 : Trace("cnf") << "ProofCnfStream::handleIte: CNF_ITE_NEG2 added "
951 : 38663 : << clauseNode << "\n";
952 : 38663 : d_ppm->normalizeAndRegister(clauseNode, d_input);
953 : 38663 : }
954 : 42265 : return lit;
955 : : }
956 : :
957 : 0 : void ProofCnfStream::dumpDimacs(std::ostream& out,
958 : : const std::vector<Node>& clauses)
959 : : {
960 : 0 : d_cnfStream.dumpDimacs(out, clauses);
961 : 0 : }
962 : :
963 : 0 : void ProofCnfStream::dumpDimacs(std::ostream& out,
964 : : const std::vector<Node>& clauses,
965 : : const std::vector<Node>& auxUnits)
966 : : {
967 : 0 : d_cnfStream.dumpDimacs(out, clauses, auxUnits);
968 : 0 : }
969 : :
970 : : } // namespace prop
971 : : } // namespace cvc5::internal
|
