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