1 /********************* */
2 /*! \file cnf_stream.cpp
4 ** Original author: taking
5 ** Major contributors: dejan
6 ** Minor contributors (to current version): mdeters, cconway
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief A CNF converter that takes in asserts and has the side effect
15 ** of given an equisatisfiable stream of assertions to PropEngine.
17 ** A CNF converter that takes in asserts and has the side effect
18 ** of given an equisatisfiable stream of assertions to PropEngine.
22 #include "prop/cnf_stream.h"
23 #include "prop/prop_engine.h"
24 #include "expr/node.h"
25 #include "util/Assert.h"
26 #include "util/output.h"
31 using namespace CVC4::kind
;
36 CnfStream::CnfStream(SatInputInterface
*satSolver
) :
37 d_satSolver(satSolver
) {
40 TseitinCnfStream::TseitinCnfStream(SatInputInterface
* satSolver
) :
41 CnfStream(satSolver
) {
44 void CnfStream::assertClause(TNode node
, SatClause
& c
) {
45 Debug("cnf") << "Inserting into stream " << c
<< endl
;
46 d_satSolver
->addClause(c
, d_assertingLemma
);
49 void CnfStream::assertClause(TNode node
, SatLiteral a
) {
52 assertClause(node
, clause
);
55 void CnfStream::assertClause(TNode node
, SatLiteral a
, SatLiteral b
) {
59 assertClause(node
, clause
);
62 void CnfStream::assertClause(TNode node
, SatLiteral a
, SatLiteral b
, SatLiteral c
) {
67 assertClause(node
, clause
);
70 bool CnfStream::isCached(TNode n
) const {
71 return d_translationCache
.find(n
) != d_translationCache
.end();
74 SatLiteral
CnfStream::lookupInCache(TNode n
) const {
75 Assert(isCached(n
), "Node is not in CNF translation cache");
76 return d_translationCache
.find(n
)->second
;
79 void CnfStream::cacheTranslation(TNode node
, SatLiteral lit
) {
80 Debug("cnf") << "caching translation " << node
<< " to " << lit
<< endl
;
81 // We always cash both the node and the negation at the same time
82 d_translationCache
[node
] = lit
;
83 d_translationCache
[node
.notNode()] = ~lit
;
86 SatLiteral
CnfStream::newLiteral(TNode node
, bool theoryLiteral
) {
87 SatLiteral lit
= Minisat::mkLit(d_satSolver
->newVar(theoryLiteral
));
88 cacheTranslation(node
, lit
);
90 d_nodeCache
[lit
] = node
;
91 d_nodeCache
[~lit
] = node
.notNode();
96 Node
CnfStream::getNode(const SatLiteral
& literal
) {
97 NodeCache::iterator find
= d_nodeCache
.find(literal
);
98 Assert(find
!= d_nodeCache
.end());
102 SatLiteral
CnfStream::convertAtom(TNode node
) {
103 Debug("cnf") << "convertAtom(" << node
<< ")" << endl
;
105 Assert(!isCached(node
), "atom already mapped!");
107 bool theoryLiteral
= node
.getKind() != kind::VARIABLE
;
108 SatLiteral lit
= newLiteral(node
, theoryLiteral
);
110 if(node
.getKind() == kind::CONST_BOOLEAN
) {
111 if(node
.getConst
<bool>()) {
112 assertClause(node
, lit
);
114 assertClause(node
, ~lit
);
121 SatLiteral
CnfStream::getLiteral(TNode node
) {
122 TranslationCache::iterator find
= d_translationCache
.find(node
);
123 Assert(find
!= d_translationCache
.end(), "Literal not in the CNF Cache");
124 SatLiteral literal
= find
->second
;
125 Debug("cnf") << "CnfStream::getLiteral(" << node
<< ") => " << literal
<< std::endl
;
129 SatLiteral
TseitinCnfStream::handleXor(TNode xorNode
) {
130 Assert(!isCached(xorNode
), "Atom already mapped!");
131 Assert(xorNode
.getKind() == XOR
, "Expecting an XOR expression!");
132 Assert(xorNode
.getNumChildren() == 2, "Expecting exactly 2 children!");
134 SatLiteral a
= toCNF(xorNode
[0]);
135 SatLiteral b
= toCNF(xorNode
[1]);
137 SatLiteral xorLit
= newLiteral(xorNode
);
139 assertClause(xorNode
, a
, b
, ~xorLit
);
140 assertClause(xorNode
, ~a
, ~b
, ~xorLit
);
141 assertClause(xorNode
, a
, ~b
, xorLit
);
142 assertClause(xorNode
, ~a
, b
, xorLit
);
147 SatLiteral
TseitinCnfStream::handleOr(TNode orNode
) {
148 Assert(!isCached(orNode
), "Atom already mapped!");
149 Assert(orNode
.getKind() == OR
, "Expecting an OR expression!");
150 Assert(orNode
.getNumChildren() > 1, "Expecting more then 1 child!");
152 // Number of children
153 unsigned n_children
= orNode
.getNumChildren();
155 // Transform all the children first
156 TNode::const_iterator node_it
= orNode
.begin();
157 TNode::const_iterator node_it_end
= orNode
.end();
158 SatClause
clause(n_children
+ 1);
159 for(int i
= 0; node_it
!= node_it_end
; ++node_it
, ++i
) {
160 clause
[i
] = toCNF(*node_it
);
163 // Get the literal for this node
164 SatLiteral orLit
= newLiteral(orNode
);
166 // lit <- (a_1 | a_2 | a_3 | ... | a_n)
167 // lit | ~(a_1 | a_2 | a_3 | ... | a_n)
168 // (lit | ~a_1) & (lit | ~a_2) & (lit & ~a_3) & ... & (lit & ~a_n)
169 for(unsigned i
= 0; i
< n_children
; ++i
) {
170 assertClause(orNode
, orLit
, ~clause
[i
]);
173 // lit -> (a_1 | a_2 | a_3 | ... | a_n)
174 // ~lit | a_1 | a_2 | a_3 | ... | a_n
175 clause
[n_children
] = ~orLit
;
176 // This needs to go last, as the clause might get modified by the SAT solver
177 assertClause(orNode
, clause
);
179 // Return the literal
183 SatLiteral
TseitinCnfStream::handleAnd(TNode andNode
) {
184 Assert(!isCached(andNode
), "Atom already mapped!");
185 Assert(andNode
.getKind() == AND
, "Expecting an AND expression!");
186 Assert(andNode
.getNumChildren() > 1, "Expecting more than 1 child!");
188 // Number of children
189 unsigned n_children
= andNode
.getNumChildren();
191 // Transform all the children first (remembering the negation)
192 TNode::const_iterator node_it
= andNode
.begin();
193 TNode::const_iterator node_it_end
= andNode
.end();
194 SatClause
clause(n_children
+ 1);
195 for(int i
= 0; node_it
!= node_it_end
; ++node_it
, ++i
) {
196 clause
[i
] = ~toCNF(*node_it
);
199 // Get the literal for this node
200 SatLiteral andLit
= newLiteral(andNode
);
202 // lit -> (a_1 & a_2 & a_3 & ... & a_n)
203 // ~lit | (a_1 & a_2 & a_3 & ... & a_n)
204 // (~lit | a_1) & (~lit | a_2) & ... & (~lit | a_n)
205 for(unsigned i
= 0; i
< n_children
; ++i
) {
206 assertClause(andNode
, ~andLit
, ~clause
[i
]);
209 // lit <- (a_1 & a_2 & a_3 & ... a_n)
210 // lit | ~(a_1 & a_2 & a_3 & ... & a_n)
211 // lit | ~a_1 | ~a_2 | ~a_3 | ... | ~a_n
212 clause
[n_children
] = andLit
;
213 // This needs to go last, as the clause might get modified by the SAT solver
214 assertClause(andNode
, clause
);
218 SatLiteral
TseitinCnfStream::handleImplies(TNode impliesNode
) {
219 Assert(!isCached(impliesNode
), "Atom already mapped!");
220 Assert(impliesNode
.getKind() == IMPLIES
, "Expecting an IMPLIES expression!");
221 Assert(impliesNode
.getNumChildren() == 2, "Expecting exactly 2 children!");
223 // Convert the children to cnf
224 SatLiteral a
= toCNF(impliesNode
[0]);
225 SatLiteral b
= toCNF(impliesNode
[1]);
227 SatLiteral impliesLit
= newLiteral(impliesNode
);
231 assertClause(impliesNode
, ~impliesLit
, ~a
, b
);
235 // (a | l) & (~b | l)
236 assertClause(impliesNode
, a
, impliesLit
);
237 assertClause(impliesNode
, ~b
, impliesLit
);
243 SatLiteral
TseitinCnfStream::handleIff(TNode iffNode
) {
244 Assert(!isCached(iffNode
), "Atom already mapped!");
245 Assert(iffNode
.getKind() == IFF
, "Expecting an IFF expression!");
246 Assert(iffNode
.getNumChildren() == 2, "Expecting exactly 2 children!");
248 Debug("cnf") << "handleIff(" << iffNode
<< ")" << endl
;
250 // Convert the children to CNF
251 SatLiteral a
= toCNF(iffNode
[0]);
252 SatLiteral b
= toCNF(iffNode
[1]);
254 // Get the now literal
255 SatLiteral iffLit
= newLiteral(iffNode
);
257 // lit -> ((a-> b) & (b->a))
258 // ~lit | ((~a | b) & (~b | a))
259 // (~a | b | ~lit) & (~b | a | ~lit)
260 assertClause(iffNode
, ~a
, b
, ~iffLit
);
261 assertClause(iffNode
, a
, ~b
, ~iffLit
);
264 // ~((a & b) | (~a & ~b)) | lit
265 // (~(a & b)) & (~(~a & ~b)) | lit
266 // ((~a | ~b) & (a | b)) | lit
267 // (~a | ~b | lit) & (a | b | lit)
268 assertClause(iffNode
, ~a
, ~b
, iffLit
);
269 assertClause(iffNode
, a
, b
, iffLit
);
275 SatLiteral
TseitinCnfStream::handleNot(TNode notNode
) {
276 Assert(!isCached(notNode
), "Atom already mapped!");
277 Assert(notNode
.getKind() == NOT
, "Expecting a NOT expression!");
278 Assert(notNode
.getNumChildren() == 1, "Expecting exactly 1 child!");
280 SatLiteral notLit
= ~toCNF(notNode
[0]);
282 // Since we don't introduce new variables, we need to cache the translation
283 cacheTranslation(notNode
, notLit
);
288 SatLiteral
TseitinCnfStream::handleIte(TNode iteNode
) {
289 Assert(iteNode
.getKind() == ITE
);
290 Assert(iteNode
.getNumChildren() == 3);
292 Debug("cnf") << "handleIte(" << iteNode
[0] << " " << iteNode
[1] << " " << iteNode
[2] << ")" << endl
;
294 SatLiteral condLit
= toCNF(iteNode
[0]);
295 SatLiteral thenLit
= toCNF(iteNode
[1]);
296 SatLiteral elseLit
= toCNF(iteNode
[2]);
298 SatLiteral iteLit
= newLiteral(iteNode
);
300 // If ITE is true then one of the branches is true and the condition
302 // lit -> (ite b t e)
303 // lit -> (t | e) & (b -> t) & (!b -> e)
304 // lit -> (t | e) & (!b | t) & (b | e)
305 // (!lit | t | e) & (!lit | !b | t) & (!lit | b | e)
306 assertClause(iteNode
, ~iteLit
, thenLit
, elseLit
);
307 assertClause(iteNode
, ~iteLit
, ~condLit
, thenLit
);
308 assertClause(iteNode
, ~iteLit
, condLit
, elseLit
);
310 // If ITE is false then one of the branches is false and the condition
312 // !lit -> !(ite b t e)
313 // !lit -> (!t | !e) & (b -> !t) & (!b -> !e)
314 // !lit -> (!t | !e) & (!b | !t) & (b | !e)
315 // (lit | !t | !e) & (lit | !b | !t) & (lit | b | !e)
316 assertClause(iteNode
, iteLit
, ~thenLit
, ~elseLit
);
317 assertClause(iteNode
, iteLit
, ~condLit
, ~thenLit
);
318 assertClause(iteNode
, iteLit
, condLit
, ~elseLit
);
324 SatLiteral
TseitinCnfStream::toCNF(TNode node
, bool negated
) {
325 Debug("cnf") << "toCNF(" << node
<< ", negated = " << (negated
? "true" : "false") << ")" << endl
;
328 Node negatedNode
= node
.notNode();
330 // If the non-negated node has already been translated, get the translation
332 nodeLit
= lookupInCache(node
);
334 // Handle each Boolean operator case
335 switch(node
.getKind()) {
337 nodeLit
= handleNot(node
);
340 nodeLit
= handleXor(node
);
343 nodeLit
= handleIte(node
);
346 nodeLit
= handleIff(node
);
349 nodeLit
= handleImplies(node
);
352 nodeLit
= handleOr(node
);
355 nodeLit
= handleAnd(node
);
358 if(node
[0].getType().isBoolean()) {
359 // should have an IFF instead
360 Unreachable("= Bool Bool shouldn't be possible ?!");
361 //nodeLit = handleIff(node[0].iffNode(node[1]));
363 nodeLit
= convertAtom(node
);
368 //TODO make sure this does not contain any boolean substructure
369 nodeLit
= convertAtom(node
);
371 //Node atomic = handleNonAtomicNode(node);
372 //return isCached(atomic) ? lookupInCache(atomic) : convertAtom(atomic);
377 // Return the appropriate (negated) literal
378 if (!negated
) return nodeLit
;
379 else return ~nodeLit
;
382 void TseitinCnfStream::convertAndAssertAnd(TNode node
, bool lemma
, bool negated
) {
383 Assert(node
.getKind() == AND
);
385 // If the node is a conjunction, we handle each conjunct separately
386 for(TNode::const_iterator conjunct
= node
.begin(), node_end
= node
.end();
387 conjunct
!= node_end
; ++conjunct
) {
388 convertAndAssert(*conjunct
, lemma
, false);
391 // If the node is a disjunction, we construct a clause and assert it
392 int nChildren
= node
.getNumChildren();
393 SatClause
clause(nChildren
);
394 TNode::const_iterator disjunct
= node
.begin();
395 for(int i
= 0; i
< nChildren
; ++ disjunct
, ++ i
) {
396 Assert( disjunct
!= node
.end() );
397 clause
[i
] = toCNF(*disjunct
, true);
399 Assert(disjunct
== node
.end());
400 assertClause(node
, clause
);
404 void TseitinCnfStream::convertAndAssertOr(TNode node
, bool lemma
, bool negated
) {
405 Assert(node
.getKind() == OR
);
407 // If the node is a disjunction, we construct a clause and assert it
408 int nChildren
= node
.getNumChildren();
409 SatClause
clause(nChildren
);
410 TNode::const_iterator disjunct
= node
.begin();
411 for(int i
= 0; i
< nChildren
; ++ disjunct
, ++ i
) {
412 Assert( disjunct
!= node
.end() );
413 clause
[i
] = toCNF(*disjunct
, false);
415 Assert(disjunct
== node
.end());
416 assertClause(node
, clause
);
418 // If the node is a conjunction, we handle each conjunct separately
419 for(TNode::const_iterator conjunct
= node
.begin(), node_end
= node
.end();
420 conjunct
!= node_end
; ++conjunct
) {
421 convertAndAssert(*conjunct
, lemma
, true);
426 void TseitinCnfStream::convertAndAssertXor(TNode node
, bool lemma
, bool negated
) {
429 SatLiteral p
= toCNF(node
[0], false);
430 SatLiteral q
= toCNF(node
[1], false);
431 // Construct the clauses (p => !q) and (!q => p)
432 SatClause
clause1(2);
435 assertClause(node
, clause1
);
436 SatClause
clause2(2);
439 assertClause(node
, clause2
);
441 // !(p XOR q) is the same as p <=> q
442 SatLiteral p
= toCNF(node
[0], false);
443 SatLiteral q
= toCNF(node
[1], false);
444 // Construct the clauses (p => q) and (q => p)
445 SatClause
clause1(2);
448 assertClause(node
, clause1
);
449 SatClause
clause2(2);
452 assertClause(node
, clause2
);
456 void TseitinCnfStream::convertAndAssertIff(TNode node
, bool lemma
, bool negated
) {
459 SatLiteral p
= toCNF(node
[0], false);
460 SatLiteral q
= toCNF(node
[1], false);
461 // Construct the clauses (p => q) and (q => p)
462 SatClause
clause1(2);
465 assertClause(node
, clause1
);
466 SatClause
clause2(2);
469 assertClause(node
, clause2
);
471 // !(p <=> q) is the same as p XOR q
472 SatLiteral p
= toCNF(node
[0], false);
473 SatLiteral q
= toCNF(node
[1], false);
474 // Construct the clauses (p => !q) and (!q => p)
475 SatClause
clause1(2);
478 assertClause(node
, clause1
);
479 SatClause
clause2(2);
482 assertClause(node
, clause2
);
486 void TseitinCnfStream::convertAndAssertImplies(TNode node
, bool lemma
, bool negated
) {
489 SatLiteral p
= toCNF(node
[0], false);
490 SatLiteral q
= toCNF(node
[1], false);
491 // Construct the clause ~p || q
495 assertClause(node
, clause
);
496 } else {// Construct the
497 // !(p => q) is the same as (p && ~q)
498 convertAndAssert(node
[0], lemma
, false);
499 convertAndAssert(node
[1], lemma
, true);
503 void TseitinCnfStream::convertAndAssertIte(TNode node
, bool lemma
, bool negated
) {
505 SatLiteral p
= toCNF(node
[0], false);
506 SatLiteral q
= toCNF(node
[1], negated
);
507 SatLiteral r
= toCNF(node
[2], negated
);
508 // Construct the clauses:
509 // (p => q) and (!p => r) and (!q => !p) and (!r => p)
510 SatClause
clause1(2);
513 assertClause(node
, clause1
);
514 SatClause
clause2(2);
517 assertClause(node
, clause2
);
518 SatClause
clause3(2);
521 assertClause(node
, clause3
);
522 SatClause
clause4(2);
525 assertClause(node
, clause4
);
528 // At the top level we must ensure that all clauses that are asserted are
529 // not unit, except for the direct assertions. This allows us to remove the
530 // clauses later when they are not needed anymore (lemmas for example).
531 void TseitinCnfStream::convertAndAssert(TNode node
, bool lemma
, bool negated
) {
532 Debug("cnf") << "convertAndAssert(" << node
<< ", negated = " << (negated
? "true" : "false") << ")" << endl
;
533 d_assertingLemma
= lemma
;
534 switch(node
.getKind()) {
536 convertAndAssertAnd(node
, lemma
, negated
);
539 convertAndAssertOr(node
, lemma
, negated
);
542 convertAndAssertIff(node
, lemma
, negated
);
545 convertAndAssertXor(node
, lemma
, negated
);
548 convertAndAssertImplies(node
, lemma
, negated
);
551 convertAndAssertIte(node
, lemma
, negated
);
554 convertAndAssert(node
[0], lemma
, !negated
);
558 assertClause(node
, toCNF(node
, negated
));
563 }/* CVC4::prop namespace */
564 }/* CVC4 namespace */