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::addSharedTerm(TNode n) {
 884   Debug("sets") << "[sets] ThoerySetsPrivate::addSharedTerm( " << n << ")" << std::endl;
 885   d_equalityEngine.addTriggerTerm(n, THEORY_SETS);
 886 }
 887
 888 void TheorySetsPrivate::conflict(TNode a, TNode b)
 889 {
 890   if (a.getKind() == kind::CONST_BOOLEAN) {
 891     d_conflictNode = explain(a.iffNode(b));
 892   } else {
 893     d_conflictNode = explain(a.eqNode(b));
 894   }
 895   d_external.d_out->conflict(d_conflictNode);
 896   Debug("sets") << "[sets] conflict: " << a << " iff " << b
 897                 << ", explaination " << d_conflictNode << std::endl;
 898   d_conflict = true;
 899 }
 900
 901 Node TheorySetsPrivate::explain(TNode literal)
 902 {
 903   Debug("sets") << "TheorySetsPrivate::explain(" << literal << ")"
 904                 << std::endl;
 905
 906   bool polarity = literal.getKind() != kind::NOT;
 907   TNode atom = polarity ? literal : literal[0];
 908   std::vector<TNode> assumptions;
 909
 910   if(atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
 911     d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
 912   } else if(atom.getKind() == kind::MEMBER) {
 913     if( !d_equalityEngine.hasTerm(atom)) {
 914       d_equalityEngine.addTerm(atom);
 915     }
 916     d_equalityEngine.explainPredicate(atom, polarity, assumptions);
 917   } else {
 918     Debug("sets") << "unhandled: " << literal << "; (" << atom << ", "
 919                   << polarity << "); kind" << atom.getKind() << std::endl;
 920     Unhandled();
 921   }
 922
 923   return mkAnd(assumptions);
 924 }
 925
 926 void TheorySetsPrivate::preRegisterTerm(TNode node)
 927 {
 928   Debug("sets") << "TheorySetsPrivate::preRegisterTerm(" << node << ")"
 929                 << std::endl;
 930
 931   switch(node.getKind()) {
 932   case kind::EQUAL:
 933     // TODO: what's the point of this
 934     d_equalityEngine.addTriggerEquality(node);
 935     break;
 936   case kind::MEMBER:
 937     // TODO: what's the point of this
 938     d_equalityEngine.addTriggerPredicate(node);
 939     break;
 940   default:
 941     d_termInfoManager->addTerm(node);
 942     d_equalityEngine.addTriggerTerm(node, THEORY_SETS);
 943     // d_equalityEngine.addTerm(node);
 944   }
 945   if(node.getKind() == kind::SET_SINGLETON) {
 946     Node true_node = NodeManager::currentNM()->mkConst<bool>(true);
 947     learnLiteral(MEMBER(node[0], node), true, true_node);
 948     //intentional fallthrough
 949   }
 950 }
 951
 952
 953
 954 /**************************** eq::NotifyClass *****************************/
 955 /**************************** eq::NotifyClass *****************************/
 956 /**************************** eq::NotifyClass *****************************/
 957
 958
 959 bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool value)
 960 {
 961   Debug("sets-eq") << "[sets-eq] eqNotifyTriggerEquality: equality = " << equality
 962                    << " value = " << value << std::endl;
 963   if (value) {
 964     return d_theory.propagate(equality);
 965   } else {
 966     // We use only literal triggers so taking not is safe
 967     return d_theory.propagate(equality.notNode());
 968   }
 969 }
 970
 971 bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value)
 972 {
 973   Debug("sets-eq") << "[sets-eq] eqNotifyTriggerPredicate: predicate = " << predicate
 974                    << " value = " << value << std::endl;
 975   if (value) {
 976     return d_theory.propagate(predicate);
 977   } else {
 978     return d_theory.propagate(predicate.notNode());
 979   }
 980 }
 981
 982 bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value)
 983 {
 984   Debug("sets-eq") << "[sets-eq] eqNotifyTriggerTermEquality: tag = " << tag
 985                    << " t1 = " << t1 << "  t2 = " << t2 << "  value = " << value << std::endl;
 986   if(value) {
 987     d_theory.d_termInfoManager->mergeTerms(t1, t2);
 988   }
 989   return true;
 990 }
 991
 992 void TheorySetsPrivate::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2)
 993 {
 994   Debug("sets-eq") << "[sets-eq] eqNotifyConstantTermMerge " << " t1 = " << t1 << " t2 = " << t2 << std::endl;
 995   d_theory.conflict(t1, t2);
 996 }
 997
 998 // void TheorySetsPrivate::NotifyClass::eqNotifyNewClass(TNode t)
 999 // {
1000 //   Debug("sets-eq") << "[sets-eq] eqNotifyNewClass:" << " t = " << t << std::endl;
1001 // }
1002
1003 // void TheorySetsPrivate::NotifyClass::eqNotifyPreMerge(TNode t1, TNode t2)
1004 // {
1005 //   Debug("sets-eq") << "[sets-eq] eqNotifyPreMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl;
1006 // }
1007
1008 // void TheorySetsPrivate::NotifyClass::eqNotifyPostMerge(TNode t1, TNode t2)
1009 // {
1010 //   Debug("sets-eq") << "[sets-eq] eqNotifyPostMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl;
1011 // }
1012
1013 // void TheorySetsPrivate::NotifyClass::eqNotifyDisequal(TNode t1, TNode t2, TNode reason)
1014 // {
1015 //   Debug("sets-eq") << "[sets-eq] eqNotifyDisequal:" << " t1 = " << t1 << " t2 = " << t2 << " reason = " << reason << std::endl;
1016 // }
1017
1018
1019 /**************************** TermInfoManager *****************************/
1020 /**************************** TermInfoManager *****************************/
1021 /**************************** TermInfoManager *****************************/
1022
1023 void TheorySetsPrivate::TermInfoManager::mergeLists
1024 (CDTNodeList* la, const CDTNodeList* lb) const {
1025   // straight from theory/arrays/array_info.cpp
1026   std::set<TNode> temp;
1027   CDTNodeList::const_iterator it;
1028   for(it = la->begin() ; it != la->end(); it++ ) {
1029     temp.insert((*it));
1030   }
1031
1032   for(it = lb->begin() ; it!= lb->end(); it++ ) {
1033     if(temp.count(*it) == 0) {
1034       la->push_back(*it);
1035     }
1036   }
1037 }
1038
1039 TheorySetsPrivate::TermInfoManager::TermInfoManager
1040 (TheorySetsPrivate& theory, context::Context* satContext, eq::EqualityEngine* eq):
1041   d_theory(theory),
1042   d_context(satContext),
1043   d_eqEngine(eq),
1044   d_terms(satContext),
1045   d_info()
1046 { }
1047
1048 TheorySetsPrivate::TermInfoManager::~TermInfoManager() {
1049   for( typeof(d_info.begin()) it = d_info.begin();
1050        it != d_info.end(); ++it) {
1051     delete (*it).second;
1052   }
1053 }
1054
1055 void TheorySetsPrivate::TermInfoManager::notifyMembership(TNode fact) {
1056   bool polarity = fact.getKind() != kind::NOT;
1057   TNode atom = polarity ? fact : fact[0];
1058
1059   TNode x = d_eqEngine->getRepresentative(atom[0]);
1060   TNode S = d_eqEngine->getRepresentative(atom[1]);
1061
1062   Debug("sets-terminfo") << "[sets-terminfo] Adding membership " << x
1063                          << " in " << S << " " << polarity << std::endl;
1064
1065   d_info[S]->addToElementList(x, polarity);
1066   d_info[x]->addToSetList(S, polarity);
1067 }
1068
1069 const CDTNodeList* TheorySetsPrivate::TermInfoManager::getParents(TNode x) {
1070   return d_info[x]->parents;
1071 }
1072
1073 const CDTNodeList* TheorySetsPrivate::TermInfoManager::getMembers(TNode S) {
1074   return d_info[S]->elementsInThisSet;
1075 }
1076
1077 const CDTNodeList* TheorySetsPrivate::TermInfoManager::getNonMembers(TNode S) {
1078   return d_info[S]->elementsNotInThisSet;
1079 }
1080
1081 void TheorySetsPrivate::TermInfoManager::addTerm(TNode n) {
1082   unsigned numChild = n.getNumChildren();
1083
1084   if(!d_terms.contains(n)) {
1085     d_terms.insert(n);
1086     d_info[n] = new TheorySetsTermInfo(d_context);
1087   }
1088
1089   if(n.getKind() == kind::UNION ||
1090      n.getKind() == kind::INTERSECTION ||
1091      n.getKind() == kind::SETMINUS) {
1092
1093     for(unsigned i = 0; i < numChild; ++i) {
1094       if(d_terms.contains(n[i])) {
1095         Debug("sets-parent") << "Adding " << n << " to parent list of "
1096                              << n[i] << std::endl;
1097         d_info[n[i]]->parents->push_back(n);
1098       }
1099     }
1100
1101   }
1102 }
1103
1104 void TheorySetsPrivate::TermInfoManager::pushToSettermPropagationQueue
1105 (TNode x, TNode S, bool polarity)
1106 {
1107   Node cur_atom = MEMBER(x, S);
1108
1109   // propagation : empty set
1110   if(polarity && S.getKind() == kind::EMPTYSET) {
1111     Debug("sets-prop") << "[sets-prop]  something in empty set? conflict."
1112                        << std::endl;
1113     d_theory.learnLiteral(cur_atom, false, cur_atom);
1114     return;
1115   }// propagation: empty set
1116
1117   // propagation : children
1118   if(S.getKind() == kind::UNION ||
1119      S.getKind() == kind::INTERSECTION ||
1120      S.getKind() == kind::SETMINUS ||
1121      S.getKind() == kind::SET_SINGLETON) {
1122     d_theory.d_settermPropagationQueue.push_back(std::make_pair(x, S));
1123   }// propagation: children
1124
1125   // propagation : parents
1126   const CDTNodeList* parentList = getParents(S);
1127   for(typeof(parentList->begin()) k = parentList->begin();
1128       k != parentList->end(); ++k) {
1129     d_theory.d_settermPropagationQueue.push_back(std::make_pair(x, *k));
1130   }// propagation : parents
1131
1132 }
1133
1134 void TheorySetsPrivate::TermInfoManager::pushToSettermPropagationQueue
1135 (TNode x, CDTNodeList* l, bool polarity)
1136 {
1137   set<TNode> alreadyProcessed;
1138
1139   BOOST_FOREACH(TNode S, (*l) ) {
1140     Debug("sets-prop") << "[sets-terminfo]  setterm todo: "
1141                        << MEMBER(x, d_eqEngine->getRepresentative(S))
1142                        << std::endl;
1143
1144     TNode repS = d_eqEngine->getRepresentative(S);
1145     if(alreadyProcessed.find(repS) != alreadyProcessed.end()) {
1146       continue;
1147     } else {
1148       alreadyProcessed.insert(repS);
1149     }
1150
1151     d_eqEngine->addTerm(MEMBER(d_eqEngine->getRepresentative(x), repS));
1152
1153     for(eq::EqClassIterator j(d_eqEngine->getRepresentative(S), d_eqEngine);
1154         !j.isFinished(); ++j) {
1155
1156       pushToSettermPropagationQueue(x, *j, polarity);
1157
1158     }//j loop
1159   }
1160 }
1161
1162 void TheorySetsPrivate::TermInfoManager::pushToSettermPropagationQueue
1163 (CDTNodeList* l, TNode S, bool polarity)
1164 {
1165   BOOST_FOREACH(TNode x, (*l) ) {
1166     Debug("sets-prop") << "[sets-terminfo]  setterm todo: "
1167                        << MEMBER(x, d_eqEngine->getRepresentative(S))
1168                        << std::endl;
1169
1170     d_eqEngine->addTerm(MEMBER(d_eqEngine->getRepresentative(x),
1171                                d_eqEngine->getRepresentative(S)));
1172
1173     for(eq::EqClassIterator j(d_eqEngine->getRepresentative(S), d_eqEngine);
1174         !j.isFinished(); ++j) {
1175
1176       pushToSettermPropagationQueue(x, *j, polarity);
1177
1178     }//j loop
1179
1180   }
1181
1182 }
1183
1184
1185
1186 void TheorySetsPrivate::TermInfoManager::mergeTerms(TNode a, TNode b) {
1187   // merge b into a
1188   Debug("sets-terminfo") << "[sets-terminfo] Merging (into) a = " << a
1189                          << ", b = " << b << std::endl;
1190   Debug("sets-terminfo") << "[sets-terminfo] reps"
1191                          << ", a: " << d_eqEngine->getRepresentative(a)
1192                          << ", b: " << d_eqEngine->getRepresentative(b)
1193                          << std::endl;
1194
1195   typeof(d_info.begin()) ita = d_info.find(a);
1196   typeof(d_info.begin()) itb = d_info.find(b);
1197
1198   Assert(ita != d_info.end());
1199   Assert(itb != d_info.end());
1200
1201   /* elements in this sets */
1202   pushToSettermPropagationQueue( (*ita).second->elementsInThisSet, b, true );
1203   pushToSettermPropagationQueue( (*ita).second->elementsNotInThisSet, b, false );
1204   pushToSettermPropagationQueue( (*itb).second->elementsNotInThisSet, a, false );
1205   pushToSettermPropagationQueue( (*itb).second->elementsInThisSet, a, true );
1206   mergeLists((*ita).second->elementsInThisSet,
1207              (*itb).second->elementsInThisSet);
1208   mergeLists((*ita).second->elementsNotInThisSet,
1209              (*itb).second->elementsNotInThisSet);
1210
1211   /* sets containing this element */
1212   // pushToSettermPropagationQueue( b, (*ita).second->setsContainingThisElement, true);
1213   // pushToSettermPropagationQueue( b, (*ita).second->setsNotContainingThisElement, false);
1214   pushToSettermPropagationQueue( a, (*itb).second->setsNotContainingThisElement, false);
1215   pushToSettermPropagationQueue( a, (*itb).second->setsContainingThisElement, true);
1216   mergeLists( (*ita).second->setsContainingThisElement,
1217               (*itb).second->setsContainingThisElement );
1218   mergeLists( (*ita).second->setsNotContainingThisElement,
1219               (*itb).second->setsNotContainingThisElement );
1220 }
1221
1222
1223 }/* CVC4::theory::sets namespace */
1224 }/* CVC4::theory namespace */
1225 }/* CVC4 namespace */