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