src/prop/cnf_stream.cpp

   1 /*********************                                                        */
   2 /*! \file cnf_stream.cpp
   3  ** \verbatim
   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
  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
  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"
  33 #include <queue>
  34
  35 using namespace std;
  36 using namespace CVC4::kind;
  37
  38 #ifdef CVC4_REPLAY
  39 #  define CVC4_USE_REPLAY true
  40 #else /* CVC4_REPLAY */
  41 #  define CVC4_USE_REPLAY false
  42 #endif /* CVC4_REPLAY */
  43
  44 namespace CVC4 {
  45 namespace prop {
  46
  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),
  55   d_removable(false) {
  56 }
  57
  58 TseitinCnfStream::TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, context::Context* context, bool fullLitToNodeMap) :
  59   CnfStream(satSolver, registrar, context, fullLitToNodeMap) {
  60 }
  61
  62 void CnfStream::assertClause(TNode node, SatClause& c) {
  63   Debug("cnf") << "Inserting into stream " << c << endl;
  64   if(Dump.isOn("clauses")) {
  65     if(c.size() == 1) {
  66       Dump("clauses") << AssertCommand(Expr(getNode(c[0]).toExpr()));
  67     } else {
  68       Assert(c.size() > 1);
  69       NodeBuilder<> b(kind::OR);
  70       for(unsigned i = 0; i < c.size(); ++i) {
  71         b << getNode(c[i]);
  72       }
  73       Node n = b;
  74       Dump("clauses") << AssertCommand(Expr(n.toExpr()));
  75     }
  76   }
  77   d_satSolver->addClause(c, d_removable, d_proofId);
  78 }
  79
  80 void CnfStream::assertClause(TNode node, SatLiteral a) {
  81   SatClause clause(1);
  82   clause[0] = a;
  83   assertClause(node, clause);
  84 }
  85
  86 void CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b) {
  87   SatClause clause(2);
  88   clause[0] = a;
  89   clause[1] = b;
  90   assertClause(node, clause);
  91 }
  92
  93 void CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c) {
  94   SatClause clause(3);
  95   clause[0] = a;
  96   clause[1] = b;
  97   clause[2] = c;
  98   assertClause(node, clause);
  99 }
 100
 101 bool CnfStream::hasLiteral(TNode n) const {
 102   NodeToLiteralMap::const_iterator find = d_nodeToLiteralMap.find(n);
 103   return find != d_nodeToLiteralMap.end();
 104 }
 105
 106 void TseitinCnfStream::ensureLiteral(TNode n) {
 107   // These are not removable and have no proof ID
 108   d_removable = false;
 109   d_proofId = uint64_t(-1);
 110
 111   Debug("cnf") << "ensureLiteral(" << n << ")" << endl;
 112   if(hasLiteral(n)) {
 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());
 118     }
 119     return;
 120   }
 121
 122   AlwaysAssertArgument(n.getType().isBoolean(), n,
 123                        "CnfStream::ensureLiteral() requires a node of Boolean type.\n"
 124                        "got node: %s\n"
 125                        "its type: %s\n",
 126                        n.toString().c_str(),
 127                        n.getType().toString().c_str());
 128
 129   bool negated CVC4_UNUSED = false;
 130   SatLiteral lit;
 131
 132   if(n.getKind() == kind::NOT) {
 133     negated = true;
 134     n = n[0];
 135   }
 136
 137   if( theory::Theory::theoryOf(n) == theory::THEORY_BOOL &&
 138       !n.isVar() ) {
 139     // If we were called with something other than a theory atom (or
 140     // Boolean variable), we get a SatLiteral that is definitionally
 141     // equal to it.
 142     lit = toCNF(n, false);
 143
 144     // Store backward-mappings
 145     // These may already exist
 146     d_literalToNodeMap.insert_safe(lit, n);
 147     d_literalToNodeMap.insert_safe(~lit, n.notNode());
 148   } else {
 149     // We have a theory atom or variable.
 150     lit = convertAtom(n);
 151   }
 152
 153   Assert(hasLiteral(n) && getNode(lit) == n);
 154   Debug("ensureLiteral") << "CnfStream::ensureLiteral(): out lit is " << lit << std::endl;
 155 }
 156
 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);
 160
 161   // Get the literal for this node
 162   SatLiteral lit;
 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());
 168       } else {
 169         lit = SatLiteral(d_satSolver->falseVar());
 170       }
 171     } else {
 172       lit = SatLiteral(d_satSolver->newVar(isTheoryAtom, preRegister, canEliminate));
 173     }
 174     d_nodeToLiteralMap.insert(node, lit);
 175     d_nodeToLiteralMap.insert(node.notNode(), ~lit);
 176   } else {
 177     lit = getLiteral(node);
 178   }
 179
 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")) ) {
 184
 185     d_literalToNodeMap.insert_safe(lit, node);
 186     d_literalToNodeMap.insert_safe(~lit, node.notNode());
 187   }
 188
 189   // If a theory literal, we pre-register it
 190   if (preRegister) {
 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;
 197   }
 198
 199   // Here, you can have it
 200   Debug("cnf") << "newLiteral(" << node << ") => " << lit << endl;
 201
 202   return lit;
 203 }
 204
 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];
 209 }
 210
 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);
 215   }
 216 }
 217
 218 SatLiteral CnfStream::convertAtom(TNode node) {
 219   Debug("cnf") << "convertAtom(" << node << ")" << endl;
 220
 221   Assert(!hasLiteral(node), "atom already mapped!");
 222
 223   bool theoryLiteral = false;
 224   bool canEliminate = true;
 225   bool preRegister = false;
 226
 227   // Is this a variable add it to the list
 228   if (node.isVar()) {
 229     d_booleanVariables.push_back(node);
 230   } else {
 231     theoryLiteral = true;
 232     canEliminate = false;
 233     preRegister = true;
 234   }
 235
 236   // Make a new literal (variables are not considered theory literals)
 237   SatLiteral lit = newLiteral(node, theoryLiteral, preRegister, canEliminate);
 238   // Return the resulting literal
 239   return lit;
 240 }
 241
 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;
 247   return literal;
 248 }
 249
 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");
 255
 256   SatLiteral a = toCNF(xorNode[0]);
 257   SatLiteral b = toCNF(xorNode[1]);
 258
 259   SatLiteral xorLit = newLiteral(xorNode);
 260
 261   assertClause(xorNode, a, b, ~xorLit);
 262   assertClause(xorNode, ~a, ~b, ~xorLit);
 263   assertClause(xorNode, a, ~b, xorLit);
 264   assertClause(xorNode, ~a, b, xorLit);
 265
 266   return xorLit;
 267 }
 268
 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");
 274
 275   // Number of children
 276   unsigned n_children = orNode.getNumChildren();
 277
 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);
 284   }
 285
 286   // Get the literal for this node
 287   SatLiteral orLit = newLiteral(orNode);
 288
 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]);
 294   }
 295
 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);
 301
 302   // Return the literal
 303   return orLit;
 304 }
 305
 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");
 311
 312   // Number of children
 313   unsigned n_children = andNode.getNumChildren();
 314
 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);
 321   }
 322
 323   // Get the literal for this node
 324   SatLiteral andLit = newLiteral(andNode);
 325
 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]);
 331   }
 332
 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);
 339
 340   return andLit;
 341 }
 342
 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");
 348
 349   // Convert the children to cnf
 350   SatLiteral a = toCNF(impliesNode[0]);
 351   SatLiteral b = toCNF(impliesNode[1]);
 352
 353   SatLiteral impliesLit = newLiteral(impliesNode);
 354
 355   // lit -> (a->b)
 356   // ~lit | ~ a | b
 357   assertClause(impliesNode, ~impliesLit, ~a, b);
 358
 359   // (a->b) -> lit
 360   // ~(~a | b) | lit
 361   // (a | l) & (~b | l)
 362   assertClause(impliesNode, a, impliesLit);
 363   assertClause(impliesNode, ~b, impliesLit);
 364
 365   return impliesLit;
 366 }
 367
 368
 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!");
 373
 374   Debug("cnf") << "handleIff(" << iffNode << ")" << endl;
 375
 376   // Convert the children to CNF
 377   SatLiteral a = toCNF(iffNode[0]);
 378   SatLiteral b = toCNF(iffNode[1]);
 379
 380   // Get the now literal
 381   SatLiteral iffLit = newLiteral(iffNode);
 382
 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);
 388
 389   // (a<->b) -> lit
 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);
 396
 397   return iffLit;
 398 }
 399
 400
 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!");
 405
 406   SatLiteral notLit = ~toCNF(notNode[0]);
 407
 408   return notLit;
 409 }
 410
 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");
 415
 416   Debug("cnf") << "handleIte(" << iteNode[0] << " " << iteNode[1] << " " << iteNode[2] << ")" << endl;
 417
 418   SatLiteral condLit = toCNF(iteNode[0]);
 419   SatLiteral thenLit = toCNF(iteNode[1]);
 420   SatLiteral elseLit = toCNF(iteNode[2]);
 421
 422   SatLiteral iteLit = newLiteral(iteNode);
 423
 424   // If ITE is true then one of the branches is true and the condition
 425   // implies which one
 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);
 433
 434   // If ITE is false then one of the branches is false and the condition
 435   // implies which one
 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);
 443
 444   return iteLit;
 445 }
 446
 447
 448 SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) {
 449   Debug("cnf") << "toCNF(" << node << ", negated = " << (negated ? "true" : "false") << ")" << endl;
 450
 451   SatLiteral nodeLit;
 452   Node negatedNode = node.notNode();
 453
 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);
 458   } else {
 459     // Handle each Boolean operator case
 460     switch(node.getKind()) {
 461     case NOT:
 462       nodeLit = handleNot(node);
 463       break;
 464     case XOR:
 465       nodeLit = handleXor(node);
 466       break;
 467     case ITE:
 468       nodeLit = handleIte(node);
 469       break;
 470     case IFF:
 471       nodeLit = handleIff(node);
 472       break;
 473     case IMPLIES:
 474       nodeLit = handleImplies(node);
 475       break;
 476     case OR:
 477       nodeLit = handleOr(node);
 478       break;
 479     case AND:
 480       nodeLit = handleAnd(node);
 481       break;
 482     case EQUAL:
 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]));
 486       } else {
 487         nodeLit = convertAtom(node);
 488       }
 489       break;
 490     default:
 491       {
 492         //TODO make sure this does not contain any boolean substructure
 493         nodeLit = convertAtom(node);
 494         //Unreachable();
 495         //Node atomic = handleNonAtomicNode(node);
 496         //return isCached(atomic) ? lookupInCache(atomic) : convertAtom(atomic);
 497       }
 498       break;
 499     }
 500   }
 501
 502   // Return the appropriate (negated) literal
 503   if (!negated) return nodeLit;
 504   else return ~nodeLit;
 505 }
 506
 507 void TseitinCnfStream::convertAndAssertAnd(TNode node, bool negated) {
 508   Assert(node.getKind() == AND);
 509   if (!negated) {
 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);
 514     }
 515   } else {
 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);
 523     }
 524     Assert(disjunct == node.end());
 525     assertClause(node, clause);
 526   }
 527 }
 528
 529 void TseitinCnfStream::convertAndAssertOr(TNode node, bool negated) {
 530   Assert(node.getKind() == OR);
 531   if (!negated) {
 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);
 539     }
 540     Assert(disjunct == node.end());
 541     assertClause(node, clause);
 542   } else {
 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);
 547     }
 548   }
 549 }
 550
 551 void TseitinCnfStream::convertAndAssertXor(TNode node, bool negated) {
 552   if (!negated) {
 553     // p XOR q
 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);
 558     clause1[0] = ~p;
 559     clause1[1] = ~q;
 560     assertClause(node, clause1);
 561     SatClause clause2(2);
 562     clause2[0] = p;
 563     clause2[1] = q;
 564     assertClause(node, clause2);
 565   } else {
 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);
 571     clause1[0] = ~p;
 572     clause1[1] = q;
 573     assertClause(node, clause1);
 574     SatClause clause2(2);
 575     clause2[0] = p;
 576     clause2[1] = ~q;
 577     assertClause(node, clause2);
 578   }
 579 }
 580
 581 void TseitinCnfStream::convertAndAssertIff(TNode node, bool negated) {
 582   if (!negated) {
 583     // p <=> q
 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);
 588     clause1[0] = ~p;
 589     clause1[1] = q;
 590     assertClause(node, clause1);
 591     SatClause clause2(2);
 592     clause2[0] = p;
 593     clause2[1] = ~q;
 594     assertClause(node, clause2);
 595   } else {
 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);
 601     clause1[0] = ~p;
 602     clause1[1] = ~q;
 603     assertClause(node, clause1);
 604     SatClause clause2(2);
 605     clause2[0] = p;
 606     clause2[1] = q;
 607     assertClause(node, clause2);
 608   }
 609 }
 610
 611 void TseitinCnfStream::convertAndAssertImplies(TNode node, bool negated) {
 612   if (!negated) {
 613     // p => q
 614     SatLiteral p = toCNF(node[0], false);
 615     SatLiteral q = toCNF(node[1], false);
 616     // Construct the clause ~p || q
 617     SatClause clause(2);
 618     clause[0] = ~p;
 619     clause[1] = 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);
 625   }
 626 }
 627
 628 void TseitinCnfStream::convertAndAssertIte(TNode node, bool negated) {
 629   // ITE(p, q, r)
 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);
 636   clause1[0] = ~p;
 637   clause1[1] = q;
 638   assertClause(node, clause1);
 639   SatClause clause2(2);
 640   clause2[0] = p;
 641   clause2[1] = r;
 642   assertClause(node, clause2);
 643 }
 644
 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;
 658   } else {
 659     // We aren't producing proofs or unsat cores; use an invalid proof id.
 660     d_proofId = uint64_t(-1);
 661   }
 662   convertAndAssert(node, negated);
 663 }
 664
 665 void TseitinCnfStream::convertAndAssert(TNode node, bool negated) {
 666   Debug("cnf") << "convertAndAssert(" << node << ", negated = " << (negated ? "true" : "false") << ")" << endl;
 667
 668   switch(node.getKind()) {
 669   case AND:
 670     convertAndAssertAnd(node, negated);
 671     break;
 672   case OR:
 673     convertAndAssertOr(node, negated);
 674     break;
 675   case IFF:
 676     convertAndAssertIff(node, negated);
 677     break;
 678   case XOR:
 679     convertAndAssertXor(node, negated);
 680     break;
 681   case IMPLIES:
 682     convertAndAssertImplies(node, negated);
 683     break;
 684   case ITE:
 685     convertAndAssertIte(node, negated);
 686     break;
 687   case NOT:
 688     convertAndAssert(node[0], !negated);
 689     break;
 690   default:
 691     // Atoms
 692     assertClause(node, toCNF(node, negated));
 693     break;
 694   }
 695 }
 696
 697 }/* CVC4::prop namespace */
 698 }/* CVC4 namespace */