1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Dejan Jovanovic, Haniel Barbosa, Liana Hadarean |
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 |
|
* A CNF converter that takes in asserts and has the side effect of given an |
14 |
|
* equisatisfiable stream of assertions to PropEngine. |
15 |
|
*/ |
16 |
|
#include "prop/cnf_stream.h" |
17 |
|
|
18 |
|
#include <queue> |
19 |
|
|
20 |
|
#include "base/check.h" |
21 |
|
#include "base/output.h" |
22 |
|
#include "expr/node.h" |
23 |
|
#include "options/bv_options.h" |
24 |
|
#include "proof/clause_id.h" |
25 |
|
#include "prop/minisat/minisat.h" |
26 |
|
#include "prop/prop_engine.h" |
27 |
|
#include "prop/theory_proxy.h" |
28 |
|
#include "smt/dump.h" |
29 |
|
#include "smt/smt_engine.h" |
30 |
|
#include "printer/printer.h" |
31 |
|
#include "smt/smt_engine_scope.h" |
32 |
|
#include "theory/theory.h" |
33 |
|
#include "theory/theory_engine.h" |
34 |
|
|
35 |
|
namespace cvc5 { |
36 |
|
namespace prop { |
37 |
|
|
38 |
18952 |
CnfStream::CnfStream(SatSolver* satSolver, |
39 |
|
Registrar* registrar, |
40 |
|
context::Context* context, |
41 |
|
OutputManager* outMgr, |
42 |
|
ResourceManager* rm, |
43 |
|
FormulaLitPolicy flpol, |
44 |
18952 |
std::string name) |
45 |
|
: d_satSolver(satSolver), |
46 |
|
d_outMgr(outMgr), |
47 |
|
d_booleanVariables(context), |
48 |
|
d_notifyFormulas(context), |
49 |
|
d_nodeToLiteralMap(context), |
50 |
|
d_literalToNodeMap(context), |
51 |
|
d_flitPolicy(flpol), |
52 |
|
d_registrar(registrar), |
53 |
|
d_name(name), |
54 |
|
d_removable(false), |
55 |
18952 |
d_resourceManager(rm) |
56 |
|
{ |
57 |
18952 |
} |
58 |
|
|
59 |
10452594 |
bool CnfStream::assertClause(TNode node, SatClause& c) |
60 |
|
{ |
61 |
10452594 |
Trace("cnf") << "Inserting into stream " << c << " node = " << node << "\n"; |
62 |
10452594 |
if (Dump.isOn("clauses") && d_outMgr != nullptr) |
63 |
|
{ |
64 |
|
const Printer& printer = d_outMgr->getPrinter(); |
65 |
|
std::ostream& out = d_outMgr->getDumpOut(); |
66 |
|
if (c.size() == 1) |
67 |
|
{ |
68 |
|
printer.toStreamCmdAssert(out, getNode(c[0])); |
69 |
|
} |
70 |
|
else |
71 |
|
{ |
72 |
|
Assert(c.size() > 1); |
73 |
|
NodeBuilder b(kind::OR); |
74 |
|
for (unsigned i = 0; i < c.size(); ++i) |
75 |
|
{ |
76 |
|
b << getNode(c[i]); |
77 |
|
} |
78 |
|
Node n = b; |
79 |
|
printer.toStreamCmdAssert(out, n); |
80 |
|
} |
81 |
|
} |
82 |
|
|
83 |
10452594 |
ClauseId clauseId = d_satSolver->addClause(c, d_removable); |
84 |
|
|
85 |
10452594 |
return clauseId != ClauseIdUndef; |
86 |
|
} |
87 |
|
|
88 |
201361 |
bool CnfStream::assertClause(TNode node, SatLiteral a) |
89 |
|
{ |
90 |
402722 |
SatClause clause(1); |
91 |
201361 |
clause[0] = a; |
92 |
402722 |
return assertClause(node, clause); |
93 |
|
} |
94 |
|
|
95 |
4660987 |
bool CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b) |
96 |
|
{ |
97 |
9321974 |
SatClause clause(2); |
98 |
4660987 |
clause[0] = a; |
99 |
4660987 |
clause[1] = b; |
100 |
9321974 |
return assertClause(node, clause); |
101 |
|
} |
102 |
|
|
103 |
3381735 |
bool CnfStream::assertClause(TNode node, |
104 |
|
SatLiteral a, |
105 |
|
SatLiteral b, |
106 |
|
SatLiteral c) |
107 |
|
{ |
108 |
6763470 |
SatClause clause(3); |
109 |
3381735 |
clause[0] = a; |
110 |
3381735 |
clause[1] = b; |
111 |
3381735 |
clause[2] = c; |
112 |
6763470 |
return assertClause(node, clause); |
113 |
|
} |
114 |
|
|
115 |
87324527 |
bool CnfStream::hasLiteral(TNode n) const { |
116 |
87324527 |
NodeToLiteralMap::const_iterator find = d_nodeToLiteralMap.find(n); |
117 |
87324527 |
return find != d_nodeToLiteralMap.end(); |
118 |
|
} |
119 |
|
|
120 |
151727 |
void CnfStream::ensureMappingForLiteral(TNode n) |
121 |
|
{ |
122 |
151727 |
SatLiteral lit = getLiteral(n); |
123 |
151727 |
if (!d_literalToNodeMap.contains(lit)) |
124 |
|
{ |
125 |
|
// Store backward-mappings |
126 |
|
d_literalToNodeMap.insert(lit, n); |
127 |
|
d_literalToNodeMap.insert(~lit, n.notNode()); |
128 |
|
} |
129 |
151727 |
} |
130 |
|
|
131 |
242420 |
void CnfStream::ensureLiteral(TNode n) |
132 |
|
{ |
133 |
242420 |
AlwaysAssertArgument( |
134 |
|
hasLiteral(n) || n.getType().isBoolean(), |
135 |
|
n, |
136 |
|
"ProofCnfStream::ensureLiteral() requires a node of Boolean type.\n" |
137 |
|
"got node: %s\n" |
138 |
|
"its type: %s\n", |
139 |
|
n.toString().c_str(), |
140 |
|
n.getType().toString().c_str()); |
141 |
242420 |
Trace("cnf") << "ensureLiteral(" << n << ")\n"; |
142 |
242420 |
if (hasLiteral(n)) |
143 |
|
{ |
144 |
133580 |
ensureMappingForLiteral(n); |
145 |
133580 |
return; |
146 |
|
} |
147 |
|
// remove top level negation |
148 |
108840 |
n = n.getKind() == kind::NOT ? n[0] : n; |
149 |
108840 |
if (theory::Theory::theoryOf(n) == theory::THEORY_BOOL && !n.isVar()) |
150 |
|
{ |
151 |
|
// If we were called with something other than a theory atom (or |
152 |
|
// Boolean variable), we get a SatLiteral that is definitionally |
153 |
|
// equal to it. |
154 |
|
// These are not removable and have no proof ID |
155 |
17036 |
d_removable = false; |
156 |
|
|
157 |
17036 |
SatLiteral lit = toCNF(n, false); |
158 |
|
|
159 |
|
// Store backward-mappings |
160 |
|
// These may already exist |
161 |
17036 |
d_literalToNodeMap.insert_safe(lit, n); |
162 |
17036 |
d_literalToNodeMap.insert_safe(~lit, n.notNode()); |
163 |
|
} |
164 |
|
else |
165 |
|
{ |
166 |
|
// We have a theory atom or variable. |
167 |
91804 |
convertAtom(n); |
168 |
|
} |
169 |
|
} |
170 |
|
|
171 |
3013327 |
SatLiteral CnfStream::newLiteral(TNode node, bool isTheoryAtom, bool preRegister, bool canEliminate) { |
172 |
6026654 |
Trace("cnf") << d_name << "::newLiteral(" << node << ", " << isTheoryAtom |
173 |
3013327 |
<< ")\n" |
174 |
3013327 |
<< push; |
175 |
3013327 |
Assert(node.getKind() != kind::NOT); |
176 |
|
|
177 |
|
// if we are tracking formulas, everything is a theory atom |
178 |
3013327 |
if (!isTheoryAtom && d_flitPolicy == FormulaLitPolicy::TRACK_AND_NOTIFY) |
179 |
|
{ |
180 |
|
isTheoryAtom = true; |
181 |
|
d_notifyFormulas.insert(node); |
182 |
|
} |
183 |
|
|
184 |
|
// Get the literal for this node |
185 |
3013327 |
SatLiteral lit; |
186 |
3013327 |
if (!hasLiteral(node)) { |
187 |
3013318 |
Trace("cnf") << d_name << "::newLiteral: node already registered\n"; |
188 |
|
// If no literal, we'll make one |
189 |
3013318 |
if (node.getKind() == kind::CONST_BOOLEAN) { |
190 |
19338 |
Trace("cnf") << d_name << "::newLiteral: boolean const\n"; |
191 |
19338 |
if (node.getConst<bool>()) { |
192 |
9619 |
lit = SatLiteral(d_satSolver->trueVar()); |
193 |
|
} else { |
194 |
9719 |
lit = SatLiteral(d_satSolver->falseVar()); |
195 |
|
} |
196 |
|
} else { |
197 |
2993980 |
Trace("cnf") << d_name << "::newLiteral: new var\n"; |
198 |
2993980 |
lit = SatLiteral(d_satSolver->newVar(isTheoryAtom, preRegister, canEliminate)); |
199 |
|
} |
200 |
3013318 |
d_nodeToLiteralMap.insert(node, lit); |
201 |
3013318 |
d_nodeToLiteralMap.insert(node.notNode(), ~lit); |
202 |
|
} else { |
203 |
9 |
lit = getLiteral(node); |
204 |
|
} |
205 |
|
|
206 |
|
// If it's a theory literal, need to store it for back queries |
207 |
5206620 |
if (isTheoryAtom || d_flitPolicy == FormulaLitPolicy::TRACK |
208 |
4837108 |
|| (Dump.isOn("clauses"))) |
209 |
|
{ |
210 |
1189546 |
d_literalToNodeMap.insert_safe(lit, node); |
211 |
1189546 |
d_literalToNodeMap.insert_safe(~lit, node.notNode()); |
212 |
|
} |
213 |
|
|
214 |
|
// If a theory literal, we pre-register it |
215 |
3013327 |
if (preRegister) { |
216 |
|
// In case we are re-entered due to lemmas, save our state |
217 |
820034 |
bool backupRemovable = d_removable; |
218 |
820038 |
d_registrar->preRegister(node); |
219 |
820030 |
d_removable = backupRemovable; |
220 |
|
} |
221 |
|
// Here, you can have it |
222 |
3013323 |
Trace("cnf") << "newLiteral(" << node << ") => " << lit << "\n" << pop; |
223 |
3013323 |
return lit; |
224 |
|
} |
225 |
|
|
226 |
16081903 |
TNode CnfStream::getNode(const SatLiteral& literal) { |
227 |
16081903 |
Trace("cnf") << "getNode(" << literal << ")\n"; |
228 |
32163806 |
Trace("cnf") << "getNode(" << literal << ") => " |
229 |
16081903 |
<< d_literalToNodeMap[literal] << "\n"; |
230 |
16081903 |
return d_literalToNodeMap[literal]; |
231 |
|
} |
232 |
|
|
233 |
4989059 |
const CnfStream::NodeToLiteralMap& CnfStream::getTranslationCache() const |
234 |
|
{ |
235 |
4989059 |
return d_nodeToLiteralMap; |
236 |
|
} |
237 |
|
|
238 |
14284592 |
const CnfStream::LiteralToNodeMap& CnfStream::getNodeCache() const |
239 |
|
{ |
240 |
14284592 |
return d_literalToNodeMap; |
241 |
|
} |
242 |
|
|
243 |
15247 |
void CnfStream::getBooleanVariables(std::vector<TNode>& outputVariables) const { |
244 |
15247 |
context::CDList<TNode>::const_iterator it, it_end; |
245 |
73495 |
for (it = d_booleanVariables.begin(); it != d_booleanVariables.end(); ++ it) { |
246 |
58248 |
outputVariables.push_back(*it); |
247 |
|
} |
248 |
15247 |
} |
249 |
|
|
250 |
|
bool CnfStream::isNotifyFormula(TNode node) const |
251 |
|
{ |
252 |
|
return d_notifyFormulas.find(node) != d_notifyFormulas.end(); |
253 |
|
} |
254 |
|
|
255 |
903387 |
SatLiteral CnfStream::convertAtom(TNode node) |
256 |
|
{ |
257 |
903387 |
Trace("cnf") << "convertAtom(" << node << ")\n"; |
258 |
|
|
259 |
903387 |
Assert(!hasLiteral(node)) << "atom already mapped!"; |
260 |
|
|
261 |
903387 |
bool theoryLiteral = false; |
262 |
903387 |
bool canEliminate = true; |
263 |
903387 |
bool preRegister = false; |
264 |
|
|
265 |
|
// Is this a variable add it to the list |
266 |
903387 |
if (node.isVar() && node.getKind() != kind::BOOLEAN_TERM_VARIABLE) |
267 |
|
{ |
268 |
83353 |
d_booleanVariables.push_back(node); |
269 |
|
} |
270 |
|
else |
271 |
|
{ |
272 |
820034 |
theoryLiteral = true; |
273 |
820034 |
canEliminate = false; |
274 |
820034 |
preRegister = true; |
275 |
|
} |
276 |
|
|
277 |
|
// Make a new literal (variables are not considered theory literals) |
278 |
903391 |
SatLiteral lit = newLiteral(node, theoryLiteral, preRegister, canEliminate); |
279 |
|
// Return the resulting literal |
280 |
903383 |
return lit; |
281 |
|
} |
282 |
|
|
283 |
64467490 |
SatLiteral CnfStream::getLiteral(TNode node) { |
284 |
64467490 |
Assert(!node.isNull()) << "CnfStream: can't getLiteral() of null node"; |
285 |
|
|
286 |
128934980 |
Assert(d_nodeToLiteralMap.contains(node)) |
287 |
64467490 |
<< "Literal not in the CNF Cache: " << node << "\n"; |
288 |
|
|
289 |
64467490 |
SatLiteral literal = d_nodeToLiteralMap[node]; |
290 |
128934980 |
Trace("cnf") << "CnfStream::getLiteral(" << node << ") => " << literal |
291 |
64467490 |
<< "\n"; |
292 |
64467490 |
return literal; |
293 |
|
} |
294 |
|
|
295 |
324635 |
SatLiteral CnfStream::handleXor(TNode xorNode) |
296 |
|
{ |
297 |
324635 |
Assert(!hasLiteral(xorNode)) << "Atom already mapped!"; |
298 |
324635 |
Assert(xorNode.getKind() == kind::XOR) << "Expecting an XOR expression!"; |
299 |
324635 |
Assert(xorNode.getNumChildren() == 2) << "Expecting exactly 2 children!"; |
300 |
324635 |
Assert(!d_removable) << "Removable clauses can not contain Boolean structure"; |
301 |
324635 |
Trace("cnf") << "CnfStream::handleXor(" << xorNode << ")\n"; |
302 |
|
|
303 |
324635 |
SatLiteral a = toCNF(xorNode[0]); |
304 |
324635 |
SatLiteral b = toCNF(xorNode[1]); |
305 |
|
|
306 |
324635 |
SatLiteral xorLit = newLiteral(xorNode); |
307 |
|
|
308 |
324635 |
assertClause(xorNode.negate(), a, b, ~xorLit); |
309 |
324635 |
assertClause(xorNode.negate(), ~a, ~b, ~xorLit); |
310 |
324635 |
assertClause(xorNode, a, ~b, xorLit); |
311 |
324635 |
assertClause(xorNode, ~a, b, xorLit); |
312 |
|
|
313 |
324635 |
return xorLit; |
314 |
|
} |
315 |
|
|
316 |
450046 |
SatLiteral CnfStream::handleOr(TNode orNode) |
317 |
|
{ |
318 |
450046 |
Assert(!hasLiteral(orNode)) << "Atom already mapped!"; |
319 |
450046 |
Assert(orNode.getKind() == kind::OR) << "Expecting an OR expression!"; |
320 |
450046 |
Assert(orNode.getNumChildren() > 1) << "Expecting more then 1 child!"; |
321 |
450046 |
Assert(!d_removable) << "Removable clauses can not contain Boolean structure"; |
322 |
450046 |
Trace("cnf") << "CnfStream::handleOr(" << orNode << ")\n"; |
323 |
|
|
324 |
|
// Number of children |
325 |
450046 |
unsigned n_children = orNode.getNumChildren(); |
326 |
|
|
327 |
|
// Transform all the children first |
328 |
450046 |
TNode::const_iterator node_it = orNode.begin(); |
329 |
450046 |
TNode::const_iterator node_it_end = orNode.end(); |
330 |
900092 |
SatClause clause(n_children + 1); |
331 |
1529199 |
for(int i = 0; node_it != node_it_end; ++node_it, ++i) { |
332 |
1079153 |
clause[i] = toCNF(*node_it); |
333 |
|
} |
334 |
|
|
335 |
|
// Get the literal for this node |
336 |
450046 |
SatLiteral orLit = newLiteral(orNode); |
337 |
|
|
338 |
|
// lit <- (a_1 | a_2 | a_3 | ... | a_n) |
339 |
|
// lit | ~(a_1 | a_2 | a_3 | ... | a_n) |
340 |
|
// (lit | ~a_1) & (lit | ~a_2) & (lit & ~a_3) & ... & (lit & ~a_n) |
341 |
1529199 |
for(unsigned i = 0; i < n_children; ++i) { |
342 |
1079153 |
assertClause(orNode, orLit, ~clause[i]); |
343 |
|
} |
344 |
|
|
345 |
|
// lit -> (a_1 | a_2 | a_3 | ... | a_n) |
346 |
|
// ~lit | a_1 | a_2 | a_3 | ... | a_n |
347 |
450046 |
clause[n_children] = ~orLit; |
348 |
|
// This needs to go last, as the clause might get modified by the SAT solver |
349 |
450046 |
assertClause(orNode.negate(), clause); |
350 |
|
|
351 |
|
// Return the literal |
352 |
900092 |
return orLit; |
353 |
|
} |
354 |
|
|
355 |
815618 |
SatLiteral CnfStream::handleAnd(TNode andNode) |
356 |
|
{ |
357 |
815618 |
Assert(!hasLiteral(andNode)) << "Atom already mapped!"; |
358 |
815618 |
Assert(andNode.getKind() == kind::AND) << "Expecting an AND expression!"; |
359 |
815618 |
Assert(andNode.getNumChildren() > 1) << "Expecting more than 1 child!"; |
360 |
815618 |
Assert(!d_removable) << "Removable clauses can not contain Boolean structure"; |
361 |
815618 |
Trace("cnf") << "handleAnd(" << andNode << ")\n"; |
362 |
|
|
363 |
|
// Number of children |
364 |
815618 |
unsigned n_children = andNode.getNumChildren(); |
365 |
|
|
366 |
|
// Transform all the children first (remembering the negation) |
367 |
815618 |
TNode::const_iterator node_it = andNode.begin(); |
368 |
815618 |
TNode::const_iterator node_it_end = andNode.end(); |
369 |
1631236 |
SatClause clause(n_children + 1); |
370 |
4177460 |
for(int i = 0; node_it != node_it_end; ++node_it, ++i) { |
371 |
3361842 |
clause[i] = ~toCNF(*node_it); |
372 |
|
} |
373 |
|
|
374 |
|
// Get the literal for this node |
375 |
815618 |
SatLiteral andLit = newLiteral(andNode); |
376 |
|
|
377 |
|
// lit -> (a_1 & a_2 & a_3 & ... & a_n) |
378 |
|
// ~lit | (a_1 & a_2 & a_3 & ... & a_n) |
379 |
|
// (~lit | a_1) & (~lit | a_2) & ... & (~lit | a_n) |
380 |
4177460 |
for(unsigned i = 0; i < n_children; ++i) { |
381 |
3361842 |
assertClause(andNode.negate(), ~andLit, ~clause[i]); |
382 |
|
} |
383 |
|
|
384 |
|
// lit <- (a_1 & a_2 & a_3 & ... a_n) |
385 |
|
// lit | ~(a_1 & a_2 & a_3 & ... & a_n) |
386 |
|
// lit | ~a_1 | ~a_2 | ~a_3 | ... | ~a_n |
387 |
815618 |
clause[n_children] = andLit; |
388 |
|
// This needs to go last, as the clause might get modified by the SAT solver |
389 |
815618 |
assertClause(andNode, clause); |
390 |
|
|
391 |
1631236 |
return andLit; |
392 |
|
} |
393 |
|
|
394 |
8412 |
SatLiteral CnfStream::handleImplies(TNode impliesNode) |
395 |
|
{ |
396 |
8412 |
Assert(!hasLiteral(impliesNode)) << "Atom already mapped!"; |
397 |
8412 |
Assert(impliesNode.getKind() == kind::IMPLIES) |
398 |
|
<< "Expecting an IMPLIES expression!"; |
399 |
8412 |
Assert(impliesNode.getNumChildren() == 2) << "Expecting exactly 2 children!"; |
400 |
8412 |
Assert(!d_removable) << "Removable clauses can not contain Boolean structure"; |
401 |
8412 |
Trace("cnf") << "handleImplies(" << impliesNode << ")\n"; |
402 |
|
|
403 |
|
// Convert the children to cnf |
404 |
8412 |
SatLiteral a = toCNF(impliesNode[0]); |
405 |
8412 |
SatLiteral b = toCNF(impliesNode[1]); |
406 |
|
|
407 |
8412 |
SatLiteral impliesLit = newLiteral(impliesNode); |
408 |
|
|
409 |
|
// lit -> (a->b) |
410 |
|
// ~lit | ~ a | b |
411 |
8412 |
assertClause(impliesNode.negate(), ~impliesLit, ~a, b); |
412 |
|
|
413 |
|
// (a->b) -> lit |
414 |
|
// ~(~a | b) | lit |
415 |
|
// (a | l) & (~b | l) |
416 |
8412 |
assertClause(impliesNode, a, impliesLit); |
417 |
8412 |
assertClause(impliesNode, ~b, impliesLit); |
418 |
|
|
419 |
8412 |
return impliesLit; |
420 |
|
} |
421 |
|
|
422 |
380925 |
SatLiteral CnfStream::handleIff(TNode iffNode) |
423 |
|
{ |
424 |
380925 |
Assert(!hasLiteral(iffNode)) << "Atom already mapped!"; |
425 |
380925 |
Assert(iffNode.getKind() == kind::EQUAL) << "Expecting an EQUAL expression!"; |
426 |
380925 |
Assert(iffNode.getNumChildren() == 2) << "Expecting exactly 2 children!"; |
427 |
380925 |
Assert(!d_removable) << "Removable clauses can not contain Boolean structure"; |
428 |
380925 |
Trace("cnf") << "handleIff(" << iffNode << ")\n"; |
429 |
|
|
430 |
|
// Convert the children to CNF |
431 |
380925 |
SatLiteral a = toCNF(iffNode[0]); |
432 |
380925 |
SatLiteral b = toCNF(iffNode[1]); |
433 |
|
|
434 |
|
// Get the now literal |
435 |
380925 |
SatLiteral iffLit = newLiteral(iffNode); |
436 |
|
|
437 |
|
// lit -> ((a-> b) & (b->a)) |
438 |
|
// ~lit | ((~a | b) & (~b | a)) |
439 |
|
// (~a | b | ~lit) & (~b | a | ~lit) |
440 |
380925 |
assertClause(iffNode.negate(), ~a, b, ~iffLit); |
441 |
380925 |
assertClause(iffNode.negate(), a, ~b, ~iffLit); |
442 |
|
|
443 |
|
// (a<->b) -> lit |
444 |
|
// ~((a & b) | (~a & ~b)) | lit |
445 |
|
// (~(a & b)) & (~(~a & ~b)) | lit |
446 |
|
// ((~a | ~b) & (a | b)) | lit |
447 |
|
// (~a | ~b | lit) & (a | b | lit) |
448 |
380925 |
assertClause(iffNode, ~a, ~b, iffLit); |
449 |
380925 |
assertClause(iffNode, a, b, iffLit); |
450 |
|
|
451 |
380925 |
return iffLit; |
452 |
|
} |
453 |
|
|
454 |
86350 |
SatLiteral CnfStream::handleIte(TNode iteNode) |
455 |
|
{ |
456 |
86350 |
Assert(!hasLiteral(iteNode)) << "Atom already mapped!"; |
457 |
86350 |
Assert(iteNode.getKind() == kind::ITE); |
458 |
86350 |
Assert(iteNode.getNumChildren() == 3); |
459 |
86350 |
Assert(!d_removable) << "Removable clauses can not contain Boolean structure"; |
460 |
172700 |
Trace("cnf") << "handleIte(" << iteNode[0] << " " << iteNode[1] << " " |
461 |
86350 |
<< iteNode[2] << ")\n"; |
462 |
|
|
463 |
86350 |
SatLiteral condLit = toCNF(iteNode[0]); |
464 |
86350 |
SatLiteral thenLit = toCNF(iteNode[1]); |
465 |
86350 |
SatLiteral elseLit = toCNF(iteNode[2]); |
466 |
|
|
467 |
86350 |
SatLiteral iteLit = newLiteral(iteNode); |
468 |
|
|
469 |
|
// If ITE is true then one of the branches is true and the condition |
470 |
|
// implies which one |
471 |
|
// lit -> (ite b t e) |
472 |
|
// lit -> (t | e) & (b -> t) & (!b -> e) |
473 |
|
// lit -> (t | e) & (!b | t) & (b | e) |
474 |
|
// (!lit | t | e) & (!lit | !b | t) & (!lit | b | e) |
475 |
86350 |
assertClause(iteNode.negate(), ~iteLit, thenLit, elseLit); |
476 |
86350 |
assertClause(iteNode.negate(), ~iteLit, ~condLit, thenLit); |
477 |
86350 |
assertClause(iteNode.negate(), ~iteLit, condLit, elseLit); |
478 |
|
|
479 |
|
// If ITE is false then one of the branches is false and the condition |
480 |
|
// implies which one |
481 |
|
// !lit -> !(ite b t e) |
482 |
|
// !lit -> (!t | !e) & (b -> !t) & (!b -> !e) |
483 |
|
// !lit -> (!t | !e) & (!b | !t) & (b | !e) |
484 |
|
// (lit | !t | !e) & (lit | !b | !t) & (lit | b | !e) |
485 |
86350 |
assertClause(iteNode, iteLit, ~thenLit, ~elseLit); |
486 |
86350 |
assertClause(iteNode, iteLit, ~condLit, ~thenLit); |
487 |
86350 |
assertClause(iteNode, iteLit, condLit, ~elseLit); |
488 |
|
|
489 |
86350 |
return iteLit; |
490 |
|
} |
491 |
|
|
492 |
9483271 |
SatLiteral CnfStream::toCNF(TNode node, bool negated) |
493 |
|
{ |
494 |
18966542 |
Trace("cnf") << "toCNF(" << node |
495 |
9483271 |
<< ", negated = " << (negated ? "true" : "false") << ")\n"; |
496 |
9483271 |
SatLiteral nodeLit; |
497 |
18966542 |
Node negatedNode = node.notNode(); |
498 |
|
|
499 |
|
// If the non-negated node has already been translated, get the translation |
500 |
9483271 |
if(hasLiteral(node)) { |
501 |
6496816 |
Trace("cnf") << "toCNF(): already translated\n"; |
502 |
6496816 |
nodeLit = getLiteral(node); |
503 |
|
// Return the (maybe negated) literal |
504 |
6496816 |
return !negated ? nodeLit : ~nodeLit; |
505 |
|
} |
506 |
|
// Handle each Boolean operator case |
507 |
2986455 |
switch (node.getKind()) |
508 |
|
{ |
509 |
201431 |
case kind::NOT: nodeLit = ~toCNF(node[0]); break; |
510 |
324635 |
case kind::XOR: nodeLit = handleXor(node); break; |
511 |
86350 |
case kind::ITE: nodeLit = handleIte(node); break; |
512 |
8412 |
case kind::IMPLIES: nodeLit = handleImplies(node); break; |
513 |
450046 |
case kind::OR: nodeLit = handleOr(node); break; |
514 |
815618 |
case kind::AND: nodeLit = handleAnd(node); break; |
515 |
611188 |
case kind::EQUAL: |
516 |
1222376 |
nodeLit = |
517 |
1833564 |
node[0].getType().isBoolean() ? handleIff(node) : convertAtom(node); |
518 |
611188 |
break; |
519 |
488775 |
default: |
520 |
|
{ |
521 |
488779 |
nodeLit = convertAtom(node); |
522 |
|
} |
523 |
488771 |
break; |
524 |
|
} |
525 |
|
// Return the (maybe negated) literal |
526 |
5972902 |
Trace("cnf") << "toCNF(): resulting literal: " |
527 |
2986451 |
<< (!negated ? nodeLit : ~nodeLit) << "\n"; |
528 |
2986451 |
return !negated ? nodeLit : ~nodeLit; |
529 |
|
} |
530 |
|
|
531 |
112629 |
void CnfStream::convertAndAssertAnd(TNode node, bool negated) |
532 |
|
{ |
533 |
112629 |
Assert(node.getKind() == kind::AND); |
534 |
225258 |
Trace("cnf") << "CnfStream::convertAndAssertAnd(" << node |
535 |
112629 |
<< ", negated = " << (negated ? "true" : "false") << ")\n"; |
536 |
112629 |
if (!negated) { |
537 |
|
// If the node is a conjunction, we handle each conjunct separately |
538 |
364447 |
for(TNode::const_iterator conjunct = node.begin(), node_end = node.end(); |
539 |
364447 |
conjunct != node_end; ++conjunct ) { |
540 |
351356 |
convertAndAssert(*conjunct, false); |
541 |
|
} |
542 |
|
} else { |
543 |
|
// If the node is a disjunction, we construct a clause and assert it |
544 |
99536 |
int nChildren = node.getNumChildren(); |
545 |
199072 |
SatClause clause(nChildren); |
546 |
99536 |
TNode::const_iterator disjunct = node.begin(); |
547 |
1410397 |
for(int i = 0; i < nChildren; ++ disjunct, ++ i) { |
548 |
1310861 |
Assert(disjunct != node.end()); |
549 |
1310861 |
clause[i] = toCNF(*disjunct, true); |
550 |
|
} |
551 |
99536 |
Assert(disjunct == node.end()); |
552 |
99536 |
assertClause(node.negate(), clause); |
553 |
|
} |
554 |
112628 |
} |
555 |
|
|
556 |
445846 |
void CnfStream::convertAndAssertOr(TNode node, bool negated) |
557 |
|
{ |
558 |
445846 |
Assert(node.getKind() == kind::OR); |
559 |
891692 |
Trace("cnf") << "CnfStream::convertAndAssertOr(" << node |
560 |
445846 |
<< ", negated = " << (negated ? "true" : "false") << ")\n"; |
561 |
445846 |
if (!negated) { |
562 |
|
// If the node is a disjunction, we construct a clause and assert it |
563 |
445545 |
int nChildren = node.getNumChildren(); |
564 |
891090 |
SatClause clause(nChildren); |
565 |
445545 |
TNode::const_iterator disjunct = node.begin(); |
566 |
1776795 |
for(int i = 0; i < nChildren; ++ disjunct, ++ i) { |
567 |
1331250 |
Assert(disjunct != node.end()); |
568 |
1331250 |
clause[i] = toCNF(*disjunct, false); |
569 |
|
} |
570 |
445545 |
Assert(disjunct == node.end()); |
571 |
445545 |
assertClause(node, clause); |
572 |
|
} else { |
573 |
|
// If the node is a conjunction, we handle each conjunct separately |
574 |
1933 |
for(TNode::const_iterator conjunct = node.begin(), node_end = node.end(); |
575 |
1933 |
conjunct != node_end; ++conjunct ) { |
576 |
1632 |
convertAndAssert(*conjunct, true); |
577 |
|
} |
578 |
|
} |
579 |
445846 |
} |
580 |
|
|
581 |
53 |
void CnfStream::convertAndAssertXor(TNode node, bool negated) |
582 |
|
{ |
583 |
53 |
Assert(node.getKind() == kind::XOR); |
584 |
106 |
Trace("cnf") << "CnfStream::convertAndAssertXor(" << node |
585 |
53 |
<< ", negated = " << (negated ? "true" : "false") << ")\n"; |
586 |
53 |
if (!negated) { |
587 |
|
// p XOR q |
588 |
53 |
SatLiteral p = toCNF(node[0], false); |
589 |
53 |
SatLiteral q = toCNF(node[1], false); |
590 |
|
// Construct the clauses (p => !q) and (!q => p) |
591 |
106 |
SatClause clause1(2); |
592 |
53 |
clause1[0] = ~p; |
593 |
53 |
clause1[1] = ~q; |
594 |
53 |
assertClause(node, clause1); |
595 |
106 |
SatClause clause2(2); |
596 |
53 |
clause2[0] = p; |
597 |
53 |
clause2[1] = q; |
598 |
53 |
assertClause(node, clause2); |
599 |
|
} else { |
600 |
|
// !(p XOR q) is the same as p <=> q |
601 |
|
SatLiteral p = toCNF(node[0], false); |
602 |
|
SatLiteral q = toCNF(node[1], false); |
603 |
|
// Construct the clauses (p => q) and (q => p) |
604 |
|
SatClause clause1(2); |
605 |
|
clause1[0] = ~p; |
606 |
|
clause1[1] = q; |
607 |
|
assertClause(node.negate(), clause1); |
608 |
|
SatClause clause2(2); |
609 |
|
clause2[0] = p; |
610 |
|
clause2[1] = ~q; |
611 |
|
assertClause(node.negate(), clause2); |
612 |
|
} |
613 |
53 |
} |
614 |
|
|
615 |
81327 |
void CnfStream::convertAndAssertIff(TNode node, bool negated) |
616 |
|
{ |
617 |
81327 |
Assert(node.getKind() == kind::EQUAL); |
618 |
162654 |
Trace("cnf") << "CnfStream::convertAndAssertIff(" << node |
619 |
81327 |
<< ", negated = " << (negated ? "true" : "false") << ")\n"; |
620 |
81327 |
if (!negated) { |
621 |
|
// p <=> q |
622 |
80794 |
SatLiteral p = toCNF(node[0], false); |
623 |
80794 |
SatLiteral q = toCNF(node[1], false); |
624 |
|
// Construct the clauses (p => q) and (q => p) |
625 |
161588 |
SatClause clause1(2); |
626 |
80794 |
clause1[0] = ~p; |
627 |
80794 |
clause1[1] = q; |
628 |
80794 |
assertClause(node, clause1); |
629 |
161588 |
SatClause clause2(2); |
630 |
80794 |
clause2[0] = p; |
631 |
80794 |
clause2[1] = ~q; |
632 |
80794 |
assertClause(node, clause2); |
633 |
|
} else { |
634 |
|
// !(p <=> q) is the same as p XOR q |
635 |
533 |
SatLiteral p = toCNF(node[0], false); |
636 |
533 |
SatLiteral q = toCNF(node[1], false); |
637 |
|
// Construct the clauses (p => !q) and (!q => p) |
638 |
1066 |
SatClause clause1(2); |
639 |
533 |
clause1[0] = ~p; |
640 |
533 |
clause1[1] = ~q; |
641 |
533 |
assertClause(node.negate(), clause1); |
642 |
1066 |
SatClause clause2(2); |
643 |
533 |
clause2[0] = p; |
644 |
533 |
clause2[1] = q; |
645 |
533 |
assertClause(node.negate(), clause2); |
646 |
|
} |
647 |
81327 |
} |
648 |
|
|
649 |
60603 |
void CnfStream::convertAndAssertImplies(TNode node, bool negated) |
650 |
|
{ |
651 |
60603 |
Assert(node.getKind() == kind::IMPLIES); |
652 |
121206 |
Trace("cnf") << "CnfStream::convertAndAssertImplies(" << node |
653 |
60603 |
<< ", negated = " << (negated ? "true" : "false") << ")\n"; |
654 |
60603 |
if (!negated) { |
655 |
|
// p => q |
656 |
60366 |
SatLiteral p = toCNF(node[0], false); |
657 |
60366 |
SatLiteral q = toCNF(node[1], false); |
658 |
|
// Construct the clause ~p || q |
659 |
120732 |
SatClause clause(2); |
660 |
60366 |
clause[0] = ~p; |
661 |
60366 |
clause[1] = q; |
662 |
60366 |
assertClause(node, clause); |
663 |
|
} else {// Construct the |
664 |
|
// !(p => q) is the same as (p && ~q) |
665 |
237 |
convertAndAssert(node[0], false); |
666 |
237 |
convertAndAssert(node[1], true); |
667 |
|
} |
668 |
60603 |
} |
669 |
|
|
670 |
18991 |
void CnfStream::convertAndAssertIte(TNode node, bool negated) |
671 |
|
{ |
672 |
18991 |
Assert(node.getKind() == kind::ITE); |
673 |
37982 |
Trace("cnf") << "CnfStream::convertAndAssertIte(" << node |
674 |
18991 |
<< ", negated = " << (negated ? "true" : "false") << ")\n"; |
675 |
|
// ITE(p, q, r) |
676 |
18991 |
SatLiteral p = toCNF(node[0], false); |
677 |
18991 |
SatLiteral q = toCNF(node[1], negated); |
678 |
18991 |
SatLiteral r = toCNF(node[2], negated); |
679 |
|
// Construct the clauses: |
680 |
|
// (p => q) and (!p => r) |
681 |
|
// |
682 |
|
// Note that below q and r can be used directly because whether they are |
683 |
|
// negated has been push to the literal definitions above |
684 |
37982 |
Node nnode = node; |
685 |
18991 |
if( negated ){ |
686 |
69 |
nnode = node.negate(); |
687 |
|
} |
688 |
37982 |
SatClause clause1(2); |
689 |
18991 |
clause1[0] = ~p; |
690 |
18991 |
clause1[1] = q; |
691 |
18991 |
assertClause(nnode, clause1); |
692 |
37982 |
SatClause clause2(2); |
693 |
18991 |
clause2[0] = p; |
694 |
18991 |
clause2[1] = r; |
695 |
18991 |
assertClause(nnode, clause2); |
696 |
18991 |
} |
697 |
|
|
698 |
|
// At the top level we must ensure that all clauses that are asserted are |
699 |
|
// not unit, except for the direct assertions. This allows us to remove the |
700 |
|
// clauses later when they are not needed anymore (lemmas for example). |
701 |
520227 |
void CnfStream::convertAndAssert(TNode node, |
702 |
|
bool removable, |
703 |
|
bool negated, |
704 |
|
bool input) |
705 |
|
{ |
706 |
1040454 |
Trace("cnf") << "convertAndAssert(" << node |
707 |
1040454 |
<< ", negated = " << (negated ? "true" : "false") |
708 |
520227 |
<< ", removable = " << (removable ? "true" : "false") << ")\n"; |
709 |
520227 |
d_removable = removable; |
710 |
520231 |
convertAndAssert(node, negated); |
711 |
520223 |
} |
712 |
|
|
713 |
924922 |
void CnfStream::convertAndAssert(TNode node, bool negated) |
714 |
|
{ |
715 |
1849844 |
Trace("cnf") << "convertAndAssert(" << node |
716 |
924922 |
<< ", negated = " << (negated ? "true" : "false") << ")\n"; |
717 |
|
|
718 |
924922 |
d_resourceManager->spendResource(Resource::CnfStep); |
719 |
|
|
720 |
924922 |
switch(node.getKind()) { |
721 |
112630 |
case kind::AND: convertAndAssertAnd(node, negated); break; |
722 |
445846 |
case kind::OR: convertAndAssertOr(node, negated); break; |
723 |
53 |
case kind::XOR: convertAndAssertXor(node, negated); break; |
724 |
60603 |
case kind::IMPLIES: convertAndAssertImplies(node, negated); break; |
725 |
18991 |
case kind::ITE: convertAndAssertIte(node, negated); break; |
726 |
51236 |
case kind::NOT: convertAndAssert(node[0], !negated); break; |
727 |
147604 |
case kind::EQUAL: |
728 |
147604 |
if (node[0].getType().isBoolean()) |
729 |
|
{ |
730 |
81327 |
convertAndAssertIff(node, negated); |
731 |
81327 |
break; |
732 |
|
} |
733 |
|
CVC5_FALLTHROUGH; |
734 |
|
default: |
735 |
|
{ |
736 |
308478 |
Node nnode = node; |
737 |
154239 |
if (negated) |
738 |
|
{ |
739 |
47326 |
nnode = node.negate(); |
740 |
|
} |
741 |
|
// Atoms |
742 |
308478 |
assertClause(nnode, toCNF(node, negated)); |
743 |
|
} |
744 |
154235 |
break; |
745 |
|
} |
746 |
924915 |
} |
747 |
|
|
748 |
|
} // namespace prop |
749 |
28191 |
} // namespace cvc5 |