src/theory/sets/theory_sets_private.cpp

   1 /*********************                                                        */
   2 /*! \file theory_sets_private.cpp
   3  ** \verbatim
   4  ** Original author: Kshitij Bansal
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2013-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 Sets theory implementation.
  13  **
  14  ** Sets theory implementation.
  15  **/
  16
  17 #include <boost/foreach.hpp>
  18
  19 #include "theory/theory_model.h"
  20 #include "theory/sets/theory_sets.h"
  21 #include "theory/sets/theory_sets_private.h"
  22
  23 #include "theory/sets/options.h"
  24 #include "theory/sets/expr_patterns.h" // ONLY included here
  25
  26 #include "util/emptyset.h"
  27 #include "util/result.h"
  28
  29 using namespace std;
  30 using namespace CVC4::expr::pattern;
  31
  32 namespace CVC4 {
  33 namespace theory {
  34 namespace sets {
  35
  36 const char* element_of_str = " \u2208 ";
  37
  38 /**************************** TheorySetsPrivate *****************************/
  39 /**************************** TheorySetsPrivate *****************************/
  40 /**************************** TheorySetsPrivate *****************************/
  41
  42 void TheorySetsPrivate::check(Theory::Effort level) {
  43
  44   CodeTimer checkCodeTimer(d_statistics.d_checkTime);
  45
  46   while(!d_external.done() && !d_conflict) {
  47     // Get all the assertions
  48     Assertion assertion = d_external.get();
  49     TNode fact = assertion.assertion;
  50
  51     Debug("sets") << "\n\n[sets] TheorySetsPrivate::check(): processing "
  52                   << fact << std::endl;
  53
  54     bool polarity = fact.getKind() != kind::NOT;
  55     TNode atom = polarity ? fact : fact[0];
  56
  57     if (!assertion.isPreregistered) {
  58       if (atom.getKind() == kind::EQUAL) {
  59         if (!d_equalityEngine.hasTerm(atom[0])) {
  60           Assert(atom[0].isConst());
  61           d_equalityEngine.addTerm(atom[0]);
  62         }
  63         if (!d_equalityEngine.hasTerm(atom[1])) {
  64           Assert(atom[1].isConst());
  65           d_equalityEngine.addTerm(atom[1]);
  66         }
  67       }
  68     }
  69
  70     // Solve each
  71     switch(atom.getKind()) {
  72     case kind::EQUAL:
  73       Debug("sets") << atom[0] << " should " << (polarity ? "":"NOT ")
  74                     << "be equal to " << atom[1] << std::endl;
  75       assertEquality(fact, fact, /* learnt = */ false);
  76       break;
  77
  78     case kind::MEMBER:
  79       Debug("sets") << atom[0] << " should " << (polarity ? "":"NOT ")
  80                     << "be in " << atom[1] << std::endl;
  81       assertMemebership(fact, fact, /* learnt = */ false);
  82       break;
  83
  84     default:
  85       Unhandled(fact.getKind());
  86     }
  87     finishPropagation();
  88
  89     Debug("sets") << "[sets]  in conflict = " << d_conflict << std::endl;
  90     Assert( d_conflict ^ d_equalityEngine.consistent() );
  91     if(d_conflict) return;
  92     Debug("sets") << "[sets]  is complete = " << isComplete() << std::endl;
  93   }
  94
  95   if( (Theory::EFFORT_FULL || options::setsEagerLemmas() ) && !isComplete()) {
  96     d_external.d_out->lemma(getLemma());
  97   }
  98
  99   return;
 100 }/* TheorySetsPrivate::check() */
 101
 102
 103 void TheorySetsPrivate::assertEquality(TNode fact, TNode reason, bool learnt)
 104 {
 105   Debug("sets-assert") << "\n[sets-assert] adding equality: " << fact
 106                        << ", " << reason
 107                        << ", " << learnt << std::endl;
 108
 109   bool polarity = fact.getKind() != kind::NOT;
 110   TNode atom = polarity ? fact : fact[0];
 111
 112   // fact already holds
 113   if( holds(atom, polarity) ) {
 114     Debug("sets-assert") << "[sets-assert]   already present, skipping" << std::endl;
 115     return;
 116   }
 117
 118   // assert fact & check for conflict
 119   if(learnt) {
 120     registerReason(reason, /*save=*/ true);
 121   }
 122   d_equalityEngine.assertEquality(atom, polarity, reason);
 123
 124   if(!d_equalityEngine.consistent()) {
 125     Debug("sets-assert") << "[sets-assert]   running into a conflict" << std::endl;
 126     d_conflict = true;
 127     return;
 128   }
 129
 130   if(!polarity && atom[0].getType().isSet()) {
 131     addToPending(atom);
 132   }
 133
 134 }/* TheorySetsPrivate::assertEquality() */
 135
 136
 137 void TheorySetsPrivate::assertMemebership(TNode fact, TNode reason, bool learnt)
 138 {
 139   Debug("sets-assert") << "\n[sets-assert] adding membership: " << fact
 140                        << ", " << reason
 141                        << ", " << learnt << std::endl;
 142
 143   bool polarity = fact.getKind() == kind::NOT ? false : true;
 144   TNode atom = polarity ? fact : fact[0];
 145
 146   // fact already holds
 147   if( holds(atom, polarity) ) {
 148     Debug("sets-assert") << "[sets-assert]   already present, skipping" << std::endl;
 149     return;
 150   }
 151
 152   // assert fact & check for conflict
 153   if(learnt) {
 154     registerReason(reason, true);
 155   }
 156   d_equalityEngine.assertPredicate(atom, polarity, reason);
 157
 158   if(!d_equalityEngine.consistent()) {
 159     Debug("sets-assert") << "[sets-assert]   running into a conflict" << std::endl;
 160     d_conflict = true;
 161     return;
 162   }
 163
 164   // update term info data structures
 165   d_termInfoManager->notifyMembership(fact);
 166
 167   // propagation
 168   TNode x = d_equalityEngine.getRepresentative(atom[0]);
 169   eq::EqClassIterator j(d_equalityEngine.getRepresentative(atom[1]),
 170                         &d_equalityEngine);
 171   TNode S = (*j);
 172   Node cur_atom = MEMBER(x, S);
 173
 174   /**
 175    * It is sufficient to do emptyset propagation outside the loop as
 176    * constant term is guaranteed to be class representative.
 177    */
 178   if(polarity && S.getKind() == kind::EMPTYSET) {
 179     Debug("sets-prop") << "[sets-prop]  something in empty set? conflict."
 180                        << std::endl;
 181     learnLiteral(cur_atom, false, cur_atom);
 182     Assert(d_conflict);
 183     return;
 184   }
 185
 186   for(; !j.isFinished(); ++j) {
 187     TNode S = (*j);
 188     Node cur_atom = MEMBER(x, S);
 189
 190     // propagation : children
 191     Debug("sets-prop") << "[sets-prop] Propagating 'down' for "
 192                        << x << element_of_str << S << std::endl;
 193     if(S.getKind() == kind::UNION ||
 194        S.getKind() == kind::INTERSECTION ||
 195        S.getKind() == kind::SETMINUS ||
 196        S.getKind() == kind::SET_SINGLETON) {
 197       doSettermPropagation(x, S);
 198       if(d_conflict) return;
 199     }// propagation: children
 200
 201
 202     // propagation : parents
 203     Debug("sets-prop") << "[sets-prop] Propagating 'up' for "
 204                        << x << element_of_str << S << std::endl;
 205     const CDTNodeList* parentList = d_termInfoManager->getParents(S);
 206     for(typeof(parentList->begin()) k = parentList->begin();
 207         k != parentList->end(); ++k) {
 208       doSettermPropagation(x, *k);
 209       if(d_conflict) return;
 210     }// propagation : parents
 211
 212
 213   }//j loop
 214
 215 }/* TheorySetsPrivate::assertMemebership() */
 216
 217
 218 void TheorySetsPrivate::doSettermPropagation(TNode x, TNode S)
 219 {
 220   Debug("sets-prop") << "[sets-prop] doSettermPropagation("
 221                      << x << ", " << S << std::endl;
 222
 223   Assert(S.getType().isSet() && S.getType().getSetElementType() == x.getType());
 224
 225   Node literal, left_literal, right_literal;
 226
 227   // axiom: literal <=> left_literal AND right_literal
 228   switch(S.getKind()) {
 229   case kind::INTERSECTION:
 230     literal       =       MEMBER(x, S)      ;
 231     left_literal  =       MEMBER(x, S[0])   ;
 232     right_literal =       MEMBER(x, S[1])   ;
 233     break;
 234   case kind::UNION:
 235     literal       = NOT(  MEMBER(x, S)     );
 236     left_literal  = NOT(  MEMBER(x, S[0])  );
 237     right_literal = NOT(  MEMBER(x, S[1])  );
 238     break;
 239   case kind::SETMINUS:
 240     literal       =       MEMBER(x, S)      ;
 241     left_literal  =       MEMBER(x, S[0])   ;
 242     right_literal = NOT(  MEMBER(x, S[1])  );
 243     break;
 244   case kind::SET_SINGLETON: {
 245     Node atom = MEMBER(x, S);
 246     if(holds(atom, true)) {
 247       learnLiteral(EQUAL(x, S[0]), true, atom);
 248     } else if(holds(atom, false)) {
 249       learnLiteral(EQUAL(x, S[0]), false, NOT(atom));
 250     }
 251     return;
 252   }
 253   default:
 254     Unhandled();
 255   }
 256
 257   Debug("sets-prop-details")
 258     << "[sets-prop-details]   " << literal << " IFF " << left_literal
 259     << " AND " << right_literal << std::endl;
 260
 261   Debug("sets-prop-details")
 262     << "[sets-prop-details]   "
 263     << (holds(literal) ? "yes" : (holds(literal.negate()) ? " no" : " _ "))
 264     << " IFF "
 265     << (holds(left_literal) ? "yes" : (holds(left_literal.negate()) ? "no " : " _ "))
 266     << " AND "
 267     << (holds(right_literal) ? "yes" : (holds(right_literal.negate()) ? "no " : " _ "))
 268     << std::endl;
 269
 270   Assert( present( MEMBER(x, S)    ) ||
 271           present( MEMBER(x, S[0]) ) ||
 272           present( MEMBER(x, S[1]) ) );
 273
 274   if( holds(literal) ) {
 275     // 1a. literal => left_literal
 276     Debug("sets-prop") << "[sets-prop]  ... via case 1a. ..." << std::endl;
 277     learnLiteral(left_literal, literal);
 278     if(d_conflict) return;
 279
 280     // 1b. literal => right_literal
 281     Debug("sets-prop") << "[sets-prop]  ... via case 1b. ..." << std::endl;
 282     learnLiteral(right_literal, literal);
 283     if(d_conflict) return;
 284
 285     // subsumption requirement met, exit
 286     return;
 287   }
 288   else if( holds(literal.negate() ) ) {
 289     // 4. neg(literal), left_literal => neg(right_literal)
 290     if( holds(left_literal) ) {
 291       Debug("sets-prop") << "[sets-prop]  ... via case 4. ..." << std::endl;
 292       learnLiteral(right_literal.negate(), AND( literal.negate(),
 293                                                 left_literal) );
 294       if(d_conflict) return;
 295     }
 296
 297     // 5. neg(literal), right_literal => neg(left_literal)
 298     if( holds(right_literal) ) {
 299       Debug("sets-prop") << "[sets-prop]  ... via case 5. ..." << std::endl;
 300       learnLiteral(left_literal.negate(), AND( literal.negate(),
 301                                                right_literal) );
 302       if(d_conflict) return;
 303     }
 304   }
 305   else {
 306     // 2,3. neg(left_literal) v neg(right_literal) => neg(literal)
 307     if(holds(left_literal.negate())) {
 308       Debug("sets-prop") << "[sets-prop]  ... via case 2. ..." << std::endl;
 309       learnLiteral(literal.negate(), left_literal.negate());
 310       if(d_conflict) return;
 311     }
 312     else if(holds(right_literal.negate())) {
 313       Debug("sets-prop") << "[sets-prop]  ... via case 3. ..." << std::endl;
 314       learnLiteral(literal.negate(), right_literal.negate());
 315       if(d_conflict) return;
 316     }
 317
 318     // 6. the axiom itself:
 319     else if(holds(left_literal) && holds(right_literal)) {
 320       Debug("sets-prop") << "[sets-prop]  ... via case 6. ..." << std::endl;
 321       learnLiteral(literal, AND(left_literal, right_literal) );
 322       if(d_conflict) return;
 323     }
 324   }
 325
 326   // check fulfilling rule
 327   Node n;
 328   switch(S.getKind()) {
 329   case kind::UNION:
 330     if( holds(MEMBER(x, S)) &&
 331         !present( MEMBER(x, S[0]) ) )
 332       addToPending( MEMBER(x, S[0]) );
 333     break;
 334   case kind::SETMINUS: // intentional fallthrough
 335   case kind::INTERSECTION:
 336     if( holds(MEMBER(x, S[0])) &&
 337         !present( MEMBER(x, S[1]) ))
 338       addToPending( MEMBER(x, S[1]) );
 339     break;
 340   default:
 341     Assert(false, "MembershipEngine::doSettermPropagation");
 342   }
 343 }
 344
 345
 346 void TheorySetsPrivate::learnLiteral(TNode atom, bool polarity, Node reason) {
 347   Debug("sets-learn") << "[sets-learn] learnLiteral(" << atom
 348                       << ", " << polarity << ")" << std::endl;
 349
 350   if( holds(atom, polarity) ) {
 351     Debug("sets-learn") << "[sets-learn] \u2514 already known, skipping" << std::endl;
 352     return;
 353   }
 354
 355   if( holds(atom, !polarity) ) {
 356     Debug("sets-learn") << "[sets-learn] \u2514 conflict found" << std::endl;
 357
 358     registerReason(reason, /*save=*/ true);
 359
 360     if(atom.getKind() == kind::EQUAL) {
 361       d_equalityEngine.assertEquality(atom, polarity, reason);
 362     } else {
 363       d_equalityEngine.assertPredicate(atom, polarity, reason);
 364     }
 365     Assert(d_conflict);       // should be marked due to equality engine
 366     return;
 367   }
 368
 369   Assert(atom.getKind() == kind::EQUAL || atom.getKind() == kind::MEMBER);
 370
 371   Node learnt_literal = polarity ? Node(atom) : NOT(atom);
 372   d_propagationQueue.push_back( make_pair(learnt_literal, reason) );
 373 }/*TheorySetsPrivate::learnLiteral(...)*/
 374
 375
 376 /******************** Model generation ********************/
 377 /******************** Model generation ********************/
 378 /******************** Model generation ********************/
 379
 380 const TheorySetsPrivate::Elements& TheorySetsPrivate::getElements
 381 (TNode setterm, SettermElementsMap& settermElementsMap) const {
 382   SettermElementsMap::const_iterator it = settermElementsMap.find(setterm);
 383   bool alreadyCalculated = (it != settermElementsMap.end());
 384   if( !alreadyCalculated ) {
 385
 386     Kind k = setterm.getKind();
 387     unsigned numChildren = setterm.getNumChildren();
 388     Elements cur;
 389     if(numChildren == 2) {
 390       const Elements& left = getElements(setterm[0], settermElementsMap);
 391       const Elements& right = getElements(setterm[1], settermElementsMap);
 392       switch(k) {
 393       case kind::UNION:
 394         if(left.size() >= right.size()) {
 395           cur = left; cur.insert(right.begin(), right.end());
 396         } else {
 397           cur = right; cur.insert(left.begin(), left.end());
 398         }
 399         break;
 400       case kind::INTERSECTION:
 401         std::set_intersection(left.begin(), left.end(), right.begin(), right.end(),
 402                               std::inserter(cur, cur.begin()) );
 403         break;
 404       case kind::SETMINUS:
 405         std::set_difference(left.begin(), left.end(), right.begin(), right.end(),
 406                             std::inserter(cur, cur.begin()) );
 407         break;
 408       default:
 409         Unhandled();
 410       }
 411     } else {
 412       Assert(k == kind::VARIABLE || k == kind::APPLY_UF);
 413       /* assign emptyset, which is default */
 414     }
 415
 416     it = settermElementsMap.insert(SettermElementsMap::value_type(setterm, cur)).first;
 417   }
 418   return it->second;
 419 }
 420
 421
 422
 423 void TheorySetsPrivate::checkModel(const SettermElementsMap& settermElementsMap, TNode S) const {
 424
 425   Debug("sets-model") << "[sets-model] checkModel(..., " << S << "): "
 426                       << std::endl;
 427
 428   Assert(S.getType().isSet());
 429
 430   Elements emptySetOfElements;
 431   const Elements& saved =
 432     d_equalityEngine.getRepresentative(S).getKind() == kind::EMPTYSET ?
 433     emptySetOfElements :
 434     settermElementsMap.find(d_equalityEngine.getRepresentative(S))->second;
 435   Debug("sets-model") << "[sets-model] saved :  { ";
 436   BOOST_FOREACH(TNode element, saved) { Debug("sets-model") << element << ", "; }
 437   Debug("sets-model") << " }" << std::endl;
 438
 439   if(S.getNumChildren() == 2) {
 440
 441     Elements cur, left, right;
 442     left = settermElementsMap.find(d_equalityEngine.getRepresentative(S[0]))->second;
 443     right = settermElementsMap.find(d_equalityEngine.getRepresentative(S[1]))->second;
 444     switch(S.getKind()) {
 445     case kind::UNION:
 446       if(left.size() >= right.size()) {
 447         cur = left; cur.insert(right.begin(), right.end());
 448       } else {
 449         cur = right; cur.insert(left.begin(), left.end());
 450       }
 451       break;
 452     case kind::INTERSECTION:
 453       std::set_intersection(left.begin(), left.end(), right.begin(), right.end(),
 454                             std::inserter(cur, cur.begin()) );
 455       break;
 456     case kind::SETMINUS:
 457       std::set_difference(left.begin(), left.end(), right.begin(), right.end(),
 458                           std::inserter(cur, cur.begin()) );
 459       break;
 460     default:
 461       Unhandled();
 462     }
 463
 464     Debug("sets-model") << "[sets-model] cur :  { ";
 465     BOOST_FOREACH(TNode element, cur) { Debug("sets-model") << element << ", "; }
 466     Debug("sets-model") << " }" << std::endl;
 467
 468     if(saved != cur) {
 469       Debug("sets-model") << "[sets-model] *** ERRROR *** cur != saved "
 470                           << std::endl;
 471       Debug("sets-model") << "[sets-model]   FYI: "
 472                           << "  [" << S << "] = " << d_equalityEngine.getRepresentative(S) << ", "
 473                           << "  [" << S[0] << "] = " << d_equalityEngine.getRepresentative(S[0]) << ", "
 474                           << "  [" << S[1] << "] = " << d_equalityEngine.getRepresentative(S[1]) << "\n";
 475
 476     }
 477     Assert( saved == cur );
 478   }
 479 }
 480
 481 Node TheorySetsPrivate::elementsToShape(Elements elements, TypeNode setType) const
 482 {
 483   NodeManager* nm = NodeManager::currentNM();
 484
 485   if(elements.size() == 0) {
 486     return nm->mkConst(EmptySet(nm->toType(setType)));
 487   } else {
 488     Elements::iterator it = elements.begin();
 489     Node cur = SET_SINGLETON(*it);
 490     while( ++it != elements.end() ) {
 491       cur = nm->mkNode(kind::UNION, cur, SET_SINGLETON(*it));
 492     }
 493     return cur;
 494   }
 495 }
 496
 497 void TheorySetsPrivate::collectModelInfo(TheoryModel* m, bool fullModel)
 498 {
 499   Debug("sets-model") << "[sets-model] collectModelInfo(..., fullModel="
 500                       << (fullModel ? "true)" : "false)") << std::endl;
 501
 502   set<Node> terms;
 503
 504   // Compute terms appearing assertions and shared terms
 505   d_external.computeRelevantTerms(terms);
 506
 507   // Compute for each setterm elements that it contains
 508   SettermElementsMap settermElementsMap;
 509   TNode true_atom = NodeManager::currentNM()->mkConst<bool>(true);
 510   TNode false_atom = NodeManager::currentNM()->mkConst<bool>(false);
 511   for(eq::EqClassIterator it_eqclasses(true_atom, &d_equalityEngine);
 512       ! it_eqclasses.isFinished() ; ++it_eqclasses) {
 513     TNode n = (*it_eqclasses);
 514     if(n.getKind() == kind::MEMBER) {
 515       Assert(d_equalityEngine.areEqual(n, true_atom));
 516       TNode x = d_equalityEngine.getRepresentative(n[0]);
 517       TNode S = d_equalityEngine.getRepresentative(n[1]);
 518       settermElementsMap[S].insert(x);
 519     }
 520   }
 521
 522   // Assert equalities and disequalities to the model
 523   m->assertEqualityEngine(&d_equalityEngine, &terms);
 524
 525   // Loop over terms to collect set-terms for which we generate models
 526   set<Node> settermsModEq;
 527   BOOST_FOREACH(TNode term, terms) {
 528     TNode n = term.getKind() == kind::NOT ? term[0] : term;
 529
 530     Debug("sets-model-details") << "[sets-model-details]  >   " << n << std::endl;
 531
 532     if(n.getType().isSet()) {
 533       n = d_equalityEngine.getRepresentative(n);
 534       if( !n.isConst() ) {
 535         settermsModEq.insert(n);
 536       }
 537     }
 538
 539   }
 540
 541   if(Debug.isOn("sets-model")) {
 542     BOOST_FOREACH( TNode node, settermsModEq ) {
 543       Debug("sets-model") << "[sets-model]   " << node << std::endl;
 544     }
 545   }
 546
 547   BOOST_FOREACH( SettermElementsMap::value_type &it, settermElementsMap ) {
 548     BOOST_FOREACH( TNode element, it.second /* elements */ ) {
 549       Debug("sets-model-details") << "[sets-model-details]  >   " <<
 550         (it.first /* setterm */) << ": " << element << std::endl;
 551     }
 552   }
 553
 554   // assign representatives to equivalence class
 555   BOOST_FOREACH( TNode setterm, settermsModEq ) {
 556     Elements elements = getElements(setterm, settermElementsMap);
 557     Node shape = elementsToShape(elements, setterm.getType());
 558     m->assertEquality(shape, setterm, true);
 559     m->assertRepresentative(shape);
 560   }
 561
 562 #ifdef CVC4_ASSERTIONS
 563   BOOST_FOREACH(TNode term, terms) {
 564     if( term.getType().isSet() ) {
 565       checkModel(settermElementsMap, term);
 566     }
 567   }
 568 #endif
 569 }
 570
 571
 572 /********************** Helper functions ***************************/
 573 /********************** Helper functions ***************************/
 574 /********************** Helper functions ***************************/
 575
 576 Node mkAnd(const std::vector<TNode>& conjunctions) {
 577   Assert(conjunctions.size() > 0);
 578
 579   std::set<TNode> all;
 580
 581   for (unsigned i = 0; i < conjunctions.size(); ++i) {
 582     TNode t = conjunctions[i];
 583
 584     if (t.getKind() == kind::AND) {
 585       for(TNode::iterator child_it = t.begin();
 586           child_it != t.end(); ++child_it) {
 587         Assert((*child_it).getKind() != kind::AND);
 588         all.insert(*child_it);
 589       }
 590     }
 591     else {
 592       all.insert(t);
 593     }
 594
 595   }
 596
 597   Assert(all.size() > 0);
 598
 599   if (all.size() == 1) {
 600     // All the same, or just one
 601     return conjunctions[0];
 602   }
 603
 604   NodeBuilder<> conjunction(kind::AND);
 605   std::set<TNode>::const_iterator it = all.begin();
 606   std::set<TNode>::const_iterator it_end = all.end();
 607   while (it != it_end) {
 608     conjunction << *it;
 609     ++ it;
 610   }
 611
 612   return conjunction;
 613 }/* mkAnd() */
 614
 615
 616 TheorySetsPrivate::Statistics::Statistics() :
 617   d_checkTime("theory::sets::time") {
 618
 619   StatisticsRegistry::registerStat(&d_checkTime);
 620 }
 621
 622
 623 TheorySetsPrivate::Statistics::~Statistics() {
 624   StatisticsRegistry::unregisterStat(&d_checkTime);
 625 }
 626
 627
 628 bool TheorySetsPrivate::present(TNode atom) {
 629   return holds(atom) || holds(atom.notNode());
 630 }
 631
 632
 633 bool TheorySetsPrivate::holds(TNode atom, bool polarity) {
 634   Node polarity_atom = NodeManager::currentNM()->mkConst<bool>(polarity);
 635
 636   Node atomModEq = NodeManager::currentNM()->mkNode
 637     (atom.getKind(), d_equalityEngine.getRepresentative(atom[0]),
 638      d_equalityEngine.getRepresentative(atom[1]) );
 639
 640   d_equalityEngine.addTerm(atomModEq);
 641
 642   return d_equalityEngine.areEqual(atomModEq, polarity_atom);
 643 }
 644
 645
 646 void TheorySetsPrivate::registerReason(TNode reason, bool save)
 647 {
 648   if(save) d_nodeSaver.insert(reason);
 649
 650   if(reason.getKind() == kind::AND) {
 651     Assert(reason.getNumChildren() == 2);
 652     registerReason(reason[0], false);
 653     registerReason(reason[1], false);
 654   } else if(reason.getKind() == kind::NOT) {
 655     registerReason(reason[0], false);
 656   } else if(reason.getKind() == kind::MEMBER) {
 657     d_equalityEngine.addTerm(reason);
 658     Assert(present(reason));
 659   } else if(reason.getKind() == kind::EQUAL) {
 660     d_equalityEngine.addTerm(reason);
 661     Assert(present(reason));
 662   } else if(reason.getKind() == kind::CONST_BOOLEAN) {
 663     // That's OK, already in EqEngine
 664   } else {
 665     Unhandled();
 666   }
 667 }
 668
 669 void TheorySetsPrivate::finishPropagation()
 670 {
 671   while(!d_conflict && !d_settermPropagationQueue.empty()) {
 672     std::pair<TNode,TNode> np = d_settermPropagationQueue.front();
 673     d_settermPropagationQueue.pop();
 674     doSettermPropagation(np.first, np.second);
 675   }
 676   while(!d_conflict && !d_propagationQueue.empty()) {
 677     std::pair<Node,Node> np = d_propagationQueue.front();
 678     d_propagationQueue.pop();
 679     TNode atom = np.first.getKind() == kind::NOT ? np.first[0] : np.first;
 680     if(atom.getKind() == kind::MEMBER) {
 681       assertMemebership(np.first, np.second, /* learnt = */ true);
 682     } else {
 683       assertEquality(np.first, np.second, /* learnt = */ true);
 684     }
 685   }
 686 }
 687
 688 void TheorySetsPrivate::addToPending(Node n) {
 689   Debug("sets-pending") << "[sets-pending] addToPending " << n << std::endl;
 690   if(d_pendingEverInserted.find(n) == d_pendingEverInserted.end()) {
 691     if(n.getKind() == kind::MEMBER) {
 692       Debug("sets-pending") << "[sets-pending] \u2514 added to member queue"
 693                             << std::endl;
 694       d_pending.push(n);
 695     } else {
 696       Debug("sets-pending") << "[sets-pending] \u2514 added to equality queue"
 697                             << std::endl;
 698       Assert(n.getKind() == kind::EQUAL);
 699       d_pendingDisequal.push(n);
 700     }
 701   }
 702 }
 703
 704 bool TheorySetsPrivate::isComplete() {
 705   while(!d_pending.empty() && present(d_pending.front())) {
 706     Debug("sets-pending") << "[sets-pending] removing as already present: "
 707                           << d_pending.front() << std::endl;
 708     d_pending.pop();
 709   }
 710   return d_pending.empty() && d_pendingDisequal.empty();
 711 }
 712
 713 Node TheorySetsPrivate::getLemma() {
 714   Assert(!d_pending.empty() || !d_pendingDisequal.empty());
 715
 716   Node lemma;
 717
 718   if(!d_pending.empty()) {
 719     Node n = d_pending.front();
 720     d_pending.pop();
 721     d_pendingEverInserted.insert(n);
 722
 723     Assert(!present(n));
 724     Assert(n.getKind() == kind::MEMBER);
 725
 726     lemma = OR(n, NOT(n));
 727   } else {
 728     Node n = d_pendingDisequal.front();
 729     d_pendingDisequal.pop();
 730     d_pendingEverInserted.insert(n);
 731
 732     Assert(n.getKind() == kind::EQUAL && n[0].getType().isSet());
 733     Node x = NodeManager::currentNM()->mkSkolem("sde_$$", n[0].getType().getSetElementType());
 734     Node l1 = MEMBER(x, n[0]), l2 = MEMBER(x, n[1]);
 735
 736     lemma = OR(n, AND(l1, NOT(l2)), AND(NOT(l1), l2));
 737   }
 738
 739   Debug("sets-lemma") << "[sets-lemma] " << lemma << std::endl;
 740
 741   return  lemma;
 742 }
 743
 744
 745 TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
 746                                      context::Context* c,
 747                                      context::UserContext* u):
 748   d_external(external),
 749   d_notify(*this),
 750   d_equalityEngine(d_notify, c, "theory::sets::TheorySetsPrivate"),
 751   d_conflict(c),
 752   d_termInfoManager(NULL),
 753   d_propagationQueue(c),
 754   d_settermPropagationQueue(c),
 755   d_nodeSaver(c),
 756   d_pending(u),
 757   d_pendingDisequal(u),
 758   d_pendingEverInserted(u)
 759 {
 760   d_termInfoManager = new TermInfoManager(*this, c, &d_equalityEngine);
 761
 762   d_equalityEngine.addFunctionKind(kind::UNION);
 763   d_equalityEngine.addFunctionKind(kind::INTERSECTION);
 764   d_equalityEngine.addFunctionKind(kind::SETMINUS);
 765
 766   d_equalityEngine.addFunctionKind(kind::MEMBER);
 767   d_equalityEngine.addFunctionKind(kind::SUBSET);
 768 }/* TheorySetsPrivate::TheorySetsPrivate() */
 769
 770
 771 TheorySetsPrivate::~TheorySetsPrivate()
 772 {
 773   delete d_termInfoManager;
 774 }
 775
 776
 777 bool TheorySetsPrivate::propagate(TNode literal) {
 778   Debug("sets-prop") << " propagate(" << literal  << ")" << std::endl;
 779
 780   // If already in conflict, no more propagation
 781   if (d_conflict) {
 782     Debug("sets-prop") << "TheoryUF::propagate(" << literal << "): already in conflict" << std::endl;
 783     return false;
 784   }
 785
 786   // Propagate out
 787   bool ok = d_external.d_out->propagate(literal);
 788   if (!ok) {
 789     d_conflict = true;
 790   }
 791
 792   return ok;
 793 }/* TheorySetsPropagate::propagate(TNode) */
 794
 795
 796 void TheorySetsPrivate::addSharedTerm(TNode n) {
 797   Debug("sets") << "[sets] ThoerySetsPrivate::addSharedTerm( " << n << ")" << std::endl;
 798   d_equalityEngine.addTriggerTerm(n, THEORY_SETS);
 799 }
 800
 801 void TheorySetsPrivate::conflict(TNode a, TNode b)
 802 {
 803   if (a.getKind() == kind::CONST_BOOLEAN) {
 804     d_conflictNode = explain(a.iffNode(b));
 805   } else {
 806     d_conflictNode = explain(a.eqNode(b));
 807   }
 808   d_external.d_out->conflict(d_conflictNode);
 809   Debug("sets") << "[sets] conflict: " << a << " iff " << b
 810                 << ", explaination " << d_conflictNode << std::endl;
 811   d_conflict = true;
 812 }
 813
 814 Node TheorySetsPrivate::explain(TNode literal)
 815 {
 816   Debug("sets") << "TheorySetsPrivate::explain(" << literal << ")"
 817                 << std::endl;
 818
 819   bool polarity = literal.getKind() != kind::NOT;
 820   TNode atom = polarity ? literal : literal[0];
 821   std::vector<TNode> assumptions;
 822
 823   if(atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
 824     d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
 825   } else if(atom.getKind() == kind::MEMBER) {
 826     if( !d_equalityEngine.hasTerm(atom)) {
 827       d_equalityEngine.addTerm(atom);
 828     }
 829     d_equalityEngine.explainPredicate(atom, polarity, assumptions);
 830   } else {
 831     Debug("sets") << "unhandled: " << literal << "; (" << atom << ", "
 832                   << polarity << "); kind" << atom.getKind() << std::endl;
 833     Unhandled();
 834   }
 835
 836   return mkAnd(assumptions);
 837 }
 838
 839 void TheorySetsPrivate::preRegisterTerm(TNode node)
 840 {
 841   Debug("sets") << "TheorySetsPrivate::preRegisterTerm(" << node << ")"
 842                 << std::endl;
 843
 844   switch(node.getKind()) {
 845   case kind::EQUAL:
 846     // TODO: what's the point of this
 847     d_equalityEngine.addTriggerEquality(node);
 848     break;
 849   case kind::MEMBER:
 850     // TODO: what's the point of this
 851     d_equalityEngine.addTriggerPredicate(node);
 852     break;
 853   default:
 854     d_termInfoManager->addTerm(node);
 855     d_equalityEngine.addTriggerTerm(node, THEORY_SETS);
 856     // d_equalityEngine.addTerm(node);
 857   }
 858   if(node.getKind() == kind::SET_SINGLETON) {
 859     Node true_node = NodeManager::currentNM()->mkConst<bool>(true);
 860     learnLiteral(MEMBER(node[0], node), true, true_node);
 861     //intentional fallthrough
 862   }
 863 }
 864
 865
 866
 867 /**************************** eq::NotifyClass *****************************/
 868 /**************************** eq::NotifyClass *****************************/
 869 /**************************** eq::NotifyClass *****************************/
 870
 871
 872 bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool value)
 873 {
 874   Debug("sets-eq") << "[sets-eq] eqNotifyTriggerEquality: equality = " << equality
 875                    << " value = " << value << std::endl;
 876   if (value) {
 877     return d_theory.propagate(equality);
 878   } else {
 879     // We use only literal triggers so taking not is safe
 880     return d_theory.propagate(equality.notNode());
 881   }
 882 }
 883
 884 bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value)
 885 {
 886   Debug("sets-eq") << "[sets-eq] eqNotifyTriggerPredicate: predicate = " << predicate
 887                    << " value = " << value << std::endl;
 888   if (value) {
 889     return d_theory.propagate(predicate);
 890   } else {
 891     return d_theory.propagate(predicate.notNode());
 892   }
 893 }
 894
 895 bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value)
 896 {
 897   Debug("sets-eq") << "[sets-eq] eqNotifyTriggerTermEquality: tag = " << tag
 898                    << " t1 = " << t1 << "  t2 = " << t2 << "  value = " << value << std::endl;
 899   if(value) {
 900     d_theory.d_termInfoManager->mergeTerms(t1, t2);
 901   }
 902   return true;
 903 }
 904
 905 void TheorySetsPrivate::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2)
 906 {
 907   Debug("sets-eq") << "[sets-eq] eqNotifyConstantTermMerge " << " t1 = " << t1 << " t2 = " << t2 << std::endl;
 908   d_theory.conflict(t1, t2);
 909 }
 910
 911 // void TheorySetsPrivate::NotifyClass::eqNotifyNewClass(TNode t)
 912 // {
 913 //   Debug("sets-eq") << "[sets-eq] eqNotifyNewClass:" << " t = " << t << std::endl;
 914 // }
 915
 916 // void TheorySetsPrivate::NotifyClass::eqNotifyPreMerge(TNode t1, TNode t2)
 917 // {
 918 //   Debug("sets-eq") << "[sets-eq] eqNotifyPreMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl;
 919 // }
 920
 921 // void TheorySetsPrivate::NotifyClass::eqNotifyPostMerge(TNode t1, TNode t2)
 922 // {
 923 //   Debug("sets-eq") << "[sets-eq] eqNotifyPostMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl;
 924 // }
 925
 926 // void TheorySetsPrivate::NotifyClass::eqNotifyDisequal(TNode t1, TNode t2, TNode reason)
 927 // {
 928 //   Debug("sets-eq") << "[sets-eq] eqNotifyDisequal:" << " t1 = " << t1 << " t2 = " << t2 << " reason = " << reason << std::endl;
 929 // }
 930
 931
 932 /**************************** TermInfoManager *****************************/
 933 /**************************** TermInfoManager *****************************/
 934 /**************************** TermInfoManager *****************************/
 935
 936 void TheorySetsPrivate::TermInfoManager::mergeLists
 937 (CDTNodeList* la, const CDTNodeList* lb) const {
 938   // straight from theory/arrays/array_info.cpp
 939   std::set<TNode> temp;
 940   CDTNodeList::const_iterator it;
 941   for(it = la->begin() ; it != la->end(); it++ ) {
 942     temp.insert((*it));
 943   }
 944
 945   for(it = lb->begin() ; it!= lb->end(); it++ ) {
 946     if(temp.count(*it) == 0) {
 947       la->push_back(*it);
 948     }
 949   }
 950 }
 951
 952 TheorySetsPrivate::TermInfoManager::TermInfoManager
 953 (TheorySetsPrivate& theory, context::Context* satContext, eq::EqualityEngine* eq):
 954   d_theory(theory),
 955   d_context(satContext),
 956   d_eqEngine(eq),
 957   d_terms(satContext),
 958   d_info()
 959 { }
 960
 961 TheorySetsPrivate::TermInfoManager::~TermInfoManager() {
 962   for( typeof(d_info.begin()) it = d_info.begin();
 963        it != d_info.end(); ++it) {
 964     delete (*it).second;
 965   }
 966 }
 967
 968 void TheorySetsPrivate::TermInfoManager::notifyMembership(TNode fact) {
 969   bool polarity = fact.getKind() != kind::NOT;
 970   TNode atom = polarity ? fact : fact[0];
 971
 972   TNode x = d_eqEngine->getRepresentative(atom[0]);
 973   TNode S = d_eqEngine->getRepresentative(atom[1]);
 974
 975   Debug("sets-terminfo") << "[sets-terminfo] Adding membership " << x
 976                          << " in " << S << " " << polarity << std::endl;
 977
 978   d_info[S]->addToElementList(x, polarity);
 979 }
 980
 981 const CDTNodeList* TheorySetsPrivate::TermInfoManager::getParents(TNode x) {
 982   return d_info[x]->parents;
 983 }
 984
 985 void TheorySetsPrivate::TermInfoManager::addTerm(TNode n) {
 986   unsigned numChild = n.getNumChildren();
 987
 988   if(!d_terms.contains(n)) {
 989     d_terms.insert(n);
 990     d_info[n] = new TheorySetsTermInfo(d_context);
 991   }
 992
 993   if(n.getKind() == kind::UNION ||
 994      n.getKind() == kind::INTERSECTION ||
 995      n.getKind() == kind::SETMINUS ||
 996      n.getKind() == kind::SET_SINGLETON) {
 997
 998     for(unsigned i = 0; i < numChild; ++i) {
 999       if(d_terms.contains(n[i])) {
1000         Debug("sets-parent") << "Adding " << n << " to parent list of "
1001                              << n[i] << std::endl;
1002         d_info[n[i]]->parents->push_back(n);
1003       }
1004     }
1005
1006   }
1007 }
1008
1009 void TheorySetsPrivate::TermInfoManager::pushToSettermPropagationQueue
1010 (CDTNodeList* l, TNode S, bool polarity)
1011 {
1012   for(typeof(l->begin()) i = l->begin(); i != l->end(); ++i) {
1013     Debug("sets-prop") << "[sets-terminfo]  setterm todo: "
1014                        << MEMBER(*i, d_eqEngine->getRepresentative(S))
1015                        << std::endl;
1016
1017     d_eqEngine->addTerm(MEMBER(d_eqEngine->getRepresentative(*i),
1018                                d_eqEngine->getRepresentative(S)));
1019
1020     for(eq::EqClassIterator j(d_eqEngine->getRepresentative(S), d_eqEngine);
1021         !j.isFinished(); ++j) {
1022
1023       TNode x = (*i);
1024       TNode S = (*j);
1025       Node cur_atom = MEMBER(x, S);
1026
1027       // propagation : empty set
1028       if(polarity && S.getKind() == kind::EMPTYSET) {
1029         Debug("sets-prop") << "[sets-prop]  something in empty set? conflict."
1030                            << std::endl;
1031         d_theory.learnLiteral(cur_atom, false, cur_atom);
1032         return;
1033       }// propagation: empty set
1034
1035       // propagation : children
1036       if(S.getKind() == kind::UNION ||
1037          S.getKind() == kind::INTERSECTION ||
1038          S.getKind() == kind::SETMINUS ||
1039          S.getKind() == kind::SET_SINGLETON) {
1040         d_theory.d_settermPropagationQueue.push_back(std::make_pair(x, S));
1041       }// propagation: children
1042
1043       // propagation : parents
1044       const CDTNodeList* parentList = getParents(S);
1045       for(typeof(parentList->begin()) k = parentList->begin();
1046           k != parentList->end(); ++k) {
1047         d_theory.d_settermPropagationQueue.push_back(std::make_pair(x, *k));
1048       }// propagation : parents
1049
1050
1051     }//j loop
1052
1053   }
1054
1055 }
1056
1057 void TheorySetsPrivate::TermInfoManager::mergeTerms(TNode a, TNode b) {
1058   // merge b into a
1059
1060   if(!a.getType().isSet()) return;
1061
1062   Debug("sets-terminfo") << "[sets-terminfo] Merging (into) a = " << a
1063                          << ", b = " << b << std::endl;
1064   Debug("sets-terminfo") << "[sets-terminfo] reps"
1065                          << ", a: " << d_eqEngine->getRepresentative(a)
1066                          << ", b: " << d_eqEngine->getRepresentative(b)
1067                          << std::endl;
1068
1069   typeof(d_info.begin()) ita = d_info.find(a);
1070   typeof(d_info.begin()) itb = d_info.find(b);
1071
1072   Assert(ita != d_info.end());
1073   Assert(itb != d_info.end());
1074
1075   pushToSettermPropagationQueue( (*ita).second->elementsInThisSet, b, true );
1076   pushToSettermPropagationQueue( (*ita).second->elementsNotInThisSet, b, false );
1077   pushToSettermPropagationQueue( (*itb).second->elementsNotInThisSet, a, false );
1078   pushToSettermPropagationQueue( (*itb).second->elementsInThisSet, a, true );
1079
1080   mergeLists((*ita).second->elementsInThisSet,
1081              (*itb).second->elementsInThisSet);
1082
1083   mergeLists((*ita).second->elementsNotInThisSet,
1084              (*itb).second->elementsNotInThisSet);
1085 }
1086
1087
1088 }/* CVC4::theory::sets namespace */
1089 }/* CVC4::theory namespace */
1090 }/* CVC4 namespace */