1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Haniel Barbosa, Andrew Reynolds, Tim King |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
7 |
|
* Copyright (c) 2009-2021 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 { |
24 |
|
namespace prop { |
25 |
|
|
26 |
64 |
ProofCnfStream::ProofCnfStream(context::UserContext* u, |
27 |
|
CnfStream& cnfStream, |
28 |
|
SatProofManager* satPM, |
29 |
64 |
ProofNodeManager* pnm) |
30 |
|
: d_cnfStream(cnfStream), |
31 |
|
d_satPM(satPM), |
32 |
|
d_proof(pnm, nullptr, u, "ProofCnfStream::LazyCDProof"), |
33 |
64 |
d_blocked(u) |
34 |
|
{ |
35 |
64 |
} |
36 |
|
|
37 |
40 |
void ProofCnfStream::addBlocked(std::shared_ptr<ProofNode> pfn) |
38 |
|
{ |
39 |
40 |
d_blocked.insert(pfn); |
40 |
40 |
} |
41 |
|
|
42 |
143 |
bool ProofCnfStream::isBlocked(std::shared_ptr<ProofNode> pfn) |
43 |
|
{ |
44 |
143 |
return d_blocked.contains(pfn); |
45 |
|
} |
46 |
|
|
47 |
40 |
std::shared_ptr<ProofNode> ProofCnfStream::getProofFor(Node f) |
48 |
|
{ |
49 |
40 |
return d_proof.getProofFor(f); |
50 |
|
} |
51 |
|
|
52 |
110 |
bool ProofCnfStream::hasProofFor(Node f) |
53 |
|
{ |
54 |
110 |
return d_proof.hasStep(f) || d_proof.hasGenerator(f); |
55 |
|
} |
56 |
|
|
57 |
|
std::string ProofCnfStream::identify() const { return "ProofCnfStream"; } |
58 |
|
|
59 |
12305 |
void ProofCnfStream::normalizeAndRegister(TNode clauseNode) |
60 |
|
{ |
61 |
24610 |
Node normClauseNode = d_psb.factorReorderElimDoubleNeg(clauseNode); |
62 |
12305 |
if (Trace.isOn("cnf") && normClauseNode != clauseNode) |
63 |
|
{ |
64 |
|
Trace("cnf") << push |
65 |
|
<< "ProofCnfStream::normalizeAndRegister: steps to normalized " |
66 |
|
<< normClauseNode << "\n" |
67 |
|
<< pop; |
68 |
|
} |
69 |
12305 |
d_satPM->registerSatAssumptions({normClauseNode}); |
70 |
12305 |
} |
71 |
|
|
72 |
3937 |
void ProofCnfStream::convertAndAssert(TNode node, |
73 |
|
bool negated, |
74 |
|
bool removable, |
75 |
|
ProofGenerator* pg) |
76 |
|
{ |
77 |
7874 |
Trace("cnf") << "ProofCnfStream::convertAndAssert(" << node |
78 |
7874 |
<< ", negated = " << (negated ? "true" : "false") |
79 |
3937 |
<< ", removable = " << (removable ? "true" : "false") << ")\n"; |
80 |
3937 |
d_cnfStream.d_removable = removable; |
81 |
3937 |
if (pg) |
82 |
|
{ |
83 |
7282 |
Trace("cnf") << "ProofCnfStream::convertAndAssert: pg: " << pg->identify() |
84 |
3641 |
<< "\n"; |
85 |
7282 |
Node toJustify = negated ? node.notNode() : static_cast<Node>(node); |
86 |
3641 |
d_proof.addLazyStep(toJustify, |
87 |
|
pg, |
88 |
|
PfRule::ASSUME, |
89 |
|
true, |
90 |
|
"ProofCnfStream::convertAndAssert:cnf"); |
91 |
|
} |
92 |
3937 |
convertAndAssert(node, negated); |
93 |
|
// process saved steps in buffer |
94 |
3937 |
const std::vector<std::pair<Node, ProofStep>>& steps = d_psb.getSteps(); |
95 |
55146 |
for (const std::pair<Node, ProofStep>& step : steps) |
96 |
|
{ |
97 |
51209 |
d_proof.addStep(step.first, step.second); |
98 |
|
} |
99 |
3937 |
d_psb.clear(); |
100 |
3937 |
} |
101 |
|
|
102 |
4762 |
void ProofCnfStream::convertAndAssert(TNode node, bool negated) |
103 |
|
{ |
104 |
9524 |
Trace("cnf") << "ProofCnfStream::convertAndAssert(" << node |
105 |
4762 |
<< ", negated = " << (negated ? "true" : "false") << ")\n"; |
106 |
4762 |
switch (node.getKind()) |
107 |
|
{ |
108 |
681 |
case kind::AND: convertAndAssertAnd(node, negated); break; |
109 |
803 |
case kind::OR: convertAndAssertOr(node, negated); break; |
110 |
|
case kind::XOR: convertAndAssertXor(node, negated); break; |
111 |
2050 |
case kind::IMPLIES: convertAndAssertImplies(node, negated); break; |
112 |
184 |
case kind::ITE: convertAndAssertIte(node, negated); break; |
113 |
114 |
case kind::NOT: |
114 |
|
{ |
115 |
|
// track double negation elimination |
116 |
114 |
if (negated) |
117 |
|
{ |
118 |
|
d_proof.addStep(node[0], PfRule::NOT_NOT_ELIM, {node.notNode()}, {}); |
119 |
|
Trace("cnf") |
120 |
|
<< "ProofCnfStream::convertAndAssert: NOT_NOT_ELIM added norm " |
121 |
|
<< node[0] << "\n"; |
122 |
|
} |
123 |
114 |
convertAndAssert(node[0], !negated); |
124 |
114 |
break; |
125 |
|
} |
126 |
613 |
case kind::EQUAL: |
127 |
613 |
if (node[0].getType().isBoolean()) |
128 |
|
{ |
129 |
2 |
convertAndAssertIff(node, negated); |
130 |
2 |
break; |
131 |
|
} |
132 |
|
CVC5_FALLTHROUGH; |
133 |
|
default: |
134 |
|
{ |
135 |
|
// negate |
136 |
1856 |
Node nnode = negated ? node.negate() : static_cast<Node>(node); |
137 |
|
// Atoms |
138 |
928 |
SatLiteral lit = toCNF(node, negated); |
139 |
928 |
bool added = d_cnfStream.assertClause(nnode, lit); |
140 |
928 |
if (negated && added && nnode != node.notNode()) |
141 |
|
{ |
142 |
|
// track double negation elimination |
143 |
|
// (not (not n)) |
144 |
|
// -------------- NOT_NOT_ELIM |
145 |
|
// n |
146 |
|
d_proof.addStep(nnode, PfRule::NOT_NOT_ELIM, {node.notNode()}, {}); |
147 |
|
Trace("cnf") |
148 |
|
<< "ProofCnfStream::convertAndAssert: NOT_NOT_ELIM added norm " |
149 |
|
<< nnode << "\n"; |
150 |
|
} |
151 |
928 |
if (added) |
152 |
|
{ |
153 |
|
// note that we do not need to do the normalization here since this is |
154 |
|
// not a clause and double negation is tracked in a dedicated manner |
155 |
|
// above |
156 |
736 |
d_satPM->registerSatAssumptions({nnode}); |
157 |
928 |
} |
158 |
|
} |
159 |
|
} |
160 |
4762 |
} |
161 |
|
|
162 |
681 |
void ProofCnfStream::convertAndAssertAnd(TNode node, bool negated) |
163 |
|
{ |
164 |
1362 |
Trace("cnf") << "ProofCnfStream::convertAndAssertAnd(" << node |
165 |
681 |
<< ", negated = " << (negated ? "true" : "false") << ")\n"; |
166 |
681 |
Assert(node.getKind() == kind::AND); |
167 |
681 |
if (!negated) |
168 |
|
{ |
169 |
|
// If the node is a conjunction, we handle each conjunct separately |
170 |
320 |
NodeManager* nm = NodeManager::currentNM(); |
171 |
1031 |
for (unsigned i = 0, size = node.getNumChildren(); i < size; ++i) |
172 |
|
{ |
173 |
|
// Create a proof step for each n_i |
174 |
1422 |
Node iNode = nm->mkConst<Rational>(i); |
175 |
711 |
d_proof.addStep(node[i], PfRule::AND_ELIM, {node}, {iNode}); |
176 |
1422 |
Trace("cnf") << "ProofCnfStream::convertAndAssertAnd: AND_ELIM " << i |
177 |
711 |
<< " added norm " << node[i] << "\n"; |
178 |
711 |
convertAndAssert(node[i], false); |
179 |
|
} |
180 |
|
} |
181 |
|
else |
182 |
|
{ |
183 |
|
// If the node is a disjunction, we construct a clause and assert it |
184 |
361 |
unsigned i, size = node.getNumChildren(); |
185 |
722 |
SatClause clause(size); |
186 |
5779 |
for (i = 0; i < size; ++i) |
187 |
|
{ |
188 |
5418 |
clause[i] = toCNF(node[i], true); |
189 |
|
} |
190 |
361 |
bool added = d_cnfStream.assertClause(node.negate(), clause); |
191 |
|
// register proof step |
192 |
361 |
if (added) |
193 |
|
{ |
194 |
722 |
std::vector<Node> disjuncts; |
195 |
5779 |
for (i = 0; i < size; ++i) |
196 |
|
{ |
197 |
5418 |
disjuncts.push_back(node[i].notNode()); |
198 |
|
} |
199 |
722 |
Node clauseNode = NodeManager::currentNM()->mkNode(kind::OR, disjuncts); |
200 |
361 |
d_proof.addStep(clauseNode, PfRule::NOT_AND, {node.notNode()}, {}); |
201 |
722 |
Trace("cnf") << "ProofCnfStream::convertAndAssertAnd: NOT_AND added " |
202 |
361 |
<< clauseNode << "\n"; |
203 |
361 |
normalizeAndRegister(clauseNode); |
204 |
|
} |
205 |
|
} |
206 |
681 |
} |
207 |
|
|
208 |
803 |
void ProofCnfStream::convertAndAssertOr(TNode node, bool negated) |
209 |
|
{ |
210 |
1606 |
Trace("cnf") << "ProofCnfStream::convertAndAssertOr(" << node |
211 |
803 |
<< ", negated = " << (negated ? "true" : "false") << ")\n"; |
212 |
803 |
Assert(node.getKind() == kind::OR); |
213 |
803 |
if (!negated) |
214 |
|
{ |
215 |
|
// If the node is a disjunction, we construct a clause and assert it |
216 |
803 |
unsigned size = node.getNumChildren(); |
217 |
1606 |
SatClause clause(size); |
218 |
2933 |
for (unsigned i = 0; i < size; ++i) |
219 |
|
{ |
220 |
2130 |
clause[i] = toCNF(node[i], false); |
221 |
|
} |
222 |
803 |
normalizeAndRegister(node); |
223 |
803 |
d_cnfStream.assertClause(node, clause); |
224 |
|
} |
225 |
|
else |
226 |
|
{ |
227 |
|
// If the node is a negated disjunction, we handle it as a conjunction of |
228 |
|
// the negated arguments |
229 |
|
NodeManager* nm = NodeManager::currentNM(); |
230 |
|
for (unsigned i = 0, size = node.getNumChildren(); i < size; ++i) |
231 |
|
{ |
232 |
|
// Create a proof step for each (not n_i) |
233 |
|
Node iNode = nm->mkConst<Rational>(i); |
234 |
|
d_proof.addStep( |
235 |
|
node[i].notNode(), PfRule::NOT_OR_ELIM, {node.notNode()}, {iNode}); |
236 |
|
Trace("cnf") << "ProofCnfStream::convertAndAssertOr: NOT_OR_ELIM " << i |
237 |
|
<< " added norm " << node[i].notNode() << "\n"; |
238 |
|
convertAndAssert(node[i], true); |
239 |
|
} |
240 |
|
} |
241 |
803 |
} |
242 |
|
|
243 |
|
void ProofCnfStream::convertAndAssertXor(TNode node, bool negated) |
244 |
|
{ |
245 |
|
Trace("cnf") << "ProofCnfStream::convertAndAssertXor(" << node |
246 |
|
<< ", negated = " << (negated ? "true" : "false") << ")\n"; |
247 |
|
if (!negated) |
248 |
|
{ |
249 |
|
// p XOR q |
250 |
|
SatLiteral p = toCNF(node[0], false); |
251 |
|
SatLiteral q = toCNF(node[1], false); |
252 |
|
bool added; |
253 |
|
NodeManager* nm = NodeManager::currentNM(); |
254 |
|
// Construct the clause (~p v ~q) |
255 |
|
SatClause clause1(2); |
256 |
|
clause1[0] = ~p; |
257 |
|
clause1[1] = ~q; |
258 |
|
added = d_cnfStream.assertClause(node, clause1); |
259 |
|
if (added) |
260 |
|
{ |
261 |
|
Node clauseNode = |
262 |
|
nm->mkNode(kind::OR, node[0].notNode(), node[1].notNode()); |
263 |
|
d_proof.addStep(clauseNode, PfRule::XOR_ELIM2, {node}, {}); |
264 |
|
Trace("cnf") << "ProofCnfStream::convertAndAssertXor: XOR_ELIM2 added " |
265 |
|
<< clauseNode << "\n"; |
266 |
|
normalizeAndRegister(clauseNode); |
267 |
|
} |
268 |
|
// Construct the clause (p v q) |
269 |
|
SatClause clause2(2); |
270 |
|
clause2[0] = p; |
271 |
|
clause2[1] = q; |
272 |
|
added = d_cnfStream.assertClause(node, clause2); |
273 |
|
if (added) |
274 |
|
{ |
275 |
|
Node clauseNode = nm->mkNode(kind::OR, node[0], node[1]); |
276 |
|
d_proof.addStep(clauseNode, PfRule::XOR_ELIM1, {node}, {}); |
277 |
|
Trace("cnf") << "ProofCnfStream::convertAndAssertXor: XOR_ELIM1 added " |
278 |
|
<< clauseNode << "\n"; |
279 |
|
normalizeAndRegister(clauseNode); |
280 |
|
} |
281 |
|
} |
282 |
|
else |
283 |
|
{ |
284 |
|
// ~(p XOR q) is the same as p <=> q |
285 |
|
SatLiteral p = toCNF(node[0], false); |
286 |
|
SatLiteral q = toCNF(node[1], false); |
287 |
|
bool added; |
288 |
|
NodeManager* nm = NodeManager::currentNM(); |
289 |
|
// Construct the clause ~p v q |
290 |
|
SatClause clause1(2); |
291 |
|
clause1[0] = ~p; |
292 |
|
clause1[1] = q; |
293 |
|
added = d_cnfStream.assertClause(node.negate(), clause1); |
294 |
|
if (added) |
295 |
|
{ |
296 |
|
Node clauseNode = nm->mkNode(kind::OR, node[0].notNode(), node[1]); |
297 |
|
d_proof.addStep(clauseNode, PfRule::NOT_XOR_ELIM2, {node.notNode()}, {}); |
298 |
|
Trace("cnf") |
299 |
|
<< "ProofCnfStream::convertAndAssertXor: NOT_XOR_ELIM2 added " |
300 |
|
<< clauseNode << "\n"; |
301 |
|
normalizeAndRegister(clauseNode); |
302 |
|
} |
303 |
|
// Construct the clause ~q v p |
304 |
|
SatClause clause2(2); |
305 |
|
clause2[0] = p; |
306 |
|
clause2[1] = ~q; |
307 |
|
added = d_cnfStream.assertClause(node.negate(), clause2); |
308 |
|
if (added) |
309 |
|
{ |
310 |
|
Node clauseNode = nm->mkNode(kind::OR, node[0], node[1].notNode()); |
311 |
|
d_proof.addStep(clauseNode, PfRule::NOT_XOR_ELIM1, {node.notNode()}, {}); |
312 |
|
Trace("cnf") |
313 |
|
<< "ProofCnfStream::convertAndAssertXor: NOT_XOR_ELIM1 added " |
314 |
|
<< clauseNode << "\n"; |
315 |
|
normalizeAndRegister(clauseNode); |
316 |
|
} |
317 |
|
} |
318 |
|
} |
319 |
|
|
320 |
2 |
void ProofCnfStream::convertAndAssertIff(TNode node, bool negated) |
321 |
|
{ |
322 |
4 |
Trace("cnf") << "ProofCnfStream::convertAndAssertIff(" << node |
323 |
2 |
<< ", negated = " << (negated ? "true" : "false") << ")\n"; |
324 |
2 |
if (!negated) |
325 |
|
{ |
326 |
|
// p <=> q |
327 |
2 |
Trace("cnf") << push; |
328 |
2 |
SatLiteral p = toCNF(node[0], false); |
329 |
2 |
SatLiteral q = toCNF(node[1], false); |
330 |
2 |
Trace("cnf") << pop; |
331 |
|
bool added; |
332 |
2 |
NodeManager* nm = NodeManager::currentNM(); |
333 |
|
// Construct the clauses ~p v q |
334 |
4 |
SatClause clause1(2); |
335 |
2 |
clause1[0] = ~p; |
336 |
2 |
clause1[1] = q; |
337 |
2 |
added = d_cnfStream.assertClause(node, clause1); |
338 |
2 |
if (added) |
339 |
|
{ |
340 |
4 |
Node clauseNode = nm->mkNode(kind::OR, node[0].notNode(), node[1]); |
341 |
2 |
d_proof.addStep(clauseNode, PfRule::EQUIV_ELIM1, {node}, {}); |
342 |
4 |
Trace("cnf") << "ProofCnfStream::convertAndAssertIff: EQUIV_ELIM1 added " |
343 |
2 |
<< clauseNode << "\n"; |
344 |
2 |
normalizeAndRegister(clauseNode); |
345 |
|
} |
346 |
|
// Construct the clauses ~q v p |
347 |
4 |
SatClause clause2(2); |
348 |
2 |
clause2[0] = p; |
349 |
2 |
clause2[1] = ~q; |
350 |
2 |
added = d_cnfStream.assertClause(node, clause2); |
351 |
2 |
if (added) |
352 |
|
{ |
353 |
4 |
Node clauseNode = nm->mkNode(kind::OR, node[0], node[1].notNode()); |
354 |
2 |
d_proof.addStep(clauseNode, PfRule::EQUIV_ELIM2, {node}, {}); |
355 |
4 |
Trace("cnf") << "ProofCnfStream::convertAndAssertIff: EQUIV_ELIM2 added " |
356 |
2 |
<< clauseNode << "\n"; |
357 |
2 |
normalizeAndRegister(clauseNode); |
358 |
|
} |
359 |
|
} |
360 |
|
else |
361 |
|
{ |
362 |
|
// ~(p <=> q) is the same as p XOR q |
363 |
|
Trace("cnf") << push; |
364 |
|
SatLiteral p = toCNF(node[0], false); |
365 |
|
SatLiteral q = toCNF(node[1], false); |
366 |
|
Trace("cnf") << pop; |
367 |
|
bool added; |
368 |
|
NodeManager* nm = NodeManager::currentNM(); |
369 |
|
// Construct the clauses ~p v ~q |
370 |
|
SatClause clause1(2); |
371 |
|
clause1[0] = ~p; |
372 |
|
clause1[1] = ~q; |
373 |
|
added = d_cnfStream.assertClause(node.negate(), clause1); |
374 |
|
if (added) |
375 |
|
{ |
376 |
|
Node clauseNode = |
377 |
|
nm->mkNode(kind::OR, node[0].notNode(), node[1].notNode()); |
378 |
|
d_proof.addStep( |
379 |
|
clauseNode, PfRule::NOT_EQUIV_ELIM2, {node.notNode()}, {}); |
380 |
|
Trace("cnf") |
381 |
|
<< "ProofCnfStream::convertAndAssertIff: NOT_EQUIV_ELIM2 added " |
382 |
|
<< clauseNode << "\n"; |
383 |
|
normalizeAndRegister(clauseNode); |
384 |
|
} |
385 |
|
// Construct the clauses q v p |
386 |
|
SatClause clause2(2); |
387 |
|
clause2[0] = p; |
388 |
|
clause2[1] = q; |
389 |
|
added = d_cnfStream.assertClause(node.negate(), clause2); |
390 |
|
if (added) |
391 |
|
{ |
392 |
|
Node clauseNode = nm->mkNode(kind::OR, node[0], node[1]); |
393 |
|
d_proof.addStep( |
394 |
|
clauseNode, PfRule::NOT_EQUIV_ELIM1, {node.notNode()}, {}); |
395 |
|
Trace("cnf") |
396 |
|
<< "ProofCnfStream::convertAndAssertIff: NOT_EQUIV_ELIM1 added " |
397 |
|
<< clauseNode << "\n"; |
398 |
|
normalizeAndRegister(clauseNode); |
399 |
|
} |
400 |
|
} |
401 |
2 |
} |
402 |
|
|
403 |
2050 |
void ProofCnfStream::convertAndAssertImplies(TNode node, bool negated) |
404 |
|
{ |
405 |
4100 |
Trace("cnf") << "ProofCnfStream::convertAndAssertImplies(" << node |
406 |
2050 |
<< ", negated = " << (negated ? "true" : "false") << ")\n"; |
407 |
2050 |
if (!negated) |
408 |
|
{ |
409 |
|
// ~p v q |
410 |
2050 |
SatLiteral p = toCNF(node[0], false); |
411 |
2050 |
SatLiteral q = toCNF(node[1], false); |
412 |
|
// Construct the clause ~p || q |
413 |
4100 |
SatClause clause(2); |
414 |
2050 |
clause[0] = ~p; |
415 |
2050 |
clause[1] = q; |
416 |
2050 |
bool added = d_cnfStream.assertClause(node, clause); |
417 |
2050 |
if (added) |
418 |
|
{ |
419 |
|
Node clauseNode = NodeManager::currentNM()->mkNode( |
420 |
3736 |
kind::OR, node[0].notNode(), node[1]); |
421 |
1868 |
d_proof.addStep(clauseNode, PfRule::IMPLIES_ELIM, {node}, {}); |
422 |
3736 |
Trace("cnf") |
423 |
1868 |
<< "ProofCnfStream::convertAndAssertImplies: IMPLIES_ELIM added " |
424 |
1868 |
<< clauseNode << "\n"; |
425 |
1868 |
normalizeAndRegister(clauseNode); |
426 |
|
} |
427 |
|
} |
428 |
|
else |
429 |
|
{ |
430 |
|
// ~(p => q) is the same as p ^ ~q |
431 |
|
// process p |
432 |
|
convertAndAssert(node[0], false); |
433 |
|
d_proof.addStep(node[0], PfRule::NOT_IMPLIES_ELIM1, {node.notNode()}, {}); |
434 |
|
Trace("cnf") |
435 |
|
<< "ProofCnfStream::convertAndAssertImplies: NOT_IMPLIES_ELIM1 added " |
436 |
|
<< node[0] << "\n"; |
437 |
|
// process ~q |
438 |
|
convertAndAssert(node[1], true); |
439 |
|
d_proof.addStep( |
440 |
|
node[1].notNode(), PfRule::NOT_IMPLIES_ELIM2, {node.notNode()}, {}); |
441 |
|
Trace("cnf") |
442 |
|
<< "ProofCnfStream::convertAndAssertImplies: NOT_IMPLIES_ELIM2 added " |
443 |
|
<< node[1].notNode() << "\n"; |
444 |
|
} |
445 |
2050 |
} |
446 |
|
|
447 |
184 |
void ProofCnfStream::convertAndAssertIte(TNode node, bool negated) |
448 |
|
{ |
449 |
368 |
Trace("cnf") << "ProofCnfStream::convertAndAssertIte(" << node |
450 |
184 |
<< ", negated = " << (negated ? "true" : "false") << ")\n"; |
451 |
|
// ITE(p, q, r) |
452 |
184 |
SatLiteral p = toCNF(node[0], false); |
453 |
184 |
SatLiteral q = toCNF(node[1], negated); |
454 |
184 |
SatLiteral r = toCNF(node[2], negated); |
455 |
|
bool added; |
456 |
184 |
NodeManager* nm = NodeManager::currentNM(); |
457 |
|
// Construct the clauses: |
458 |
|
// (~p v q) and (p v r) |
459 |
|
// |
460 |
|
// Note that below q and r can be used directly because whether they are |
461 |
|
// negated has been push to the literal definitions above |
462 |
368 |
Node nnode = negated ? node.negate() : static_cast<Node>(node); |
463 |
|
// (~p v q) |
464 |
368 |
SatClause clause1(2); |
465 |
184 |
clause1[0] = ~p; |
466 |
184 |
clause1[1] = q; |
467 |
184 |
added = d_cnfStream.assertClause(nnode, clause1); |
468 |
184 |
if (added) |
469 |
|
{ |
470 |
|
// redo the negation here to avoid silent double negation elimination |
471 |
184 |
if (!negated) |
472 |
|
{ |
473 |
368 |
Node clauseNode = nm->mkNode(kind::OR, node[0].notNode(), node[1]); |
474 |
184 |
d_proof.addStep(clauseNode, PfRule::ITE_ELIM1, {node}, {}); |
475 |
368 |
Trace("cnf") << "ProofCnfStream::convertAndAssertIte: ITE_ELIM1 added " |
476 |
184 |
<< clauseNode << "\n"; |
477 |
184 |
normalizeAndRegister(clauseNode); |
478 |
|
} |
479 |
|
else |
480 |
|
{ |
481 |
|
Node clauseNode = |
482 |
|
nm->mkNode(kind::OR, node[0].notNode(), node[1].notNode()); |
483 |
|
d_proof.addStep(clauseNode, PfRule::NOT_ITE_ELIM1, {node.notNode()}, {}); |
484 |
|
Trace("cnf") |
485 |
|
<< "ProofCnfStream::convertAndAssertIte: NOT_ITE_ELIM1 added " |
486 |
|
<< clauseNode << "\n"; |
487 |
|
normalizeAndRegister(clauseNode); |
488 |
|
} |
489 |
|
} |
490 |
|
// (p v r) |
491 |
368 |
SatClause clause2(2); |
492 |
184 |
clause2[0] = p; |
493 |
184 |
clause2[1] = r; |
494 |
184 |
added = d_cnfStream.assertClause(nnode, clause2); |
495 |
184 |
if (added) |
496 |
|
{ |
497 |
|
// redo the negation here to avoid silent double negation elimination |
498 |
152 |
if (!negated) |
499 |
|
{ |
500 |
304 |
Node clauseNode = nm->mkNode(kind::OR, node[0], node[2]); |
501 |
152 |
d_proof.addStep(clauseNode, PfRule::ITE_ELIM2, {node}, {}); |
502 |
304 |
Trace("cnf") << "ProofCnfStream::convertAndAssertIte: ITE_ELIM2 added " |
503 |
152 |
<< clauseNode << "\n"; |
504 |
152 |
normalizeAndRegister(clauseNode); |
505 |
|
} |
506 |
|
else |
507 |
|
{ |
508 |
|
Node clauseNode = nm->mkNode(kind::OR, node[0], node[2].notNode()); |
509 |
|
d_proof.addStep(clauseNode, PfRule::NOT_ITE_ELIM2, {node.notNode()}, {}); |
510 |
|
Trace("cnf") |
511 |
|
<< "ProofCnfStream::convertAndAssertIte: NOT_ITE_ELIM2 added " |
512 |
|
<< clauseNode << "\n"; |
513 |
|
normalizeAndRegister(clauseNode); |
514 |
|
} |
515 |
|
} |
516 |
184 |
} |
517 |
|
|
518 |
229 |
void ProofCnfStream::convertPropagation(TrustNode trn) |
519 |
|
{ |
520 |
458 |
Node proven = trn.getProven(); |
521 |
458 |
Trace("cnf") << "ProofCnfStream::convertPropagation: proven explanation" |
522 |
229 |
<< proven << "\n"; |
523 |
|
// If we are not producing proofs in the theory engine there is no need to |
524 |
|
// keep track in d_proof of the clausification. We still need however to let |
525 |
|
// the SAT proof manager know that this clause is an assumption. |
526 |
229 |
bool proofLogging = trn.getGenerator() != nullptr; |
527 |
229 |
if (proofLogging) |
528 |
|
{ |
529 |
229 |
Assert(trn.getGenerator()->getProofFor(proven)->isClosed()); |
530 |
458 |
Trace("cnf-steps") << proven << " by explainPropagation " |
531 |
229 |
<< trn.identifyGenerator() << std::endl; |
532 |
229 |
d_proof.addLazyStep(proven, |
533 |
|
trn.getGenerator(), |
534 |
|
PfRule::ASSUME, |
535 |
|
true, |
536 |
|
"ProofCnfStream::convertPropagation"); |
537 |
|
} |
538 |
|
// since the propagation is added directly to the SAT solver via theoryProxy, |
539 |
|
// do the transformation of the lemma E1 ^ ... ^ En => P into CNF here |
540 |
229 |
NodeManager* nm = NodeManager::currentNM(); |
541 |
458 |
Node clauseImpliesElim; |
542 |
229 |
if (proofLogging) |
543 |
|
{ |
544 |
229 |
clauseImpliesElim = nm->mkNode(kind::OR, proven[0].notNode(), proven[1]); |
545 |
458 |
Trace("cnf") << "ProofCnfStream::convertPropagation: adding " |
546 |
458 |
<< PfRule::IMPLIES_ELIM << " rule to conclude " |
547 |
229 |
<< clauseImpliesElim << "\n"; |
548 |
229 |
d_proof.addStep(clauseImpliesElim, PfRule::IMPLIES_ELIM, {proven}, {}); |
549 |
|
} |
550 |
458 |
Node clauseExp; |
551 |
|
// need to eliminate AND |
552 |
229 |
if (proven[0].getKind() == kind::AND) |
553 |
|
{ |
554 |
378 |
std::vector<Node> disjunctsAndNeg{proven[0]}; |
555 |
378 |
std::vector<Node> disjunctsRes; |
556 |
1106 |
for (unsigned i = 0, size = proven[0].getNumChildren(); i < size; ++i) |
557 |
|
{ |
558 |
917 |
disjunctsAndNeg.push_back(proven[0][i].notNode()); |
559 |
917 |
disjunctsRes.push_back(proven[0][i].notNode()); |
560 |
|
} |
561 |
189 |
disjunctsRes.push_back(proven[1]); |
562 |
189 |
clauseExp = nm->mkNode(kind::OR, disjunctsRes); |
563 |
189 |
if (proofLogging) |
564 |
|
{ |
565 |
|
// add proof steps to convert into clause |
566 |
378 |
Node clauseAndNeg = nm->mkNode(kind::OR, disjunctsAndNeg); |
567 |
189 |
d_proof.addStep(clauseAndNeg, PfRule::CNF_AND_NEG, {}, {proven[0]}); |
568 |
945 |
d_proof.addStep(clauseExp, |
569 |
|
PfRule::RESOLUTION, |
570 |
|
{clauseAndNeg, clauseImpliesElim}, |
571 |
756 |
{nm->mkConst(true), proven[0]}); |
572 |
|
} |
573 |
|
} |
574 |
|
else |
575 |
|
{ |
576 |
40 |
clauseExp = nm->mkNode(kind::OR, proven[0].notNode(), proven[1]); |
577 |
|
} |
578 |
229 |
normalizeAndRegister(clauseExp); |
579 |
|
// consume steps |
580 |
229 |
if (proofLogging) |
581 |
|
{ |
582 |
229 |
const std::vector<std::pair<Node, ProofStep>>& steps = d_psb.getSteps(); |
583 |
1706 |
for (const std::pair<Node, ProofStep>& step : steps) |
584 |
|
{ |
585 |
1477 |
d_proof.addStep(step.first, step.second); |
586 |
|
} |
587 |
229 |
d_psb.clear(); |
588 |
|
} |
589 |
229 |
} |
590 |
|
|
591 |
2540 |
void ProofCnfStream::ensureLiteral(TNode n) |
592 |
|
{ |
593 |
2540 |
Trace("cnf") << "ProofCnfStream::ensureLiteral(" << n << ")\n"; |
594 |
2540 |
if (d_cnfStream.hasLiteral(n)) |
595 |
|
{ |
596 |
2514 |
d_cnfStream.ensureMappingForLiteral(n); |
597 |
2514 |
return; |
598 |
|
} |
599 |
|
// remove top level negation. We don't need to track this because it's a |
600 |
|
// literal. |
601 |
26 |
n = n.getKind() == kind::NOT ? n[0] : n; |
602 |
26 |
if (theory::Theory::theoryOf(n) == theory::THEORY_BOOL && !n.isVar()) |
603 |
|
{ |
604 |
|
// These are not removable |
605 |
|
d_cnfStream.d_removable = false; |
606 |
|
SatLiteral lit = toCNF(n, false); |
607 |
|
// Store backward-mappings |
608 |
|
// These may already exist |
609 |
|
d_cnfStream.d_literalToNodeMap.insert_safe(lit, n); |
610 |
|
d_cnfStream.d_literalToNodeMap.insert_safe(~lit, n.notNode()); |
611 |
|
} |
612 |
|
else |
613 |
|
{ |
614 |
26 |
d_cnfStream.convertAtom(n); |
615 |
|
} |
616 |
|
} |
617 |
|
|
618 |
25032 |
SatLiteral ProofCnfStream::toCNF(TNode node, bool negated) |
619 |
|
{ |
620 |
50064 |
Trace("cnf") << "toCNF(" << node |
621 |
25032 |
<< ", negated = " << (negated ? "true" : "false") << ")\n"; |
622 |
25032 |
SatLiteral lit; |
623 |
|
// If the node has already has a literal, return it (maybe negated) |
624 |
25032 |
if (d_cnfStream.hasLiteral(node)) |
625 |
|
{ |
626 |
19397 |
Trace("cnf") << "toCNF(): already translated\n"; |
627 |
19397 |
lit = d_cnfStream.getLiteral(node); |
628 |
|
// Return the (maybe negated) literal |
629 |
19397 |
return !negated ? lit : ~lit; |
630 |
|
} |
631 |
|
|
632 |
|
// Handle each Boolean operator case |
633 |
5635 |
switch (node.getKind()) |
634 |
|
{ |
635 |
1391 |
case kind::AND: lit = handleAnd(node); break; |
636 |
136 |
case kind::OR: lit = handleOr(node); break; |
637 |
|
case kind::XOR: lit = handleXor(node); break; |
638 |
|
case kind::IMPLIES: lit = handleImplies(node); break; |
639 |
|
case kind::ITE: lit = handleIte(node); break; |
640 |
480 |
case kind::NOT: lit = ~toCNF(node[0]); break; |
641 |
2496 |
case kind::EQUAL: |
642 |
7484 |
lit = node[0].getType().isBoolean() ? handleIff(node) |
643 |
4988 |
: d_cnfStream.convertAtom(node); |
644 |
2496 |
break; |
645 |
1132 |
default: |
646 |
|
{ |
647 |
1132 |
lit = d_cnfStream.convertAtom(node); |
648 |
|
} |
649 |
1132 |
break; |
650 |
|
} |
651 |
|
// Return the (maybe negated) literal |
652 |
5635 |
return !negated ? lit : ~lit; |
653 |
|
} |
654 |
|
|
655 |
1391 |
SatLiteral ProofCnfStream::handleAnd(TNode node) |
656 |
|
{ |
657 |
1391 |
Assert(!d_cnfStream.hasLiteral(node)) << "Atom already mapped!"; |
658 |
1391 |
Assert(node.getKind() == kind::AND) << "Expecting an AND expression!"; |
659 |
1391 |
Assert(node.getNumChildren() > 1) << "Expecting more than 1 child!"; |
660 |
1391 |
Assert(!d_cnfStream.d_removable) |
661 |
|
<< "Removable clauses cannot contain Boolean structure"; |
662 |
1391 |
Trace("cnf") << "ProofCnfStream::handleAnd(" << node << ")\n"; |
663 |
|
// Number of children |
664 |
1391 |
unsigned size = node.getNumChildren(); |
665 |
|
// Transform all the children first (remembering the negation) |
666 |
2782 |
SatClause clause(size + 1); |
667 |
12509 |
for (unsigned i = 0; i < size; ++i) |
668 |
|
{ |
669 |
11118 |
Trace("cnf") << push; |
670 |
11118 |
clause[i] = ~toCNF(node[i]); |
671 |
11118 |
Trace("cnf") << pop; |
672 |
|
} |
673 |
|
// Create literal for the node |
674 |
1391 |
SatLiteral lit = d_cnfStream.newLiteral(node); |
675 |
|
bool added; |
676 |
1391 |
NodeManager* nm = NodeManager::currentNM(); |
677 |
|
// lit -> (a_1 & a_2 & a_3 & ... & a_n) |
678 |
|
// ~lit | (a_1 & a_2 & a_3 & ... & a_n) |
679 |
|
// (~lit | a_1) & (~lit | a_2) & ... & (~lit | a_n) |
680 |
12509 |
for (unsigned i = 0; i < size; ++i) |
681 |
|
{ |
682 |
11118 |
Trace("cnf") << push; |
683 |
11118 |
added = d_cnfStream.assertClause(node.negate(), ~lit, ~clause[i]); |
684 |
11118 |
Trace("cnf") << pop; |
685 |
11118 |
if (added) |
686 |
|
{ |
687 |
13812 |
Node clauseNode = nm->mkNode(kind::OR, node.notNode(), node[i]); |
688 |
13812 |
Node iNode = nm->mkConst<Rational>(i); |
689 |
6906 |
d_proof.addStep(clauseNode, PfRule::CNF_AND_POS, {}, {node, iNode}); |
690 |
13812 |
Trace("cnf") << "ProofCnfStream::handleAnd: CNF_AND_POS " << i |
691 |
6906 |
<< " added " << clauseNode << "\n"; |
692 |
6906 |
normalizeAndRegister(clauseNode); |
693 |
|
} |
694 |
|
} |
695 |
|
// lit <- (a_1 & a_2 & a_3 & ... a_n) |
696 |
|
// lit | ~(a_1 & a_2 & a_3 & ... & a_n) |
697 |
|
// lit | ~a_1 | ~a_2 | ~a_3 | ... | ~a_n |
698 |
1391 |
clause[size] = lit; |
699 |
|
// This needs to go last, as the clause might get modified by the SAT solver |
700 |
1391 |
Trace("cnf") << push; |
701 |
1391 |
added = d_cnfStream.assertClause(node, clause); |
702 |
1391 |
Trace("cnf") << pop; |
703 |
1391 |
if (added) |
704 |
|
{ |
705 |
2782 |
std::vector<Node> disjuncts{node}; |
706 |
12509 |
for (unsigned i = 0; i < size; ++i) |
707 |
|
{ |
708 |
11118 |
disjuncts.push_back(node[i].notNode()); |
709 |
|
} |
710 |
2782 |
Node clauseNode = nm->mkNode(kind::OR, disjuncts); |
711 |
1391 |
d_proof.addStep(clauseNode, PfRule::CNF_AND_NEG, {}, {node}); |
712 |
2782 |
Trace("cnf") << "ProofCnfStream::handleAnd: CNF_AND_NEG added " |
713 |
1391 |
<< clauseNode << "\n"; |
714 |
1391 |
normalizeAndRegister(clauseNode); |
715 |
|
} |
716 |
2782 |
return lit; |
717 |
|
} |
718 |
|
|
719 |
136 |
SatLiteral ProofCnfStream::handleOr(TNode node) |
720 |
|
{ |
721 |
136 |
Assert(!d_cnfStream.hasLiteral(node)) << "Atom already mapped!"; |
722 |
136 |
Assert(node.getKind() == kind::OR) << "Expecting an OR expression!"; |
723 |
136 |
Assert(node.getNumChildren() > 1) << "Expecting more then 1 child!"; |
724 |
136 |
Assert(!d_cnfStream.d_removable) |
725 |
|
<< "Removable clauses can not contain Boolean structure"; |
726 |
136 |
Trace("cnf") << "ProofCnfStream::handleOr(" << node << ")\n"; |
727 |
|
// Number of children |
728 |
136 |
unsigned size = node.getNumChildren(); |
729 |
|
// Transform all the children first |
730 |
272 |
SatClause clause(size + 1); |
731 |
430 |
for (unsigned i = 0; i < size; ++i) |
732 |
|
{ |
733 |
294 |
clause[i] = toCNF(node[i]); |
734 |
|
} |
735 |
|
// Create literal for the node |
736 |
136 |
SatLiteral lit = d_cnfStream.newLiteral(node); |
737 |
|
bool added; |
738 |
136 |
NodeManager* nm = NodeManager::currentNM(); |
739 |
|
// lit <- (a_1 | a_2 | a_3 | ... | a_n) |
740 |
|
// lit | ~(a_1 | a_2 | a_3 | ... | a_n) |
741 |
|
// (lit | ~a_1) & (lit | ~a_2) & (lit & ~a_3) & ... & (lit & ~a_n) |
742 |
430 |
for (unsigned i = 0; i < size; ++i) |
743 |
|
{ |
744 |
294 |
added = d_cnfStream.assertClause(node, lit, ~clause[i]); |
745 |
294 |
if (added) |
746 |
|
{ |
747 |
510 |
Node clauseNode = nm->mkNode(kind::OR, node, node[i].notNode()); |
748 |
510 |
Node iNode = nm->mkConst<Rational>(i); |
749 |
255 |
d_proof.addStep(clauseNode, PfRule::CNF_OR_NEG, {}, {node, iNode}); |
750 |
510 |
Trace("cnf") << "ProofCnfStream::handleOr: CNF_OR_NEG " << i << " added " |
751 |
255 |
<< clauseNode << "\n"; |
752 |
255 |
normalizeAndRegister(clauseNode); |
753 |
|
} |
754 |
|
} |
755 |
|
// lit -> (a_1 | a_2 | a_3 | ... | a_n) |
756 |
|
// ~lit | a_1 | a_2 | a_3 | ... | a_n |
757 |
136 |
clause[size] = ~lit; |
758 |
|
// This needs to go last, as the clause might get modified by the SAT solver |
759 |
136 |
added = d_cnfStream.assertClause(node.negate(), clause); |
760 |
136 |
if (added) |
761 |
|
{ |
762 |
272 |
std::vector<Node> disjuncts{node.notNode()}; |
763 |
430 |
for (unsigned i = 0; i < size; ++i) |
764 |
|
{ |
765 |
294 |
disjuncts.push_back(node[i]); |
766 |
|
} |
767 |
272 |
Node clauseNode = nm->mkNode(kind::OR, disjuncts); |
768 |
136 |
d_proof.addStep(clauseNode, PfRule::CNF_OR_POS, {}, {node}); |
769 |
272 |
Trace("cnf") << "ProofCnfStream::handleOr: CNF_OR_POS added " << clauseNode |
770 |
136 |
<< "\n"; |
771 |
136 |
normalizeAndRegister(clauseNode); |
772 |
|
} |
773 |
272 |
return lit; |
774 |
|
} |
775 |
|
|
776 |
|
SatLiteral ProofCnfStream::handleXor(TNode node) |
777 |
|
{ |
778 |
|
Assert(!d_cnfStream.hasLiteral(node)) << "Atom already mapped!"; |
779 |
|
Assert(node.getKind() == kind::XOR) << "Expecting an XOR expression!"; |
780 |
|
Assert(node.getNumChildren() == 2) << "Expecting exactly 2 children!"; |
781 |
|
Assert(!d_cnfStream.d_removable) |
782 |
|
<< "Removable clauses can not contain Boolean structure"; |
783 |
|
Trace("cnf") << "ProofCnfStream::handleXor(" << node << ")\n"; |
784 |
|
SatLiteral a = toCNF(node[0]); |
785 |
|
SatLiteral b = toCNF(node[1]); |
786 |
|
SatLiteral lit = d_cnfStream.newLiteral(node); |
787 |
|
bool added; |
788 |
|
added = d_cnfStream.assertClause(node.negate(), a, b, ~lit); |
789 |
|
if (added) |
790 |
|
{ |
791 |
|
Node clauseNode = NodeManager::currentNM()->mkNode( |
792 |
|
kind::OR, node.notNode(), node[0], node[1]); |
793 |
|
d_proof.addStep(clauseNode, PfRule::CNF_XOR_POS1, {}, {node}); |
794 |
|
Trace("cnf") << "ProofCnfStream::handleXor: CNF_XOR_POS1 added " |
795 |
|
<< clauseNode << "\n"; |
796 |
|
normalizeAndRegister(clauseNode); |
797 |
|
} |
798 |
|
added = d_cnfStream.assertClause(node.negate(), ~a, ~b, ~lit); |
799 |
|
if (added) |
800 |
|
{ |
801 |
|
Node clauseNode = NodeManager::currentNM()->mkNode( |
802 |
|
kind::OR, node.notNode(), node[0].notNode(), node[1].notNode()); |
803 |
|
d_proof.addStep(clauseNode, PfRule::CNF_XOR_POS2, {}, {node}); |
804 |
|
Trace("cnf") << "ProofCnfStream::handleXor: CNF_XOR_POS2 added " |
805 |
|
<< clauseNode << "\n"; |
806 |
|
normalizeAndRegister(clauseNode); |
807 |
|
} |
808 |
|
added = d_cnfStream.assertClause(node, a, ~b, lit); |
809 |
|
if (added) |
810 |
|
{ |
811 |
|
Node clauseNode = NodeManager::currentNM()->mkNode( |
812 |
|
kind::OR, node, node[0], node[1].notNode()); |
813 |
|
d_proof.addStep(clauseNode, PfRule::CNF_XOR_NEG2, {}, {node}); |
814 |
|
Trace("cnf") << "ProofCnfStream::handleXor: CNF_XOR_NEG2 added " |
815 |
|
<< clauseNode << "\n"; |
816 |
|
normalizeAndRegister(clauseNode); |
817 |
|
} |
818 |
|
added = d_cnfStream.assertClause(node, ~a, b, lit); |
819 |
|
if (added) |
820 |
|
{ |
821 |
|
Node clauseNode = NodeManager::currentNM()->mkNode( |
822 |
|
kind::OR, node, node[0].notNode(), node[1]); |
823 |
|
d_proof.addStep(clauseNode, PfRule::CNF_XOR_NEG1, {}, {node}); |
824 |
|
Trace("cnf") << "ProofCnfStream::handleXor: CNF_XOR_NEG1 added " |
825 |
|
<< clauseNode << "\n"; |
826 |
|
normalizeAndRegister(clauseNode); |
827 |
|
} |
828 |
|
return lit; |
829 |
|
} |
830 |
|
|
831 |
4 |
SatLiteral ProofCnfStream::handleIff(TNode node) |
832 |
|
{ |
833 |
4 |
Assert(!d_cnfStream.hasLiteral(node)) << "Atom already mapped!"; |
834 |
4 |
Assert(node.getKind() == kind::EQUAL) << "Expecting an EQUAL expression!"; |
835 |
4 |
Assert(node.getNumChildren() == 2) << "Expecting exactly 2 children!"; |
836 |
4 |
Trace("cnf") << "handleIff(" << node << ")\n"; |
837 |
|
// Convert the children to CNF |
838 |
4 |
SatLiteral a = toCNF(node[0]); |
839 |
4 |
SatLiteral b = toCNF(node[1]); |
840 |
|
// Create literal for the node |
841 |
4 |
SatLiteral lit = d_cnfStream.newLiteral(node); |
842 |
|
bool added; |
843 |
4 |
NodeManager* nm = NodeManager::currentNM(); |
844 |
|
// lit -> ((a-> b) & (b->a)) |
845 |
|
// ~lit | ((~a | b) & (~b | a)) |
846 |
|
// (~a | b | ~lit) & (~b | a | ~lit) |
847 |
4 |
added = d_cnfStream.assertClause(node.negate(), ~a, b, ~lit); |
848 |
4 |
if (added) |
849 |
|
{ |
850 |
|
Node clauseNode = |
851 |
8 |
nm->mkNode(kind::OR, node.notNode(), node[0].notNode(), node[1]); |
852 |
4 |
d_proof.addStep(clauseNode, PfRule::CNF_EQUIV_POS1, {}, {node}); |
853 |
8 |
Trace("cnf") << "ProofCnfStream::handleIff: CNF_EQUIV_POS1 added " |
854 |
4 |
<< clauseNode << "\n"; |
855 |
4 |
normalizeAndRegister(clauseNode); |
856 |
|
} |
857 |
4 |
added = d_cnfStream.assertClause(node.negate(), a, ~b, ~lit); |
858 |
4 |
if (added) |
859 |
|
{ |
860 |
|
Node clauseNode = |
861 |
8 |
nm->mkNode(kind::OR, node.notNode(), node[0], node[1].notNode()); |
862 |
4 |
d_proof.addStep(clauseNode, PfRule::CNF_EQUIV_POS2, {}, {node}); |
863 |
8 |
Trace("cnf") << "ProofCnfStream::handleIff: CNF_EQUIV_POS2 added " |
864 |
4 |
<< clauseNode << "\n"; |
865 |
4 |
normalizeAndRegister(clauseNode); |
866 |
|
} |
867 |
|
// (a<->b) -> lit |
868 |
|
// ~((a & b) | (~a & ~b)) | lit |
869 |
|
// (~(a & b)) & (~(~a & ~b)) | lit |
870 |
|
// ((~a | ~b) & (a | b)) | lit |
871 |
|
// (~a | ~b | lit) & (a | b | lit) |
872 |
4 |
added = d_cnfStream.assertClause(node, ~a, ~b, lit); |
873 |
4 |
if (added) |
874 |
|
{ |
875 |
|
Node clauseNode = |
876 |
8 |
nm->mkNode(kind::OR, node, node[0].notNode(), node[1].notNode()); |
877 |
4 |
d_proof.addStep(clauseNode, PfRule::CNF_EQUIV_NEG2, {}, {node}); |
878 |
8 |
Trace("cnf") << "ProofCnfStream::handleIff: CNF_EQUIV_NEG2 added " |
879 |
4 |
<< clauseNode << "\n"; |
880 |
4 |
normalizeAndRegister(clauseNode); |
881 |
|
} |
882 |
4 |
added = d_cnfStream.assertClause(node, a, b, lit); |
883 |
4 |
if (added) |
884 |
|
{ |
885 |
8 |
Node clauseNode = nm->mkNode(kind::OR, node, node[0], node[1]); |
886 |
4 |
d_proof.addStep(clauseNode, PfRule::CNF_EQUIV_NEG1, {}, {node}); |
887 |
8 |
Trace("cnf") << "ProofCnfStream::handleIff: CNF_EQUIV_NEG1 added " |
888 |
4 |
<< clauseNode << "\n"; |
889 |
4 |
normalizeAndRegister(clauseNode); |
890 |
|
} |
891 |
4 |
return lit; |
892 |
|
} |
893 |
|
|
894 |
|
SatLiteral ProofCnfStream::handleImplies(TNode node) |
895 |
|
{ |
896 |
|
Assert(!d_cnfStream.hasLiteral(node)) << "Atom already mapped!"; |
897 |
|
Assert(node.getKind() == kind::IMPLIES) << "Expecting an IMPLIES expression!"; |
898 |
|
Assert(node.getNumChildren() == 2) << "Expecting exactly 2 children!"; |
899 |
|
Assert(!d_cnfStream.d_removable) |
900 |
|
<< "Removable clauses can not contain Boolean structure"; |
901 |
|
Trace("cnf") << "ProofCnfStream::handleImplies(" << node << ")\n"; |
902 |
|
// Convert the children to cnf |
903 |
|
SatLiteral a = toCNF(node[0]); |
904 |
|
SatLiteral b = toCNF(node[1]); |
905 |
|
SatLiteral lit = d_cnfStream.newLiteral(node); |
906 |
|
bool added; |
907 |
|
NodeManager* nm = NodeManager::currentNM(); |
908 |
|
// lit -> (a->b) |
909 |
|
// ~lit | ~ a | b |
910 |
|
added = d_cnfStream.assertClause(node.negate(), ~lit, ~a, b); |
911 |
|
if (added) |
912 |
|
{ |
913 |
|
Node clauseNode = |
914 |
|
nm->mkNode(kind::OR, node.notNode(), node[0].notNode(), node[1]); |
915 |
|
d_proof.addStep(clauseNode, PfRule::CNF_IMPLIES_POS, {}, {node}); |
916 |
|
Trace("cnf") << "ProofCnfStream::handleImplies: CNF_IMPLIES_POS added " |
917 |
|
<< clauseNode << "\n"; |
918 |
|
normalizeAndRegister(clauseNode); |
919 |
|
} |
920 |
|
// (a->b) -> lit |
921 |
|
// ~(~a | b) | lit |
922 |
|
// (a | l) & (~b | l) |
923 |
|
added = d_cnfStream.assertClause(node, a, lit); |
924 |
|
if (added) |
925 |
|
{ |
926 |
|
Node clauseNode = nm->mkNode(kind::OR, node, node[0]); |
927 |
|
d_proof.addStep(clauseNode, PfRule::CNF_IMPLIES_NEG1, {}, {node}); |
928 |
|
Trace("cnf") << "ProofCnfStream::handleImplies: CNF_IMPLIES_NEG1 added " |
929 |
|
<< clauseNode << "\n"; |
930 |
|
normalizeAndRegister(clauseNode); |
931 |
|
} |
932 |
|
added = d_cnfStream.assertClause(node, ~b, lit); |
933 |
|
if (added) |
934 |
|
{ |
935 |
|
Node clauseNode = nm->mkNode(kind::OR, node, node[1].notNode()); |
936 |
|
d_proof.addStep(clauseNode, PfRule::CNF_IMPLIES_NEG2, {}, {node}); |
937 |
|
Trace("cnf") << "ProofCnfStream::handleImplies: CNF_IMPLIES_NEG2 added " |
938 |
|
<< clauseNode << "\n"; |
939 |
|
normalizeAndRegister(clauseNode); |
940 |
|
} |
941 |
|
return lit; |
942 |
|
} |
943 |
|
|
944 |
|
SatLiteral ProofCnfStream::handleIte(TNode node) |
945 |
|
{ |
946 |
|
Assert(!d_cnfStream.hasLiteral(node)) << "Atom already mapped!"; |
947 |
|
Assert(node.getKind() == kind::ITE); |
948 |
|
Assert(node.getNumChildren() == 3); |
949 |
|
Assert(!d_cnfStream.d_removable) |
950 |
|
<< "Removable clauses can not contain Boolean structure"; |
951 |
|
Trace("cnf") << "handleIte(" << node[0] << " " << node[1] << " " << node[2] |
952 |
|
<< ")\n"; |
953 |
|
SatLiteral condLit = toCNF(node[0]); |
954 |
|
SatLiteral thenLit = toCNF(node[1]); |
955 |
|
SatLiteral elseLit = toCNF(node[2]); |
956 |
|
// create literal to the node |
957 |
|
SatLiteral lit = d_cnfStream.newLiteral(node); |
958 |
|
bool added; |
959 |
|
NodeManager* nm = NodeManager::currentNM(); |
960 |
|
// If ITE is true then one of the branches is true and the condition |
961 |
|
// implies which one |
962 |
|
// lit -> (ite b t e) |
963 |
|
// lit -> (t | e) & (b -> t) & (!b -> e) |
964 |
|
// lit -> (t | e) & (!b | t) & (b | e) |
965 |
|
// (!lit | t | e) & (!lit | !b | t) & (!lit | b | e) |
966 |
|
added = d_cnfStream.assertClause(node.negate(), ~lit, thenLit, elseLit); |
967 |
|
if (added) |
968 |
|
{ |
969 |
|
Node clauseNode = nm->mkNode(kind::OR, node.notNode(), node[1], node[2]); |
970 |
|
d_proof.addStep(clauseNode, PfRule::CNF_ITE_POS3, {}, {node}); |
971 |
|
Trace("cnf") << "ProofCnfStream::handleIte: CNF_ITE_POS3 added " |
972 |
|
<< clauseNode << "\n"; |
973 |
|
normalizeAndRegister(clauseNode); |
974 |
|
} |
975 |
|
added = d_cnfStream.assertClause(node.negate(), ~lit, ~condLit, thenLit); |
976 |
|
if (added) |
977 |
|
{ |
978 |
|
Node clauseNode = |
979 |
|
nm->mkNode(kind::OR, node.notNode(), node[0].notNode(), node[1]); |
980 |
|
d_proof.addStep(clauseNode, PfRule::CNF_ITE_POS1, {}, {node}); |
981 |
|
Trace("cnf") << "ProofCnfStream::handleIte: CNF_ITE_POS1 added " |
982 |
|
<< clauseNode << "\n"; |
983 |
|
normalizeAndRegister(clauseNode); |
984 |
|
} |
985 |
|
added = d_cnfStream.assertClause(node.negate(), ~lit, condLit, elseLit); |
986 |
|
if (added) |
987 |
|
{ |
988 |
|
Node clauseNode = nm->mkNode(kind::OR, node.notNode(), node[0], node[2]); |
989 |
|
d_proof.addStep(clauseNode, PfRule::CNF_ITE_POS2, {}, {node}); |
990 |
|
Trace("cnf") << "ProofCnfStream::handleIte: CNF_ITE_POS2 added " |
991 |
|
<< clauseNode << "\n"; |
992 |
|
normalizeAndRegister(clauseNode); |
993 |
|
} |
994 |
|
// If ITE is false then one of the branches is false and the condition |
995 |
|
// implies which one |
996 |
|
// !lit -> !(ite b t e) |
997 |
|
// !lit -> (!t | !e) & (b -> !t) & (!b -> !e) |
998 |
|
// !lit -> (!t | !e) & (!b | !t) & (b | !e) |
999 |
|
// (lit | !t | !e) & (lit | !b | !t) & (lit | b | !e) |
1000 |
|
added = d_cnfStream.assertClause(node, lit, ~thenLit, ~elseLit); |
1001 |
|
if (added) |
1002 |
|
{ |
1003 |
|
Node clauseNode = |
1004 |
|
nm->mkNode(kind::OR, node, node[1].notNode(), node[2].notNode()); |
1005 |
|
d_proof.addStep(clauseNode, PfRule::CNF_ITE_NEG3, {}, {node}); |
1006 |
|
Trace("cnf") << "ProofCnfStream::handleIte: CNF_ITE_NEG3 added " |
1007 |
|
<< clauseNode << "\n"; |
1008 |
|
normalizeAndRegister(clauseNode); |
1009 |
|
} |
1010 |
|
added = d_cnfStream.assertClause(node, lit, ~condLit, ~thenLit); |
1011 |
|
if (added) |
1012 |
|
{ |
1013 |
|
Node clauseNode = |
1014 |
|
nm->mkNode(kind::OR, node, node[0].notNode(), node[1].notNode()); |
1015 |
|
d_proof.addStep(clauseNode, PfRule::CNF_ITE_NEG1, {}, {node}); |
1016 |
|
Trace("cnf") << "ProofCnfStream::handleIte: CNF_ITE_NEG1 added " |
1017 |
|
<< clauseNode << "\n"; |
1018 |
|
normalizeAndRegister(clauseNode); |
1019 |
|
} |
1020 |
|
added = d_cnfStream.assertClause(node, lit, condLit, ~elseLit); |
1021 |
|
if (added) |
1022 |
|
{ |
1023 |
|
Node clauseNode = nm->mkNode(kind::OR, node, node[0], node[2].notNode()); |
1024 |
|
d_proof.addStep(clauseNode, PfRule::CNF_ITE_NEG2, {}, {node}); |
1025 |
|
Trace("cnf") << "ProofCnfStream::handleIte: CNF_ITE_NEG2 added " |
1026 |
|
<< clauseNode << "\n"; |
1027 |
|
normalizeAndRegister(clauseNode); |
1028 |
|
} |
1029 |
|
return lit; |
1030 |
|
} |
1031 |
|
|
1032 |
|
} // namespace prop |
1033 |
22746 |
} // namespace cvc5 |