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