Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Dejan Jovanovic, Haniel Barbosa, Andrew Reynolds
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 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 : 92096 : CnfStream::CnfStream(Env& env,
37 : : SatSolver* satSolver,
38 : : Registrar* registrar,
39 : : context::Context* c,
40 : : FormulaLitPolicy flpol,
41 : 92096 : 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 : 92096 : d_stats(statisticsRegistry(), name)
53 : : {
54 : 92096 : }
55 : :
56 : 12141700 : bool CnfStream::assertClause(TNode node, SatClause& c)
57 : : {
58 [ + - ]: 12141700 : Trace("cnf") << "Inserting into stream " << c << " node = " << node << "\n";
59 : :
60 : 12141700 : ClauseId clauseId = d_satSolver->addClause(c, d_removable);
61 : :
62 : 12141700 : return clauseId != ClauseIdUndef;
63 : : }
64 : :
65 : 644257 : bool CnfStream::assertClause(TNode node, SatLiteral a)
66 : : {
67 : 644257 : SatClause clause(1);
68 : 644257 : clause[0] = a;
69 : 1288510 : return assertClause(node, clause);
70 : : }
71 : :
72 : 5502060 : bool CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b)
73 : : {
74 : 5502060 : SatClause clause(2);
75 : 5502060 : clause[0] = a;
76 : 5502060 : clause[1] = b;
77 : 11004100 : return assertClause(node, clause);
78 : : }
79 : :
80 : 3460560 : bool CnfStream::assertClause(TNode node,
81 : : SatLiteral a,
82 : : SatLiteral b,
83 : : SatLiteral c)
84 : : {
85 : 3460560 : SatClause clause(3);
86 : 3460560 : clause[0] = a;
87 : 3460560 : clause[1] = b;
88 : 3460560 : clause[2] = c;
89 : 6921130 : return assertClause(node, clause);
90 : : }
91 : :
92 : 136736000 : bool CnfStream::hasLiteral(TNode n) const {
93 : 136736000 : NodeToLiteralMap::const_iterator find = d_nodeToLiteralMap.find(n);
94 : 136736000 : return find != d_nodeToLiteralMap.end();
95 : : }
96 : :
97 : 8069530 : void CnfStream::ensureMappingForLiteral(TNode n)
98 : : {
99 : 8069530 : SatLiteral lit = getLiteral(n);
100 [ + + ]: 8069530 : if (!d_literalToNodeMap.contains(lit))
101 : : {
102 : : // Store backward-mappings
103 : 449 : d_literalToNodeMap.insert(lit, n);
104 : 449 : d_literalToNodeMap.insert(~lit, n.notNode());
105 : : }
106 : 8069530 : }
107 : :
108 : 7801160 : void CnfStream::ensureLiteral(TNode n)
109 : : {
110 : 7801160 : 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 [ + - ]: 7801160 : Trace("cnf") << "ensureLiteral(" << n << ")\n";
119 : 7801160 : TimerStat::CodeTimer codeTimer(d_stats.d_cnfConversionTime, true);
120 [ + + ]: 7801160 : if (hasLiteral(n))
121 : : {
122 : 7754160 : ensureMappingForLiteral(n);
123 : 7754160 : return;
124 : : }
125 : : // remove top level negation
126 [ + + ]: 46993 : n = n.getKind() == Kind::NOT ? n[0] : n;
127 [ + + ][ + + ]: 46993 : 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 : 35139 : d_removable = false;
134 : :
135 : 35139 : SatLiteral lit = toCNF(n, false);
136 : :
137 : : // Store backward-mappings
138 : : // These may already exist
139 : 35139 : d_literalToNodeMap.insert_safe(lit, n);
140 : 35139 : d_literalToNodeMap.insert_safe(~lit, n.notNode());
141 : : }
142 : : else
143 : : {
144 : : // We have a theory atom or variable.
145 : 11854 : convertAtom(n);
146 : : }
147 : : }
148 : :
149 : 3927190 : SatLiteral CnfStream::newLiteral(TNode node,
150 : : bool isTheoryAtom,
151 : : bool notifyTheory,
152 : : bool canEliminate)
153 : : {
154 [ + - ]: 7854370 : Trace("cnf") << d_name << "::newLiteral(" << node << ", " << isTheoryAtom
155 : 0 : << ")\n"
156 : 3927190 : << push;
157 [ - + ][ - + ]: 3927190 : Assert(node.getKind() != Kind::NOT);
[ - - ]
158 : :
159 : : // if we are tracking formulas, everything is a theory atom
160 [ + + ][ - + ]: 3927190 : 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 : 3927190 : SatLiteral lit;
168 [ + + ]: 3927190 : if (!hasLiteral(node))
169 : : {
170 [ + - ]: 3927180 : Trace("cnf") << d_name << "::newLiteral: node already registered\n";
171 : : // If no literal, we'll make one
172 [ + + ]: 3927180 : if (node.getKind() == Kind::CONST_BOOLEAN)
173 : : {
174 [ + - ]: 104302 : Trace("cnf") << d_name << "::newLiteral: boolean const\n";
175 [ + + ]: 104302 : if (node.getConst<bool>())
176 : : {
177 : 52088 : lit = SatLiteral(d_satSolver->trueVar());
178 : : }
179 : : else
180 : : {
181 : 52214 : lit = SatLiteral(d_satSolver->falseVar());
182 : : }
183 : : }
184 : : else
185 : : {
186 [ + - ]: 3822880 : Trace("cnf") << d_name << "::newLiteral: new var\n";
187 : 3822880 : lit = SatLiteral(d_satSolver->newVar(isTheoryAtom, canEliminate));
188 : 3822880 : d_stats.d_numAtoms++;
189 : : }
190 : 3927180 : d_nodeToLiteralMap.insert(node, lit);
191 : 3927180 : d_nodeToLiteralMap.insert(node.notNode(), ~lit);
192 : : }
193 : : else
194 : : {
195 [ + - ]: 7 : Trace("cnf") << d_name << "::newLiteral: node already registered\n";
196 : 7 : lit = getLiteral(node);
197 : : }
198 : :
199 : : // If it's a theory literal, need to store it for back queries
200 [ + + ][ + + ]: 3927190 : if (isTheoryAtom || d_flitPolicy == FormulaLitPolicy::TRACK
201 [ - + ]: 1270180 : || d_flitPolicy == FormulaLitPolicy::TRACK_AND_NOTIFY_VAR)
202 : : {
203 : 2657000 : d_literalToNodeMap.insert_safe(lit, node);
204 : 2657000 : d_literalToNodeMap.insert_safe(~lit, node.notNode());
205 : : }
206 : :
207 : : // If a theory literal, we pre-register it
208 [ + + ]: 3927190 : if (notifyTheory)
209 : : {
210 : : // In case we are re-entered due to lemmas, save our state
211 : 1639870 : bool backupRemovable = d_removable;
212 : 1639880 : d_registrar->notifySatLiteral(node);
213 : 1639850 : d_removable = backupRemovable;
214 : : }
215 : : // Here, you can have it
216 [ + - ]: 3927170 : Trace("cnf") << "newLiteral(" << node << ") => " << lit << "\n" << pop;
217 : 3927170 : return lit;
218 : : }
219 : :
220 : 107965000 : TNode CnfStream::getNode(const SatLiteral& literal)
221 : : {
222 [ - + ][ - + ]: 107965000 : Assert(d_literalToNodeMap.find(literal) != d_literalToNodeMap.end());
[ - - ]
223 [ + - ]: 107965000 : Trace("cnf") << "getNode(" << literal << ")\n";
224 [ + - ]: 215930000 : Trace("cnf") << "getNode(" << literal << ") => "
225 : 107965000 : << d_literalToNodeMap[literal] << "\n";
226 : 107965000 : return d_literalToNodeMap[literal];
227 : : }
228 : :
229 : 2484740 : const CnfStream::NodeToLiteralMap& CnfStream::getTranslationCache() const
230 : : {
231 : 2484740 : return d_nodeToLiteralMap;
232 : : }
233 : :
234 : 12308500 : const CnfStream::LiteralToNodeMap& CnfStream::getNodeCache() const
235 : : {
236 : 12308500 : return d_literalToNodeMap;
237 : : }
238 : :
239 : 36100 : void CnfStream::getBooleanVariables(std::vector<TNode>& outputVariables) const {
240 : 36100 : outputVariables.insert(outputVariables.end(),
241 : : d_booleanVariables.begin(),
242 : 72200 : d_booleanVariables.end());
243 : 36100 : }
244 : :
245 : 0 : bool CnfStream::isNotifyFormula(TNode node) const
246 : : {
247 : 0 : return d_notifyFormulas.find(node) != d_notifyFormulas.end();
248 : : }
249 : :
250 : 1687900 : SatLiteral CnfStream::convertAtom(TNode node)
251 : : {
252 [ + - ]: 1687900 : Trace("cnf") << "convertAtom(" << node << ")\n";
253 : :
254 [ - + ][ - + ]: 1687900 : Assert(!hasLiteral(node)) << "atom already mapped!";
[ - - ]
255 : :
256 : 1687900 : bool theoryLiteral = false;
257 : 1687900 : bool canEliminate = true;
258 : 1687900 : 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 : 1687900 : bool isInternalBoolVar = false;
267 [ + + ]: 1687900 : if (node.isVar())
268 : : {
269 : 51551 : isInternalBoolVar = !d_env.isBooleanTermSkolem(node);
270 : : }
271 [ + + ]: 1687900 : if (isInternalBoolVar)
272 : : {
273 : 48027 : 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 [ - + ]: 48027 : if (d_flitPolicy == FormulaLitPolicy::TRACK_AND_NOTIFY_VAR)
277 : : {
278 : 0 : theoryLiteral = true;
279 : : }
280 : : }
281 : : else
282 : : {
283 : 1639870 : theoryLiteral = true;
284 : 1639870 : canEliminate = false;
285 : 1639870 : preRegister = true;
286 : : }
287 : :
288 : : // Make a new literal (variables are not considered theory literals)
289 : 1687910 : SatLiteral lit = newLiteral(node, theoryLiteral, preRegister, canEliminate);
290 : : // Return the resulting literal
291 : 1687880 : return lit;
292 : : }
293 : :
294 : 128154000 : SatLiteral CnfStream::getLiteral(TNode node) {
295 [ - + ][ - + ]: 128154000 : Assert(!node.isNull()) << "CnfStream: can't getLiteral() of null node";
[ - - ]
296 : :
297 [ - + ][ - - ]: 256308000 : Assert(d_nodeToLiteralMap.contains(node))
298 [ - + ][ - + ]: 128154000 : << "Literal not in the CNF Cache: " << node << "\n";
[ - - ]
299 : :
300 : 128154000 : SatLiteral literal = d_nodeToLiteralMap[node];
301 [ + - ]: 256308000 : Trace("cnf") << "CnfStream::getLiteral(" << node << ") => " << literal
302 : 128154000 : << "\n";
303 : 128154000 : return literal;
304 : : }
305 : :
306 : 256816 : void CnfStream::handleXor(TNode xorNode)
307 : : {
308 [ - + ][ - + ]: 256816 : Assert(!hasLiteral(xorNode)) << "Atom already mapped!";
[ - - ]
309 [ - + ][ - + ]: 256816 : Assert(xorNode.getKind() == Kind::XOR) << "Expecting an XOR expression!";
[ - - ]
310 [ - + ][ - + ]: 256816 : Assert(xorNode.getNumChildren() == 2) << "Expecting exactly 2 children!";
[ - - ]
311 [ - + ][ - + ]: 256816 : Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
[ - - ]
312 [ + - ]: 256816 : Trace("cnf") << "CnfStream::handleXor(" << xorNode << ")\n";
313 : :
314 : 256816 : SatLiteral a = getLiteral(xorNode[0]);
315 : 256816 : SatLiteral b = getLiteral(xorNode[1]);
316 : :
317 : 256816 : SatLiteral xorLit = newLiteral(xorNode);
318 : :
319 : 256816 : assertClause(xorNode.negate(), a, b, ~xorLit);
320 : 256816 : assertClause(xorNode.negate(), ~a, ~b, ~xorLit);
321 : 256816 : assertClause(xorNode, a, ~b, xorLit);
322 : 256816 : assertClause(xorNode, ~a, b, xorLit);
323 : 256816 : }
324 : :
325 : 308395 : void CnfStream::handleOr(TNode orNode)
326 : : {
327 [ - + ][ - + ]: 308395 : Assert(!hasLiteral(orNode)) << "Atom already mapped!";
[ - - ]
328 [ - + ][ - + ]: 308395 : Assert(orNode.getKind() == Kind::OR) << "Expecting an OR expression!";
[ - - ]
329 [ - + ][ - + ]: 308395 : Assert(orNode.getNumChildren() > 1) << "Expecting more then 1 child!";
[ - - ]
330 [ - + ][ - + ]: 308395 : Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
[ - - ]
331 [ + - ]: 308395 : Trace("cnf") << "CnfStream::handleOr(" << orNode << ")\n";
332 : :
333 : : // Number of children
334 : 308395 : size_t numChildren = orNode.getNumChildren();
335 : :
336 : : // Get the literal for this node
337 : 308395 : SatLiteral orLit = newLiteral(orNode);
338 : :
339 : : // Transform all the children first
340 : 308395 : SatClause clause(numChildren + 1);
341 [ + + ]: 1119250 : for (size_t i = 0; i < numChildren; ++i)
342 : : {
343 : 810858 : 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 : 810858 : 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 : 308395 : clause[numChildren] = ~orLit;
354 : : // This needs to go last, as the clause might get modified by the SAT solver
355 : 308395 : assertClause(orNode.negate(), clause);
356 : 308395 : }
357 : :
358 : 631167 : void CnfStream::handleAnd(TNode andNode)
359 : : {
360 [ - + ][ - + ]: 631167 : Assert(!hasLiteral(andNode)) << "Atom already mapped!";
[ - - ]
361 [ - + ][ - + ]: 631167 : Assert(andNode.getKind() == Kind::AND) << "Expecting an AND expression!";
[ - - ]
362 [ - + ][ - + ]: 631167 : Assert(andNode.getNumChildren() > 1) << "Expecting more than 1 child!";
[ - - ]
363 [ - + ][ - + ]: 631167 : Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
[ - - ]
364 [ + - ]: 631167 : Trace("cnf") << "handleAnd(" << andNode << ")\n";
365 : :
366 : : // Number of children
367 : 631167 : size_t numChildren = andNode.getNumChildren();
368 : :
369 : : // Get the literal for this node
370 : 631167 : SatLiteral andLit = newLiteral(andNode);
371 : :
372 : : // Transform all the children first (remembering the negation)
373 : 631167 : SatClause clause(numChildren + 1);
374 [ + + ]: 3485700 : for (size_t i = 0; i < numChildren; ++i)
375 : : {
376 : 2854530 : 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 : 2854530 : 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 : 631167 : clause[numChildren] = andLit;
388 : : // This needs to go last, as the clause might get modified by the SAT solver
389 : 631167 : assertClause(andNode, clause);
390 : 631167 : }
391 : :
392 : 2744 : void CnfStream::handleImplies(TNode impliesNode)
393 : : {
394 [ - + ][ - + ]: 2744 : Assert(!hasLiteral(impliesNode)) << "Atom already mapped!";
[ - - ]
395 [ - + ][ - + ]: 2744 : Assert(impliesNode.getKind() == Kind::IMPLIES)
[ - - ]
396 : 0 : << "Expecting an IMPLIES expression!";
397 [ - + ][ - + ]: 2744 : Assert(impliesNode.getNumChildren() == 2) << "Expecting exactly 2 children!";
[ - - ]
398 [ - + ][ - + ]: 2744 : Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
[ - - ]
399 [ + - ]: 2744 : Trace("cnf") << "handleImplies(" << impliesNode << ")\n";
400 : :
401 : : // Convert the children to cnf
402 : 2744 : SatLiteral a = getLiteral(impliesNode[0]);
403 : 2744 : SatLiteral b = getLiteral(impliesNode[1]);
404 : :
405 : 2744 : SatLiteral impliesLit = newLiteral(impliesNode);
406 : :
407 : : // lit -> (a->b)
408 : : // ~lit | ~ a | b
409 : 2744 : assertClause(impliesNode.negate(), ~impliesLit, ~a, b);
410 : :
411 : : // (a->b) -> lit
412 : : // ~(~a | b) | lit
413 : : // (a | l) & (~b | l)
414 : 2744 : assertClause(impliesNode, a, impliesLit);
415 : 2744 : assertClause(impliesNode, ~b, impliesLit);
416 : 2744 : }
417 : :
418 : 223275 : void CnfStream::handleIff(TNode iffNode)
419 : : {
420 [ - + ][ - + ]: 223275 : Assert(!hasLiteral(iffNode)) << "Atom already mapped!";
[ - - ]
421 [ - + ][ - + ]: 223275 : Assert(iffNode.getKind() == Kind::EQUAL) << "Expecting an EQUAL expression!";
[ - - ]
422 [ - + ][ - + ]: 223275 : Assert(iffNode.getNumChildren() == 2) << "Expecting exactly 2 children!";
[ - - ]
423 [ - + ][ - + ]: 223275 : Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
[ - - ]
424 [ + - ]: 223275 : Trace("cnf") << "handleIff(" << iffNode << ")\n";
425 : :
426 : : // Convert the children to CNF
427 : 223275 : SatLiteral a = getLiteral(iffNode[0]);
428 : 223275 : SatLiteral b = getLiteral(iffNode[1]);
429 : :
430 : : // Get the now literal
431 : 223275 : 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 : 223275 : assertClause(iffNode.negate(), ~a, b, ~iffLit);
437 : 223275 : 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 : 223275 : assertClause(iffNode, ~a, ~b, iffLit);
445 : 223275 : assertClause(iffNode, a, b, iffLit);
446 : 223275 : }
447 : :
448 : 76860 : void CnfStream::handleIte(TNode iteNode)
449 : : {
450 [ - + ][ - + ]: 76860 : Assert(!hasLiteral(iteNode)) << "Atom already mapped!";
[ - - ]
451 [ - + ][ - + ]: 76860 : Assert(iteNode.getKind() == Kind::ITE);
[ - - ]
452 [ - + ][ - + ]: 76860 : Assert(iteNode.getNumChildren() == 3);
[ - - ]
453 [ - + ][ - + ]: 76860 : Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
[ - - ]
454 : 153720 : Trace("cnf") << "handleIte(" << iteNode[0] << " " << iteNode[1] << " "
455 [ - + ][ - + ]: 76860 : << iteNode[2] << ")\n";
[ - - ]
456 : :
457 : 76860 : SatLiteral condLit = getLiteral(iteNode[0]);
458 : 76860 : SatLiteral thenLit = getLiteral(iteNode[1]);
459 : 76860 : SatLiteral elseLit = getLiteral(iteNode[2]);
460 : :
461 : 76860 : 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 : 76860 : assertClause(iteNode.negate(), ~iteLit, thenLit, elseLit);
470 : 76860 : assertClause(iteNode.negate(), ~iteLit, ~condLit, thenLit);
471 : 76860 : 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 : 76860 : assertClause(iteNode, iteLit, ~thenLit, ~elseLit);
480 : 76860 : assertClause(iteNode, iteLit, ~condLit, ~thenLit);
481 : 76860 : assertClause(iteNode, iteLit, condLit, ~elseLit);
482 : 76860 : }
483 : :
484 : 2389050 : SatLiteral CnfStream::toCNF(TNode node, bool negated)
485 : : {
486 [ + - ]: 4778110 : Trace("cnf") << "toCNF(" << node
487 [ - - ]: 2389050 : << ", negated = " << (negated ? "true" : "false") << ")\n";
488 : :
489 : 4778110 : TNode cur;
490 : 2389050 : SatLiteral nodeLit;
491 : 4778110 : std::vector<TNode> visit;
492 : 4778110 : std::unordered_map<TNode, bool> cache;
493 : :
494 : 2389050 : visit.push_back(node);
495 [ + + ]: 12230400 : while (!visit.empty())
496 : : {
497 : 9841390 : cur = visit.back();
498 [ - + ][ - + ]: 9841390 : Assert(cur.getType().isBoolean());
[ - - ]
499 : :
500 [ + + ]: 9841390 : if (hasLiteral(cur))
501 : : {
502 : 5204680 : visit.pop_back();
503 : 7613810 : continue;
504 : : }
505 : :
506 : 4636710 : const auto& it = cache.find(cur);
507 [ + + ]: 4636710 : if (it == cache.end())
508 : : {
509 : 2409130 : cache.emplace(cur, false);
510 : 2409130 : Kind k = cur.getKind();
511 : : // Only traverse Boolean nodes
512 [ + + ][ + + ]: 2227580 : if (k == Kind::NOT || k == Kind::XOR || k == Kind::ITE
513 [ + + ][ + + ]: 1893900 : || k == Kind::IMPLIES || k == Kind::OR || k == Kind::AND
[ + + ]
514 : 4636710 : || (k == Kind::EQUAL && cur[0].getType().isBoolean()))
515 : : {
516 : : // Preserve the order of the recursive version
517 [ + + ]: 6724020 : for (size_t i = 0, size = cur.getNumChildren(); i < size; ++i)
518 : : {
519 : 5043200 : visit.push_back(cur[size - 1 - i]);
520 : : }
521 : : }
522 : 2409130 : continue;
523 : : }
524 [ + - ]: 2227580 : else if (!it->second)
525 : : {
526 : 2227580 : it->second = true;
527 : 2227580 : Kind k = cur.getKind();
528 [ - + ][ + + ]: 2227580 : switch (k)
[ + + ][ + ]
529 : : {
530 : 0 : case Kind::NOT: Assert(hasLiteral(cur[0])); break;
531 : 256816 : case Kind::XOR: handleXor(cur); break;
532 : 76860 : case Kind::ITE: handleIte(cur); break;
533 : 2744 : case Kind::IMPLIES: handleImplies(cur); break;
534 : 308395 : case Kind::OR: handleOr(cur); break;
535 : 631167 : case Kind::AND: handleAnd(cur); break;
536 : 951593 : default:
537 : 951593 : if (k == Kind::EQUAL && cur[0].getType().isBoolean())
538 : : {
539 : 223275 : handleIff(cur);
540 : : }
541 : : else
542 : : {
543 : 728334 : convertAtom(cur);
544 : : }
545 : 951577 : break;
546 : : }
547 : : }
548 : 2227560 : visit.pop_back();
549 : : }
550 : :
551 : 2389040 : nodeLit = getLiteral(node);
552 [ + - ]: 4778070 : Trace("cnf") << "toCNF(): resulting literal: "
553 [ - - ]: 2389040 : << (!negated ? nodeLit : ~nodeLit) << "\n";
554 [ + + ]: 4778070 : return negated ? ~nodeLit : nodeLit;
555 : : }
556 : :
557 : 100208 : void CnfStream::convertAndAssertAnd(TNode node, bool negated)
558 : : {
559 [ - + ][ - + ]: 100208 : Assert(node.getKind() == Kind::AND);
[ - - ]
560 [ + - ]: 200416 : Trace("cnf") << "CnfStream::convertAndAssertAnd(" << node
561 [ - - ]: 100208 : << ", negated = " << (negated ? "true" : "false") << ")\n";
562 [ + + ]: 100208 : if (!negated) {
563 : : // If the node is a conjunction, we handle each conjunct separately
564 : 58426 : for(TNode::const_iterator conjunct = node.begin(), node_end = node.end();
565 [ + + ]: 58426 : conjunct != node_end; ++conjunct ) {
566 : 44810 : convertAndAssert(*conjunct, false);
567 : : }
568 : : } else {
569 : : // If the node is a disjunction, we construct a clause and assert it
570 : 86588 : int nChildren = node.getNumChildren();
571 : 86588 : SatClause clause(nChildren);
572 : 86588 : TNode::const_iterator disjunct = node.begin();
573 [ + + ]: 1247160 : for(int i = 0; i < nChildren; ++ disjunct, ++ i) {
574 [ - + ][ - + ]: 1160570 : Assert(disjunct != node.end());
[ - - ]
575 : 1160570 : clause[i] = toCNF(*disjunct, true);
576 : : }
577 [ - + ][ - + ]: 86588 : Assert(disjunct == node.end());
[ - - ]
578 : 86588 : assertClause(node.negate(), clause);
579 : : }
580 : 100206 : }
581 : :
582 : 233266 : void CnfStream::convertAndAssertOr(TNode node, bool negated)
583 : : {
584 [ - + ][ - + ]: 233266 : Assert(node.getKind() == Kind::OR);
[ - - ]
585 [ + - ]: 466532 : Trace("cnf") << "CnfStream::convertAndAssertOr(" << node
586 [ - - ]: 233266 : << ", negated = " << (negated ? "true" : "false") << ")\n";
587 [ + + ]: 233266 : if (!negated) {
588 : : // If the node is a disjunction, we construct a clause and assert it
589 : 233052 : int nChildren = node.getNumChildren();
590 : 233052 : SatClause clause(nChildren);
591 : 233052 : TNode::const_iterator disjunct = node.begin();
592 [ + + ]: 894011 : for(int i = 0; i < nChildren; ++ disjunct, ++ i) {
593 [ - + ][ - + ]: 660959 : Assert(disjunct != node.end());
[ - - ]
594 : 660959 : clause[i] = toCNF(*disjunct, false);
595 : : }
596 [ - + ][ - + ]: 233052 : Assert(disjunct == node.end());
[ - - ]
597 : 233052 : assertClause(node, clause);
598 : : } else {
599 : : // If the node is a conjunction, we handle each conjunct separately
600 : 1293 : for(TNode::const_iterator conjunct = node.begin(), node_end = node.end();
601 [ + + ]: 1293 : conjunct != node_end; ++conjunct ) {
602 : 1079 : convertAndAssert(*conjunct, true);
603 : : }
604 : : }
605 : 233266 : }
606 : :
607 : 70 : void CnfStream::convertAndAssertXor(TNode node, bool negated)
608 : : {
609 [ - + ][ - + ]: 70 : Assert(node.getKind() == Kind::XOR);
[ - - ]
610 [ + - ]: 140 : Trace("cnf") << "CnfStream::convertAndAssertXor(" << node
611 [ - - ]: 70 : << ", negated = " << (negated ? "true" : "false") << ")\n";
612 [ + + ]: 70 : if (!negated) {
613 : : // p XOR q
614 : 66 : SatLiteral p = toCNF(node[0], false);
615 : 66 : SatLiteral q = toCNF(node[1], false);
616 : : // Construct the clauses (p => !q) and (!q => p)
617 : 132 : SatClause clause1(2);
618 : 66 : clause1[0] = ~p;
619 : 66 : clause1[1] = ~q;
620 : 66 : assertClause(node, clause1);
621 : 66 : SatClause clause2(2);
622 : 66 : clause2[0] = p;
623 : 66 : clause2[1] = q;
624 : 66 : 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 : 70 : }
640 : :
641 : 8687 : void CnfStream::convertAndAssertIff(TNode node, bool negated)
642 : : {
643 [ - + ][ - + ]: 8687 : Assert(node.getKind() == Kind::EQUAL);
[ - - ]
644 [ + - ]: 17374 : Trace("cnf") << "CnfStream::convertAndAssertIff(" << node
645 [ - - ]: 8687 : << ", negated = " << (negated ? "true" : "false") << ")\n";
646 [ + + ]: 8687 : if (!negated) {
647 : : // p <=> q
648 : 8191 : SatLiteral p = toCNF(node[0], false);
649 : 8191 : SatLiteral q = toCNF(node[1], false);
650 : : // Construct the clauses (p => q) and (q => p)
651 : 16382 : SatClause clause1(2);
652 : 8191 : clause1[0] = ~p;
653 : 8191 : clause1[1] = q;
654 : 8191 : assertClause(node, clause1);
655 : 8191 : SatClause clause2(2);
656 : 8191 : clause2[0] = p;
657 : 8191 : clause2[1] = ~q;
658 : 8191 : assertClause(node, clause2);
659 : : } else {
660 : : // !(p <=> q) is the same as p XOR q
661 : 496 : SatLiteral p = toCNF(node[0], false);
662 : 496 : SatLiteral q = toCNF(node[1], false);
663 : : // Construct the clauses (p => !q) and (!q => p)
664 : 992 : SatClause clause1(2);
665 : 496 : clause1[0] = ~p;
666 : 496 : clause1[1] = ~q;
667 : 496 : assertClause(node.negate(), clause1);
668 : 496 : SatClause clause2(2);
669 : 496 : clause2[0] = p;
670 : 496 : clause2[1] = q;
671 : 496 : assertClause(node.negate(), clause2);
672 : : }
673 : 8687 : }
674 : :
675 : 57856 : void CnfStream::convertAndAssertImplies(TNode node, bool negated)
676 : : {
677 [ - + ][ - + ]: 57856 : Assert(node.getKind() == Kind::IMPLIES);
[ - - ]
678 [ + - ]: 115712 : Trace("cnf") << "CnfStream::convertAndAssertImplies(" << node
679 [ - - ]: 57856 : << ", negated = " << (negated ? "true" : "false") << ")\n";
680 [ + + ]: 57856 : if (!negated) {
681 : : // p => q
682 : 57677 : SatLiteral p = toCNF(node[0], false);
683 : 57677 : SatLiteral q = toCNF(node[1], false);
684 : : // Construct the clause ~p || q
685 : 57677 : SatClause clause(2);
686 : 57677 : clause[0] = ~p;
687 : 57677 : clause[1] = q;
688 : 57677 : 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 : 57856 : }
695 : :
696 : 19781 : void CnfStream::convertAndAssertIte(TNode node, bool negated)
697 : : {
698 [ - + ][ - + ]: 19781 : Assert(node.getKind() == Kind::ITE);
[ - - ]
699 [ + - ]: 39562 : Trace("cnf") << "CnfStream::convertAndAssertIte(" << node
700 [ - - ]: 19781 : << ", negated = " << (negated ? "true" : "false") << ")\n";
701 : : // ITE(p, q, r)
702 : 19781 : SatLiteral p = toCNF(node[0], false);
703 : 19781 : SatLiteral q = toCNF(node[1], negated);
704 : 19781 : 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 : 39562 : Node nnode = node;
711 [ + + ]: 19781 : if( negated ){
712 : 105 : nnode = node.negate();
713 : : }
714 : 39562 : SatClause clause1(2);
715 : 19781 : clause1[0] = ~p;
716 : 19781 : clause1[1] = q;
717 : 19781 : assertClause(nnode, clause1);
718 : 19781 : SatClause clause2(2);
719 : 19781 : clause2[0] = p;
720 : 19781 : clause2[1] = r;
721 : 19781 : assertClause(nnode, clause2);
722 : 19781 : }
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 : 713798 : void CnfStream::convertAndAssert(TNode node, bool removable, bool negated)
728 : : {
729 [ + - ]: 1427600 : Trace("cnf") << "convertAndAssert(" << node
730 [ - - ]: 0 : << ", negated = " << (negated ? "true" : "false")
731 [ - - ]: 713798 : << ", removable = " << (removable ? "true" : "false") << ")\n";
732 : 713798 : d_removable = removable;
733 : 713814 : TimerStat::CodeTimer codeTimer(d_stats.d_cnfConversionTime, true);
734 : 713814 : convertAndAssert(node, negated);
735 : 713782 : }
736 : :
737 : 865928 : void CnfStream::convertAndAssert(TNode node, bool negated)
738 : : {
739 [ + - ]: 1731860 : Trace("cnf") << "convertAndAssert(" << node
740 [ - - ]: 865928 : << ", negated = " << (negated ? "true" : "false") << ")\n";
741 : :
742 : 865928 : resourceManager()->spendResource(Resource::CnfStep);
743 : :
744 [ + + ][ + + ]: 865928 : switch(node.getKind()) {
[ + + ][ + + ]
745 : 100210 : case Kind::AND: convertAndAssertAnd(node, negated); break;
746 : 233266 : case Kind::OR: convertAndAssertOr(node, negated); break;
747 : 70 : case Kind::XOR: convertAndAssertXor(node, negated); break;
748 : 57856 : case Kind::IMPLIES: convertAndAssertImplies(node, negated); break;
749 : 19781 : case Kind::ITE: convertAndAssertIte(node, negated); break;
750 : 105895 : case Kind::NOT: convertAndAssert(node[0], !negated); break;
751 : 85066 : case Kind::EQUAL:
752 [ + + ]: 85066 : if (node[0].getType().isBoolean())
753 : : {
754 : 8687 : convertAndAssertIff(node, negated);
755 : 8687 : break;
756 : : }
757 : : CVC5_FALLTHROUGH;
758 : : default:
759 : : {
760 : 340191 : Node nnode = node;
761 [ + + ]: 340175 : if (negated)
762 : : {
763 : 99559 : nnode = node.negate();
764 : : }
765 : : // Atoms
766 : 340191 : assertClause(nnode, toCNF(node, negated));
767 : : }
768 : 340159 : break;
769 : : }
770 : 865900 : }
771 : :
772 : 92096 : CnfStream::Statistics::Statistics(StatisticsRegistry& sr,
773 : 92096 : const std::string& name)
774 : : : d_cnfConversionTime(
775 : 92096 : sr.registerTimer(name + "::CnfStream::cnfConversionTime")),
776 : 92096 : d_numAtoms(sr.registerInt(name + "::CnfStream::numAtoms"))
777 : : {
778 : 92096 : }
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
|
