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