src/prop/cnf_stream.cpp

   1 /*********************                                                        */
   2 /*! \file cnf_stream.cpp
   3  ** \verbatim
   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
  13  **
  14  ** \brief A CNF converter that takes in asserts and has the side effect
  15  ** of given an equisatisfiable stream of assertions to PropEngine.
  16  **
  17  ** A CNF converter that takes in asserts and has the side effect
  18  ** of given an equisatisfiable stream of assertions to PropEngine.
  19  **/
  20
  21 #include "sat.h"
  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"
  27
  28 #include <queue>
  29
  30 using namespace std;
  31 using namespace CVC4::kind;
  32
  33 namespace CVC4 {
  34 namespace prop {
  35
  36 CnfStream::CnfStream(SatInputInterface *satSolver) :
  37   d_satSolver(satSolver) {
  38 }
  39
  40 TseitinCnfStream::TseitinCnfStream(SatInputInterface* satSolver) :
  41   CnfStream(satSolver) {
  42 }
  43
  44 void CnfStream::assertClause(TNode node, SatClause& c) {
  45   Debug("cnf") << "Inserting into stream " << c << endl;
  46   d_satSolver->addClause(c, d_assertingLemma);
  47 }
  48
  49 void CnfStream::assertClause(TNode node, SatLiteral a) {
  50   SatClause clause(1);
  51   clause[0] = a;
  52   assertClause(node, clause);
  53 }
  54
  55 void CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b) {
  56   SatClause clause(2);
  57   clause[0] = a;
  58   clause[1] = b;
  59   assertClause(node, clause);
  60 }
  61
  62 void CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c) {
  63   SatClause clause(3);
  64   clause[0] = a;
  65   clause[1] = b;
  66   clause[2] = c;
  67   assertClause(node, clause);
  68 }
  69
  70 bool CnfStream::isCached(TNode n) const {
  71   return d_translationCache.find(n) != d_translationCache.end();
  72 }
  73
  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;
  77 }
  78
  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;
  84 }
  85
  86 SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) {
  87   SatLiteral lit = Minisat::mkLit(d_satSolver->newVar(theoryLiteral));
  88   cacheTranslation(node, lit);
  89   if (theoryLiteral) {
  90     d_nodeCache[lit] = node;
  91     d_nodeCache[~lit] = node.notNode();
  92   }
  93   return lit;
  94 }
  95
  96 Node CnfStream::getNode(const SatLiteral& literal) {
  97   NodeCache::iterator find = d_nodeCache.find(literal);
  98   Assert(find != d_nodeCache.end());
  99   return find->second;
 100 }
 101
 102 SatLiteral CnfStream::convertAtom(TNode node) {
 103   Debug("cnf") << "convertAtom(" << node << ")" << endl;
 104
 105   Assert(!isCached(node), "atom already mapped!");
 106
 107   bool theoryLiteral = node.getKind() != kind::VARIABLE;
 108   SatLiteral lit = newLiteral(node, theoryLiteral);
 109
 110   if(node.getKind() == kind::CONST_BOOLEAN) {
 111     if(node.getConst<bool>()) {
 112       assertClause(node, lit);
 113     } else {
 114       assertClause(node, ~lit);
 115     }
 116   }
 117
 118   return lit;
 119 }
 120
 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;
 126   return literal;
 127 }
 128
 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!");
 133
 134   SatLiteral a = toCNF(xorNode[0]);
 135   SatLiteral b = toCNF(xorNode[1]);
 136
 137   SatLiteral xorLit = newLiteral(xorNode);
 138
 139   assertClause(xorNode, a, b, ~xorLit);
 140   assertClause(xorNode, ~a, ~b, ~xorLit);
 141   assertClause(xorNode, a, ~b, xorLit);
 142   assertClause(xorNode, ~a, b, xorLit);
 143
 144   return xorLit;
 145 }
 146
 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!");
 151
 152   // Number of children
 153   unsigned n_children = orNode.getNumChildren();
 154
 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);
 161   }
 162
 163   // Get the literal for this node
 164   SatLiteral orLit = newLiteral(orNode);
 165
 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]);
 171   }
 172
 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);
 178
 179   // Return the literal
 180   return orLit;
 181 }
 182
 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!");
 187
 188   // Number of children
 189   unsigned n_children = andNode.getNumChildren();
 190
 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);
 197   }
 198
 199   // Get the literal for this node
 200   SatLiteral andLit = newLiteral(andNode);
 201
 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]);
 207   }
 208
 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);
 215   return andLit;
 216 }
 217
 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!");
 222
 223   // Convert the children to cnf
 224   SatLiteral a = toCNF(impliesNode[0]);
 225   SatLiteral b = toCNF(impliesNode[1]);
 226
 227   SatLiteral impliesLit = newLiteral(impliesNode);
 228
 229   // lit -> (a->b)
 230   // ~lit | ~ a | b
 231   assertClause(impliesNode, ~impliesLit, ~a, b);
 232
 233   // (a->b) -> lit
 234   // ~(~a | b) | lit
 235   // (a | l) & (~b | l)
 236   assertClause(impliesNode, a, impliesLit);
 237   assertClause(impliesNode, ~b, impliesLit);
 238
 239   return impliesLit;
 240 }
 241
 242
 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!");
 247
 248   Debug("cnf") << "handleIff(" << iffNode << ")" << endl;
 249
 250   // Convert the children to CNF
 251   SatLiteral a = toCNF(iffNode[0]);
 252   SatLiteral b = toCNF(iffNode[1]);
 253
 254   // Get the now literal
 255   SatLiteral iffLit = newLiteral(iffNode);
 256
 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);
 262
 263   // (a<->b) -> lit
 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);
 270
 271   return iffLit;
 272 }
 273
 274
 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!");
 279
 280   SatLiteral notLit = ~toCNF(notNode[0]);
 281
 282   // Since we don't introduce new variables, we need to cache the translation
 283   cacheTranslation(notNode, notLit);
 284
 285   return notLit;
 286 }
 287
 288 SatLiteral TseitinCnfStream::handleIte(TNode iteNode) {
 289   Assert(iteNode.getKind() == ITE);
 290   Assert(iteNode.getNumChildren() == 3);
 291
 292   Debug("cnf") << "handleIte(" << iteNode[0] << " " << iteNode[1] << " " << iteNode[2] << ")" << endl;
 293
 294   SatLiteral condLit = toCNF(iteNode[0]);
 295   SatLiteral thenLit = toCNF(iteNode[1]);
 296   SatLiteral elseLit = toCNF(iteNode[2]);
 297
 298   SatLiteral iteLit = newLiteral(iteNode);
 299
 300   // If ITE is true then one of the branches is true and the condition
 301   // implies which one
 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);
 309
 310   // If ITE is false then one of the branches is false and the condition
 311   // implies which one
 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);
 319
 320   return iteLit;
 321 }
 322
 323
 324 SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) {
 325   Debug("cnf") << "toCNF(" << node << ", negated = " << (negated ? "true" : "false") << ")" << endl;
 326
 327   SatLiteral nodeLit;
 328   Node negatedNode = node.notNode();
 329
 330   // If the non-negated node has already been translated, get the translation
 331   if(isCached(node)) {
 332     nodeLit = lookupInCache(node);
 333   } else {
 334     // Handle each Boolean operator case
 335     switch(node.getKind()) {
 336     case NOT:
 337       nodeLit = handleNot(node);
 338       break;
 339     case XOR:
 340       nodeLit = handleXor(node);
 341       break;
 342     case ITE:
 343       nodeLit = handleIte(node);
 344       break;
 345     case IFF:
 346       nodeLit = handleIff(node);
 347       break;
 348     case IMPLIES:
 349       nodeLit = handleImplies(node);
 350       break;
 351     case OR:
 352       nodeLit = handleOr(node);
 353       break;
 354     case AND:
 355       nodeLit = handleAnd(node);
 356       break;
 357     case EQUAL:
 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]));
 362       } else {
 363         nodeLit = convertAtom(node);
 364       }
 365       break;
 366     default:
 367       {
 368         //TODO make sure this does not contain any boolean substructure
 369         nodeLit = convertAtom(node);
 370         //Unreachable();
 371         //Node atomic = handleNonAtomicNode(node);
 372         //return isCached(atomic) ? lookupInCache(atomic) : convertAtom(atomic);
 373       }
 374     }
 375   }
 376
 377   // Return the appropriate (negated) literal
 378   if (!negated) return nodeLit;
 379   else return ~nodeLit;
 380 }
 381
 382 void TseitinCnfStream::convertAndAssertAnd(TNode node, bool lemma, bool negated) {
 383   Assert(node.getKind() == AND);
 384   if (!negated) {
 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);
 389     }
 390   } else {
 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);
 398     }
 399     Assert(disjunct == node.end());
 400     assertClause(node, clause);
 401   }
 402 }
 403
 404 void TseitinCnfStream::convertAndAssertOr(TNode node, bool lemma, bool negated) {
 405   Assert(node.getKind() == OR);
 406   if (!negated) {
 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);
 414     }
 415     Assert(disjunct == node.end());
 416     assertClause(node, clause);
 417   } else {
 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);
 422     }
 423   }
 424 }
 425
 426 void TseitinCnfStream::convertAndAssertXor(TNode node, bool lemma, bool negated) {
 427   if (!negated) {
 428     // p XOR q
 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);
 433     clause1[0] = ~p;
 434     clause1[1] = ~q;
 435     assertClause(node, clause1);
 436     SatClause clause2(2);
 437     clause2[0] = p;
 438     clause2[1] = q;
 439     assertClause(node, clause2);
 440   } else {
 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);
 446     clause1[0] = ~p;
 447     clause1[1] = q;
 448     assertClause(node, clause1);
 449     SatClause clause2(2);
 450     clause2[0] = p;
 451     clause2[1] = ~q;
 452     assertClause(node, clause2);
 453   }
 454 }
 455
 456 void TseitinCnfStream::convertAndAssertIff(TNode node, bool lemma, bool negated) {
 457   if (!negated) {
 458     // p <=> q
 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);
 463     clause1[0] = ~p;
 464     clause1[1] = q;
 465     assertClause(node, clause1);
 466     SatClause clause2(2);
 467     clause2[0] = p;
 468     clause2[1] = ~q;
 469     assertClause(node, clause2);
 470   } else {
 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);
 476     clause1[0] = ~p;
 477     clause1[1] = ~q;
 478     assertClause(node, clause1);
 479     SatClause clause2(2);
 480     clause2[0] = p;
 481     clause2[1] = q;
 482     assertClause(node, clause2);
 483   }
 484 }
 485
 486 void TseitinCnfStream::convertAndAssertImplies(TNode node, bool lemma, bool negated) {
 487   if (!negated) {
 488     // p => q
 489     SatLiteral p = toCNF(node[0], false);
 490     SatLiteral q = toCNF(node[1], false);
 491     // Construct the clause ~p || q
 492     SatClause clause(2);
 493     clause[0] = ~p;
 494     clause[1] = 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);
 500   }
 501 }
 502
 503 void TseitinCnfStream::convertAndAssertIte(TNode node, bool lemma, bool negated) {
 504   // ITE(p, q, r)
 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);
 511   clause1[0] = ~p;
 512   clause1[1] = q;
 513   assertClause(node, clause1);
 514   SatClause clause2(2);
 515   clause2[0] = p;
 516   clause2[1] = r;
 517   assertClause(node, clause2);
 518   SatClause clause3(2);
 519   clause3[0] = q;
 520   clause3[1] = ~p;
 521   assertClause(node, clause3);
 522   SatClause clause4(2);
 523   clause4[0] = r;
 524   clause4[1] = p;
 525   assertClause(node, clause4);
 526 }
 527
 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()) {
 535   case AND:
 536     convertAndAssertAnd(node, lemma, negated);
 537     break;
 538   case OR:
 539     convertAndAssertOr(node, lemma, negated);
 540     break;
 541   case IFF:
 542     convertAndAssertIff(node, lemma, negated);
 543     break;
 544   case XOR:
 545     convertAndAssertXor(node, lemma, negated);
 546     break;
 547   case IMPLIES:
 548     convertAndAssertImplies(node, lemma, negated);
 549     break;
 550   case ITE:
 551     convertAndAssertIte(node, lemma, negated);
 552     break;
 553   case NOT:
 554     convertAndAssert(node[0], lemma, !negated);
 555     break;
 556   default:
 557     // Atoms
 558     assertClause(node, toCNF(node, negated));
 559     break;
 560   }
 561 }
 562
 563 }/* CVC4::prop namespace */
 564 }/* CVC4 namespace */