Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Dejan Jovanovic, Haniel Barbosa, Mathias Preiner
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
8 : : * in the top-level source directory and their institutional affiliations.
9 : : * All rights reserved. See the file COPYING in the top-level source
10 : : * directory for licensing information.
11 : : * ****************************************************************************
12 : : *
13 : : * 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 "printer/printer.h"
25 : : #include "proof/clause_id.h"
26 : : #include "prop/minisat/minisat.h"
27 : : #include "prop/prop_engine.h"
28 : : #include "prop/theory_proxy.h"
29 : : #include "smt/env.h"
30 : : #include "theory/theory.h"
31 : : #include "theory/theory_engine.h"
32 : :
33 : : namespace cvc5::internal {
34 : : namespace prop {
35 : :
36 : 89857 : CnfStream::CnfStream(Env& env,
37 : : SatSolver* satSolver,
38 : : Registrar* registrar,
39 : : context::Context* c,
40 : : FormulaLitPolicy flpol,
41 : 89857 : std::string name)
42 : : : EnvObj(env),
43 : : d_satSolver(satSolver),
44 : : d_booleanVariables(c),
45 : : d_notifyFormulas(c),
46 : : d_nodeToLiteralMap(c),
47 : : d_literalToNodeMap(c),
48 : : d_flitPolicy(flpol),
49 : : d_registrar(registrar),
50 : : d_name(name),
51 : : d_removable(false),
52 : 89857 : d_stats(statisticsRegistry(), name)
53 : : {
54 : 89857 : }
55 : :
56 : 11611300 : bool CnfStream::assertClause(TNode node, SatClause& c)
57 : : {
58 [ + - ]: 11611300 : Trace("cnf") << "Inserting into stream " << c << " node = " << node << "\n";
59 : :
60 : 11611300 : ClauseId clauseId = d_satSolver->addClause(c, d_removable);
61 : :
62 : 11611300 : return clauseId != ClauseIdUndef;
63 : : }
64 : :
65 : 617408 : bool CnfStream::assertClause(TNode node, SatLiteral a)
66 : : {
67 : 617408 : SatClause clause(1);
68 : 617408 : clause[0] = a;
69 : 1234820 : return assertClause(node, clause);
70 : : }
71 : :
72 : 5246640 : bool CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b)
73 : : {
74 : 5246640 : SatClause clause(2);
75 : 5246640 : clause[0] = a;
76 : 5246640 : clause[1] = b;
77 : 10493300 : return assertClause(node, clause);
78 : : }
79 : :
80 : 3308950 : bool CnfStream::assertClause(TNode node,
81 : : SatLiteral a,
82 : : SatLiteral b,
83 : : SatLiteral c)
84 : : {
85 : 3308950 : SatClause clause(3);
86 : 3308950 : clause[0] = a;
87 : 3308950 : clause[1] = b;
88 : 3308950 : clause[2] = c;
89 : 6617900 : return assertClause(node, clause);
90 : : }
91 : :
92 : 113416000 : bool CnfStream::hasLiteral(TNode n) const {
93 : 113416000 : NodeToLiteralMap::const_iterator find = d_nodeToLiteralMap.find(n);
94 : 113416000 : return find != d_nodeToLiteralMap.end();
95 : : }
96 : :
97 : 6554730 : void CnfStream::ensureMappingForLiteral(TNode n)
98 : : {
99 : 6554730 : SatLiteral lit = getLiteral(n);
100 [ + + ]: 6554730 : if (!d_literalToNodeMap.contains(lit))
101 : : {
102 : : // Store backward-mappings
103 : 435 : d_literalToNodeMap.insert(lit, n);
104 : 435 : d_literalToNodeMap.insert(~lit, n.notNode());
105 : : }
106 : 6554730 : }
107 : :
108 : 6545510 : void CnfStream::ensureLiteral(TNode n)
109 : : {
110 : 6545510 : AlwaysAssertArgument(
111 : : hasLiteral(n) || n.getType().isBoolean(),
112 : : n,
113 : : "ProofCnfStream::ensureLiteral() requires a node of Boolean type.\n"
114 : : "got node: %s\n"
115 : : "its type: %s\n",
116 : : n.toString().c_str(),
117 : : n.getType().toString().c_str());
118 [ + - ]: 6545510 : Trace("cnf") << "ensureLiteral(" << n << ")\n";
119 : 6545510 : TimerStat::CodeTimer codeTimer(d_stats.d_cnfConversionTime, true);
120 [ + + ]: 6545510 : if (hasLiteral(n))
121 : : {
122 : 6411390 : ensureMappingForLiteral(n);
123 : 6411390 : return;
124 : : }
125 : : // remove top level negation
126 [ + + ]: 134122 : n = n.getKind() == Kind::NOT ? n[0] : n;
127 [ + + ][ + + ]: 134122 : if (d_env.theoryOf(n) == theory::THEORY_BOOL && !n.isVar())
[ + - ][ + + ]
[ - - ]
128 : : {
129 : : // If we were called with something other than a theory atom (or
130 : : // Boolean variable), we get a SatLiteral that is definitionally
131 : : // equal to it.
132 : : // These are not removable and have no proof ID
133 : 88260 : d_removable = false;
134 : :
135 : 88260 : SatLiteral lit = toCNF(n, false);
136 : :
137 : : // Store backward-mappings
138 : : // These may already exist
139 : 88260 : d_literalToNodeMap.insert_safe(lit, n);
140 : 88260 : d_literalToNodeMap.insert_safe(~lit, n.notNode());
141 : : }
142 : : else
143 : : {
144 : : // We have a theory atom or variable.
145 : 45862 : convertAtom(n);
146 : : }
147 : : }
148 : :
149 : 3691160 : SatLiteral CnfStream::newLiteral(TNode node,
150 : : bool isTheoryAtom,
151 : : bool notifyTheory,
152 : : bool canEliminate)
153 : : {
154 [ + - ]: 7382320 : Trace("cnf") << d_name << "::newLiteral(" << node << ", " << isTheoryAtom
155 : 0 : << ")\n"
156 : 3691160 : << push;
157 [ - + ][ - + ]: 3691160 : Assert(node.getKind() != Kind::NOT);
[ - - ]
158 : :
159 : : // if we are tracking formulas, everything is a theory atom
160 [ + + ][ - + ]: 3691160 : if (!isTheoryAtom && d_flitPolicy == FormulaLitPolicy::TRACK_AND_NOTIFY)
161 : : {
162 : 0 : isTheoryAtom = true;
163 : 0 : d_notifyFormulas.insert(node);
164 : : }
165 : :
166 : : // Get the literal for this node
167 : 3691160 : SatLiteral lit;
168 [ + + ]: 3691160 : if (!hasLiteral(node))
169 : : {
170 [ + - ]: 3691160 : Trace("cnf") << d_name << "::newLiteral: node already registered\n";
171 : : // If no literal, we'll make one
172 [ + + ]: 3691160 : if (node.getKind() == Kind::CONST_BOOLEAN)
173 : : {
174 [ + - ]: 101171 : Trace("cnf") << d_name << "::newLiteral: boolean const\n";
175 [ + + ]: 101171 : if (node.getConst<bool>())
176 : : {
177 : 50527 : lit = SatLiteral(d_satSolver->trueVar());
178 : : }
179 : : else
180 : : {
181 : 50644 : lit = SatLiteral(d_satSolver->falseVar());
182 : : }
183 : : }
184 : : else
185 : : {
186 [ + - ]: 3589980 : Trace("cnf") << d_name << "::newLiteral: new var\n";
187 : 3589980 : lit = SatLiteral(d_satSolver->newVar(isTheoryAtom, canEliminate));
188 : 3589980 : d_stats.d_numAtoms++;
189 : : }
190 : 3691160 : d_nodeToLiteralMap.insert(node, lit);
191 : 3691160 : d_nodeToLiteralMap.insert(node.notNode(), ~lit);
192 : : }
193 : : else
194 : : {
195 [ + - ]: 4 : Trace("cnf") << d_name << "::newLiteral: node already registered\n";
196 : 4 : lit = getLiteral(node);
197 : : }
198 : :
199 : : // If it's a theory literal, need to store it for back queries
200 [ + + ][ + + ]: 3691160 : if (isTheoryAtom || d_flitPolicy == FormulaLitPolicy::TRACK
201 [ - + ]: 1218080 : || d_flitPolicy == FormulaLitPolicy::TRACK_AND_NOTIFY_VAR)
202 : : {
203 : 2473080 : d_literalToNodeMap.insert_safe(lit, node);
204 : 2473080 : d_literalToNodeMap.insert_safe(~lit, node.notNode());
205 : : }
206 : :
207 : : // If a theory literal, we pre-register it
208 [ + + ]: 3691160 : if (notifyTheory)
209 : : {
210 : : // In case we are re-entered due to lemmas, save our state
211 : 1505480 : bool backupRemovable = d_removable;
212 : 1505490 : d_registrar->notifySatLiteral(node);
213 : 1505460 : d_removable = backupRemovable;
214 : : }
215 : : // Here, you can have it
216 [ + - ]: 3691140 : Trace("cnf") << "newLiteral(" << node << ") => " << lit << "\n" << pop;
217 : 3691140 : return lit;
218 : : }
219 : :
220 : 113773000 : TNode CnfStream::getNode(const SatLiteral& literal)
221 : : {
222 [ - + ][ - + ]: 113773000 : Assert(d_literalToNodeMap.find(literal) != d_literalToNodeMap.end());
[ - - ]
223 [ + - ]: 113773000 : Trace("cnf") << "getNode(" << literal << ")\n";
224 [ + - ]: 227546000 : Trace("cnf") << "getNode(" << literal << ") => "
225 : 113773000 : << d_literalToNodeMap[literal] << "\n";
226 : 113773000 : return d_literalToNodeMap[literal];
227 : : }
228 : :
229 : 1952810 : const CnfStream::NodeToLiteralMap& CnfStream::getTranslationCache() const
230 : : {
231 : 1952810 : return d_nodeToLiteralMap;
232 : : }
233 : :
234 : 9617830 : const CnfStream::LiteralToNodeMap& CnfStream::getNodeCache() const
235 : : {
236 : 9617830 : return d_literalToNodeMap;
237 : : }
238 : :
239 : 42656 : void CnfStream::getBooleanVariables(std::vector<TNode>& outputVariables) const {
240 : 42656 : outputVariables.insert(outputVariables.end(),
241 : : d_booleanVariables.begin(),
242 : 85312 : d_booleanVariables.end());
243 : 42656 : }
244 : :
245 : 0 : bool CnfStream::isNotifyFormula(TNode node) const
246 : : {
247 : 0 : return d_notifyFormulas.find(node) != d_notifyFormulas.end();
248 : : }
249 : :
250 : 1551990 : SatLiteral CnfStream::convertAtom(TNode node)
251 : : {
252 [ + - ]: 1551990 : Trace("cnf") << "convertAtom(" << node << ")\n";
253 : :
254 [ - + ][ - + ]: 1551990 : Assert(!hasLiteral(node)) << "atom already mapped!";
[ - - ]
255 : :
256 : 1551990 : bool theoryLiteral = false;
257 : 1551990 : bool canEliminate = true;
258 : 1551990 : bool preRegister = false;
259 : :
260 : : // Is this a variable add it to the list. We distinguish whether a Boolean
261 : : // variable has been marked as a "Boolean term skolem". These variables are
262 : : // introduced by the term formula removal pass (term_formula_removal.h)
263 : : // and maintained by Env (smt/env.h). We treat such variables as theory atoms
264 : : // since they may occur in term positions and thus need to be considered e.g.
265 : : // for theory combination.
266 : 1551990 : bool isInternalBoolVar = false;
267 [ + + ]: 1551990 : if (node.isVar())
268 : : {
269 : 49073 : isInternalBoolVar = !d_env.isBooleanTermSkolem(node);
270 : : }
271 [ + + ]: 1551990 : if (isInternalBoolVar)
272 : : {
273 : 46516 : d_booleanVariables.push_back(node);
274 : : // if TRACK_AND_NOTIFY_VAR, we are notified when Boolean variables are
275 : : // asserted. Thus, they are marked as theory literals.
276 [ - + ]: 46516 : if (d_flitPolicy == FormulaLitPolicy::TRACK_AND_NOTIFY_VAR)
277 : : {
278 : 0 : theoryLiteral = true;
279 : : }
280 : : }
281 : : else
282 : : {
283 : 1505480 : theoryLiteral = true;
284 : 1505480 : canEliminate = false;
285 : 1505480 : preRegister = true;
286 : : }
287 : :
288 : : // Make a new literal (variables are not considered theory literals)
289 : 1552010 : SatLiteral lit = newLiteral(node, theoryLiteral, preRegister, canEliminate);
290 : : // Return the resulting literal
291 : 1551980 : return lit;
292 : : }
293 : :
294 : 107910000 : SatLiteral CnfStream::getLiteral(TNode node) {
295 [ - + ][ - + ]: 107910000 : Assert(!node.isNull()) << "CnfStream: can't getLiteral() of null node";
[ - - ]
296 : :
297 [ - + ][ - - ]: 215819000 : Assert(d_nodeToLiteralMap.contains(node))
298 [ - + ][ - + ]: 107910000 : << "Literal not in the CNF Cache: " << node << "\n";
[ - - ]
299 : :
300 : 107910000 : SatLiteral literal = d_nodeToLiteralMap[node];
301 [ + - ]: 215819000 : Trace("cnf") << "CnfStream::getLiteral(" << node << ") => " << literal
302 : 107910000 : << "\n";
303 : 107910000 : return literal;
304 : : }
305 : :
306 : 246591 : void CnfStream::handleXor(TNode xorNode)
307 : : {
308 [ - + ][ - + ]: 246591 : Assert(!hasLiteral(xorNode)) << "Atom already mapped!";
[ - - ]
309 [ - + ][ - + ]: 246591 : Assert(xorNode.getKind() == Kind::XOR) << "Expecting an XOR expression!";
[ - - ]
310 [ - + ][ - + ]: 246591 : Assert(xorNode.getNumChildren() == 2) << "Expecting exactly 2 children!";
[ - - ]
311 [ - + ][ - + ]: 246591 : Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
[ - - ]
312 [ + - ]: 246591 : Trace("cnf") << "CnfStream::handleXor(" << xorNode << ")\n";
313 : :
314 : 246591 : SatLiteral a = getLiteral(xorNode[0]);
315 : 246591 : SatLiteral b = getLiteral(xorNode[1]);
316 : :
317 : 246591 : SatLiteral xorLit = newLiteral(xorNode);
318 : :
319 : 246591 : assertClause(xorNode.negate(), a, b, ~xorLit);
320 : 246591 : assertClause(xorNode.negate(), ~a, ~b, ~xorLit);
321 : 246591 : assertClause(xorNode, a, ~b, xorLit);
322 : 246591 : assertClause(xorNode, ~a, b, xorLit);
323 : 246591 : }
324 : :
325 : 363788 : void CnfStream::handleOr(TNode orNode)
326 : : {
327 [ - + ][ - + ]: 363788 : Assert(!hasLiteral(orNode)) << "Atom already mapped!";
[ - - ]
328 [ - + ][ - + ]: 363788 : Assert(orNode.getKind() == Kind::OR) << "Expecting an OR expression!";
[ - - ]
329 [ - + ][ - + ]: 363788 : Assert(orNode.getNumChildren() > 1) << "Expecting more then 1 child!";
[ - - ]
330 [ - + ][ - + ]: 363788 : Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
[ - - ]
331 [ + - ]: 363788 : Trace("cnf") << "CnfStream::handleOr(" << orNode << ")\n";
332 : :
333 : : // Number of children
334 : 363788 : size_t numChildren = orNode.getNumChildren();
335 : :
336 : : // Get the literal for this node
337 : 363788 : SatLiteral orLit = newLiteral(orNode);
338 : :
339 : : // Transform all the children first
340 : 363788 : SatClause clause(numChildren + 1);
341 [ + + ]: 1356210 : for (size_t i = 0; i < numChildren; ++i)
342 : : {
343 : 992426 : clause[i] = getLiteral(orNode[i]);
344 : :
345 : : // lit <- (a_1 | a_2 | a_3 | ... | a_n)
346 : : // lit | ~(a_1 | a_2 | a_3 | ... | a_n)
347 : : // (lit | ~a_1) & (lit | ~a_2) & (lit & ~a_3) & ... & (lit & ~a_n)
348 : 992426 : assertClause(orNode, orLit, ~clause[i]);
349 : : }
350 : :
351 : : // lit -> (a_1 | a_2 | a_3 | ... | a_n)
352 : : // ~lit | a_1 | a_2 | a_3 | ... | a_n
353 : 363788 : clause[numChildren] = ~orLit;
354 : : // This needs to go last, as the clause might get modified by the SAT solver
355 : 363788 : assertClause(orNode.negate(), clause);
356 : 363788 : }
357 : :
358 : 648739 : void CnfStream::handleAnd(TNode andNode)
359 : : {
360 [ - + ][ - + ]: 648739 : Assert(!hasLiteral(andNode)) << "Atom already mapped!";
[ - - ]
361 [ - + ][ - + ]: 648739 : Assert(andNode.getKind() == Kind::AND) << "Expecting an AND expression!";
[ - - ]
362 [ - + ][ - + ]: 648739 : Assert(andNode.getNumChildren() > 1) << "Expecting more than 1 child!";
[ - - ]
363 [ - + ][ - + ]: 648739 : Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
[ - - ]
364 [ + - ]: 648739 : Trace("cnf") << "handleAnd(" << andNode << ")\n";
365 : :
366 : : // Number of children
367 : 648739 : size_t numChildren = andNode.getNumChildren();
368 : :
369 : : // Get the literal for this node
370 : 648739 : SatLiteral andLit = newLiteral(andNode);
371 : :
372 : : // Transform all the children first (remembering the negation)
373 : 648739 : SatClause clause(numChildren + 1);
374 [ + + ]: 3551860 : for (size_t i = 0; i < numChildren; ++i)
375 : : {
376 : 2903120 : clause[i] = ~getLiteral(andNode[i]);
377 : :
378 : : // lit -> (a_1 & a_2 & a_3 & ... & a_n)
379 : : // ~lit | (a_1 & a_2 & a_3 & ... & a_n)
380 : : // (~lit | a_1) & (~lit | a_2) & ... & (~lit | a_n)
381 : 2903120 : 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 : 648739 : clause[numChildren] = andLit;
388 : : // This needs to go last, as the clause might get modified by the SAT solver
389 : 648739 : assertClause(andNode, clause);
390 : 648739 : }
391 : :
392 : 5107 : void CnfStream::handleImplies(TNode impliesNode)
393 : : {
394 [ - + ][ - + ]: 5107 : Assert(!hasLiteral(impliesNode)) << "Atom already mapped!";
[ - - ]
395 [ - + ][ - + ]: 5107 : Assert(impliesNode.getKind() == Kind::IMPLIES)
[ - - ]
396 : 0 : << "Expecting an IMPLIES expression!";
397 [ - + ][ - + ]: 5107 : Assert(impliesNode.getNumChildren() == 2) << "Expecting exactly 2 children!";
[ - - ]
398 [ - + ][ - + ]: 5107 : Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
[ - - ]
399 [ + - ]: 5107 : Trace("cnf") << "handleImplies(" << impliesNode << ")\n";
400 : :
401 : : // Convert the children to cnf
402 : 5107 : SatLiteral a = getLiteral(impliesNode[0]);
403 : 5107 : SatLiteral b = getLiteral(impliesNode[1]);
404 : :
405 : 5107 : SatLiteral impliesLit = newLiteral(impliesNode);
406 : :
407 : : // lit -> (a->b)
408 : : // ~lit | ~ a | b
409 : 5107 : assertClause(impliesNode.negate(), ~impliesLit, ~a, b);
410 : :
411 : : // (a->b) -> lit
412 : : // ~(~a | b) | lit
413 : : // (a | l) & (~b | l)
414 : 5107 : assertClause(impliesNode, a, impliesLit);
415 : 5107 : assertClause(impliesNode, ~b, impliesLit);
416 : 5107 : }
417 : :
418 : 226945 : void CnfStream::handleIff(TNode iffNode)
419 : : {
420 [ - + ][ - + ]: 226945 : Assert(!hasLiteral(iffNode)) << "Atom already mapped!";
[ - - ]
421 [ - + ][ - + ]: 226945 : Assert(iffNode.getKind() == Kind::EQUAL) << "Expecting an EQUAL expression!";
[ - - ]
422 [ - + ][ - + ]: 226945 : Assert(iffNode.getNumChildren() == 2) << "Expecting exactly 2 children!";
[ - - ]
423 [ - + ][ - + ]: 226945 : Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
[ - - ]
424 [ + - ]: 226945 : Trace("cnf") << "handleIff(" << iffNode << ")\n";
425 : :
426 : : // Convert the children to CNF
427 : 226945 : SatLiteral a = getLiteral(iffNode[0]);
428 : 226945 : SatLiteral b = getLiteral(iffNode[1]);
429 : :
430 : : // Get the now literal
431 : 226945 : SatLiteral iffLit = newLiteral(iffNode);
432 : :
433 : : // lit -> ((a-> b) & (b->a))
434 : : // ~lit | ((~a | b) & (~b | a))
435 : : // (~a | b | ~lit) & (~b | a | ~lit)
436 : 226945 : assertClause(iffNode.negate(), ~a, b, ~iffLit);
437 : 226945 : assertClause(iffNode.negate(), a, ~b, ~iffLit);
438 : :
439 : : // (a<->b) -> lit
440 : : // ~((a & b) | (~a & ~b)) | lit
441 : : // (~(a & b)) & (~(~a & ~b)) | lit
442 : : // ((~a | ~b) & (a | b)) | lit
443 : : // (~a | ~b | lit) & (a | b | lit)
444 : 226945 : assertClause(iffNode, ~a, ~b, iffLit);
445 : 226945 : assertClause(iffNode, a, b, iffLit);
446 : 226945 : }
447 : :
448 : 81593 : void CnfStream::handleIte(TNode iteNode)
449 : : {
450 [ - + ][ - + ]: 81593 : Assert(!hasLiteral(iteNode)) << "Atom already mapped!";
[ - - ]
451 [ - + ][ - + ]: 81593 : Assert(iteNode.getKind() == Kind::ITE);
[ - - ]
452 [ - + ][ - + ]: 81593 : Assert(iteNode.getNumChildren() == 3);
[ - - ]
453 [ - + ][ - + ]: 81593 : Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
[ - - ]
454 : 163186 : Trace("cnf") << "handleIte(" << iteNode[0] << " " << iteNode[1] << " "
455 [ - + ][ - + ]: 81593 : << iteNode[2] << ")\n";
[ - - ]
456 : :
457 : 81593 : SatLiteral condLit = getLiteral(iteNode[0]);
458 : 81593 : SatLiteral thenLit = getLiteral(iteNode[1]);
459 : 81593 : SatLiteral elseLit = getLiteral(iteNode[2]);
460 : :
461 : 81593 : SatLiteral iteLit = newLiteral(iteNode);
462 : :
463 : : // If ITE is true then one of the branches is true and the condition
464 : : // implies which one
465 : : // lit -> (ite b t e)
466 : : // lit -> (t | e) & (b -> t) & (!b -> e)
467 : : // lit -> (t | e) & (!b | t) & (b | e)
468 : : // (!lit | t | e) & (!lit | !b | t) & (!lit | b | e)
469 : 81593 : assertClause(iteNode.negate(), ~iteLit, thenLit, elseLit);
470 : 81593 : assertClause(iteNode.negate(), ~iteLit, ~condLit, thenLit);
471 : 81593 : assertClause(iteNode.negate(), ~iteLit, condLit, elseLit);
472 : :
473 : : // If ITE is false then one of the branches is false and the condition
474 : : // implies which one
475 : : // !lit -> !(ite b t e)
476 : : // !lit -> (!t | !e) & (b -> !t) & (!b -> !e)
477 : : // !lit -> (!t | !e) & (!b | !t) & (b | !e)
478 : : // (lit | !t | !e) & (lit | !b | !t) & (lit | b | !e)
479 : 81593 : assertClause(iteNode, iteLit, ~thenLit, ~elseLit);
480 : 81593 : assertClause(iteNode, iteLit, ~condLit, ~thenLit);
481 : 81593 : assertClause(iteNode, iteLit, condLit, ~elseLit);
482 : 81593 : }
483 : :
484 : 3066120 : SatLiteral CnfStream::toCNF(TNode node, bool negated)
485 : : {
486 [ + - ]: 6132240 : Trace("cnf") << "toCNF(" << node
487 [ - - ]: 3066120 : << ", negated = " << (negated ? "true" : "false") << ")\n";
488 : :
489 : 6132240 : TNode cur;
490 : 3066120 : SatLiteral nodeLit;
491 : 6132240 : std::vector<TNode> visit;
492 : 6132240 : std::unordered_map<TNode, bool> cache;
493 : :
494 : 3066120 : visit.push_back(node);
495 [ + + ]: 14143600 : while (!visit.empty())
496 : : {
497 : 11077500 : cur = visit.back();
498 [ - + ][ - + ]: 11077500 : Assert(cur.getType().isBoolean());
[ - - ]
499 : :
500 [ + + ]: 11077500 : if (hasLiteral(cur))
501 : : {
502 : 5952370 : visit.pop_back();
503 : 8631980 : continue;
504 : : }
505 : :
506 : 5125120 : const auto& it = cache.find(cur);
507 [ + + ]: 5125120 : if (it == cache.end())
508 : : {
509 : 2679620 : cache.emplace(cur, false);
510 : 2679620 : Kind k = cur.getKind();
511 : : // Only traverse Boolean nodes
512 [ + + ][ + + ]: 2445500 : if (k == Kind::NOT || k == Kind::XOR || k == Kind::ITE
513 [ + + ][ + + ]: 2117320 : || k == Kind::IMPLIES || k == Kind::OR || k == Kind::AND
[ + + ]
514 : 5125120 : || (k == Kind::EQUAL && cur[0].getType().isBoolean()))
515 : : {
516 : : // Preserve the order of the recursive version
517 [ + + ]: 7138630 : for (size_t i = 0, size = cur.getNumChildren(); i < size; ++i)
518 : : {
519 : 5331740 : visit.push_back(cur[size - 1 - i]);
520 : : }
521 : : }
522 : 2679620 : continue;
523 : : }
524 [ + - ]: 2445500 : else if (!it->second)
525 : : {
526 : 2445500 : it->second = true;
527 : 2445500 : Kind k = cur.getKind();
528 [ - + ][ + + ]: 2445500 : switch (k)
[ + + ][ + ]
529 : : {
530 : 0 : case Kind::NOT: Assert(hasLiteral(cur[0])); break;
531 : 246591 : case Kind::XOR: handleXor(cur); break;
532 : 81593 : case Kind::ITE: handleIte(cur); break;
533 : 5107 : case Kind::IMPLIES: handleImplies(cur); break;
534 : 363788 : case Kind::OR: handleOr(cur); break;
535 : 648739 : case Kind::AND: handleAnd(cur); break;
536 : 1099680 : default:
537 : 1099680 : if (k == Kind::EQUAL && cur[0].getType().isBoolean())
538 : : {
539 : 226945 : handleIff(cur);
540 : : }
541 : : else
542 : : {
543 : 872750 : convertAtom(cur);
544 : : }
545 : 1099660 : break;
546 : : }
547 : : }
548 : 2445480 : visit.pop_back();
549 : : }
550 : :
551 : 3066100 : nodeLit = getLiteral(node);
552 [ + - ]: 6132210 : Trace("cnf") << "toCNF(): resulting literal: "
553 [ - - ]: 3066100 : << (!negated ? nodeLit : ~nodeLit) << "\n";
554 [ + + ]: 6132210 : return negated ? ~nodeLit : nodeLit;
555 : : }
556 : :
557 : 142789 : void CnfStream::convertAndAssertAnd(TNode node, bool negated)
558 : : {
559 [ - + ][ - + ]: 142789 : Assert(node.getKind() == Kind::AND);
[ - - ]
560 [ + - ]: 285578 : Trace("cnf") << "CnfStream::convertAndAssertAnd(" << node
561 [ - - ]: 142789 : << ", negated = " << (negated ? "true" : "false") << ")\n";
562 [ + + ]: 142789 : if (!negated) {
563 : : // If the node is a conjunction, we handle each conjunct separately
564 : 75613 : for(TNode::const_iterator conjunct = node.begin(), node_end = node.end();
565 [ + + ]: 75613 : conjunct != node_end; ++conjunct ) {
566 : 57236 : convertAndAssert(*conjunct, false);
567 : : }
568 : : } else {
569 : : // If the node is a disjunction, we construct a clause and assert it
570 : 124408 : int nChildren = node.getNumChildren();
571 : 124408 : SatClause clause(nChildren);
572 : 124408 : TNode::const_iterator disjunct = node.begin();
573 [ + + ]: 1628630 : for(int i = 0; i < nChildren; ++ disjunct, ++ i) {
574 [ - + ][ - + ]: 1504220 : Assert(disjunct != node.end());
[ - - ]
575 : 1504220 : clause[i] = toCNF(*disjunct, true);
576 : : }
577 [ - + ][ - + ]: 124408 : Assert(disjunct == node.end());
[ - - ]
578 : 124408 : assertClause(node.negate(), clause);
579 : : }
580 : 142787 : }
581 : :
582 : 296341 : void CnfStream::convertAndAssertOr(TNode node, bool negated)
583 : : {
584 [ - + ][ - + ]: 296341 : Assert(node.getKind() == Kind::OR);
[ - - ]
585 [ + - ]: 592682 : Trace("cnf") << "CnfStream::convertAndAssertOr(" << node
586 [ - - ]: 296341 : << ", negated = " << (negated ? "true" : "false") << ")\n";
587 [ + + ]: 296341 : if (!negated) {
588 : : // If the node is a disjunction, we construct a clause and assert it
589 : 296129 : int nChildren = node.getNumChildren();
590 : 296129 : SatClause clause(nChildren);
591 : 296129 : TNode::const_iterator disjunct = node.begin();
592 [ + + ]: 1188850 : for(int i = 0; i < nChildren; ++ disjunct, ++ i) {
593 [ - + ][ - + ]: 892721 : Assert(disjunct != node.end());
[ - - ]
594 : 892721 : clause[i] = toCNF(*disjunct, false);
595 : : }
596 [ - + ][ - + ]: 296129 : Assert(disjunct == node.end());
[ - - ]
597 : 296129 : assertClause(node, clause);
598 : : } else {
599 : : // If the node is a conjunction, we handle each conjunct separately
600 : 1279 : for(TNode::const_iterator conjunct = node.begin(), node_end = node.end();
601 [ + + ]: 1279 : conjunct != node_end; ++conjunct ) {
602 : 1067 : convertAndAssert(*conjunct, true);
603 : : }
604 : : }
605 : 296341 : }
606 : :
607 : 72 : void CnfStream::convertAndAssertXor(TNode node, bool negated)
608 : : {
609 [ - + ][ - + ]: 72 : Assert(node.getKind() == Kind::XOR);
[ - - ]
610 [ + - ]: 144 : Trace("cnf") << "CnfStream::convertAndAssertXor(" << node
611 [ - - ]: 72 : << ", negated = " << (negated ? "true" : "false") << ")\n";
612 [ + + ]: 72 : if (!negated) {
613 : : // p XOR q
614 : 68 : SatLiteral p = toCNF(node[0], false);
615 : 68 : SatLiteral q = toCNF(node[1], false);
616 : : // Construct the clauses (p => !q) and (!q => p)
617 : 136 : SatClause clause1(2);
618 : 68 : clause1[0] = ~p;
619 : 68 : clause1[1] = ~q;
620 : 68 : assertClause(node, clause1);
621 : 68 : SatClause clause2(2);
622 : 68 : clause2[0] = p;
623 : 68 : clause2[1] = q;
624 : 68 : assertClause(node, clause2);
625 : : } else {
626 : : // !(p XOR q) is the same as p <=> q
627 : 4 : SatLiteral p = toCNF(node[0], false);
628 : 4 : SatLiteral q = toCNF(node[1], false);
629 : : // Construct the clauses (p => q) and (q => p)
630 : 8 : SatClause clause1(2);
631 : 4 : clause1[0] = ~p;
632 : 4 : clause1[1] = q;
633 : 4 : assertClause(node.negate(), clause1);
634 : 4 : SatClause clause2(2);
635 : 4 : clause2[0] = p;
636 : 4 : clause2[1] = ~q;
637 : 4 : assertClause(node.negate(), clause2);
638 : : }
639 : 72 : }
640 : :
641 : 8803 : void CnfStream::convertAndAssertIff(TNode node, bool negated)
642 : : {
643 [ - + ][ - + ]: 8803 : Assert(node.getKind() == Kind::EQUAL);
[ - - ]
644 [ + - ]: 17606 : Trace("cnf") << "CnfStream::convertAndAssertIff(" << node
645 [ - - ]: 8803 : << ", negated = " << (negated ? "true" : "false") << ")\n";
646 [ + + ]: 8803 : if (!negated) {
647 : : // p <=> q
648 : 8313 : SatLiteral p = toCNF(node[0], false);
649 : 8313 : SatLiteral q = toCNF(node[1], false);
650 : : // Construct the clauses (p => q) and (q => p)
651 : 16626 : SatClause clause1(2);
652 : 8313 : clause1[0] = ~p;
653 : 8313 : clause1[1] = q;
654 : 8313 : assertClause(node, clause1);
655 : 8313 : SatClause clause2(2);
656 : 8313 : clause2[0] = p;
657 : 8313 : clause2[1] = ~q;
658 : 8313 : assertClause(node, clause2);
659 : : } else {
660 : : // !(p <=> q) is the same as p XOR q
661 : 490 : SatLiteral p = toCNF(node[0], false);
662 : 490 : SatLiteral q = toCNF(node[1], false);
663 : : // Construct the clauses (p => !q) and (!q => p)
664 : 980 : SatClause clause1(2);
665 : 490 : clause1[0] = ~p;
666 : 490 : clause1[1] = ~q;
667 : 490 : assertClause(node.negate(), clause1);
668 : 490 : SatClause clause2(2);
669 : 490 : clause2[0] = p;
670 : 490 : clause2[1] = q;
671 : 490 : assertClause(node.negate(), clause2);
672 : : }
673 : 8803 : }
674 : :
675 : 78480 : void CnfStream::convertAndAssertImplies(TNode node, bool negated)
676 : : {
677 [ - + ][ - + ]: 78480 : Assert(node.getKind() == Kind::IMPLIES);
[ - - ]
678 [ + - ]: 156960 : Trace("cnf") << "CnfStream::convertAndAssertImplies(" << node
679 [ - - ]: 78480 : << ", negated = " << (negated ? "true" : "false") << ")\n";
680 [ + + ]: 78480 : if (!negated) {
681 : : // p => q
682 : 78301 : SatLiteral p = toCNF(node[0], false);
683 : 78301 : SatLiteral q = toCNF(node[1], false);
684 : : // Construct the clause ~p || q
685 : 78301 : SatClause clause(2);
686 : 78301 : clause[0] = ~p;
687 : 78301 : clause[1] = q;
688 : 78301 : assertClause(node, clause);
689 : : } else {// Construct the
690 : : // !(p => q) is the same as (p && ~q)
691 : 179 : convertAndAssert(node[0], false);
692 : 179 : convertAndAssert(node[1], true);
693 : : }
694 : 78480 : }
695 : :
696 : 19286 : void CnfStream::convertAndAssertIte(TNode node, bool negated)
697 : : {
698 [ - + ][ - + ]: 19286 : Assert(node.getKind() == Kind::ITE);
[ - - ]
699 [ + - ]: 38572 : Trace("cnf") << "CnfStream::convertAndAssertIte(" << node
700 [ - - ]: 19286 : << ", negated = " << (negated ? "true" : "false") << ")\n";
701 : : // ITE(p, q, r)
702 : 19286 : SatLiteral p = toCNF(node[0], false);
703 : 19286 : SatLiteral q = toCNF(node[1], negated);
704 : 19286 : SatLiteral r = toCNF(node[2], negated);
705 : : // Construct the clauses:
706 : : // (p => q) and (!p => r)
707 : : //
708 : : // Note that below q and r can be used directly because whether they are
709 : : // negated has been push to the literal definitions above
710 : 38572 : Node nnode = node;
711 [ + + ]: 19286 : if( negated ){
712 : 105 : nnode = node.negate();
713 : : }
714 : 38572 : SatClause clause1(2);
715 : 19286 : clause1[0] = ~p;
716 : 19286 : clause1[1] = q;
717 : 19286 : assertClause(nnode, clause1);
718 : 19286 : SatClause clause2(2);
719 : 19286 : clause2[0] = p;
720 : 19286 : clause2[1] = r;
721 : 19286 : assertClause(nnode, clause2);
722 : 19286 : }
723 : :
724 : : // At the top level we must ensure that all clauses that are asserted are
725 : : // not unit, except for the direct assertions. This allows us to remove the
726 : : // clauses later when they are not needed anymore (lemmas for example).
727 : 835818 : void CnfStream::convertAndAssert(TNode node, bool removable, bool negated)
728 : : {
729 [ + - ]: 1671640 : Trace("cnf") << "convertAndAssert(" << node
730 [ - - ]: 0 : << ", negated = " << (negated ? "true" : "false")
731 [ - - ]: 835818 : << ", removable = " << (removable ? "true" : "false") << ")\n";
732 : 835818 : d_removable = removable;
733 : 835834 : TimerStat::CodeTimer codeTimer(d_stats.d_cnfConversionTime, true);
734 : 835834 : convertAndAssert(node, negated);
735 : 835802 : }
736 : :
737 : 1000470 : void CnfStream::convertAndAssert(TNode node, bool negated)
738 : : {
739 [ + - ]: 2000950 : Trace("cnf") << "convertAndAssert(" << node
740 [ - - ]: 1000470 : << ", negated = " << (negated ? "true" : "false") << ")\n";
741 : :
742 : 1000470 : resourceManager()->spendResource(Resource::CnfStep);
743 : :
744 [ + + ][ + + ]: 1000470 : switch(node.getKind()) {
[ + + ][ + + ]
745 : 142791 : case Kind::AND: convertAndAssertAnd(node, negated); break;
746 : 296341 : case Kind::OR: convertAndAssertOr(node, negated); break;
747 : 72 : case Kind::XOR: convertAndAssertXor(node, negated); break;
748 : 78480 : case Kind::IMPLIES: convertAndAssertImplies(node, negated); break;
749 : 19286 : case Kind::ITE: convertAndAssertIte(node, negated); break;
750 : 106006 : case Kind::NOT: convertAndAssert(node[0], !negated); break;
751 : 96256 : case Kind::EQUAL:
752 [ + + ]: 96256 : if (node[0].getType().isBoolean())
753 : : {
754 : 8803 : convertAndAssertIff(node, negated);
755 : 8803 : break;
756 : : }
757 : : CVC5_FALLTHROUGH;
758 : : default:
759 : : {
760 : 348722 : Node nnode = node;
761 [ + + ]: 348706 : if (negated)
762 : : {
763 : 100451 : nnode = node.negate();
764 : : }
765 : : // Atoms
766 : 348722 : assertClause(nnode, toCNF(node, negated));
767 : : }
768 : 348690 : break;
769 : : }
770 : 1000440 : }
771 : :
772 : 89857 : CnfStream::Statistics::Statistics(StatisticsRegistry& sr,
773 : 89857 : const std::string& name)
774 : : : d_cnfConversionTime(
775 : 89857 : sr.registerTimer(name + "::CnfStream::cnfConversionTime")),
776 : 89857 : d_numAtoms(sr.registerInt(name + "::CnfStream::numAtoms"))
777 : : {
778 : 89857 : }
779 : :
780 : 0 : void CnfStream::dumpDimacs(std::ostream& out, const std::vector<Node>& clauses)
781 : : {
782 : 0 : std::vector<Node> auxUnits;
783 : 0 : dumpDimacs(out, clauses, auxUnits);
784 : 0 : }
785 : :
786 : 0 : void CnfStream::dumpDimacs(std::ostream& out,
787 : : const std::vector<Node>& clauses,
788 : : const std::vector<Node>& auxUnits)
789 : : {
790 : 0 : std::stringstream dclauses;
791 : 0 : SatVariable maxVar = 0;
792 [ - - ]: 0 : for (size_t j = 0; j < 2; j++)
793 : : {
794 [ - - ]: 0 : const std::vector<Node>& cls = j == 0 ? clauses : auxUnits;
795 [ - - ]: 0 : for (const Node& i : cls)
796 : : {
797 : 0 : std::vector<Node> lits;
798 : 0 : if (j == 0 && i.getKind() == Kind::OR)
799 : : {
800 : : // print as clause if not an auxiliary unit
801 : 0 : lits.insert(lits.end(), i.begin(), i.end());
802 : : }
803 : : else
804 : : {
805 : 0 : lits.push_back(i);
806 : : }
807 [ - - ]: 0 : Trace("dimacs-debug") << "Print " << i << std::endl;
808 [ - - ]: 0 : for (const Node& l : lits)
809 : : {
810 : 0 : bool negated = l.getKind() == Kind::NOT;
811 [ - - ]: 0 : const Node& atom = negated ? l[0] : l;
812 : 0 : SatLiteral lit = getLiteral(atom);
813 : 0 : SatVariable v = lit.getSatVariable();
814 [ - - ]: 0 : maxVar = v > maxVar ? v : maxVar;
815 [ - - ]: 0 : dclauses << (negated ? "-" : "") << v << " ";
816 : : }
817 : 0 : dclauses << "0" << std::endl;
818 : : }
819 : : }
820 : :
821 : 0 : out << "p cnf " << maxVar << " " << (clauses.size() + auxUnits.size())
822 : 0 : << std::endl;
823 : 0 : out << dclauses.str();
824 : 0 : }
825 : :
826 : : } // namespace prop
827 : : } // namespace cvc5::internal
|
