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