1 /********************* */
2 /*! \file cnf_stream.cpp
4 ** Original author: Tim King
5 ** Major contributors: Morgan Deters, Dejan Jovanovic
6 ** Minor contributors (to current version): Kshitij Bansal, Liana Hadarean, Christopher L. Conway
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2014 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief A CNF converter that takes in asserts and has the side effect
13 ** of given an equisatisfiable stream of assertions to PropEngine.
15 ** A CNF converter that takes in asserts and has the side effect
16 ** of given an equisatisfiable stream of assertions to PropEngine.
19 #include "prop/cnf_stream.h"
20 #include "prop/prop_engine.h"
21 #include "theory/theory_engine.h"
22 #include "theory/theory.h"
23 #include "expr/node.h"
24 #include "util/cvc4_assert.h"
25 #include "util/output.h"
26 #include "expr/command.h"
27 #include "expr/expr.h"
28 #include "prop/theory_proxy.h"
29 #include "theory/bv/options.h"
30 #include "proof/proof_manager.h"
31 #include "proof/sat_proof.h"
32 #include "prop/minisat/minisat.h"
36 using namespace CVC4::kind
;
39 # define CVC4_USE_REPLAY true
40 #else /* CVC4_REPLAY */
41 # define CVC4_USE_REPLAY false
42 #endif /* CVC4_REPLAY */
47 CnfStream::CnfStream(SatSolver
*satSolver
, Registrar
* registrar
, context::Context
* context
, bool fullLitToNodeMap
) :
48 d_satSolver(satSolver
),
49 d_booleanVariables(context
),
50 d_nodeToLiteralMap(context
),
51 d_literalToNodeMap(context
),
52 d_fullLitToNodeMap(fullLitToNodeMap
),
53 d_registrar(registrar
),
54 d_assertionTable(context
),
58 TseitinCnfStream::TseitinCnfStream(SatSolver
* satSolver
, Registrar
* registrar
, context::Context
* context
, bool fullLitToNodeMap
) :
59 CnfStream(satSolver
, registrar
, context
, fullLitToNodeMap
) {
62 void CnfStream::assertClause(TNode node
, SatClause
& c
) {
63 Debug("cnf") << "Inserting into stream " << c
<< endl
;
64 if(Dump
.isOn("clauses")) {
66 Dump("clauses") << AssertCommand(Expr(getNode(c
[0]).toExpr()));
69 NodeBuilder
<> b(kind::OR
);
70 for(unsigned i
= 0; i
< c
.size(); ++i
) {
74 Dump("clauses") << AssertCommand(Expr(n
.toExpr()));
77 d_satSolver
->addClause(c
, d_removable
, d_proofId
);
80 void CnfStream::assertClause(TNode node
, SatLiteral a
) {
83 assertClause(node
, clause
);
86 void CnfStream::assertClause(TNode node
, SatLiteral a
, SatLiteral b
) {
90 assertClause(node
, clause
);
93 void CnfStream::assertClause(TNode node
, SatLiteral a
, SatLiteral b
, SatLiteral c
) {
98 assertClause(node
, clause
);
101 bool CnfStream::hasLiteral(TNode n
) const {
102 NodeToLiteralMap::const_iterator find
= d_nodeToLiteralMap
.find(n
);
103 return find
!= d_nodeToLiteralMap
.end();
106 void TseitinCnfStream::ensureLiteral(TNode n
) {
107 // These are not removable and have no proof ID
109 d_proofId
= uint64_t(-1);
111 Debug("cnf") << "ensureLiteral(" << n
<< ")" << endl
;
113 SatLiteral lit
= getLiteral(n
);
114 if(!d_literalToNodeMap
.contains(lit
)){
115 // Store backward-mappings
116 d_literalToNodeMap
.insert(lit
, n
);
117 d_literalToNodeMap
.insert(~lit
, n
.notNode());
122 AlwaysAssertArgument(n
.getType().isBoolean(), n
,
123 "CnfStream::ensureLiteral() requires a node of Boolean type.\n"
126 n
.toString().c_str(),
127 n
.getType().toString().c_str());
129 bool negated CVC4_UNUSED
= false;
132 if(n
.getKind() == kind::NOT
) {
137 if( theory::Theory::theoryOf(n
) == theory::THEORY_BOOL
&&
139 // If we were called with something other than a theory atom (or
140 // Boolean variable), we get a SatLiteral that is definitionally
142 lit
= toCNF(n
, false);
144 // Store backward-mappings
145 // These may already exist
146 d_literalToNodeMap
.insert_safe(lit
, n
);
147 d_literalToNodeMap
.insert_safe(~lit
, n
.notNode());
149 // We have a theory atom or variable.
150 lit
= convertAtom(n
);
153 Assert(hasLiteral(n
) && getNode(lit
) == n
);
154 Debug("ensureLiteral") << "CnfStream::ensureLiteral(): out lit is " << lit
<< std::endl
;
157 SatLiteral
CnfStream::newLiteral(TNode node
, bool isTheoryAtom
, bool preRegister
, bool canEliminate
) {
158 Debug("cnf") << "newLiteral(" << node
<< ", " << isTheoryAtom
<< ")" << endl
;
159 Assert(node
.getKind() != kind::NOT
);
161 // Get the literal for this node
163 if (!hasLiteral(node
)) {
164 // If no literal, we'll make one
165 if (node
.getKind() == kind::CONST_BOOLEAN
) {
166 if (node
.getConst
<bool>()) {
167 lit
= SatLiteral(d_satSolver
->trueVar());
169 lit
= SatLiteral(d_satSolver
->falseVar());
172 lit
= SatLiteral(d_satSolver
->newVar(isTheoryAtom
, preRegister
, canEliminate
));
174 d_nodeToLiteralMap
.insert(node
, lit
);
175 d_nodeToLiteralMap
.insert(node
.notNode(), ~lit
);
177 lit
= getLiteral(node
);
180 // If it's a theory literal, need to store it for back queries
181 if ( isTheoryAtom
|| d_fullLitToNodeMap
||
182 ( CVC4_USE_REPLAY
&& options::replayLog() != NULL
) ||
183 (Dump
.isOn("clauses")) ) {
185 d_literalToNodeMap
.insert_safe(lit
, node
);
186 d_literalToNodeMap
.insert_safe(~lit
, node
.notNode());
189 // If a theory literal, we pre-register it
191 // In case we are re-entered due to lemmas, save our state
192 bool backupRemovable
= d_removable
;
193 uint64_t backupProofId
= d_proofId
;
194 d_registrar
->preRegister(node
);
195 d_removable
= backupRemovable
;
196 d_proofId
= backupProofId
;
199 // Here, you can have it
200 Debug("cnf") << "newLiteral(" << node
<< ") => " << lit
<< endl
;
205 TNode
CnfStream::getNode(const SatLiteral
& literal
) {
206 Debug("cnf") << "getNode(" << literal
<< ")" << endl
;
207 Debug("cnf") << "getNode(" << literal
<< ") => " << d_literalToNodeMap
[literal
] << endl
;
208 return d_literalToNodeMap
[literal
];
211 void CnfStream::getBooleanVariables(std::vector
<TNode
>& outputVariables
) const {
212 context::CDList
<TNode
>::const_iterator it
, it_end
;
213 for (it
= d_booleanVariables
.begin(); it
!= d_booleanVariables
.end(); ++ it
) {
214 outputVariables
.push_back(*it
);
218 SatLiteral
CnfStream::convertAtom(TNode node
) {
219 Debug("cnf") << "convertAtom(" << node
<< ")" << endl
;
221 Assert(!hasLiteral(node
), "atom already mapped!");
223 bool theoryLiteral
= false;
224 bool canEliminate
= true;
225 bool preRegister
= false;
227 // Is this a variable add it to the list
229 d_booleanVariables
.push_back(node
);
231 theoryLiteral
= true;
232 canEliminate
= false;
236 // Make a new literal (variables are not considered theory literals)
237 SatLiteral lit
= newLiteral(node
, theoryLiteral
, preRegister
, canEliminate
);
238 // Return the resulting literal
242 SatLiteral
CnfStream::getLiteral(TNode node
) {
243 Assert(!node
.isNull(), "CnfStream: can't getLiteral() of null node");
244 Assert(d_nodeToLiteralMap
.contains(node
), "Literal not in the CNF Cache: %s\n", node
.toString().c_str());
245 SatLiteral literal
= d_nodeToLiteralMap
[node
];
246 Debug("cnf") << "CnfStream::getLiteral(" << node
<< ") => " << literal
<< std::endl
;
250 SatLiteral
TseitinCnfStream::handleXor(TNode xorNode
) {
251 Assert(!hasLiteral(xorNode
), "Atom already mapped!");
252 Assert(xorNode
.getKind() == XOR
, "Expecting an XOR expression!");
253 Assert(xorNode
.getNumChildren() == 2, "Expecting exactly 2 children!");
254 Assert(!d_removable
, "Removable clauses can not contain Boolean structure");
256 SatLiteral a
= toCNF(xorNode
[0]);
257 SatLiteral b
= toCNF(xorNode
[1]);
259 SatLiteral xorLit
= newLiteral(xorNode
);
261 assertClause(xorNode
, a
, b
, ~xorLit
);
262 assertClause(xorNode
, ~a
, ~b
, ~xorLit
);
263 assertClause(xorNode
, a
, ~b
, xorLit
);
264 assertClause(xorNode
, ~a
, b
, xorLit
);
269 SatLiteral
TseitinCnfStream::handleOr(TNode orNode
) {
270 Assert(!hasLiteral(orNode
), "Atom already mapped!");
271 Assert(orNode
.getKind() == OR
, "Expecting an OR expression!");
272 Assert(orNode
.getNumChildren() > 1, "Expecting more then 1 child!");
273 Assert(!d_removable
, "Removable clauses can not contain Boolean structure");
275 // Number of children
276 unsigned n_children
= orNode
.getNumChildren();
278 // Transform all the children first
279 TNode::const_iterator node_it
= orNode
.begin();
280 TNode::const_iterator node_it_end
= orNode
.end();
281 SatClause
clause(n_children
+ 1);
282 for(int i
= 0; node_it
!= node_it_end
; ++node_it
, ++i
) {
283 clause
[i
] = toCNF(*node_it
);
286 // Get the literal for this node
287 SatLiteral orLit
= newLiteral(orNode
);
289 // lit <- (a_1 | a_2 | a_3 | ... | a_n)
290 // lit | ~(a_1 | a_2 | a_3 | ... | a_n)
291 // (lit | ~a_1) & (lit | ~a_2) & (lit & ~a_3) & ... & (lit & ~a_n)
292 for(unsigned i
= 0; i
< n_children
; ++i
) {
293 assertClause(orNode
, orLit
, ~clause
[i
]);
296 // lit -> (a_1 | a_2 | a_3 | ... | a_n)
297 // ~lit | a_1 | a_2 | a_3 | ... | a_n
298 clause
[n_children
] = ~orLit
;
299 // This needs to go last, as the clause might get modified by the SAT solver
300 assertClause(orNode
, clause
);
302 // Return the literal
306 SatLiteral
TseitinCnfStream::handleAnd(TNode andNode
) {
307 Assert(!hasLiteral(andNode
), "Atom already mapped!");
308 Assert(andNode
.getKind() == AND
, "Expecting an AND expression!");
309 Assert(andNode
.getNumChildren() > 1, "Expecting more than 1 child!");
310 Assert(!d_removable
, "Removable clauses can not contain Boolean structure");
312 // Number of children
313 unsigned n_children
= andNode
.getNumChildren();
315 // Transform all the children first (remembering the negation)
316 TNode::const_iterator node_it
= andNode
.begin();
317 TNode::const_iterator node_it_end
= andNode
.end();
318 SatClause
clause(n_children
+ 1);
319 for(int i
= 0; node_it
!= node_it_end
; ++node_it
, ++i
) {
320 clause
[i
] = ~toCNF(*node_it
);
323 // Get the literal for this node
324 SatLiteral andLit
= newLiteral(andNode
);
326 // lit -> (a_1 & a_2 & a_3 & ... & a_n)
327 // ~lit | (a_1 & a_2 & a_3 & ... & a_n)
328 // (~lit | a_1) & (~lit | a_2) & ... & (~lit | a_n)
329 for(unsigned i
= 0; i
< n_children
; ++i
) {
330 assertClause(andNode
, ~andLit
, ~clause
[i
]);
333 // lit <- (a_1 & a_2 & a_3 & ... a_n)
334 // lit | ~(a_1 & a_2 & a_3 & ... & a_n)
335 // lit | ~a_1 | ~a_2 | ~a_3 | ... | ~a_n
336 clause
[n_children
] = andLit
;
337 // This needs to go last, as the clause might get modified by the SAT solver
338 assertClause(andNode
, clause
);
343 SatLiteral
TseitinCnfStream::handleImplies(TNode impliesNode
) {
344 Assert(!hasLiteral(impliesNode
), "Atom already mapped!");
345 Assert(impliesNode
.getKind() == IMPLIES
, "Expecting an IMPLIES expression!");
346 Assert(impliesNode
.getNumChildren() == 2, "Expecting exactly 2 children!");
347 Assert(!d_removable
, "Removable clauses can not contain Boolean structure");
349 // Convert the children to cnf
350 SatLiteral a
= toCNF(impliesNode
[0]);
351 SatLiteral b
= toCNF(impliesNode
[1]);
353 SatLiteral impliesLit
= newLiteral(impliesNode
);
357 assertClause(impliesNode
, ~impliesLit
, ~a
, b
);
361 // (a | l) & (~b | l)
362 assertClause(impliesNode
, a
, impliesLit
);
363 assertClause(impliesNode
, ~b
, impliesLit
);
369 SatLiteral
TseitinCnfStream::handleIff(TNode iffNode
) {
370 Assert(!hasLiteral(iffNode
), "Atom already mapped!");
371 Assert(iffNode
.getKind() == IFF
, "Expecting an IFF expression!");
372 Assert(iffNode
.getNumChildren() == 2, "Expecting exactly 2 children!");
374 Debug("cnf") << "handleIff(" << iffNode
<< ")" << endl
;
376 // Convert the children to CNF
377 SatLiteral a
= toCNF(iffNode
[0]);
378 SatLiteral b
= toCNF(iffNode
[1]);
380 // Get the now literal
381 SatLiteral iffLit
= newLiteral(iffNode
);
383 // lit -> ((a-> b) & (b->a))
384 // ~lit | ((~a | b) & (~b | a))
385 // (~a | b | ~lit) & (~b | a | ~lit)
386 assertClause(iffNode
, ~a
, b
, ~iffLit
);
387 assertClause(iffNode
, a
, ~b
, ~iffLit
);
390 // ~((a & b) | (~a & ~b)) | lit
391 // (~(a & b)) & (~(~a & ~b)) | lit
392 // ((~a | ~b) & (a | b)) | lit
393 // (~a | ~b | lit) & (a | b | lit)
394 assertClause(iffNode
, ~a
, ~b
, iffLit
);
395 assertClause(iffNode
, a
, b
, iffLit
);
401 SatLiteral
TseitinCnfStream::handleNot(TNode notNode
) {
402 Assert(!hasLiteral(notNode
), "Atom already mapped!");
403 Assert(notNode
.getKind() == NOT
, "Expecting a NOT expression!");
404 Assert(notNode
.getNumChildren() == 1, "Expecting exactly 1 child!");
406 SatLiteral notLit
= ~toCNF(notNode
[0]);
411 SatLiteral
TseitinCnfStream::handleIte(TNode iteNode
) {
412 Assert(iteNode
.getKind() == ITE
);
413 Assert(iteNode
.getNumChildren() == 3);
414 Assert(!d_removable
, "Removable clauses can not contain Boolean structure");
416 Debug("cnf") << "handleIte(" << iteNode
[0] << " " << iteNode
[1] << " " << iteNode
[2] << ")" << endl
;
418 SatLiteral condLit
= toCNF(iteNode
[0]);
419 SatLiteral thenLit
= toCNF(iteNode
[1]);
420 SatLiteral elseLit
= toCNF(iteNode
[2]);
422 SatLiteral iteLit
= newLiteral(iteNode
);
424 // If ITE is true then one of the branches is true and the condition
426 // lit -> (ite b t e)
427 // lit -> (t | e) & (b -> t) & (!b -> e)
428 // lit -> (t | e) & (!b | t) & (b | e)
429 // (!lit | t | e) & (!lit | !b | t) & (!lit | b | e)
430 assertClause(iteNode
, ~iteLit
, thenLit
, elseLit
);
431 assertClause(iteNode
, ~iteLit
, ~condLit
, thenLit
);
432 assertClause(iteNode
, ~iteLit
, condLit
, elseLit
);
434 // If ITE is false then one of the branches is false and the condition
436 // !lit -> !(ite b t e)
437 // !lit -> (!t | !e) & (b -> !t) & (!b -> !e)
438 // !lit -> (!t | !e) & (!b | !t) & (b | !e)
439 // (lit | !t | !e) & (lit | !b | !t) & (lit | b | !e)
440 assertClause(iteNode
, iteLit
, ~thenLit
, ~elseLit
);
441 assertClause(iteNode
, iteLit
, ~condLit
, ~thenLit
);
442 assertClause(iteNode
, iteLit
, condLit
, ~elseLit
);
448 SatLiteral
TseitinCnfStream::toCNF(TNode node
, bool negated
) {
449 Debug("cnf") << "toCNF(" << node
<< ", negated = " << (negated
? "true" : "false") << ")" << endl
;
452 Node negatedNode
= node
.notNode();
454 // If the non-negated node has already been translated, get the translation
455 if(hasLiteral(node
)) {
456 Debug("cnf") << "toCNF(): already translated" << endl
;
457 nodeLit
= getLiteral(node
);
459 // Handle each Boolean operator case
460 switch(node
.getKind()) {
462 nodeLit
= handleNot(node
);
465 nodeLit
= handleXor(node
);
468 nodeLit
= handleIte(node
);
471 nodeLit
= handleIff(node
);
474 nodeLit
= handleImplies(node
);
477 nodeLit
= handleOr(node
);
480 nodeLit
= handleAnd(node
);
483 if(node
[0].getType().isBoolean()) {
484 // normally this is an IFF, but EQUAL is possible with pseudobooleans
485 nodeLit
= handleIff(node
[0].iffNode(node
[1]));
487 nodeLit
= convertAtom(node
);
492 //TODO make sure this does not contain any boolean substructure
493 nodeLit
= convertAtom(node
);
495 //Node atomic = handleNonAtomicNode(node);
496 //return isCached(atomic) ? lookupInCache(atomic) : convertAtom(atomic);
502 // Return the appropriate (negated) literal
503 if (!negated
) return nodeLit
;
504 else return ~nodeLit
;
507 void TseitinCnfStream::convertAndAssertAnd(TNode node
, bool negated
) {
508 Assert(node
.getKind() == AND
);
510 // If the node is a conjunction, we handle each conjunct separately
511 for(TNode::const_iterator conjunct
= node
.begin(), node_end
= node
.end();
512 conjunct
!= node_end
; ++conjunct
) {
513 convertAndAssert(*conjunct
, false);
516 // If the node is a disjunction, we construct a clause and assert it
517 int nChildren
= node
.getNumChildren();
518 SatClause
clause(nChildren
);
519 TNode::const_iterator disjunct
= node
.begin();
520 for(int i
= 0; i
< nChildren
; ++ disjunct
, ++ i
) {
521 Assert( disjunct
!= node
.end() );
522 clause
[i
] = toCNF(*disjunct
, true);
524 Assert(disjunct
== node
.end());
525 assertClause(node
, clause
);
529 void TseitinCnfStream::convertAndAssertOr(TNode node
, bool negated
) {
530 Assert(node
.getKind() == OR
);
532 // If the node is a disjunction, we construct a clause and assert it
533 int nChildren
= node
.getNumChildren();
534 SatClause
clause(nChildren
);
535 TNode::const_iterator disjunct
= node
.begin();
536 for(int i
= 0; i
< nChildren
; ++ disjunct
, ++ i
) {
537 Assert( disjunct
!= node
.end() );
538 clause
[i
] = toCNF(*disjunct
, false);
540 Assert(disjunct
== node
.end());
541 assertClause(node
, clause
);
543 // If the node is a conjunction, we handle each conjunct separately
544 for(TNode::const_iterator conjunct
= node
.begin(), node_end
= node
.end();
545 conjunct
!= node_end
; ++conjunct
) {
546 convertAndAssert(*conjunct
, true);
551 void TseitinCnfStream::convertAndAssertXor(TNode node
, bool negated
) {
554 SatLiteral p
= toCNF(node
[0], false);
555 SatLiteral q
= toCNF(node
[1], false);
556 // Construct the clauses (p => !q) and (!q => p)
557 SatClause
clause1(2);
560 assertClause(node
, clause1
);
561 SatClause
clause2(2);
564 assertClause(node
, clause2
);
566 // !(p XOR q) is the same as p <=> q
567 SatLiteral p
= toCNF(node
[0], false);
568 SatLiteral q
= toCNF(node
[1], false);
569 // Construct the clauses (p => q) and (q => p)
570 SatClause
clause1(2);
573 assertClause(node
, clause1
);
574 SatClause
clause2(2);
577 assertClause(node
, clause2
);
581 void TseitinCnfStream::convertAndAssertIff(TNode node
, bool negated
) {
584 SatLiteral p
= toCNF(node
[0], false);
585 SatLiteral q
= toCNF(node
[1], false);
586 // Construct the clauses (p => q) and (q => p)
587 SatClause
clause1(2);
590 assertClause(node
, clause1
);
591 SatClause
clause2(2);
594 assertClause(node
, clause2
);
596 // !(p <=> q) is the same as p XOR q
597 SatLiteral p
= toCNF(node
[0], false);
598 SatLiteral q
= toCNF(node
[1], false);
599 // Construct the clauses (p => !q) and (!q => p)
600 SatClause
clause1(2);
603 assertClause(node
, clause1
);
604 SatClause
clause2(2);
607 assertClause(node
, clause2
);
611 void TseitinCnfStream::convertAndAssertImplies(TNode node
, bool negated
) {
614 SatLiteral p
= toCNF(node
[0], false);
615 SatLiteral q
= toCNF(node
[1], false);
616 // Construct the clause ~p || q
620 assertClause(node
, clause
);
621 } else {// Construct the
622 // !(p => q) is the same as (p && ~q)
623 convertAndAssert(node
[0], false);
624 convertAndAssert(node
[1], true);
628 void TseitinCnfStream::convertAndAssertIte(TNode node
, bool negated
) {
630 SatLiteral p
= toCNF(node
[0], false);
631 SatLiteral q
= toCNF(node
[1], negated
);
632 SatLiteral r
= toCNF(node
[2], negated
);
633 // Construct the clauses:
634 // (p => q) and (!p => r)
635 SatClause
clause1(2);
638 assertClause(node
, clause1
);
639 SatClause
clause2(2);
642 assertClause(node
, clause2
);
645 // At the top level we must ensure that all clauses that are asserted are
646 // not unit, except for the direct assertions. This allows us to remove the
647 // clauses later when they are not needed anymore (lemmas for example).
648 void TseitinCnfStream::convertAndAssert(TNode node
, bool removable
, bool negated
, ProofRule proof_id
, TNode from
) {
649 Debug("cnf") << "convertAndAssert(" << node
<< ", removable = " << (removable
? "true" : "false") << ", negated = " << (negated
? "true" : "false") << ")" << endl
;
650 d_removable
= removable
;
651 if(options::proof() || options::unsatCores()) {
652 // Encode the assertion ID in the proof_id to store with generated clauses.
653 uint64_t assertionTableIndex
= d_assertionTable
.size();
654 Assert((uint64_t(proof_id
) & 0xffffffff00000000llu
) == 0 && (assertionTableIndex
& 0xffffffff00000000llu
) == 0, "proof_id/table_index collision");
655 d_proofId
= assertionTableIndex
| (uint64_t(proof_id
) << 32);
656 d_assertionTable
.push_back(from
.isNull() ? node
: from
);
657 Debug("cores") << "cnf ix " << assertionTableIndex
<< " asst " << node
<< " proof_id " << proof_id
<< " from " << from
<< endl
;
659 // We aren't producing proofs or unsat cores; use an invalid proof id.
660 d_proofId
= uint64_t(-1);
662 convertAndAssert(node
, negated
);
665 void TseitinCnfStream::convertAndAssert(TNode node
, bool negated
) {
666 Debug("cnf") << "convertAndAssert(" << node
<< ", negated = " << (negated
? "true" : "false") << ")" << endl
;
668 switch(node
.getKind()) {
670 convertAndAssertAnd(node
, negated
);
673 convertAndAssertOr(node
, negated
);
676 convertAndAssertIff(node
, negated
);
679 convertAndAssertXor(node
, negated
);
682 convertAndAssertImplies(node
, negated
);
685 convertAndAssertIte(node
, negated
);
688 convertAndAssert(node
[0], !negated
);
692 assertClause(node
, toCNF(node
, negated
));
697 }/* CVC4::prop namespace */
698 }/* CVC4 namespace */