Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * A CNF converter that takes in asserts and has the side effect of given an
11 : : * equisatisfiable stream of assertions to PropEngine.
12 : : */
13 : : #include "prop/cnf_stream.h"
14 : :
15 : : #include "base/check.h"
16 : : #include "base/output.h"
17 : : #include "expr/node.h"
18 : : #include "options/bv_options.h"
19 : : #include "printer/printer.h"
20 : : #include "proof/clause_id.h"
21 : : #include "prop/minisat/minisat.h"
22 : : #include "prop/prop_engine.h"
23 : : #include "prop/theory_proxy.h"
24 : : #include "smt/env.h"
25 : : #include "theory/theory.h"
26 : : #include "theory/theory_engine.h"
27 : :
28 : : namespace cvc5::internal {
29 : : namespace prop {
30 : :
31 : 91815 : CnfStream::CnfStream(Env& env,
32 : : SatSolver* satSolver,
33 : : Registrar* registrar,
34 : : context::Context* c,
35 : : FormulaLitPolicy flpol,
36 : 91815 : std::string name)
37 : : : EnvObj(env),
38 : 91815 : d_satSolver(satSolver),
39 : 0 : d_booleanVariables(c),
40 : 91815 : d_notifyFormulas(c),
41 : 91815 : d_nodeToLiteralMap(c),
42 : 91815 : d_literalToNodeMap(c),
43 : 91815 : d_flitPolicy(flpol),
44 : 91815 : d_registrar(registrar),
45 : 91815 : d_name(name),
46 : 91815 : d_removable(false),
47 : 183630 : d_stats(statisticsRegistry(), name)
48 : : {
49 : 91815 : }
50 : :
51 : 12600361 : bool CnfStream::assertClause(TNode node, SatClause& c)
52 : : {
53 [ + - ]: 12600361 : Trace("cnf") << "Inserting into stream " << c << " node = " << node << "\n";
54 : :
55 : : // Filter out duplicate literals. Don't rely on the SAT solver to do it.
56 : : // The ProofCnfStream assumes this happens in every SAT solver implicitely.
57 : : // However, CaDiCaL generates additional proof steps if clauses with
58 : : // duplicate literals are added.
59 : 12600361 : std::unordered_set<uint64_t> cache;
60 : 12600361 : SatClause cl;
61 [ + + ]: 47806425 : for (const auto& lit : c)
62 : : {
63 [ + + ]: 35206064 : if (cache.insert(lit.toInt()).second)
64 : : {
65 : 35168294 : cl.push_back(lit);
66 : : }
67 : : }
68 : :
69 : 12600361 : ClauseId clauseId = d_satSolver->addClause(cl, d_removable);
70 : :
71 : 12600361 : return clauseId != ClauseIdUndef;
72 : 12600361 : }
73 : :
74 : 441429 : bool CnfStream::assertClause(TNode node, SatLiteral a)
75 : : {
76 : 441429 : SatClause clause(1);
77 : 441429 : clause[0] = a;
78 : 882858 : return assertClause(node, clause);
79 : 441429 : }
80 : :
81 : 5840736 : bool CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b)
82 : : {
83 : 5840736 : SatClause clause(2);
84 : 5840736 : clause[0] = a;
85 : 5840736 : clause[1] = b;
86 : 11681472 : return assertClause(node, clause);
87 : 5840736 : }
88 : :
89 : 3763925 : bool CnfStream::assertClause(TNode node,
90 : : SatLiteral a,
91 : : SatLiteral b,
92 : : SatLiteral c)
93 : : {
94 : 3763925 : SatClause clause(3);
95 : 3763925 : clause[0] = a;
96 : 3763925 : clause[1] = b;
97 : 3763925 : clause[2] = c;
98 : 7527850 : return assertClause(node, clause);
99 : 3763925 : }
100 : :
101 : 122621138 : bool CnfStream::hasLiteral(TNode n) const
102 : : {
103 : 122621138 : NodeToLiteralMap::const_iterator find = d_nodeToLiteralMap.find(n);
104 : 122621138 : return find != d_nodeToLiteralMap.end();
105 : : }
106 : :
107 : 8152759 : void CnfStream::ensureMappingForLiteral(TNode n)
108 : : {
109 : 8152759 : SatLiteral lit = getLiteral(n);
110 [ + + ]: 8152759 : if (!d_literalToNodeMap.contains(lit))
111 : : {
112 : : // Store backward-mappings
113 : 443 : d_literalToNodeMap.insert(lit, n);
114 : 443 : d_literalToNodeMap.insert(~lit, n.notNode());
115 : : }
116 : 8152759 : }
117 : :
118 : 7948563 : void CnfStream::ensureLiteral(TNode n)
119 : : {
120 : 7948563 : AlwaysAssertArgument(
121 : : hasLiteral(n) || n.getType().isBoolean(),
122 : : n,
123 : : "ProofCnfStream::ensureLiteral() requires a node of Boolean type.\n"
124 : : "got node: %s\n"
125 : : "its type: %s\n",
126 : : n.toString().c_str(),
127 : : n.getType().toString().c_str());
128 [ + - ]: 7948563 : Trace("cnf") << "ensureLiteral(" << n << ")\n";
129 : 7948563 : TimerStat::CodeTimer codeTimer(d_stats.d_cnfConversionTime, true);
130 [ + + ]: 7948563 : if (hasLiteral(n))
131 : : {
132 : 7899289 : ensureMappingForLiteral(n);
133 : 7899289 : return;
134 : : }
135 : : // remove top level negation
136 [ + + ]: 49274 : n = n.getKind() == Kind::NOT ? n[0] : n;
137 [ + + ][ + + ]: 49274 : if (d_env.theoryOf(n) == theory::THEORY_BOOL && !n.isVar())
[ + - ][ + + ]
[ - - ]
138 : : {
139 : : // If we were called with something other than a theory atom (or
140 : : // Boolean variable), we get a SatLiteral that is definitionally
141 : : // equal to it.
142 : : // These are not removable and have no proof ID
143 : 37628 : d_removable = false;
144 : :
145 : 37628 : SatLiteral lit = toCNF(n, false);
146 : :
147 : : // Store backward-mappings
148 : : // These may already exist
149 : 37628 : d_literalToNodeMap.insert_safe(lit, n);
150 : 37628 : d_literalToNodeMap.insert_safe(~lit, n.notNode());
151 : : }
152 : : else
153 : : {
154 : : // We have a theory atom or variable.
155 : 11646 : convertAtom(n);
156 : : }
157 [ + + ]: 7948563 : }
158 : :
159 : 3832855 : SatLiteral CnfStream::newLiteral(TNode node,
160 : : bool isTheoryAtom,
161 : : bool notifyTheory,
162 : : bool canEliminate)
163 : : {
164 [ + - ]: 7665710 : Trace("cnf") << d_name << "::newLiteral(" << node << ", " << isTheoryAtom
165 : 0 : << ")\n"
166 : 3832855 : << push;
167 [ - + ][ - + ]: 3832855 : Assert(node.getKind() != Kind::NOT);
[ - - ]
168 : :
169 : : // if we are tracking formulas, everything is a theory atom
170 [ + + ][ - + ]: 3832855 : if (!isTheoryAtom && d_flitPolicy == FormulaLitPolicy::TRACK_AND_NOTIFY)
171 : : {
172 : 0 : isTheoryAtom = true;
173 : 0 : d_notifyFormulas.insert(node);
174 : : }
175 : :
176 : : // Get the literal for this node
177 : 3832855 : SatLiteral lit;
178 [ + + ]: 3832855 : if (!hasLiteral(node))
179 : : {
180 [ + - ]: 3832850 : Trace("cnf") << d_name << "::newLiteral: node already registered\n";
181 : : // If no literal, we'll make one
182 [ + + ]: 3832850 : if (node.getKind() == Kind::CONST_BOOLEAN)
183 : : {
184 [ + - ]: 64198 : Trace("cnf") << d_name << "::newLiteral: boolean const\n";
185 [ + + ]: 64198 : if (node.getConst<bool>())
186 : : {
187 : 39368 : lit = SatLiteral(d_satSolver->trueVar());
188 : : }
189 : : else
190 : : {
191 : 24830 : lit = SatLiteral(d_satSolver->falseVar());
192 : : }
193 : : }
194 : : else
195 : : {
196 [ + - ]: 3768652 : Trace("cnf") << d_name << "::newLiteral: new var\n";
197 : 3768652 : lit = SatLiteral(d_satSolver->newVar(isTheoryAtom, canEliminate));
198 : 3768652 : d_stats.d_numAtoms++;
199 : : }
200 : 3832850 : d_nodeToLiteralMap.insert(node, lit);
201 : 3832850 : d_nodeToLiteralMap.insert(node.notNode(), ~lit);
202 : : }
203 : : else
204 : : {
205 [ + - ]: 5 : Trace("cnf") << d_name << "::newLiteral: node already registered\n";
206 : 5 : lit = getLiteral(node);
207 : : }
208 : :
209 : : // If it's a theory literal, need to store it for back queries
210 [ + + ][ + + ]: 3832855 : if (isTheoryAtom || d_flitPolicy == FormulaLitPolicy::TRACK
211 [ - + ]: 1458141 : || d_flitPolicy == FormulaLitPolicy::TRACK_AND_NOTIFY_VAR)
212 : : {
213 : 2374714 : d_literalToNodeMap.insert_safe(lit, node);
214 : 2374714 : d_literalToNodeMap.insert_safe(~lit, node.notNode());
215 : : }
216 : :
217 : : // If a theory literal, we pre-register it
218 [ + + ]: 3832855 : if (notifyTheory)
219 : : {
220 : : // In case we are re-entered due to lemmas, save our state
221 : 1432060 : bool backupRemovable = d_removable;
222 : 1432076 : d_registrar->notifySatLiteral(node);
223 : 1432044 : d_removable = backupRemovable;
224 : : }
225 : : // Here, you can have it
226 [ + - ]: 3832839 : Trace("cnf") << "newLiteral(" << node << ") => " << lit << "\n" << pop;
227 : 3832839 : return lit;
228 : : }
229 : :
230 : 69788632 : TNode CnfStream::getNode(const SatLiteral& literal)
231 : : {
232 [ - + ][ - + ]: 69788632 : Assert(d_literalToNodeMap.find(literal) != d_literalToNodeMap.end());
[ - - ]
233 [ + - ]: 69788632 : Trace("cnf") << "getNode(" << literal << ")\n";
234 [ + - ]: 139577264 : Trace("cnf") << "getNode(" << literal << ") => "
235 : 69788632 : << d_literalToNodeMap[literal] << "\n";
236 : 69788632 : return d_literalToNodeMap[literal];
237 : : }
238 : :
239 : 2062692 : const CnfStream::NodeToLiteralMap& CnfStream::getTranslationCache() const
240 : : {
241 : 2062692 : return d_nodeToLiteralMap;
242 : : }
243 : :
244 : 9744838 : const CnfStream::LiteralToNodeMap& CnfStream::getNodeCache() const
245 : : {
246 : 9744838 : return d_literalToNodeMap;
247 : : }
248 : :
249 : 35499 : void CnfStream::getBooleanVariables(std::vector<TNode>& outputVariables) const
250 : : {
251 : 35499 : outputVariables.insert(outputVariables.end(),
252 : : d_booleanVariables.begin(),
253 : : d_booleanVariables.end());
254 : 35499 : }
255 : :
256 : 0 : bool CnfStream::isNotifyFormula(TNode node) const
257 : : {
258 : 0 : return d_notifyFormulas.find(node) != d_notifyFormulas.end();
259 : : }
260 : :
261 : 1475787 : SatLiteral CnfStream::convertAtom(TNode node)
262 : : {
263 [ + - ]: 1475787 : Trace("cnf") << "convertAtom(" << node << ")\n";
264 : :
265 [ - + ][ - + ]: 1475787 : Assert(!hasLiteral(node)) << "atom already mapped!";
[ - - ]
266 : :
267 : 1475787 : bool theoryLiteral = false;
268 : 1475787 : bool canEliminate = true;
269 : 1475787 : bool preRegister = false;
270 : :
271 : : // Is this a variable add it to the list. We distinguish whether a Boolean
272 : : // variable has been marked as a "Boolean term skolem". These variables are
273 : : // introduced by the term formula removal pass (term_formula_removal.h)
274 : : // and maintained by Env (smt/env.h). We treat such variables as theory atoms
275 : : // since they may occur in term positions and thus need to be considered e.g.
276 : : // for theory combination.
277 : 1475787 : bool isInternalBoolVar = false;
278 [ + + ]: 1475787 : if (node.isVar())
279 : : {
280 : 47206 : isInternalBoolVar = !d_env.isBooleanTermSkolem(node);
281 : : }
282 [ + + ]: 1475787 : if (isInternalBoolVar)
283 : : {
284 : 43727 : d_booleanVariables.push_back(node);
285 : : // if TRACK_AND_NOTIFY_VAR, we are notified when Boolean variables are
286 : : // asserted. Thus, they are marked as theory literals.
287 [ - + ]: 43727 : if (d_flitPolicy == FormulaLitPolicy::TRACK_AND_NOTIFY_VAR)
288 : : {
289 : 0 : theoryLiteral = true;
290 : : }
291 : : }
292 : : else
293 : : {
294 : 1432060 : theoryLiteral = true;
295 : 1432060 : canEliminate = false;
296 : 1432060 : preRegister = true;
297 : : }
298 : :
299 : : // Make a new literal (variables are not considered theory literals)
300 : 1475803 : SatLiteral lit = newLiteral(node, theoryLiteral, preRegister, canEliminate);
301 : : // Return the resulting literal
302 : 1475771 : return lit;
303 : : }
304 : :
305 : 99188079 : SatLiteral CnfStream::getLiteral(TNode node)
306 : : {
307 [ - + ][ - + ]: 99188079 : Assert(!node.isNull()) << "CnfStream: can't getLiteral() of null node";
[ - - ]
308 : :
309 [ - + ][ - - ]: 198376158 : Assert(d_nodeToLiteralMap.contains(node))
310 [ - + ][ - + ]: 99188079 : << "Literal not in the CNF Cache: " << node << "\n";
[ - - ]
311 : :
312 : 99188079 : SatLiteral literal = d_nodeToLiteralMap[node];
313 [ + - ]: 198376158 : Trace("cnf") << "CnfStream::getLiteral(" << node << ") => " << literal
314 : 99188079 : << "\n";
315 : 99188079 : return literal;
316 : : }
317 : :
318 : 292883 : void CnfStream::handleXor(TNode xorNode)
319 : : {
320 [ - + ][ - + ]: 292883 : Assert(!hasLiteral(xorNode)) << "Atom already mapped!";
[ - - ]
321 [ - + ][ - + ]: 292883 : Assert(xorNode.getKind() == Kind::XOR) << "Expecting an XOR expression!";
[ - - ]
322 [ - + ][ - + ]: 292883 : Assert(xorNode.getNumChildren() == 2) << "Expecting exactly 2 children!";
[ - - ]
323 [ - + ][ - + ]: 292883 : Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
[ - - ]
324 [ + - ]: 292883 : Trace("cnf") << "CnfStream::handleXor(" << xorNode << ")\n";
325 : :
326 : 292883 : SatLiteral a = getLiteral(xorNode[0]);
327 : 292883 : SatLiteral b = getLiteral(xorNode[1]);
328 : :
329 : 292883 : SatLiteral xorLit = newLiteral(xorNode);
330 : :
331 : 292883 : assertClause(xorNode.negate(), a, b, ~xorLit);
332 : 292883 : assertClause(xorNode.negate(), ~a, ~b, ~xorLit);
333 : 292883 : assertClause(xorNode, a, ~b, xorLit);
334 : 292883 : assertClause(xorNode, ~a, b, xorLit);
335 : 292883 : }
336 : :
337 : 346555 : void CnfStream::handleOr(TNode orNode)
338 : : {
339 [ - + ][ - + ]: 346555 : Assert(!hasLiteral(orNode)) << "Atom already mapped!";
[ - - ]
340 [ - + ][ - + ]: 346555 : Assert(orNode.getKind() == Kind::OR) << "Expecting an OR expression!";
[ - - ]
341 [ - + ][ - + ]: 346555 : Assert(orNode.getNumChildren() > 1) << "Expecting more then 1 child!";
[ - - ]
342 [ - + ][ - + ]: 346555 : Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
[ - - ]
343 [ + - ]: 346555 : Trace("cnf") << "CnfStream::handleOr(" << orNode << ")\n";
344 : :
345 : : // Number of children
346 : 346555 : size_t numChildren = orNode.getNumChildren();
347 : :
348 : : // Get the literal for this node
349 : 346555 : SatLiteral orLit = newLiteral(orNode);
350 : :
351 : : // Transform all the children first
352 : 346555 : SatClause clause(numChildren + 1);
353 [ + + ]: 1260532 : for (size_t i = 0; i < numChildren; ++i)
354 : : {
355 : 913977 : clause[i] = getLiteral(orNode[i]);
356 : :
357 : : // lit <- (a_1 | a_2 | a_3 | ... | a_n)
358 : : // lit | ~(a_1 | a_2 | a_3 | ... | a_n)
359 : : // (lit | ~a_1) & (lit | ~a_2) & (lit & ~a_3) & ... & (lit & ~a_n)
360 : 913977 : assertClause(orNode, orLit, ~clause[i]);
361 : : }
362 : :
363 : : // lit -> (a_1 | a_2 | a_3 | ... | a_n)
364 : : // ~lit | a_1 | a_2 | a_3 | ... | a_n
365 : 346555 : clause[numChildren] = ~orLit;
366 : : // This needs to go last, as the clause might get modified by the SAT solver
367 : 346555 : assertClause(orNode.negate(), clause);
368 : 346555 : }
369 : :
370 : 685239 : void CnfStream::handleAnd(TNode andNode)
371 : : {
372 [ - + ][ - + ]: 685239 : Assert(!hasLiteral(andNode)) << "Atom already mapped!";
[ - - ]
373 [ - + ][ - + ]: 685239 : Assert(andNode.getKind() == Kind::AND) << "Expecting an AND expression!";
[ - - ]
374 [ - + ][ - + ]: 685239 : Assert(andNode.getNumChildren() > 1) << "Expecting more than 1 child!";
[ - - ]
375 [ - + ][ - + ]: 685239 : Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
[ - - ]
376 [ + - ]: 685239 : Trace("cnf") << "handleAnd(" << andNode << ")\n";
377 : :
378 : : // Number of children
379 : 685239 : size_t numChildren = andNode.getNumChildren();
380 : :
381 : : // Get the literal for this node
382 : 685239 : SatLiteral andLit = newLiteral(andNode);
383 : :
384 : : // Transform all the children first (remembering the negation)
385 : 685239 : SatClause clause(numChildren + 1);
386 [ + + ]: 3976079 : for (size_t i = 0; i < numChildren; ++i)
387 : : {
388 : 3290840 : clause[i] = ~getLiteral(andNode[i]);
389 : :
390 : : // lit -> (a_1 & a_2 & a_3 & ... & a_n)
391 : : // ~lit | (a_1 & a_2 & a_3 & ... & a_n)
392 : : // (~lit | a_1) & (~lit | a_2) & ... & (~lit | a_n)
393 : 3290840 : assertClause(andNode.negate(), ~andLit, ~clause[i]);
394 : : }
395 : :
396 : : // lit <- (a_1 & a_2 & a_3 & ... a_n)
397 : : // lit | ~(a_1 & a_2 & a_3 & ... & a_n)
398 : : // lit | ~a_1 | ~a_2 | ~a_3 | ... | ~a_n
399 : 685239 : clause[numChildren] = andLit;
400 : : // This needs to go last, as the clause might get modified by the SAT solver
401 : 685239 : assertClause(andNode, clause);
402 : 685239 : }
403 : :
404 : 2717 : void CnfStream::handleImplies(TNode impliesNode)
405 : : {
406 [ - + ][ - + ]: 2717 : Assert(!hasLiteral(impliesNode)) << "Atom already mapped!";
[ - - ]
407 [ - + ][ - + ]: 2717 : Assert(impliesNode.getKind() == Kind::IMPLIES)
[ - - ]
408 : 0 : << "Expecting an IMPLIES expression!";
409 [ - + ][ - + ]: 2717 : Assert(impliesNode.getNumChildren() == 2) << "Expecting exactly 2 children!";
[ - - ]
410 [ - + ][ - + ]: 2717 : Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
[ - - ]
411 [ + - ]: 2717 : Trace("cnf") << "handleImplies(" << impliesNode << ")\n";
412 : :
413 : : // Convert the children to cnf
414 : 2717 : SatLiteral a = getLiteral(impliesNode[0]);
415 : 2717 : SatLiteral b = getLiteral(impliesNode[1]);
416 : :
417 : 2717 : SatLiteral impliesLit = newLiteral(impliesNode);
418 : :
419 : : // lit -> (a->b)
420 : : // ~lit | ~ a | b
421 : 2717 : assertClause(impliesNode.negate(), ~impliesLit, ~a, b);
422 : :
423 : : // (a->b) -> lit
424 : : // ~(~a | b) | lit
425 : : // (a | l) & (~b | l)
426 : 2717 : assertClause(impliesNode, a, impliesLit);
427 : 2717 : assertClause(impliesNode, ~b, impliesLit);
428 : 2717 : }
429 : :
430 : 257622 : void CnfStream::handleIff(TNode iffNode)
431 : : {
432 [ - + ][ - + ]: 257622 : Assert(!hasLiteral(iffNode)) << "Atom already mapped!";
[ - - ]
433 [ - + ][ - + ]: 257622 : Assert(iffNode.getKind() == Kind::EQUAL) << "Expecting an EQUAL expression!";
[ - - ]
434 [ - + ][ - + ]: 257622 : Assert(iffNode.getNumChildren() == 2) << "Expecting exactly 2 children!";
[ - - ]
435 [ - + ][ - + ]: 257622 : Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
[ - - ]
436 [ + - ]: 257622 : Trace("cnf") << "handleIff(" << iffNode << ")\n";
437 : :
438 : : // Convert the children to CNF
439 : 257622 : SatLiteral a = getLiteral(iffNode[0]);
440 : 257622 : SatLiteral b = getLiteral(iffNode[1]);
441 : :
442 : : // Get the now literal
443 : 257622 : SatLiteral iffLit = newLiteral(iffNode);
444 : :
445 : : // lit -> ((a-> b) & (b->a))
446 : : // ~lit | ((~a | b) & (~b | a))
447 : : // (~a | b | ~lit) & (~b | a | ~lit)
448 : 257622 : assertClause(iffNode.negate(), ~a, b, ~iffLit);
449 : 257622 : assertClause(iffNode.negate(), a, ~b, ~iffLit);
450 : :
451 : : // (a<->b) -> lit
452 : : // ~((a & b) | (~a & ~b)) | lit
453 : : // (~(a & b)) & (~(~a & ~b)) | lit
454 : : // ((~a | ~b) & (a | b)) | lit
455 : : // (~a | ~b | lit) & (a | b | lit)
456 : 257622 : assertClause(iffNode, ~a, ~b, iffLit);
457 : 257622 : assertClause(iffNode, a, b, iffLit);
458 : 257622 : }
459 : :
460 : 103393 : void CnfStream::handleIte(TNode iteNode)
461 : : {
462 [ - + ][ - + ]: 103393 : Assert(!hasLiteral(iteNode)) << "Atom already mapped!";
[ - - ]
463 [ - + ][ - + ]: 103393 : Assert(iteNode.getKind() == Kind::ITE);
[ - - ]
464 [ - + ][ - + ]: 103393 : Assert(iteNode.getNumChildren() == 3);
[ - - ]
465 [ - + ][ - + ]: 103393 : Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
[ - - ]
466 : 206786 : Trace("cnf") << "handleIte(" << iteNode[0] << " " << iteNode[1] << " "
467 [ - + ][ - + ]: 103393 : << iteNode[2] << ")\n";
[ - - ]
468 : :
469 : 103393 : SatLiteral condLit = getLiteral(iteNode[0]);
470 : 103393 : SatLiteral thenLit = getLiteral(iteNode[1]);
471 : 103393 : SatLiteral elseLit = getLiteral(iteNode[2]);
472 : :
473 : 103393 : SatLiteral iteLit = newLiteral(iteNode);
474 : :
475 : : // If ITE is true then one of the branches is true and the condition
476 : : // implies which one
477 : : // lit -> (ite b t e)
478 : : // lit -> (t | e) & (b -> t) & (!b -> e)
479 : : // lit -> (t | e) & (!b | t) & (b | e)
480 : : // (!lit | t | e) & (!lit | !b | t) & (!lit | b | e)
481 : 103393 : assertClause(iteNode.negate(), ~iteLit, thenLit, elseLit);
482 : 103393 : assertClause(iteNode.negate(), ~iteLit, ~condLit, thenLit);
483 : 103393 : assertClause(iteNode.negate(), ~iteLit, condLit, elseLit);
484 : :
485 : : // If ITE is false then one of the branches is false and the condition
486 : : // implies which one
487 : : // !lit -> !(ite b t e)
488 : : // !lit -> (!t | !e) & (b -> !t) & (!b -> !e)
489 : : // !lit -> (!t | !e) & (!b | !t) & (b | !e)
490 : : // (lit | !t | !e) & (lit | !b | !t) & (lit | b | !e)
491 : 103393 : assertClause(iteNode, iteLit, ~thenLit, ~elseLit);
492 : 103393 : assertClause(iteNode, iteLit, ~condLit, ~thenLit);
493 : 103393 : assertClause(iteNode, iteLit, condLit, ~elseLit);
494 : 103393 : }
495 : :
496 : 2285102 : SatLiteral CnfStream::toCNF(TNode node, bool negated)
497 : : {
498 [ + - ]: 4570204 : Trace("cnf") << "toCNF(" << node
499 [ - - ]: 2285102 : << ", negated = " << (negated ? "true" : "false") << ")\n";
500 : :
501 : 2285102 : TNode cur;
502 : 2285102 : SatLiteral nodeLit;
503 : 2285102 : std::vector<TNode> visit;
504 : 2285102 : std::unordered_map<TNode, bool> cache;
505 : :
506 : 2285102 : visit.push_back(node);
507 [ + + ]: 12893884 : while (!visit.empty())
508 : : {
509 : 10608798 : cur = visit.back();
510 [ - + ][ - + ]: 10608798 : Assert(cur.getType().isBoolean());
[ - - ]
511 : :
512 [ + + ]: 10608798 : if (hasLiteral(cur))
513 : : {
514 : 5754968 : visit.pop_back();
515 : 8273662 : continue;
516 : : }
517 : :
518 : 4853830 : const auto& it = cache.find(cur);
519 [ + + ]: 4853830 : if (it == cache.end())
520 : : {
521 : 2518694 : cache.emplace(cur, false);
522 : 2518694 : Kind k = cur.getKind();
523 : : // Only traverse Boolean nodes
524 [ + + ][ + + ]: 2335140 : if (k == Kind::NOT || k == Kind::XOR || k == Kind::ITE
525 [ + + ][ + + ]: 1938864 : || k == Kind::IMPLIES || k == Kind::OR || k == Kind::AND
[ + + ]
526 : 4853834 : || (k == Kind::EQUAL && cur[0].getType().isBoolean()))
527 : : {
528 : : // Preserve the order of the recursive version
529 [ + + ]: 7676969 : for (size_t i = 0, size = cur.getNumChildren(); i < size; ++i)
530 : : {
531 : 5805002 : visit.push_back(cur[size - 1 - i]);
532 : : }
533 : : }
534 : 2518694 : continue;
535 : 2518694 : }
536 [ + - ]: 2335136 : else if (!it->second)
537 : : {
538 : 2335136 : it->second = true;
539 : 2335136 : Kind k = cur.getKind();
540 [ - + ][ + + ]: 2335136 : switch (k)
[ + + ][ + ]
541 : : {
542 : 0 : case Kind::NOT: Assert(hasLiteral(cur[0])); break;
543 : 292883 : case Kind::XOR: handleXor(cur); break;
544 : 103393 : case Kind::ITE: handleIte(cur); break;
545 : 2717 : case Kind::IMPLIES: handleImplies(cur); break;
546 : 346555 : case Kind::OR: handleOr(cur); break;
547 : 685239 : case Kind::AND: handleAnd(cur); break;
548 : 904349 : default:
549 : 904349 : if (k == Kind::EQUAL && cur[0].getType().isBoolean())
550 : : {
551 : 257622 : handleIff(cur);
552 : : }
553 : : else
554 : : {
555 : 646743 : convertAtom(cur);
556 : : }
557 : 904333 : break;
558 : : }
559 : : }
560 : 2335120 : visit.pop_back();
561 : : }
562 : :
563 : 2285086 : nodeLit = getLiteral(node);
564 [ + - ]: 4570172 : Trace("cnf") << "toCNF(): resulting literal: "
565 [ - - ]: 2285086 : << (!negated ? nodeLit : ~nodeLit) << "\n";
566 [ + + ]: 4570172 : return negated ? ~nodeLit : nodeLit;
567 : 2285134 : }
568 : :
569 : 101075 : void CnfStream::convertAndAssertAnd(TNode node, bool negated)
570 : : {
571 [ - + ][ - + ]: 101075 : Assert(node.getKind() == Kind::AND);
[ - - ]
572 [ + - ]: 202150 : Trace("cnf") << "CnfStream::convertAndAssertAnd(" << node
573 [ - - ]: 101075 : << ", negated = " << (negated ? "true" : "false") << ")\n";
574 [ + + ]: 101075 : if (!negated)
575 : : {
576 : : // If the node is a conjunction, we handle each conjunct separately
577 : 14467 : for (TNode::const_iterator conjunct = node.begin(), node_end = node.end();
578 [ + + ]: 51891 : conjunct != node_end;
579 : 37424 : ++conjunct)
580 : : {
581 : 37428 : convertAndAssert(*conjunct, false);
582 : : }
583 : : }
584 : : else
585 : : {
586 : : // If the node is a disjunction, we construct a clause and assert it
587 : 86608 : int nChildren = node.getNumChildren();
588 : 86608 : SatClause clause(nChildren);
589 : 86608 : TNode::const_iterator disjunct = node.begin();
590 [ + + ]: 1258969 : for (int i = 0; i < nChildren; ++disjunct, ++i)
591 : : {
592 [ - + ][ - + ]: 1172361 : Assert(disjunct != node.end());
[ - - ]
593 : 1172361 : clause[i] = toCNF(*disjunct, true);
594 : : }
595 [ - + ][ - + ]: 86608 : Assert(disjunct == node.end());
[ - - ]
596 : 86608 : assertClause(node.negate(), clause);
597 : 86608 : }
598 : 101073 : }
599 : :
600 : 232129 : void CnfStream::convertAndAssertOr(TNode node, bool negated)
601 : : {
602 [ - + ][ - + ]: 232129 : Assert(node.getKind() == Kind::OR);
[ - - ]
603 [ + - ]: 464258 : Trace("cnf") << "CnfStream::convertAndAssertOr(" << node
604 [ - - ]: 232129 : << ", negated = " << (negated ? "true" : "false") << ")\n";
605 [ + + ]: 232129 : if (!negated)
606 : : {
607 : : // If the node is a disjunction, we construct a clause and assert it
608 : 231923 : int nChildren = node.getNumChildren();
609 : 231923 : SatClause clause(nChildren);
610 : 231923 : TNode::const_iterator disjunct = node.begin();
611 [ + + ]: 890771 : for (int i = 0; i < nChildren; ++disjunct, ++i)
612 : : {
613 [ - + ][ - + ]: 658848 : Assert(disjunct != node.end());
[ - - ]
614 : 658848 : clause[i] = toCNF(*disjunct, false);
615 : : }
616 [ - + ][ - + ]: 231923 : Assert(disjunct == node.end());
[ - - ]
617 : 231923 : assertClause(node, clause);
618 : 231923 : }
619 : : else
620 : : {
621 : : // If the node is a conjunction, we handle each conjunct separately
622 : 206 : for (TNode::const_iterator conjunct = node.begin(), node_end = node.end();
623 [ + + ]: 1272 : conjunct != node_end;
624 : 1066 : ++conjunct)
625 : : {
626 : 1066 : convertAndAssert(*conjunct, true);
627 : : }
628 : : }
629 : 232129 : }
630 : :
631 : 70 : void CnfStream::convertAndAssertXor(TNode node, bool negated)
632 : : {
633 [ - + ][ - + ]: 70 : Assert(node.getKind() == Kind::XOR);
[ - - ]
634 [ + - ]: 140 : Trace("cnf") << "CnfStream::convertAndAssertXor(" << node
635 [ - - ]: 70 : << ", negated = " << (negated ? "true" : "false") << ")\n";
636 [ + + ]: 70 : if (!negated)
637 : : {
638 : : // p XOR q
639 : 66 : SatLiteral p = toCNF(node[0], false);
640 : 66 : SatLiteral q = toCNF(node[1], false);
641 : : // Construct the clauses (p => !q) and (!q => p)
642 : 66 : SatClause clause1(2);
643 : 66 : clause1[0] = ~p;
644 : 66 : clause1[1] = ~q;
645 : 66 : assertClause(node, clause1);
646 : 66 : SatClause clause2(2);
647 : 66 : clause2[0] = p;
648 : 66 : clause2[1] = q;
649 : 66 : assertClause(node, clause2);
650 : 66 : }
651 : : else
652 : : {
653 : : // !(p XOR q) is the same as p <=> q
654 : 4 : SatLiteral p = toCNF(node[0], false);
655 : 4 : SatLiteral q = toCNF(node[1], false);
656 : : // Construct the clauses (p => q) and (q => p)
657 : 4 : SatClause clause1(2);
658 : 4 : clause1[0] = ~p;
659 : 4 : clause1[1] = q;
660 : 4 : assertClause(node.negate(), clause1);
661 : 4 : SatClause clause2(2);
662 : 4 : clause2[0] = p;
663 : 4 : clause2[1] = ~q;
664 : 4 : assertClause(node.negate(), clause2);
665 : 4 : }
666 : 70 : }
667 : :
668 : 8069 : void CnfStream::convertAndAssertIff(TNode node, bool negated)
669 : : {
670 [ - + ][ - + ]: 8069 : Assert(node.getKind() == Kind::EQUAL);
[ - - ]
671 [ + - ]: 16138 : Trace("cnf") << "CnfStream::convertAndAssertIff(" << node
672 [ - - ]: 8069 : << ", negated = " << (negated ? "true" : "false") << ")\n";
673 [ + + ]: 8069 : if (!negated)
674 : : {
675 : : // p <=> q
676 : 7657 : SatLiteral p = toCNF(node[0], false);
677 : 7657 : SatLiteral q = toCNF(node[1], false);
678 : : // Construct the clauses (p => q) and (q => p)
679 : 7657 : SatClause clause1(2);
680 : 7657 : clause1[0] = ~p;
681 : 7657 : clause1[1] = q;
682 : 7657 : assertClause(node, clause1);
683 : 7657 : SatClause clause2(2);
684 : 7657 : clause2[0] = p;
685 : 7657 : clause2[1] = ~q;
686 : 7657 : assertClause(node, clause2);
687 : 7657 : }
688 : : else
689 : : {
690 : : // !(p <=> q) is the same as p XOR q
691 : 412 : SatLiteral p = toCNF(node[0], false);
692 : 412 : SatLiteral q = toCNF(node[1], false);
693 : : // Construct the clauses (p => !q) and (!q => p)
694 : 412 : SatClause clause1(2);
695 : 412 : clause1[0] = ~p;
696 : 412 : clause1[1] = ~q;
697 : 412 : assertClause(node.negate(), clause1);
698 : 412 : SatClause clause2(2);
699 : 412 : clause2[0] = p;
700 : 412 : clause2[1] = q;
701 : 412 : assertClause(node.negate(), clause2);
702 : 412 : }
703 : 8069 : }
704 : :
705 : 60870 : void CnfStream::convertAndAssertImplies(TNode node, bool negated)
706 : : {
707 [ - + ][ - + ]: 60870 : Assert(node.getKind() == Kind::IMPLIES);
[ - - ]
708 [ + - ]: 121740 : Trace("cnf") << "CnfStream::convertAndAssertImplies(" << node
709 [ - - ]: 60870 : << ", negated = " << (negated ? "true" : "false") << ")\n";
710 [ + + ]: 60870 : if (!negated)
711 : : {
712 : : // p => q
713 : 60683 : SatLiteral p = toCNF(node[0], false);
714 : 60683 : SatLiteral q = toCNF(node[1], false);
715 : : // Construct the clause ~p || q
716 : 60683 : SatClause clause(2);
717 : 60683 : clause[0] = ~p;
718 : 60683 : clause[1] = q;
719 : 60683 : assertClause(node, clause);
720 : 60683 : }
721 : : else
722 : : { // Construct the
723 : : // !(p => q) is the same as (p && ~q)
724 : 187 : convertAndAssert(node[0], false);
725 : 187 : convertAndAssert(node[1], true);
726 : : }
727 : 60870 : }
728 : :
729 : 20165 : void CnfStream::convertAndAssertIte(TNode node, bool negated)
730 : : {
731 [ - + ][ - + ]: 20165 : Assert(node.getKind() == Kind::ITE);
[ - - ]
732 [ + - ]: 40330 : Trace("cnf") << "CnfStream::convertAndAssertIte(" << node
733 [ - - ]: 20165 : << ", negated = " << (negated ? "true" : "false") << ")\n";
734 : : // ITE(p, q, r)
735 : 20165 : SatLiteral p = toCNF(node[0], false);
736 : 20165 : SatLiteral q = toCNF(node[1], negated);
737 : 20165 : SatLiteral r = toCNF(node[2], negated);
738 : : // Construct the clauses:
739 : : // (p => q) and (!p => r)
740 : : //
741 : : // Note that below q and r can be used directly because whether they are
742 : : // negated has been push to the literal definitions above
743 : 20165 : Node nnode = node;
744 [ + + ]: 20165 : if (negated)
745 : : {
746 : 88 : nnode = node.negate();
747 : : }
748 : 20165 : SatClause clause1(2);
749 : 20165 : clause1[0] = ~p;
750 : 20165 : clause1[1] = q;
751 : 20165 : assertClause(nnode, clause1);
752 : 20165 : SatClause clause2(2);
753 : 20165 : clause2[0] = p;
754 : 20165 : clause2[1] = r;
755 : 20165 : assertClause(nnode, clause2);
756 : 20165 : }
757 : :
758 : : // At the top level we must ensure that all clauses that are asserted are
759 : : // not unit, except for the direct assertions. This allows us to remove the
760 : : // clauses later when they are not needed anymore (lemmas for example).
761 : 601638 : void CnfStream::convertAndAssert(TNode node, bool removable, bool negated)
762 : : {
763 [ + - ]: 1203276 : Trace("cnf") << "convertAndAssert(" << node
764 [ - - ]: 0 : << ", negated = " << (negated ? "true" : "false")
765 [ - - ]: 601638 : << ", removable = " << (removable ? "true" : "false") << ")\n";
766 : 601638 : d_removable = removable;
767 : 601638 : TimerStat::CodeTimer codeTimer(d_stats.d_cnfConversionTime, true);
768 : 601654 : convertAndAssert(node, negated);
769 : 601638 : }
770 : :
771 : 674528 : void CnfStream::convertAndAssert(TNode node, bool negated)
772 : : {
773 [ + - ]: 1349056 : Trace("cnf") << "convertAndAssert(" << node
774 [ - - ]: 674528 : << ", negated = " << (negated ? "true" : "false") << ")\n";
775 : :
776 : 674528 : resourceManager()->spendResource(Resource::CnfStep);
777 : :
778 [ + + ][ + + ]: 674528 : switch (node.getKind())
[ + + ][ + + ]
779 : : {
780 : 101077 : case Kind::AND: convertAndAssertAnd(node, negated); break;
781 : 232129 : case Kind::OR: convertAndAssertOr(node, negated); break;
782 : 70 : case Kind::XOR: convertAndAssertXor(node, negated); break;
783 : 60870 : case Kind::IMPLIES: convertAndAssertImplies(node, negated); break;
784 : 20165 : case Kind::ITE: convertAndAssertIte(node, negated); break;
785 : 34034 : case Kind::NOT: convertAndAssert(node[0], !negated); break;
786 : 66629 : case Kind::EQUAL:
787 [ + + ]: 66629 : if (node[0].getType().isBoolean())
788 : : {
789 : 8069 : convertAndAssertIff(node, negated);
790 : 8069 : break;
791 : : }
792 : : CVC5_FALLTHROUGH;
793 : : default:
794 : : {
795 : 218126 : Node nnode = node;
796 [ + + ]: 218126 : if (negated)
797 : : {
798 : 28035 : nnode = node.negate();
799 : : }
800 : : // Atoms
801 : 218142 : assertClause(nnode, toCNF(node, negated));
802 : 218126 : }
803 : 218110 : break;
804 : : }
805 : 674500 : }
806 : :
807 : 91815 : CnfStream::Statistics::Statistics(StatisticsRegistry& sr,
808 : 91815 : const std::string& name)
809 : : : d_cnfConversionTime(
810 : 91815 : sr.registerTimer(name + "::CnfStream::cnfConversionTime")),
811 : 91815 : d_numAtoms(sr.registerInt(name + "::CnfStream::numAtoms"))
812 : : {
813 : 91815 : }
814 : :
815 : 0 : void CnfStream::dumpDimacs(std::ostream& out, const std::vector<Node>& clauses)
816 : : {
817 : 0 : std::vector<Node> auxUnits;
818 : 0 : dumpDimacs(out, clauses, auxUnits);
819 : 0 : }
820 : :
821 : 0 : void CnfStream::dumpDimacs(std::ostream& out,
822 : : const std::vector<Node>& clauses,
823 : : const std::vector<Node>& auxUnits)
824 : : {
825 : 0 : std::stringstream dclauses;
826 : 0 : SatVariable maxVar = 0;
827 [ - - ]: 0 : for (size_t j = 0; j < 2; j++)
828 : : {
829 [ - - ]: 0 : const std::vector<Node>& cls = j == 0 ? clauses : auxUnits;
830 [ - - ]: 0 : for (const Node& i : cls)
831 : : {
832 : 0 : std::vector<Node> lits;
833 : 0 : if (j == 0 && i.getKind() == Kind::OR)
834 : : {
835 : : // print as clause if not an auxiliary unit
836 : 0 : lits.insert(lits.end(), i.begin(), i.end());
837 : : }
838 : : else
839 : : {
840 : 0 : lits.push_back(i);
841 : : }
842 [ - - ]: 0 : Trace("dimacs-debug") << "Print " << i << std::endl;
843 [ - - ]: 0 : for (const Node& l : lits)
844 : : {
845 : 0 : bool negated = l.getKind() == Kind::NOT;
846 [ - - ]: 0 : const Node& atom = negated ? l[0] : l;
847 : 0 : SatLiteral lit = getLiteral(atom);
848 : 0 : SatVariable v = lit.getSatVariable();
849 [ - - ]: 0 : maxVar = v > maxVar ? v : maxVar;
850 [ - - ]: 0 : dclauses << (negated ? "-" : "") << v << " ";
851 : 0 : }
852 : 0 : dclauses << "0" << std::endl;
853 : 0 : }
854 : : }
855 : :
856 : 0 : out << "p cnf " << maxVar << " " << (clauses.size() + auxUnits.size())
857 : 0 : << std::endl;
858 : 0 : out << dclauses.str();
859 : 0 : }
860 : :
861 : : } // namespace prop
862 : : } // namespace cvc5::internal
|
