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 : 15206 : ProofCnfStream::ProofCnfStream(Env& env,
24 : : CnfStream& cnfStream,
25 : 15206 : PropPfManager* ppm)
26 : : : EnvObj(env),
27 : 15206 : d_cnfStream(cnfStream),
28 : 15206 : d_ppm(ppm),
29 : 15206 : d_proof(ppm->getCnfProof())
30 : : {
31 : 15206 : }
32 : :
33 : 754855 : void ProofCnfStream::convertAndAssert(
34 : : TNode node, bool negated, bool removable, bool input, ProofGenerator* pg)
35 : : {
36 : : // this method is re-entrant due to lemmas sent during preregistration of new
37 : : // lemmas, thus we must remember and revert d_input below.
38 : 754855 : bool backupInput = d_input;
39 [ + - ]: 1509710 : Trace("cnf") << "ProofCnfStream::convertAndAssert(" << node
40 [ - - ]: 0 : << ", negated = " << (negated ? "true" : "false")
41 [ - - ]: 0 : << ", removable = " << (removable ? "true" : "false")
42 [ - - ]: 0 : << ", input = " << (input ? "true" : "false") << "), level "
43 : 754855 : << userContext()->getLevel() << "\n";
44 : 754855 : d_cnfStream.d_removable = removable;
45 : 754855 : d_input = input;
46 [ + + ]: 754855 : if (pg)
47 : : {
48 [ + - ][ - + ]: 909562 : Trace("cnf") << "ProofCnfStream::convertAndAssert: pg: " << pg->identify()
[ - - ]
49 : 454781 : << "\n";
50 [ + + ]: 454781 : Node toJustify = negated ? node.notNode() : static_cast<Node>(node);
51 : 454781 : d_proof->addLazyStep(toJustify,
52 : : pg,
53 : : TrustId::NONE,
54 : : true,
55 : : "ProofCnfStream::convertAndAssert:cnf");
56 : 454781 : }
57 : 754855 : convertAndAssert(node, negated);
58 : 754855 : d_input = backupInput;
59 : 754855 : }
60 : :
61 : 852246 : void ProofCnfStream::convertAndAssert(TNode node, bool negated)
62 : : {
63 [ + - ]: 1704492 : Trace("cnf") << "ProofCnfStream::convertAndAssert(" << node
64 [ - - ]: 852246 : << ", negated = " << (negated ? "true" : "false") << ")\n"
65 : 852246 : << push;
66 [ + + ][ + + ]: 852246 : switch (node.getKind())
[ + + ][ + + ]
67 : : {
68 : 140585 : case Kind::AND: convertAndAssertAnd(node, negated); break;
69 : 249666 : case Kind::OR: convertAndAssertOr(node, negated); break;
70 : 42 : case Kind::XOR: convertAndAssertXor(node, negated); break;
71 : 151209 : case Kind::IMPLIES: convertAndAssertImplies(node, negated); break;
72 : 28245 : case Kind::ITE: convertAndAssertIte(node, negated); break;
73 : 38792 : case Kind::NOT:
74 : : {
75 : : // track double negation elimination
76 [ + + ]: 38792 : if (negated)
77 : : {
78 : 4672 : d_proof->addStep(
79 : : node[0], ProofRule::NOT_NOT_ELIM, {node.notNode()}, {});
80 [ + - ]: 4672 : Trace("cnf")
81 : 0 : << "ProofCnfStream::convertAndAssert: NOT_NOT_ELIM added norm "
82 [ - + ][ - - ]: 2336 : << node[0] << "\n";
83 : : }
84 : 38792 : convertAndAssert(node[0], !negated);
85 : 38792 : break;
86 : : }
87 : 109489 : case Kind::EQUAL:
88 [ + + ]: 109489 : if (node[0].getType().isBoolean())
89 : : {
90 : 33118 : convertAndAssertIff(node, negated);
91 : 33118 : break;
92 : : }
93 : : CVC5_FALLTHROUGH;
94 : : default:
95 : : {
96 : : // negate
97 [ + + ]: 210589 : Node nnode = negated ? node.negate() : static_cast<Node>(node);
98 : : // Atoms
99 : 210589 : SatLiteral lit = toCNF(node, negated);
100 [ + + ][ - + ]: 210589 : if (negated && nnode != node.notNode())
[ + + ][ - + ]
[ - - ]
101 : : {
102 : : // track double negation elimination
103 : : // (not (not n))
104 : : // -------------- NOT_NOT_ELIM
105 : : // n
106 : 0 : d_proof->addStep(nnode, ProofRule::NOT_NOT_ELIM, {node.notNode()}, {});
107 [ - - ]: 0 : Trace("cnf")
108 : 0 : << "ProofCnfStream::convertAndAssert: NOT_NOT_ELIM added norm "
109 : 0 : << nnode << "\n";
110 : : }
111 : : // note that we do not need to do the normalization here, just add it,
112 : : // since this is not a clause and double negation is tracked in a
113 : : // dedicated manner above
114 : 210589 : d_ppm->normalizeAndRegister(nnode, d_input, false);
115 : 210589 : d_cnfStream.assertClause(nnode, lit);
116 : 210589 : }
117 : : }
118 [ + - ]: 852246 : Trace("cnf") << pop;
119 : 852246 : }
120 : :
121 : 140585 : void ProofCnfStream::convertAndAssertAnd(TNode node, bool negated)
122 : : {
123 [ + - ]: 281170 : Trace("cnf") << "ProofCnfStream::convertAndAssertAnd(" << node
124 [ - - ]: 140585 : << ", negated = " << (negated ? "true" : "false") << ")\n"
125 : 140585 : << push;
126 [ - + ][ - + ]: 140585 : Assert(node.getKind() == Kind::AND);
[ - - ]
127 [ + + ]: 140585 : if (!negated)
128 : : {
129 : : // If the node is a conjunction, we handle each conjunct separately
130 : 21681 : NodeManager* nm = nodeManager();
131 [ + + ]: 76521 : for (unsigned i = 0, size = node.getNumChildren(); i < size; ++i)
132 : : {
133 : : // Create a proof step for each n_i
134 : 54840 : Node iNode = nm->mkConstInt(i);
135 : 164520 : d_proof->addStep(node[i], ProofRule::AND_ELIM, {node}, {iNode});
136 [ + - ]: 109680 : Trace("cnf") << "ProofCnfStream::convertAndAssertAnd: AND_ELIM " << i
137 [ - + ][ - - ]: 54840 : << " added norm " << node[i] << "\n";
138 : 54840 : convertAndAssert(node[i], false);
139 : 54840 : }
140 : : }
141 : : else
142 : : {
143 : : // If the node is a disjunction, we construct a clause and assert it
144 : 118904 : unsigned i, size = node.getNumChildren();
145 : 118904 : SatClause clause(size);
146 [ + + ]: 1195436 : for (i = 0; i < size; ++i)
147 : : {
148 : 1076532 : clause[i] = toCNF(node[i], true);
149 : : }
150 : : // register proof step
151 : 118904 : std::vector<Node> disjuncts;
152 [ + + ]: 1195436 : for (i = 0; i < size; ++i)
153 : : {
154 : 1076532 : disjuncts.push_back(node[i].notNode());
155 : : }
156 : 118904 : Node clauseNode = nodeManager()->mkNode(Kind::OR, disjuncts);
157 : 237808 : d_proof->addStep(clauseNode, ProofRule::NOT_AND, {node.notNode()}, {});
158 [ + - ]: 237808 : Trace("cnf") << "ProofCnfStream::convertAndAssertAnd: NOT_AND added "
159 : 118904 : << clauseNode << "\n";
160 : 118904 : d_ppm->normalizeAndRegister(clauseNode, d_input);
161 : 118904 : d_cnfStream.assertClause(node.negate(), clause);
162 : 118904 : }
163 [ + - ]: 140585 : Trace("cnf") << pop;
164 : 140585 : }
165 : :
166 : 249666 : void ProofCnfStream::convertAndAssertOr(TNode node, bool negated)
167 : : {
168 [ + - ]: 499332 : Trace("cnf") << "ProofCnfStream::convertAndAssertOr(" << node
169 [ - - ]: 249666 : << ", negated = " << (negated ? "true" : "false") << ")\n"
170 : 249666 : << push;
171 [ - + ][ - + ]: 249666 : Assert(node.getKind() == Kind::OR);
[ - - ]
172 [ + + ]: 249666 : if (!negated)
173 : : {
174 : : // If the node is a disjunction, we construct a clause and assert it
175 : 249422 : unsigned size = node.getNumChildren();
176 : 249422 : SatClause clause(size);
177 [ + + ]: 1061419 : for (unsigned i = 0; i < size; ++i)
178 : : {
179 : 811997 : clause[i] = toCNF(node[i], false);
180 : : }
181 : 249422 : d_ppm->normalizeAndRegister(node, d_input);
182 : 249422 : d_cnfStream.assertClause(node, clause);
183 : 249422 : }
184 : : else
185 : : {
186 : : // If the node is a negated disjunction, we handle it as a conjunction of
187 : : // the negated arguments
188 : 244 : NodeManager* nm = nodeManager();
189 [ + + ]: 3103 : for (unsigned i = 0, size = node.getNumChildren(); i < size; ++i)
190 : : {
191 : : // Create a proof step for each (not n_i)
192 : 2859 : Node iNode = nm->mkConstInt(i);
193 : : // Use notNode to ensure deterministic node ID assignments
194 : 2859 : Node notNode = node.notNode();
195 : 14295 : d_proof->addStep(
196 : 5718 : node[i].notNode(), ProofRule::NOT_OR_ELIM, {notNode}, {iNode});
197 [ + - ]: 5718 : Trace("cnf") << "ProofCnfStream::convertAndAssertOr: NOT_OR_ELIM " << i
198 : 2859 : << " added norm " << node[i].notNode() << "\n";
199 : 2859 : convertAndAssert(node[i], true);
200 : 2859 : }
201 : : }
202 [ + - ]: 249666 : Trace("cnf") << pop;
203 : 249666 : }
204 : :
205 : 42 : void ProofCnfStream::convertAndAssertXor(TNode node, bool negated)
206 : : {
207 [ + - ]: 84 : Trace("cnf") << "ProofCnfStream::convertAndAssertXor(" << node
208 [ - - ]: 42 : << ", negated = " << (negated ? "true" : "false") << ")\n"
209 : 42 : << push;
210 [ + + ]: 42 : if (!negated)
211 : : {
212 : : // p XOR q
213 : 33 : SatLiteral p = toCNF(node[0], false);
214 : 33 : SatLiteral q = toCNF(node[1], false);
215 : 33 : NodeManager* nm = nodeManager();
216 : : // Construct the clause (~p v ~q)
217 : 33 : SatClause clause1(2);
218 : 33 : clause1[0] = ~p;
219 : 33 : clause1[1] = ~q;
220 : : Node clauseNode0 =
221 : 132 : nm->mkNode(Kind::OR, {node[0].notNode(), node[1].notNode()});
222 : 66 : d_proof->addStep(clauseNode0, ProofRule::XOR_ELIM2, {node}, {});
223 [ + - ]: 66 : Trace("cnf") << "ProofCnfStream::convertAndAssertXor: XOR_ELIM2 added "
224 : 33 : << clauseNode0 << "\n";
225 : 33 : d_ppm->normalizeAndRegister(clauseNode0, d_input);
226 : 33 : d_cnfStream.assertClause(node, clause1);
227 : : // Construct the clause (p v q)
228 : 33 : SatClause clause2(2);
229 : 33 : clause2[0] = p;
230 : 33 : clause2[1] = q;
231 : 66 : Node clauseNode1 = nm->mkNode(Kind::OR, node[0], node[1]);
232 : 66 : d_proof->addStep(clauseNode1, ProofRule::XOR_ELIM1, {node}, {});
233 [ + - ]: 66 : Trace("cnf") << "ProofCnfStream::convertAndAssertXor: XOR_ELIM1 added "
234 : 33 : << clauseNode1 << "\n";
235 : 33 : d_ppm->normalizeAndRegister(clauseNode1, d_input);
236 : 33 : d_cnfStream.assertClause(node, clause2);
237 : 33 : }
238 : : else
239 : : {
240 : : // ~(p XOR q) is the same as p <=> q
241 : 9 : SatLiteral p = toCNF(node[0], false);
242 : 9 : SatLiteral q = toCNF(node[1], false);
243 : 9 : NodeManager* nm = nodeManager();
244 : : // Construct the clause ~p v q
245 : 9 : SatClause clause1(2);
246 : 9 : clause1[0] = ~p;
247 : 9 : clause1[1] = q;
248 : 18 : Node clauseNode0 = nm->mkNode(Kind::OR, node[0].notNode(), node[1]);
249 : 18 : d_proof->addStep(
250 : : clauseNode0, ProofRule::NOT_XOR_ELIM2, {node.notNode()}, {});
251 [ + - ]: 18 : Trace("cnf") << "ProofCnfStream::convertAndAssertXor: NOT_XOR_ELIM2 added "
252 : 9 : << clauseNode0 << "\n";
253 : 9 : d_ppm->normalizeAndRegister(clauseNode0, d_input);
254 : 9 : d_cnfStream.assertClause(node.negate(), clause1);
255 : : // Construct the clause ~q v p
256 : 9 : SatClause clause2(2);
257 : 9 : clause2[0] = p;
258 : 9 : clause2[1] = ~q;
259 : 18 : Node clauseNode1 = nm->mkNode(Kind::OR, node[0], node[1].notNode());
260 : 18 : d_proof->addStep(
261 : : clauseNode1, ProofRule::NOT_XOR_ELIM1, {node.notNode()}, {});
262 [ + - ]: 18 : Trace("cnf") << "ProofCnfStream::convertAndAssertXor: NOT_XOR_ELIM1 added "
263 : 9 : << clauseNode1 << "\n";
264 : 9 : d_ppm->normalizeAndRegister(clauseNode1, d_input);
265 : 9 : d_cnfStream.assertClause(node.negate(), clause2);
266 : 9 : }
267 [ + - ]: 42 : Trace("cnf") << pop;
268 : 42 : }
269 : :
270 : 33118 : void ProofCnfStream::convertAndAssertIff(TNode node, bool negated)
271 : : {
272 [ + - ]: 66236 : Trace("cnf") << "ProofCnfStream::convertAndAssertIff(" << node
273 [ - - ]: 33118 : << ", negated = " << (negated ? "true" : "false") << ")\n"
274 : 33118 : << push;
275 [ + + ]: 33118 : if (!negated)
276 : : {
277 : : // p <=> q
278 [ + - ]: 32874 : Trace("cnf") << push;
279 : 32874 : SatLiteral p = toCNF(node[0], false);
280 : 32874 : SatLiteral q = toCNF(node[1], false);
281 [ + - ]: 32874 : Trace("cnf") << pop;
282 : 32874 : NodeManager* nm = nodeManager();
283 : : // Construct the clauses ~p v q
284 : 32874 : SatClause clause1(2);
285 : 32874 : clause1[0] = ~p;
286 : 32874 : clause1[1] = q;
287 : 65748 : Node clauseNode0 = nm->mkNode(Kind::OR, node[0].notNode(), node[1]);
288 : 65748 : d_proof->addStep(clauseNode0, ProofRule::EQUIV_ELIM1, {node}, {});
289 [ + - ]: 65748 : Trace("cnf") << "ProofCnfStream::convertAndAssertIff: EQUIV_ELIM1 added "
290 : 32874 : << clauseNode0 << "\n";
291 : 32874 : d_ppm->normalizeAndRegister(clauseNode0, d_input);
292 : 32874 : d_cnfStream.assertClause(node, clause1);
293 : : // Construct the clauses ~q v p
294 : 32874 : SatClause clause2(2);
295 : 32874 : clause2[0] = p;
296 : 32874 : clause2[1] = ~q;
297 : 65748 : Node clauseNode1 = nm->mkNode(Kind::OR, node[0], node[1].notNode());
298 : 65748 : d_proof->addStep(clauseNode1, ProofRule::EQUIV_ELIM2, {node}, {});
299 [ + - ]: 65748 : Trace("cnf") << "ProofCnfStream::convertAndAssertIff: EQUIV_ELIM2 added "
300 : 32874 : << clauseNode1 << "\n";
301 : 32874 : d_ppm->normalizeAndRegister(clauseNode1, d_input);
302 : 32874 : d_cnfStream.assertClause(node, clause2);
303 : 32874 : }
304 : : else
305 : : {
306 : : // ~(p <=> q) is the same as p XOR q
307 [ + - ]: 244 : Trace("cnf") << push;
308 : 244 : SatLiteral p = toCNF(node[0], false);
309 : 244 : SatLiteral q = toCNF(node[1], false);
310 [ + - ]: 244 : Trace("cnf") << pop;
311 : 244 : NodeManager* nm = nodeManager();
312 : : // Construct the clauses ~p v ~q
313 : 244 : SatClause clause1(2);
314 : 244 : clause1[0] = ~p;
315 : 244 : clause1[1] = ~q;
316 : : Node clauseNode0 =
317 : 976 : nm->mkNode(Kind::OR, {node[0].notNode(), node[1].notNode()});
318 : 488 : d_proof->addStep(
319 : : clauseNode0, ProofRule::NOT_EQUIV_ELIM2, {node.notNode()}, {});
320 [ + - ]: 488 : Trace("cnf")
321 : 0 : << "ProofCnfStream::convertAndAssertIff: NOT_EQUIV_ELIM2 added "
322 : 244 : << clauseNode0 << "\n";
323 : 244 : d_ppm->normalizeAndRegister(clauseNode0, d_input);
324 : 244 : d_cnfStream.assertClause(node.negate(), clause1);
325 : : // Construct the clauses q v p
326 : 244 : SatClause clause2(2);
327 : 244 : clause2[0] = p;
328 : 244 : clause2[1] = q;
329 : 488 : Node clauseNode1 = nm->mkNode(Kind::OR, node[0], node[1]);
330 : 488 : d_proof->addStep(
331 : : clauseNode1, ProofRule::NOT_EQUIV_ELIM1, {node.notNode()}, {});
332 [ + - ]: 488 : Trace("cnf")
333 : 0 : << "ProofCnfStream::convertAndAssertIff: NOT_EQUIV_ELIM1 added "
334 : 244 : << clauseNode1 << "\n";
335 : 244 : d_ppm->normalizeAndRegister(clauseNode1, d_input);
336 : 244 : d_cnfStream.assertClause(node.negate(), clause2);
337 : 244 : }
338 [ + - ]: 33118 : Trace("cnf") << pop;
339 : 33118 : }
340 : :
341 : 151209 : void ProofCnfStream::convertAndAssertImplies(TNode node, bool negated)
342 : : {
343 [ + - ]: 302418 : Trace("cnf") << "ProofCnfStream::convertAndAssertImplies(" << node
344 [ - - ]: 151209 : << ", negated = " << (negated ? "true" : "false") << ")\n"
345 : 151209 : << push;
346 [ + + ]: 151209 : if (!negated)
347 : : {
348 : : // ~p v q
349 : 150759 : SatLiteral p = toCNF(node[0], false);
350 : 150759 : SatLiteral q = toCNF(node[1], false);
351 : : // Construct the clause ~p || q
352 : 150759 : SatClause clause(2);
353 : 150759 : clause[0] = ~p;
354 : 150759 : clause[1] = q;
355 : : Node clauseNode =
356 : 301518 : nodeManager()->mkNode(Kind::OR, node[0].notNode(), node[1]);
357 : 301518 : d_proof->addStep(clauseNode, ProofRule::IMPLIES_ELIM, {node}, {});
358 [ + - ]: 301518 : Trace("cnf")
359 : 0 : << "ProofCnfStream::convertAndAssertImplies: IMPLIES_ELIM added "
360 : 150759 : << clauseNode << "\n";
361 : 150759 : d_ppm->normalizeAndRegister(clauseNode, d_input);
362 : 150759 : d_cnfStream.assertClause(node, clause);
363 : 150759 : }
364 : : else
365 : : {
366 : : // ~(p => q) is the same as p ^ ~q
367 : : // process p
368 : 450 : convertAndAssert(node[0], false);
369 : 900 : d_proof->addStep(
370 : : node[0], ProofRule::NOT_IMPLIES_ELIM1, {node.notNode()}, {});
371 [ + - ]: 900 : Trace("cnf")
372 : 0 : << "ProofCnfStream::convertAndAssertImplies: NOT_IMPLIES_ELIM1 added "
373 [ - + ][ - - ]: 450 : << node[0] << "\n";
374 : : // process ~q
375 : 450 : convertAndAssert(node[1], true);
376 : : // Use notNode to ensure deterministic node ID assignments
377 : 450 : Node notNode = node.notNode();
378 : 1800 : d_proof->addStep(
379 : 900 : node[1].notNode(), ProofRule::NOT_IMPLIES_ELIM2, {notNode}, {});
380 [ + - ]: 900 : Trace("cnf")
381 : 0 : << "ProofCnfStream::convertAndAssertImplies: NOT_IMPLIES_ELIM2 added "
382 : 450 : << node[1].notNode() << "\n";
383 : 450 : }
384 [ + - ]: 151209 : Trace("cnf") << pop;
385 : 151209 : }
386 : :
387 : 28245 : void ProofCnfStream::convertAndAssertIte(TNode node, bool negated)
388 : : {
389 [ + - ]: 56490 : Trace("cnf") << "ProofCnfStream::convertAndAssertIte(" << node
390 [ - - ]: 28245 : << ", negated = " << (negated ? "true" : "false") << ")\n"
391 : 28245 : << push;
392 : : // ITE(p, q, r)
393 : 28245 : SatLiteral p = toCNF(node[0], false);
394 : 28245 : SatLiteral q = toCNF(node[1], negated);
395 : 28245 : SatLiteral r = toCNF(node[2], negated);
396 : 28245 : NodeManager* nm = nodeManager();
397 : : // Construct the clauses:
398 : : // (~p v q) and (p v r)
399 : : //
400 : : // Note that below q and r can be used directly because whether they are
401 : : // negated has been push to the literal definitions above
402 [ + + ]: 28245 : Node nnode = negated ? node.negate() : static_cast<Node>(node);
403 : : // (~p v q)
404 : 28245 : SatClause clause1(2);
405 : 28245 : clause1[0] = ~p;
406 : 28245 : clause1[1] = q;
407 : : // redo the negation here to avoid silent double negation elimination
408 [ + + ]: 28245 : if (!negated)
409 : : {
410 : 56408 : Node clauseNode = nm->mkNode(Kind::OR, node[0].notNode(), node[1]);
411 : 56408 : d_proof->addStep(clauseNode, ProofRule::ITE_ELIM1, {node}, {});
412 [ + - ]: 56408 : Trace("cnf") << "ProofCnfStream::convertAndAssertIte: ITE_ELIM1 added "
413 : 28204 : << clauseNode << "\n";
414 : 28204 : d_ppm->normalizeAndRegister(clauseNode, d_input);
415 : 28204 : }
416 : : else
417 : : {
418 : : Node clauseNode =
419 : 164 : nm->mkNode(Kind::OR, {node[0].notNode(), node[1].notNode()});
420 : 82 : d_proof->addStep(
421 : : clauseNode, ProofRule::NOT_ITE_ELIM1, {node.notNode()}, {});
422 [ + - ]: 82 : Trace("cnf") << "ProofCnfStream::convertAndAssertIte: NOT_ITE_ELIM1 added "
423 : 41 : << clauseNode << "\n";
424 : 41 : d_ppm->normalizeAndRegister(clauseNode, d_input);
425 : 41 : }
426 : 28245 : d_cnfStream.assertClause(nnode, clause1);
427 : : // (p v r)
428 : 28245 : SatClause clause2(2);
429 : 28245 : clause2[0] = p;
430 : 28245 : clause2[1] = r;
431 : : // redo the negation here to avoid silent double negation elimination
432 [ + + ]: 28245 : if (!negated)
433 : : {
434 : 56408 : Node clauseNode = nm->mkNode(Kind::OR, node[0], node[2]);
435 : 56408 : d_proof->addStep(clauseNode, ProofRule::ITE_ELIM2, {node}, {});
436 [ + - ]: 56408 : Trace("cnf") << "ProofCnfStream::convertAndAssertIte: ITE_ELIM2 added "
437 : 28204 : << clauseNode << "\n";
438 : 28204 : d_ppm->normalizeAndRegister(clauseNode, d_input);
439 : 28204 : }
440 : : else
441 : : {
442 : 82 : Node clauseNode = nm->mkNode(Kind::OR, node[0], node[2].notNode());
443 : 82 : d_proof->addStep(
444 : : clauseNode, ProofRule::NOT_ITE_ELIM2, {node.notNode()}, {});
445 [ + - ]: 82 : Trace("cnf") << "ProofCnfStream::convertAndAssertIte: NOT_ITE_ELIM2 added "
446 : 41 : << clauseNode << "\n";
447 : 41 : d_ppm->normalizeAndRegister(clauseNode, d_input);
448 : 41 : }
449 : 28245 : d_cnfStream.assertClause(nnode, clause2);
450 [ + - ]: 28245 : Trace("cnf") << pop;
451 : 28245 : }
452 : :
453 : 348476 : void ProofCnfStream::ensureLiteral(TNode n)
454 : : {
455 [ + - ]: 348476 : Trace("cnf") << "ProofCnfStream::ensureLiteral(" << n << ")\n";
456 [ + + ]: 348476 : if (d_cnfStream.hasLiteral(n))
457 : : {
458 : 257292 : d_cnfStream.ensureMappingForLiteral(n);
459 : 257292 : return;
460 : : }
461 : : // remove top level negation. We don't need to track this because it's a
462 : : // literal.
463 [ + + ]: 91184 : n = n.getKind() == Kind::NOT ? n[0] : n;
464 [ + + ][ + + ]: 91184 : if (d_env.theoryOf(n) == theory::THEORY_BOOL && !n.isVar())
[ + - ][ + + ]
[ - - ]
465 : : {
466 : : // These are not removable
467 : 54325 : d_cnfStream.d_removable = false;
468 : 54325 : SatLiteral lit = toCNF(n, false);
469 : : // Store backward-mappings
470 : : // These may already exist
471 : 54325 : d_cnfStream.d_literalToNodeMap.insert_safe(lit, n);
472 : 54325 : d_cnfStream.d_literalToNodeMap.insert_safe(~lit, n.notNode());
473 : : }
474 : : else
475 : : {
476 : 36859 : d_cnfStream.convertAtom(n);
477 : : }
478 : : }
479 : :
480 : 0 : bool ProofCnfStream::hasLiteral(TNode n) const
481 : : {
482 : 0 : return d_cnfStream.hasLiteral(n);
483 : : }
484 : :
485 : 0 : SatLiteral ProofCnfStream::getLiteral(TNode node)
486 : : {
487 : 0 : return d_cnfStream.getLiteral(node);
488 : : }
489 : :
490 : 0 : void ProofCnfStream::getBooleanVariables(
491 : : std::vector<TNode>& outputVariables) const
492 : : {
493 : 0 : d_cnfStream.getBooleanVariables(outputVariables);
494 : 0 : }
495 : :
496 : 4881275 : SatLiteral ProofCnfStream::toCNF(TNode node, bool negated)
497 : : {
498 [ + - ]: 9762550 : Trace("cnf") << "toCNF(" << node
499 [ - - ]: 4881275 : << ", negated = " << (negated ? "true" : "false") << ")\n";
500 : 4881275 : SatLiteral lit;
501 : : // If the node has already has a literal, return it (maybe negated)
502 [ + + ]: 4881275 : if (d_cnfStream.hasLiteral(node))
503 : : {
504 [ + - ]: 3275099 : Trace("cnf") << "toCNF(): already translated\n";
505 : 3275099 : lit = d_cnfStream.getLiteral(node);
506 : : // Return the (maybe negated) literal
507 [ + + ]: 3275099 : return !negated ? lit : ~lit;
508 : : }
509 : :
510 : : // Handle each Boolean operator case
511 [ + + ][ + + ]: 1606176 : switch (node.getKind())
[ + + ][ + + ]
512 : : {
513 : 269896 : case Kind::AND: lit = handleAnd(node); break;
514 : 183658 : case Kind::OR: lit = handleOr(node); break;
515 : 41267 : case Kind::XOR: lit = handleXor(node); break;
516 : 5050 : case Kind::IMPLIES: lit = handleImplies(node); break;
517 : 42587 : case Kind::ITE: lit = handleIte(node); break;
518 : 155940 : case Kind::NOT: lit = ~toCNF(node[0]); break;
519 : 465742 : case Kind::EQUAL:
520 [ + + ][ - - ]: 931484 : lit = node[0].getType().isBoolean() ? handleIff(node)
521 [ + + ][ + + ]: 465742 : : d_cnfStream.convertAtom(node);
[ - - ]
522 : 465742 : break;
523 : 442036 : default:
524 : : {
525 : 442036 : lit = d_cnfStream.convertAtom(node);
526 : : }
527 : 442036 : break;
528 : : }
529 : : // Return the (maybe negated) literal
530 [ + + ]: 1606176 : return !negated ? lit : ~lit;
531 : : }
532 : :
533 : 269896 : SatLiteral ProofCnfStream::handleAnd(TNode node)
534 : : {
535 [ - + ][ - + ]: 269896 : Assert(!d_cnfStream.hasLiteral(node)) << "Atom already mapped!";
[ - - ]
536 [ - + ][ - + ]: 269896 : Assert(node.getKind() == Kind::AND) << "Expecting an AND expression!";
[ - - ]
537 [ - + ][ - + ]: 269896 : Assert(node.getNumChildren() > 1) << "Expecting more than 1 child!";
[ - - ]
538 [ - + ][ - + ]: 269896 : Assert(!d_cnfStream.d_removable)
[ - - ]
539 : 0 : << "Removable clauses cannot contain Boolean structure";
540 [ + - ]: 269896 : Trace("cnf") << "ProofCnfStream::handleAnd(" << node << ")\n";
541 : : // Number of children
542 : 269896 : unsigned size = node.getNumChildren();
543 : : // Transform all the children first (remembering the negation)
544 : 269896 : SatClause clause(size + 1);
545 [ + + ]: 1326216 : for (unsigned i = 0; i < size; ++i)
546 : : {
547 [ + - ]: 1056320 : Trace("cnf") << push;
548 : 1056320 : clause[i] = ~toCNF(node[i]);
549 [ + - ]: 1056320 : Trace("cnf") << pop;
550 : : }
551 : : // Create literal for the node
552 : 269896 : SatLiteral lit = d_cnfStream.newLiteral(node);
553 : 269896 : NodeManager* nm = nodeManager();
554 : : // lit -> (a_1 & a_2 & a_3 & ... & a_n)
555 : : // ~lit | (a_1 & a_2 & a_3 & ... & a_n)
556 : : // (~lit | a_1) & (~lit | a_2) & ... & (~lit | a_n)
557 [ + + ]: 1326216 : for (unsigned i = 0; i < size; ++i)
558 : : {
559 [ + - ]: 1056320 : Trace("cnf") << push;
560 : 2112640 : Node clauseNode = nm->mkNode(Kind::OR, node.notNode(), node[i]);
561 : 1056320 : Node iNode = nm->mkConstInt(i);
562 [ + + ][ - - ]: 3168960 : d_proof->addStep(clauseNode, ProofRule::CNF_AND_POS, {}, {node, iNode});
563 [ + - ]: 2112640 : Trace("cnf") << "ProofCnfStream::handleAnd: CNF_AND_POS " << i << " added "
564 : 1056320 : << clauseNode << "\n";
565 : 1056320 : d_ppm->normalizeAndRegister(clauseNode, d_input);
566 : 1056320 : d_cnfStream.assertClause(node.negate(), ~lit, ~clause[i]);
567 [ + - ]: 1056320 : Trace("cnf") << pop;
568 : 1056320 : }
569 : : // lit <- (a_1 & a_2 & a_3 & ... a_n)
570 : : // lit | ~(a_1 & a_2 & a_3 & ... & a_n)
571 : : // lit | ~a_1 | ~a_2 | ~a_3 | ... | ~a_n
572 : 269896 : clause[size] = lit;
573 : : // This needs to go last, as the clause might get modified by the SAT solver
574 [ + - ]: 269896 : Trace("cnf") << push;
575 : 809688 : std::vector<Node> disjuncts{node};
576 [ + + ]: 1326216 : for (unsigned i = 0; i < size; ++i)
577 : : {
578 : 1056320 : disjuncts.push_back(node[i].notNode());
579 : : }
580 : 269896 : Node clauseNode = nm->mkNode(Kind::OR, disjuncts);
581 : 539792 : d_proof->addStep(clauseNode, ProofRule::CNF_AND_NEG, {}, {node});
582 [ + - ]: 539792 : Trace("cnf") << "ProofCnfStream::handleAnd: CNF_AND_NEG added " << clauseNode
583 : 269896 : << "\n";
584 : 269896 : d_ppm->normalizeAndRegister(clauseNode, d_input);
585 : 269896 : d_cnfStream.assertClause(node, clause);
586 [ + - ]: 269896 : Trace("cnf") << pop;
587 : 269896 : return lit;
588 : 269896 : }
589 : :
590 : 183658 : SatLiteral ProofCnfStream::handleOr(TNode node)
591 : : {
592 [ - + ][ - + ]: 183658 : Assert(!d_cnfStream.hasLiteral(node)) << "Atom already mapped!";
[ - - ]
593 [ - + ][ - + ]: 183658 : Assert(node.getKind() == Kind::OR) << "Expecting an OR expression!";
[ - - ]
594 [ - + ][ - + ]: 183658 : Assert(node.getNumChildren() > 1) << "Expecting more then 1 child!";
[ - - ]
595 [ - + ][ - + ]: 183658 : Assert(!d_cnfStream.d_removable)
[ - - ]
596 : 0 : << "Removable clauses can not contain Boolean structure";
597 [ + - ]: 183658 : Trace("cnf") << "ProofCnfStream::handleOr(" << node << ")\n";
598 : : // Number of children
599 : 183658 : unsigned size = node.getNumChildren();
600 : : // Transform all the children first
601 : 183658 : SatClause clause(size + 1);
602 [ + + ]: 766638 : for (unsigned i = 0; i < size; ++i)
603 : : {
604 : 582980 : clause[i] = toCNF(node[i]);
605 : : }
606 : : // Create literal for the node
607 : 183658 : SatLiteral lit = d_cnfStream.newLiteral(node);
608 : 183658 : NodeManager* nm = nodeManager();
609 : : // lit <- (a_1 | a_2 | a_3 | ... | a_n)
610 : : // lit | ~(a_1 | a_2 | a_3 | ... | a_n)
611 : : // (lit | ~a_1) & (lit | ~a_2) & (lit & ~a_3) & ... & (lit & ~a_n)
612 [ + + ]: 766638 : for (unsigned i = 0; i < size; ++i)
613 : : {
614 : 1165960 : Node clauseNode = nm->mkNode(Kind::OR, node, node[i].notNode());
615 : 582980 : Node iNode = nm->mkConstInt(i);
616 [ + + ][ - - ]: 1748940 : d_proof->addStep(clauseNode, ProofRule::CNF_OR_NEG, {}, {node, iNode});
617 [ + - ]: 1165960 : Trace("cnf") << "ProofCnfStream::handleOr: CNF_OR_NEG " << i << " added "
618 : 582980 : << clauseNode << "\n";
619 : 582980 : d_ppm->normalizeAndRegister(clauseNode, d_input);
620 : 582980 : d_cnfStream.assertClause(node, lit, ~clause[i]);
621 : 582980 : }
622 : : // lit -> (a_1 | a_2 | a_3 | ... | a_n)
623 : : // ~lit | a_1 | a_2 | a_3 | ... | a_n
624 : 183658 : clause[size] = ~lit;
625 : : // This needs to go last, as the clause might get modified by the SAT solver
626 : 550974 : std::vector<Node> disjuncts{node.notNode()};
627 [ + + ]: 766638 : for (unsigned i = 0; i < size; ++i)
628 : : {
629 : 582980 : disjuncts.push_back(node[i]);
630 : : }
631 : 183658 : Node clauseNode = nm->mkNode(Kind::OR, disjuncts);
632 : 367316 : d_proof->addStep(clauseNode, ProofRule::CNF_OR_POS, {}, {node});
633 [ + - ]: 367316 : Trace("cnf") << "ProofCnfStream::handleOr: CNF_OR_POS added " << clauseNode
634 : 183658 : << "\n";
635 : 183658 : d_ppm->normalizeAndRegister(clauseNode, d_input);
636 : 183658 : d_cnfStream.assertClause(node.negate(), clause);
637 : 183658 : return lit;
638 : 183658 : }
639 : :
640 : 41267 : SatLiteral ProofCnfStream::handleXor(TNode node)
641 : : {
642 [ - + ][ - + ]: 41267 : Assert(!d_cnfStream.hasLiteral(node)) << "Atom already mapped!";
[ - - ]
643 [ - + ][ - + ]: 41267 : Assert(node.getKind() == Kind::XOR) << "Expecting an XOR expression!";
[ - - ]
644 [ - + ][ - + ]: 41267 : Assert(node.getNumChildren() == 2) << "Expecting exactly 2 children!";
[ - - ]
645 [ - + ][ - + ]: 41267 : Assert(!d_cnfStream.d_removable)
[ - - ]
646 : 0 : << "Removable clauses can not contain Boolean structure";
647 [ + - ]: 41267 : Trace("cnf") << "ProofCnfStream::handleXor(" << node << ")\n";
648 : 41267 : SatLiteral a = toCNF(node[0]);
649 : 41267 : SatLiteral b = toCNF(node[1]);
650 : 41267 : SatLiteral lit = d_cnfStream.newLiteral(node);
651 : : Node clauseNode0 =
652 : 82534 : nodeManager()->mkNode(Kind::OR, node.notNode(), node[0], node[1]);
653 : 82534 : d_proof->addStep(clauseNode0, ProofRule::CNF_XOR_POS1, {}, {node});
654 [ + - ]: 82534 : Trace("cnf") << "ProofCnfStream::handleXor: CNF_XOR_POS1 added "
655 : 41267 : << clauseNode0 << "\n";
656 : 41267 : d_ppm->normalizeAndRegister(clauseNode0, d_input);
657 : 41267 : d_cnfStream.assertClause(node.negate(), a, b, ~lit);
658 : 206335 : Node clauseNode1 = nodeManager()->mkNode(
659 : 82534 : Kind::OR, {node.notNode(), node[0].notNode(), node[1].notNode()});
660 : 82534 : d_proof->addStep(clauseNode1, ProofRule::CNF_XOR_POS2, {}, {node});
661 [ + - ]: 82534 : Trace("cnf") << "ProofCnfStream::handleXor: CNF_XOR_POS2 added "
662 : 41267 : << clauseNode1 << "\n";
663 : 41267 : d_ppm->normalizeAndRegister(clauseNode1, d_input);
664 : 41267 : d_cnfStream.assertClause(node.negate(), ~a, ~b, ~lit);
665 : : Node clauseNode2 =
666 : 82534 : nodeManager()->mkNode(Kind::OR, node, node[0], node[1].notNode());
667 : 82534 : d_proof->addStep(clauseNode2, ProofRule::CNF_XOR_NEG2, {}, {node});
668 [ + - ]: 82534 : Trace("cnf") << "ProofCnfStream::handleXor: CNF_XOR_NEG2 added "
669 : 41267 : << clauseNode2 << "\n";
670 : 41267 : d_ppm->normalizeAndRegister(clauseNode2, d_input);
671 : 41267 : d_cnfStream.assertClause(node, a, ~b, lit);
672 : : Node clauseNode3 =
673 : 82534 : nodeManager()->mkNode(Kind::OR, node, node[0].notNode(), node[1]);
674 : 82534 : d_proof->addStep(clauseNode3, ProofRule::CNF_XOR_NEG1, {}, {node});
675 [ + - ]: 82534 : Trace("cnf") << "ProofCnfStream::handleXor: CNF_XOR_NEG1 added "
676 : 41267 : << clauseNode3 << "\n";
677 : 41267 : d_ppm->normalizeAndRegister(clauseNode3, d_input);
678 : 41267 : d_cnfStream.assertClause(node, ~a, b, lit);
679 : 41267 : return lit;
680 : 41267 : }
681 : :
682 : 129812 : SatLiteral ProofCnfStream::handleIff(TNode node)
683 : : {
684 [ - + ][ - + ]: 129812 : Assert(!d_cnfStream.hasLiteral(node)) << "Atom already mapped!";
[ - - ]
685 [ - + ][ - + ]: 129812 : Assert(node.getKind() == Kind::EQUAL) << "Expecting an EQUAL expression!";
[ - - ]
686 [ - + ][ - + ]: 129812 : Assert(node.getNumChildren() == 2) << "Expecting exactly 2 children!";
[ - - ]
687 [ + - ]: 129812 : Trace("cnf") << "handleIff(" << node << ")\n";
688 : : // Convert the children to CNF
689 : 129812 : SatLiteral a = toCNF(node[0]);
690 : 129812 : SatLiteral b = toCNF(node[1]);
691 : : // Create literal for the node
692 : 129812 : SatLiteral lit = d_cnfStream.newLiteral(node);
693 : 129812 : NodeManager* nm = nodeManager();
694 : : // lit -> ((a-> b) & (b->a))
695 : : // ~lit | ((~a | b) & (~b | a))
696 : : // (~a | b | ~lit) & (~b | a | ~lit)
697 : : Node clauseNode0 =
698 : 649060 : nm->mkNode(Kind::OR, {node.notNode(), node[0].notNode(), node[1]});
699 : 259624 : d_proof->addStep(clauseNode0, ProofRule::CNF_EQUIV_POS1, {}, {node});
700 [ + - ]: 259624 : Trace("cnf") << "ProofCnfStream::handleIff: CNF_EQUIV_POS1 added "
701 : 129812 : << clauseNode0 << "\n";
702 : 129812 : d_ppm->normalizeAndRegister(clauseNode0, d_input);
703 : 129812 : d_cnfStream.assertClause(node.negate(), ~a, b, ~lit);
704 : : Node clauseNode1 =
705 : 649060 : nm->mkNode(Kind::OR, {node.notNode(), node[0], node[1].notNode()});
706 : 259624 : d_proof->addStep(clauseNode1, ProofRule::CNF_EQUIV_POS2, {}, {node});
707 [ + - ]: 259624 : Trace("cnf") << "ProofCnfStream::handleIff: CNF_EQUIV_POS2 added "
708 : 129812 : << clauseNode1 << "\n";
709 : 129812 : d_ppm->normalizeAndRegister(clauseNode1, d_input);
710 : 129812 : d_cnfStream.assertClause(node.negate(), a, ~b, ~lit);
711 : : // (a<->b) -> lit
712 : : // ~((a & b) | (~a & ~b)) | lit
713 : : // (~(a & b)) & (~(~a & ~b)) | lit
714 : : // ((~a | ~b) & (a | b)) | lit
715 : : // (~a | ~b | lit) & (a | b | lit)
716 : : Node clauseNode2 =
717 : 649060 : nm->mkNode(Kind::OR, {node, node[0].notNode(), node[1].notNode()});
718 : 259624 : d_proof->addStep(clauseNode2, ProofRule::CNF_EQUIV_NEG2, {}, {node});
719 [ + - ]: 259624 : Trace("cnf") << "ProofCnfStream::handleIff: CNF_EQUIV_NEG2 added "
720 : 129812 : << clauseNode2 << "\n";
721 : 129812 : d_ppm->normalizeAndRegister(clauseNode2, d_input);
722 : 129812 : d_cnfStream.assertClause(node, ~a, ~b, lit);
723 : 259624 : Node clauseNode3 = nm->mkNode(Kind::OR, node, node[0], node[1]);
724 : 259624 : d_proof->addStep(clauseNode3, ProofRule::CNF_EQUIV_NEG1, {}, {node});
725 [ + - ]: 259624 : Trace("cnf") << "ProofCnfStream::handleIff: CNF_EQUIV_NEG1 added "
726 : 129812 : << clauseNode3 << "\n";
727 : 129812 : d_ppm->normalizeAndRegister(clauseNode3, d_input);
728 : 129812 : d_cnfStream.assertClause(node, a, b, lit);
729 : 129812 : return lit;
730 : 129812 : }
731 : :
732 : 5050 : SatLiteral ProofCnfStream::handleImplies(TNode node)
733 : : {
734 [ - + ][ - + ]: 5050 : Assert(!d_cnfStream.hasLiteral(node)) << "Atom already mapped!";
[ - - ]
735 [ - + ][ - + ]: 5050 : Assert(node.getKind() == Kind::IMPLIES) << "Expecting an IMPLIES expression!";
[ - - ]
736 [ - + ][ - + ]: 5050 : Assert(node.getNumChildren() == 2) << "Expecting exactly 2 children!";
[ - - ]
737 [ - + ][ - + ]: 5050 : Assert(!d_cnfStream.d_removable)
[ - - ]
738 : 0 : << "Removable clauses can not contain Boolean structure";
739 [ + - ]: 5050 : Trace("cnf") << "ProofCnfStream::handleImplies(" << node << ")\n";
740 : : // Convert the children to cnf
741 : 5050 : SatLiteral a = toCNF(node[0]);
742 : 5050 : SatLiteral b = toCNF(node[1]);
743 : 5050 : SatLiteral lit = d_cnfStream.newLiteral(node);
744 : 5050 : NodeManager* nm = nodeManager();
745 : : // lit -> (a->b)
746 : : // ~lit | ~ a | b
747 : : Node clauseNode0 =
748 : 25250 : nm->mkNode(Kind::OR, {node.notNode(), node[0].notNode(), node[1]});
749 : 10100 : d_proof->addStep(clauseNode0, ProofRule::CNF_IMPLIES_POS, {}, {node});
750 [ + - ]: 10100 : Trace("cnf") << "ProofCnfStream::handleImplies: CNF_IMPLIES_POS added "
751 : 5050 : << clauseNode0 << "\n";
752 : 5050 : d_ppm->normalizeAndRegister(clauseNode0, d_input);
753 : 5050 : d_cnfStream.assertClause(node.negate(), ~lit, ~a, b);
754 : : // (a->b) -> lit
755 : : // ~(~a | b) | lit
756 : : // (a | l) & (~b | l)
757 : 10100 : Node clauseNode1 = nm->mkNode(Kind::OR, node, node[0]);
758 : 10100 : d_proof->addStep(clauseNode1, ProofRule::CNF_IMPLIES_NEG1, {}, {node});
759 [ + - ]: 10100 : Trace("cnf") << "ProofCnfStream::handleImplies: CNF_IMPLIES_NEG1 added "
760 : 5050 : << clauseNode1 << "\n";
761 : 5050 : d_ppm->normalizeAndRegister(clauseNode1, d_input);
762 : 5050 : d_cnfStream.assertClause(node, a, lit);
763 : 10100 : Node clauseNode2 = nm->mkNode(Kind::OR, node, node[1].notNode());
764 : 10100 : d_proof->addStep(clauseNode2, ProofRule::CNF_IMPLIES_NEG2, {}, {node});
765 [ + - ]: 10100 : Trace("cnf") << "ProofCnfStream::handleImplies: CNF_IMPLIES_NEG2 added "
766 : 5050 : << clauseNode2 << "\n";
767 : 5050 : d_ppm->normalizeAndRegister(clauseNode2, d_input);
768 : 5050 : d_cnfStream.assertClause(node, ~b, lit);
769 : 5050 : return lit;
770 : 5050 : }
771 : :
772 : 42587 : SatLiteral ProofCnfStream::handleIte(TNode node)
773 : : {
774 [ - + ][ - + ]: 42587 : Assert(!d_cnfStream.hasLiteral(node)) << "Atom already mapped!";
[ - - ]
775 [ - + ][ - + ]: 42587 : Assert(node.getKind() == Kind::ITE);
[ - - ]
776 [ - + ][ - + ]: 42587 : Assert(node.getNumChildren() == 3);
[ - - ]
777 [ - + ][ - + ]: 42587 : Assert(!d_cnfStream.d_removable)
[ - - ]
778 : 0 : << "Removable clauses can not contain Boolean structure";
779 : 85174 : Trace("cnf") << "handleIte(" << node[0] << " " << node[1] << " " << node[2]
780 : 42587 : << ")\n";
781 : 42587 : SatLiteral condLit = toCNF(node[0]);
782 : 42587 : SatLiteral thenLit = toCNF(node[1]);
783 : 42587 : SatLiteral elseLit = toCNF(node[2]);
784 : : // create literal to the node
785 : 42587 : SatLiteral lit = d_cnfStream.newLiteral(node);
786 : 42587 : NodeManager* nm = nodeManager();
787 : : // If ITE is true then one of the branches is true and the condition
788 : : // implies which one
789 : : // lit -> (ite b t e)
790 : : // lit -> (t | e) & (b -> t) & (!b -> e)
791 : : // lit -> (t | e) & (!b | t) & (b | e)
792 : : // (!lit | t | e) & (!lit | !b | t) & (!lit | b | e)
793 : 85174 : Node clauseNode0 = nm->mkNode(Kind::OR, node.notNode(), node[1], node[2]);
794 : 85174 : d_proof->addStep(clauseNode0, ProofRule::CNF_ITE_POS3, {}, {node});
795 [ + - ]: 85174 : Trace("cnf") << "ProofCnfStream::handleIte: CNF_ITE_POS3 added "
796 : 42587 : << clauseNode0 << "\n";
797 : 42587 : d_ppm->normalizeAndRegister(clauseNode0, d_input);
798 : 42587 : d_cnfStream.assertClause(node.negate(), ~lit, thenLit, elseLit);
799 : : Node clauseNode1 =
800 : 212935 : nm->mkNode(Kind::OR, {node.notNode(), node[0].notNode(), node[1]});
801 : 85174 : d_proof->addStep(clauseNode1, ProofRule::CNF_ITE_POS1, {}, {node});
802 [ + - ]: 85174 : Trace("cnf") << "ProofCnfStream::handleIte: CNF_ITE_POS1 added "
803 : 42587 : << clauseNode1 << "\n";
804 : 42587 : d_ppm->normalizeAndRegister(clauseNode1, d_input);
805 : 42587 : d_cnfStream.assertClause(node.negate(), ~lit, ~condLit, thenLit);
806 : 85174 : Node clauseNode2 = nm->mkNode(Kind::OR, node.notNode(), node[0], node[2]);
807 : 85174 : d_proof->addStep(clauseNode2, ProofRule::CNF_ITE_POS2, {}, {node});
808 [ + - ]: 85174 : Trace("cnf") << "ProofCnfStream::handleIte: CNF_ITE_POS2 added "
809 : 42587 : << clauseNode2 << "\n";
810 : 42587 : d_ppm->normalizeAndRegister(clauseNode2, d_input);
811 : 42587 : d_cnfStream.assertClause(node.negate(), ~lit, condLit, elseLit);
812 : : // If ITE is false then one of the branches is false and the condition
813 : : // implies which one
814 : : // !lit -> !(ite b t e)
815 : : // !lit -> (!t | !e) & (b -> !t) & (!b -> !e)
816 : : // !lit -> (!t | !e) & (!b | !t) & (b | !e)
817 : : // (lit | !t | !e) & (lit | !b | !t) & (lit | b | !e)
818 : : Node clauseNode3 =
819 : 212935 : nm->mkNode(Kind::OR, {node, node[1].notNode(), node[2].notNode()});
820 : 85174 : d_proof->addStep(clauseNode3, ProofRule::CNF_ITE_NEG3, {}, {node});
821 [ + - ]: 85174 : Trace("cnf") << "ProofCnfStream::handleIte: CNF_ITE_NEG3 added "
822 : 42587 : << clauseNode3 << "\n";
823 : 42587 : d_ppm->normalizeAndRegister(clauseNode3, d_input);
824 : 42587 : d_cnfStream.assertClause(node, lit, ~thenLit, ~elseLit);
825 : : Node clauseNode4 =
826 : 212935 : nm->mkNode(Kind::OR, {node, node[0].notNode(), node[1].notNode()});
827 : 85174 : d_proof->addStep(clauseNode4, ProofRule::CNF_ITE_NEG1, {}, {node});
828 [ + - ]: 85174 : Trace("cnf") << "ProofCnfStream::handleIte: CNF_ITE_NEG1 added "
829 : 42587 : << clauseNode4 << "\n";
830 : 42587 : d_ppm->normalizeAndRegister(clauseNode4, d_input);
831 : 42587 : d_cnfStream.assertClause(node, lit, ~condLit, ~thenLit);
832 : 85174 : Node clauseNode5 = nm->mkNode(Kind::OR, node, node[0], node[2].notNode());
833 : 85174 : d_proof->addStep(clauseNode5, ProofRule::CNF_ITE_NEG2, {}, {node});
834 [ + - ]: 85174 : Trace("cnf") << "ProofCnfStream::handleIte: CNF_ITE_NEG2 added "
835 : 42587 : << clauseNode5 << "\n";
836 : 42587 : d_ppm->normalizeAndRegister(clauseNode5, d_input);
837 : 42587 : d_cnfStream.assertClause(node, lit, condLit, ~elseLit);
838 : 42587 : return lit;
839 : 42587 : }
840 : :
841 : 0 : void ProofCnfStream::dumpDimacs(std::ostream& out,
842 : : const std::vector<Node>& clauses)
843 : : {
844 : 0 : d_cnfStream.dumpDimacs(out, clauses);
845 : 0 : }
846 : :
847 : 0 : void ProofCnfStream::dumpDimacs(std::ostream& out,
848 : : const std::vector<Node>& clauses,
849 : : const std::vector<Node>& auxUnits)
850 : : {
851 : 0 : d_cnfStream.dumpDimacs(out, clauses, auxUnits);
852 : 0 : }
853 : :
854 : : } // namespace prop
855 : : } // namespace cvc5::internal
|
