src/prop/cnf_stream.cpp

   1 /*********************                                                        */
   2 /*! \file cnf_stream.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Dejan Jovanovic, Liana Hadarean, Tim King
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 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.\endverbatim
  11  **
  12  ** \brief A CNF converter that takes in asserts and has the side effect
  13  ** of given an equisatisfiable stream of assertions to PropEngine.
  14  **
  15  ** A CNF converter that takes in asserts and has the side effect
  16  ** of given an equisatisfiable stream of assertions to PropEngine.
  17  **/
  18 #include "prop/cnf_stream.h"
  19
  20 #include <queue>
  21
  22 #include "base/check.h"
  23 #include "base/output.h"
  24 #include "expr/expr.h"
  25 #include "expr/node.h"
  26 #include "options/bv_options.h"
  27 #include "proof/clause_id.h"
  28 #include "proof/cnf_proof.h"
  29 #include "proof/proof_manager.h"
  30 #include "proof/sat_proof.h"
  31 #include "prop/minisat/minisat.h"
  32 #include "prop/prop_engine.h"
  33 #include "prop/theory_proxy.h"
  34 #include "smt/command.h"
  35 #include "smt/smt_engine_scope.h"
  36 #include "theory/theory.h"
  37 #include "theory/theory_engine.h"
  38
  39 using namespace std;
  40 using namespace CVC4::kind;
  41
  42 namespace CVC4 {
  43 namespace prop {
  44
  45 CnfStream::CnfStream(SatSolver* satSolver, Registrar* registrar,
  46                      context::Context* context, bool fullLitToNodeMap,
  47                      std::string name)
  48     : d_satSolver(satSolver),
  49       d_booleanVariables(context),
  50       d_nodeToLiteralMap(context),
  51       d_literalToNodeMap(context),
  52       d_fullLitToNodeMap(fullLitToNodeMap),
  53       d_convertAndAssertCounter(0),
  54       d_registrar(registrar),
  55       d_name(name),
  56       d_cnfProof(NULL),
  57       d_removable(false) {
  58 }
  59
  60 TseitinCnfStream::TseitinCnfStream(SatSolver* satSolver,
  61                                    Registrar* registrar,
  62                                    context::Context* context,
  63                                    ResourceManager* rm,
  64                                    bool fullLitToNodeMap,
  65                                    std::string name)
  66     : CnfStream(satSolver, registrar, context, fullLitToNodeMap, name),
  67       d_resourceManager(rm)
  68 {}
  69
  70 void CnfStream::assertClause(TNode node, SatClause& c) {
  71   Debug("cnf") << "Inserting into stream " << c << " node = " << node << endl;
  72   if(Dump.isOn("clauses")) {
  73     if(c.size() == 1) {
  74       Dump("clauses") << AssertCommand(Expr(getNode(c[0]).toExpr()));
  75     } else {
  76       Assert(c.size() > 1);
  77       NodeBuilder<> b(kind::OR);
  78       for(unsigned i = 0; i < c.size(); ++i) {
  79         b << getNode(c[i]);
  80       }
  81       Node n = b;
  82       Dump("clauses") << AssertCommand(Expr(n.toExpr()));
  83     }
  84   }
  85
  86   if (PROOF_ON() && d_cnfProof)
  87   {
  88     d_cnfProof->pushCurrentDefinition(node);
  89   }
  90
  91   ClauseId clause_id = d_satSolver->addClause(c, d_removable);
  92   if (clause_id == ClauseIdUndef) return; // nothing to store (no clause was added)
  93
  94   if (PROOF_ON() && d_cnfProof)
  95   {
  96     if (clause_id != ClauseIdError)
  97     {
  98       d_cnfProof->registerConvertedClause(clause_id);
  99     }
 100     d_cnfProof->popCurrentDefinition();
 101   };
 102 }
 103
 104 void CnfStream::assertClause(TNode node, SatLiteral a) {
 105   SatClause clause(1);
 106   clause[0] = a;
 107   assertClause(node, clause);
 108 }
 109
 110 void CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b) {
 111   SatClause clause(2);
 112   clause[0] = a;
 113   clause[1] = b;
 114   assertClause(node, clause);
 115 }
 116
 117 void CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c) {
 118   SatClause clause(3);
 119   clause[0] = a;
 120   clause[1] = b;
 121   clause[2] = c;
 122   assertClause(node, clause);
 123 }
 124
 125 bool CnfStream::hasLiteral(TNode n) const {
 126   NodeToLiteralMap::const_iterator find = d_nodeToLiteralMap.find(n);
 127   return find != d_nodeToLiteralMap.end();
 128 }
 129
 130 void TseitinCnfStream::ensureLiteral(TNode n, bool noPreregistration) {
 131   // These are not removable and have no proof ID
 132   d_removable = false;
 133
 134   Debug("cnf") << "ensureLiteral(" << n << ")" << endl;
 135   if(hasLiteral(n)) {
 136     SatLiteral lit = getLiteral(n);
 137     if(!d_literalToNodeMap.contains(lit)){
 138       // Store backward-mappings
 139       d_literalToNodeMap.insert(lit, n);
 140       d_literalToNodeMap.insert(~lit, n.notNode());
 141     }
 142     return;
 143   }
 144
 145   AlwaysAssertArgument(
 146       n.getType().isBoolean(),
 147       n,
 148       "CnfStream::ensureLiteral() requires a node of Boolean type.\n"
 149       "got node: %s\n"
 150       "its type: %s\n",
 151       n.toString().c_str(),
 152       n.getType().toString().c_str());
 153
 154   bool negated CVC4_UNUSED = false;
 155   SatLiteral lit;
 156
 157   if(n.getKind() == kind::NOT) {
 158     negated = true;
 159     n = n[0];
 160   }
 161
 162   if( theory::Theory::theoryOf(n) == theory::THEORY_BOOL &&
 163       !n.isVar() ) {
 164     // If we were called with something other than a theory atom (or
 165     // Boolean variable), we get a SatLiteral that is definitionally
 166     // equal to it.
 167     //
 168     // We are setting the current assertion to be null. This is because `toCNF`
 169     // may add clauses to the SAT solver and we look up the current assertion
 170     // in that case. Setting it to null ensures that the assertion stack is
 171     // non-empty and that we are not associating a bogus assertion with the
 172     // clause. This should be ok because we use the mapping back to assertions
 173     // for clauses from input assertions only.
 174     PROOF(if (d_cnfProof) { d_cnfProof->pushCurrentAssertion(Node::null()); });
 175
 176     lit = toCNF(n, false);
 177
 178     PROOF(if (d_cnfProof) { d_cnfProof->popCurrentAssertion(); });
 179
 180     // Store backward-mappings
 181     // These may already exist
 182     d_literalToNodeMap.insert_safe(lit, n);
 183     d_literalToNodeMap.insert_safe(~lit, n.notNode());
 184   } else {
 185     // We have a theory atom or variable.
 186     lit = convertAtom(n, noPreregistration);
 187   }
 188
 189   Assert(hasLiteral(n) && getNode(lit) == n);
 190   Debug("ensureLiteral") << "CnfStream::ensureLiteral(): out lit is " << lit << std::endl;
 191 }
 192
 193 SatLiteral CnfStream::newLiteral(TNode node, bool isTheoryAtom, bool preRegister, bool canEliminate) {
 194   Debug("cnf") << d_name << "::newLiteral(" << node << ", " << isTheoryAtom << ")" << endl;
 195   Assert(node.getKind() != kind::NOT);
 196
 197   // Get the literal for this node
 198   SatLiteral lit;
 199   if (!hasLiteral(node)) {
 200     // If no literal, we'll make one
 201     if (node.getKind() == kind::CONST_BOOLEAN) {
 202       if (node.getConst<bool>()) {
 203         lit = SatLiteral(d_satSolver->trueVar());
 204       } else {
 205         lit = SatLiteral(d_satSolver->falseVar());
 206       }
 207     } else {
 208       lit = SatLiteral(d_satSolver->newVar(isTheoryAtom, preRegister, canEliminate));
 209     }
 210     d_nodeToLiteralMap.insert(node, lit);
 211     d_nodeToLiteralMap.insert(node.notNode(), ~lit);
 212   } else {
 213     lit = getLiteral(node);
 214   }
 215
 216   // If it's a theory literal, need to store it for back queries
 217   if ( isTheoryAtom || d_fullLitToNodeMap || (Dump.isOn("clauses")) ) {
 218     d_literalToNodeMap.insert_safe(lit, node);
 219     d_literalToNodeMap.insert_safe(~lit, node.notNode());
 220   }
 221
 222   // If a theory literal, we pre-register it
 223   if (preRegister) {
 224     // In case we are re-entered due to lemmas, save our state
 225     bool backupRemovable = d_removable;
 226     // Should be fine since cnfProof current assertion is stack based.
 227     d_registrar->preRegister(node);
 228     d_removable = backupRemovable;
 229   }
 230
 231   // Here, you can have it
 232   Debug("cnf") << "newLiteral(" << node << ") => " << lit << endl;
 233
 234   return lit;
 235 }
 236
 237 TNode CnfStream::getNode(const SatLiteral& literal) {
 238   Debug("cnf") << "getNode(" << literal << ")" << endl;
 239   Debug("cnf") << "getNode(" << literal << ") => " << d_literalToNodeMap[literal] << endl;
 240   return d_literalToNodeMap[literal];
 241 }
 242
 243 void CnfStream::getBooleanVariables(std::vector<TNode>& outputVariables) const {
 244   context::CDList<TNode>::const_iterator it, it_end;
 245   for (it = d_booleanVariables.begin(); it != d_booleanVariables.end(); ++ it) {
 246     outputVariables.push_back(*it);
 247   }
 248 }
 249
 250 void CnfStream::setProof(CnfProof* proof) {
 251   Assert(d_cnfProof == NULL);
 252   d_cnfProof = proof;
 253 }
 254
 255 SatLiteral CnfStream::convertAtom(TNode node, bool noPreregistration) {
 256   Debug("cnf") << "convertAtom(" << node << ")" << endl;
 257
 258   Assert(!hasLiteral(node)) << "atom already mapped!";
 259
 260   bool theoryLiteral = false;
 261   bool canEliminate = true;
 262   bool preRegister = false;
 263
 264   // Is this a variable add it to the list
 265   if (node.isVar() && node.getKind()!=BOOLEAN_TERM_VARIABLE) {
 266     d_booleanVariables.push_back(node);
 267   } else {
 268     theoryLiteral = true;
 269     canEliminate = false;
 270     preRegister = !noPreregistration;
 271   }
 272
 273   // Make a new literal (variables are not considered theory literals)
 274   SatLiteral lit = newLiteral(node, theoryLiteral, preRegister, canEliminate);
 275   // Return the resulting literal
 276   return lit;
 277 }
 278
 279 SatLiteral CnfStream::getLiteral(TNode node) {
 280   Assert(!node.isNull()) << "CnfStream: can't getLiteral() of null node";
 281
 282   Assert(d_nodeToLiteralMap.contains(node))
 283       << "Literal not in the CNF Cache: " << node << "\n";
 284
 285   SatLiteral literal = d_nodeToLiteralMap[node];
 286   Debug("cnf") << "CnfStream::getLiteral(" << node << ") => " << literal << std::endl;
 287   return literal;
 288 }
 289
 290 SatLiteral TseitinCnfStream::handleXor(TNode xorNode) {
 291   Assert(!hasLiteral(xorNode)) << "Atom already mapped!";
 292   Assert(xorNode.getKind() == XOR) << "Expecting an XOR expression!";
 293   Assert(xorNode.getNumChildren() == 2) << "Expecting exactly 2 children!";
 294   Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
 295
 296   SatLiteral a = toCNF(xorNode[0]);
 297   SatLiteral b = toCNF(xorNode[1]);
 298
 299   SatLiteral xorLit = newLiteral(xorNode);
 300
 301   assertClause(xorNode.negate(), a, b, ~xorLit);
 302   assertClause(xorNode.negate(), ~a, ~b, ~xorLit);
 303   assertClause(xorNode, a, ~b, xorLit);
 304   assertClause(xorNode, ~a, b, xorLit);
 305
 306   return xorLit;
 307 }
 308
 309 SatLiteral TseitinCnfStream::handleOr(TNode orNode) {
 310   Assert(!hasLiteral(orNode)) << "Atom already mapped!";
 311   Assert(orNode.getKind() == OR) << "Expecting an OR expression!";
 312   Assert(orNode.getNumChildren() > 1) << "Expecting more then 1 child!";
 313   Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
 314
 315   // Number of children
 316   unsigned n_children = orNode.getNumChildren();
 317
 318   // Transform all the children first
 319   TNode::const_iterator node_it = orNode.begin();
 320   TNode::const_iterator node_it_end = orNode.end();
 321   SatClause clause(n_children + 1);
 322   for(int i = 0; node_it != node_it_end; ++node_it, ++i) {
 323     clause[i] = toCNF(*node_it);
 324   }
 325
 326   // Get the literal for this node
 327   SatLiteral orLit = newLiteral(orNode);
 328
 329   // lit <- (a_1 | a_2 | a_3 | ... | a_n)
 330   // lit | ~(a_1 | a_2 | a_3 | ... | a_n)
 331   // (lit | ~a_1) & (lit | ~a_2) & (lit & ~a_3) & ... & (lit & ~a_n)
 332   for(unsigned i = 0; i < n_children; ++i) {
 333     assertClause(orNode, orLit, ~clause[i]);
 334   }
 335
 336   // lit -> (a_1 | a_2 | a_3 | ... | a_n)
 337   // ~lit | a_1 | a_2 | a_3 | ... | a_n
 338   clause[n_children] = ~orLit;
 339   // This needs to go last, as the clause might get modified by the SAT solver
 340   assertClause(orNode.negate(), clause);
 341
 342   // Return the literal
 343   return orLit;
 344 }
 345
 346 SatLiteral TseitinCnfStream::handleAnd(TNode andNode) {
 347   Assert(!hasLiteral(andNode)) << "Atom already mapped!";
 348   Assert(andNode.getKind() == AND) << "Expecting an AND expression!";
 349   Assert(andNode.getNumChildren() > 1) << "Expecting more than 1 child!";
 350   Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
 351
 352   // Number of children
 353   unsigned n_children = andNode.getNumChildren();
 354
 355   // Transform all the children first (remembering the negation)
 356   TNode::const_iterator node_it = andNode.begin();
 357   TNode::const_iterator node_it_end = andNode.end();
 358   SatClause clause(n_children + 1);
 359   for(int i = 0; node_it != node_it_end; ++node_it, ++i) {
 360     clause[i] = ~toCNF(*node_it);
 361   }
 362
 363   // Get the literal for this node
 364   SatLiteral andLit = newLiteral(andNode);
 365
 366   // lit -> (a_1 & a_2 & a_3 & ... & a_n)
 367   // ~lit | (a_1 & a_2 & a_3 & ... & a_n)
 368   // (~lit | a_1) & (~lit | a_2) & ... & (~lit | a_n)
 369   for(unsigned i = 0; i < n_children; ++i) {
 370     assertClause(andNode.negate(), ~andLit, ~clause[i]);
 371   }
 372
 373   // lit <- (a_1 & a_2 & a_3 & ... a_n)
 374   // lit | ~(a_1 & a_2 & a_3 & ... & a_n)
 375   // lit | ~a_1 | ~a_2 | ~a_3 | ... | ~a_n
 376   clause[n_children] = andLit;
 377   // This needs to go last, as the clause might get modified by the SAT solver
 378   assertClause(andNode, clause);
 379
 380   return andLit;
 381 }
 382
 383 SatLiteral TseitinCnfStream::handleImplies(TNode impliesNode) {
 384   Assert(!hasLiteral(impliesNode)) << "Atom already mapped!";
 385   Assert(impliesNode.getKind() == IMPLIES)
 386       << "Expecting an IMPLIES expression!";
 387   Assert(impliesNode.getNumChildren() == 2) << "Expecting exactly 2 children!";
 388   Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
 389
 390   // Convert the children to cnf
 391   SatLiteral a = toCNF(impliesNode[0]);
 392   SatLiteral b = toCNF(impliesNode[1]);
 393
 394   SatLiteral impliesLit = newLiteral(impliesNode);
 395
 396   // lit -> (a->b)
 397   // ~lit | ~ a | b
 398   assertClause(impliesNode.negate(), ~impliesLit, ~a, b);
 399
 400   // (a->b) -> lit
 401   // ~(~a | b) | lit
 402   // (a | l) & (~b | l)
 403   assertClause(impliesNode, a, impliesLit);
 404   assertClause(impliesNode, ~b, impliesLit);
 405
 406   return impliesLit;
 407 }
 408
 409
 410 SatLiteral TseitinCnfStream::handleIff(TNode iffNode) {
 411   Assert(!hasLiteral(iffNode)) << "Atom already mapped!";
 412   Assert(iffNode.getKind() == EQUAL) << "Expecting an EQUAL expression!";
 413   Assert(iffNode.getNumChildren() == 2) << "Expecting exactly 2 children!";
 414
 415   Debug("cnf") << "handleIff(" << iffNode << ")" << endl;
 416
 417   // Convert the children to CNF
 418   SatLiteral a = toCNF(iffNode[0]);
 419   SatLiteral b = toCNF(iffNode[1]);
 420
 421   // Get the now literal
 422   SatLiteral iffLit = newLiteral(iffNode);
 423
 424   // lit -> ((a-> b) & (b->a))
 425   // ~lit | ((~a | b) & (~b | a))
 426   // (~a | b | ~lit) & (~b | a | ~lit)
 427   assertClause(iffNode.negate(), ~a, b, ~iffLit);
 428   assertClause(iffNode.negate(), a, ~b, ~iffLit);
 429
 430   // (a<->b) -> lit
 431   // ~((a & b) | (~a & ~b)) | lit
 432   // (~(a & b)) & (~(~a & ~b)) | lit
 433   // ((~a | ~b) & (a | b)) | lit
 434   // (~a | ~b | lit) & (a | b | lit)
 435   assertClause(iffNode, ~a, ~b, iffLit);
 436   assertClause(iffNode, a, b, iffLit);
 437
 438   return iffLit;
 439 }
 440
 441
 442 SatLiteral TseitinCnfStream::handleNot(TNode notNode) {
 443   Assert(!hasLiteral(notNode)) << "Atom already mapped!";
 444   Assert(notNode.getKind() == NOT) << "Expecting a NOT expression!";
 445   Assert(notNode.getNumChildren() == 1) << "Expecting exactly 1 child!";
 446
 447   SatLiteral notLit = ~toCNF(notNode[0]);
 448
 449   return notLit;
 450 }
 451
 452 SatLiteral TseitinCnfStream::handleIte(TNode iteNode) {
 453   Assert(iteNode.getKind() == ITE);
 454   Assert(iteNode.getNumChildren() == 3);
 455   Assert(!d_removable) << "Removable clauses can not contain Boolean structure";
 456
 457   Debug("cnf") << "handleIte(" << iteNode[0] << " " << iteNode[1] << " " << iteNode[2] << ")" << endl;
 458
 459   SatLiteral condLit = toCNF(iteNode[0]);
 460   SatLiteral thenLit = toCNF(iteNode[1]);
 461   SatLiteral elseLit = toCNF(iteNode[2]);
 462
 463   SatLiteral iteLit = newLiteral(iteNode);
 464
 465   // If ITE is true then one of the branches is true and the condition
 466   // implies which one
 467   // lit -> (ite b t e)
 468   // lit -> (t | e) & (b -> t) & (!b -> e)
 469   // lit -> (t | e) & (!b | t) & (b | e)
 470   // (!lit | t | e) & (!lit | !b | t) & (!lit | b | e)
 471   assertClause(iteNode.negate(), ~iteLit, thenLit, elseLit);
 472   assertClause(iteNode.negate(), ~iteLit, ~condLit, thenLit);
 473   assertClause(iteNode.negate(), ~iteLit, condLit, elseLit);
 474
 475   // If ITE is false then one of the branches is false and the condition
 476   // implies which one
 477   // !lit -> !(ite b t e)
 478   // !lit -> (!t | !e) & (b -> !t) & (!b -> !e)
 479   // !lit -> (!t | !e) & (!b | !t) & (b | !e)
 480   // (lit | !t | !e) & (lit | !b | !t) & (lit | b | !e)
 481   assertClause(iteNode, iteLit, ~thenLit, ~elseLit);
 482   assertClause(iteNode, iteLit, ~condLit, ~thenLit);
 483   assertClause(iteNode, iteLit, condLit, ~elseLit);
 484
 485   return iteLit;
 486 }
 487
 488
 489 SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) {
 490   Debug("cnf") << "toCNF(" << node << ", negated = " << (negated ? "true" : "false") << ")" << endl;
 491
 492   SatLiteral nodeLit;
 493   Node negatedNode = node.notNode();
 494
 495   // If the non-negated node has already been translated, get the translation
 496   if(hasLiteral(node)) {
 497     Debug("cnf") << "toCNF(): already translated" << endl;
 498     nodeLit = getLiteral(node);
 499   } else {
 500     // Handle each Boolean operator case
 501     switch(node.getKind()) {
 502     case NOT:
 503       nodeLit = handleNot(node);
 504       break;
 505     case XOR:
 506       nodeLit = handleXor(node);
 507       break;
 508     case ITE:
 509       nodeLit = handleIte(node);
 510       break;
 511     case IMPLIES:
 512       nodeLit = handleImplies(node);
 513       break;
 514     case OR:
 515       nodeLit = handleOr(node);
 516       break;
 517     case AND:
 518       nodeLit = handleAnd(node);
 519       break;
 520     case EQUAL:
 521       if(node[0].getType().isBoolean()) {
 522         nodeLit = handleIff(node);
 523       } else {
 524         nodeLit = convertAtom(node);
 525       }
 526       break;
 527     default:
 528       {
 529         //TODO make sure this does not contain any boolean substructure
 530         nodeLit = convertAtom(node);
 531         //Unreachable();
 532         //Node atomic = handleNonAtomicNode(node);
 533         //return isCached(atomic) ? lookupInCache(atomic) : convertAtom(atomic);
 534       }
 535       break;
 536     }
 537   }
 538
 539   // Return the appropriate (negated) literal
 540   if (!negated) return nodeLit;
 541   else return ~nodeLit;
 542 }
 543
 544 void TseitinCnfStream::convertAndAssertAnd(TNode node, bool negated) {
 545   Assert(node.getKind() == AND);
 546   if (!negated) {
 547     // If the node is a conjunction, we handle each conjunct separately
 548     for(TNode::const_iterator conjunct = node.begin(), node_end = node.end();
 549         conjunct != node_end; ++conjunct ) {
 550       PROOF(if (d_cnfProof) d_cnfProof->setCnfDependence(*conjunct, node););
 551       convertAndAssert(*conjunct, false);
 552     }
 553   } else {
 554     // If the node is a disjunction, we construct a clause and assert it
 555     int nChildren = node.getNumChildren();
 556     SatClause clause(nChildren);
 557     TNode::const_iterator disjunct = node.begin();
 558     for(int i = 0; i < nChildren; ++ disjunct, ++ i) {
 559       Assert(disjunct != node.end());
 560       clause[i] = toCNF(*disjunct, true);
 561     }
 562     Assert(disjunct == node.end());
 563     assertClause(node.negate(), clause);
 564   }
 565 }
 566
 567 void TseitinCnfStream::convertAndAssertOr(TNode node, bool negated) {
 568   Assert(node.getKind() == OR);
 569   if (!negated) {
 570     // If the node is a disjunction, we construct a clause and assert it
 571     int nChildren = node.getNumChildren();
 572     SatClause clause(nChildren);
 573     TNode::const_iterator disjunct = node.begin();
 574     for(int i = 0; i < nChildren; ++ disjunct, ++ i) {
 575       Assert(disjunct != node.end());
 576       clause[i] = toCNF(*disjunct, false);
 577     }
 578     Assert(disjunct == node.end());
 579     assertClause(node, clause);
 580   } else {
 581     // If the node is a conjunction, we handle each conjunct separately
 582     for(TNode::const_iterator conjunct = node.begin(), node_end = node.end();
 583         conjunct != node_end; ++conjunct ) {
 584       PROOF(if (d_cnfProof) d_cnfProof->setCnfDependence((*conjunct).negate(), node.negate()););
 585       convertAndAssert(*conjunct, true);
 586     }
 587   }
 588 }
 589
 590 void TseitinCnfStream::convertAndAssertXor(TNode node, bool negated) {
 591   if (!negated) {
 592     // p XOR q
 593     SatLiteral p = toCNF(node[0], false);
 594     SatLiteral q = toCNF(node[1], false);
 595     // Construct the clauses (p => !q) and (!q => p)
 596     SatClause clause1(2);
 597     clause1[0] = ~p;
 598     clause1[1] = ~q;
 599     assertClause(node, clause1);
 600     SatClause clause2(2);
 601     clause2[0] = p;
 602     clause2[1] = q;
 603     assertClause(node, clause2);
 604   } else {
 605     // !(p XOR q) is the same as p <=> q
 606     SatLiteral p = toCNF(node[0], false);
 607     SatLiteral q = toCNF(node[1], false);
 608     // Construct the clauses (p => q) and (q => p)
 609     SatClause clause1(2);
 610     clause1[0] = ~p;
 611     clause1[1] = q;
 612     assertClause(node.negate(), clause1);
 613     SatClause clause2(2);
 614     clause2[0] = p;
 615     clause2[1] = ~q;
 616     assertClause(node.negate(), clause2);
 617   }
 618 }
 619
 620 void TseitinCnfStream::convertAndAssertIff(TNode node, bool negated) {
 621   if (!negated) {
 622     // p <=> q
 623     SatLiteral p = toCNF(node[0], false);
 624     SatLiteral q = toCNF(node[1], false);
 625     // Construct the clauses (p => q) and (q => p)
 626     SatClause clause1(2);
 627     clause1[0] = ~p;
 628     clause1[1] = q;
 629     assertClause(node, clause1);
 630     SatClause clause2(2);
 631     clause2[0] = p;
 632     clause2[1] = ~q;
 633     assertClause(node, clause2);
 634   } else {
 635     // !(p <=> q) is the same as p XOR q
 636     SatLiteral p = toCNF(node[0], false);
 637     SatLiteral q = toCNF(node[1], false);
 638     // Construct the clauses (p => !q) and (!q => p)
 639     SatClause clause1(2);
 640     clause1[0] = ~p;
 641     clause1[1] = ~q;
 642     assertClause(node.negate(), clause1);
 643     SatClause clause2(2);
 644     clause2[0] = p;
 645     clause2[1] = q;
 646     assertClause(node.negate(), clause2);
 647   }
 648 }
 649
 650 void TseitinCnfStream::convertAndAssertImplies(TNode node, bool negated) {
 651   if (!negated) {
 652     // p => q
 653     SatLiteral p = toCNF(node[0], false);
 654     SatLiteral q = toCNF(node[1], false);
 655     // Construct the clause ~p || q
 656     SatClause clause(2);
 657     clause[0] = ~p;
 658     clause[1] = q;
 659     assertClause(node, clause);
 660   } else {// Construct the
 661     PROOF(if (d_cnfProof) d_cnfProof->setCnfDependence(node[0], node.negate()););
 662     PROOF(if (d_cnfProof) d_cnfProof->setCnfDependence(node[1].negate(), node.negate()););
 663     // !(p => q) is the same as (p && ~q)
 664     convertAndAssert(node[0], false);
 665     convertAndAssert(node[1], true);
 666   }
 667 }
 668
 669 void TseitinCnfStream::convertAndAssertIte(TNode node, bool negated) {
 670   // ITE(p, q, r)
 671   SatLiteral p = toCNF(node[0], false);
 672   SatLiteral q = toCNF(node[1], negated);
 673   SatLiteral r = toCNF(node[2], negated);
 674   // Construct the clauses:
 675   // (p => q) and (!p => r)
 676   Node nnode = node;
 677   if( negated ){
 678     nnode = node.negate();
 679   }
 680   SatClause clause1(2);
 681   clause1[0] = ~p;
 682   clause1[1] = q;
 683   assertClause(nnode, clause1);
 684   SatClause clause2(2);
 685   clause2[0] = p;
 686   clause2[1] = r;
 687   assertClause(nnode, clause2);
 688 }
 689
 690 // At the top level we must ensure that all clauses that are asserted are
 691 // not unit, except for the direct assertions. This allows us to remove the
 692 // clauses later when they are not needed anymore (lemmas for example).
 693 void TseitinCnfStream::convertAndAssert(TNode node,
 694                                         bool removable,
 695                                         bool negated,
 696                                         ProofRule proof_id,
 697                                         TNode from) {
 698   Debug("cnf") << "convertAndAssert(" << node
 699                << ", removable = " << (removable ? "true" : "false")
 700                << ", negated = " << (negated ? "true" : "false") << ")" << endl;
 701   d_removable = removable;
 702   PROOF
 703     (if (d_cnfProof) {
 704       Node assertion = negated ? node.notNode() : (Node)node;
 705       Node from_assertion = negated? from.notNode() : (Node) from;
 706
 707       if (proof_id != RULE_INVALID) {
 708         d_cnfProof->pushCurrentAssertion(from.isNull() ? assertion : from_assertion);
 709         d_cnfProof->registerAssertion(from.isNull() ? assertion : from_assertion, proof_id);
 710       }
 711       else {
 712         d_cnfProof->pushCurrentAssertion(assertion);
 713         d_cnfProof->registerAssertion(assertion, proof_id);
 714       }
 715     });
 716
 717   convertAndAssert(node, negated);
 718   PROOF
 719     (if (d_cnfProof) {
 720       d_cnfProof->popCurrentAssertion();
 721     });
 722 }
 723
 724 void TseitinCnfStream::convertAndAssert(TNode node, bool negated) {
 725   Debug("cnf") << "convertAndAssert(" << node
 726                << ", negated = " << (negated ? "true" : "false") << ")" << endl;
 727
 728   if (d_convertAndAssertCounter % ResourceManager::getFrequencyCount() == 0) {
 729     d_resourceManager->spendResource(ResourceManager::Resource::CnfStep);
 730     d_convertAndAssertCounter = 0;
 731   }
 732   ++d_convertAndAssertCounter;
 733
 734   switch(node.getKind()) {
 735   case AND:
 736     convertAndAssertAnd(node, negated);
 737     break;
 738   case OR:
 739     convertAndAssertOr(node, negated);
 740     break;
 741   case XOR:
 742     convertAndAssertXor(node, negated);
 743     break;
 744   case IMPLIES:
 745     convertAndAssertImplies(node, negated);
 746     break;
 747   case ITE:
 748     convertAndAssertIte(node, negated);
 749     break;
 750   case NOT:
 751     convertAndAssert(node[0], !negated);
 752     break;
 753   case EQUAL:
 754     if( node[0].getType().isBoolean() ){
 755       convertAndAssertIff(node, negated);
 756       break;
 757     }
 758     CVC4_FALLTHROUGH;
 759   default:
 760   {
 761     Node nnode = node;
 762     if( negated ){
 763       nnode = node.negate();
 764     }
 765     // Atoms
 766     assertClause(nnode, toCNF(node, negated));
 767   }
 768     break;
 769   }
 770 }
 771
 772 }/* CVC4::prop namespace */
 773 }/* CVC4 namespace */