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): Andrew Reynolds
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-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     // ^ doesn't hold when we propagate equality/disequality between shared terms
  95     // and that leads to conflict (externally).
  96     if(d_conflict) { return; }
  97     Debug("sets") << "[sets]  is complete = " << isComplete() << std::endl;
  98   }
  99
 100   if( (level == Theory::EFFORT_FULL || options::setsEagerLemmas() ) && !isComplete()) {
 101     d_external.d_out->lemma(getLemma());
 102     return;
 103   }
 104
 105   // if we are here, there is no conflict and we are complete
 106   if(Debug.isOn("sets-scrutinize")) { d_scrutinize->postCheckInvariants(); }
 107
 108   return;
 109 }/* TheorySetsPrivate::check() */
 110
 111
 112 void TheorySetsPrivate::assertEquality(TNode fact, TNode reason, bool learnt)
 113 {
 114   Debug("sets-assert") << "\n[sets-assert] adding equality: " << fact
 115                        << ", " << reason
 116                        << ", " << learnt << std::endl;
 117
 118   bool polarity = fact.getKind() != kind::NOT;
 119   TNode atom = polarity ? fact : fact[0];
 120
 121   // fact already holds
 122   if( holds(atom, polarity) ) {
 123     Debug("sets-assert") << "[sets-assert]   already present, skipping" << std::endl;
 124     return;
 125   }
 126
 127   // assert fact & check for conflict
 128   if(learnt) {
 129     registerReason(reason, /*save=*/ true);
 130   }
 131   d_equalityEngine.assertEquality(atom, polarity, reason);
 132
 133   if(!d_equalityEngine.consistent()) {
 134     Debug("sets-assert") << "[sets-assert]   running into a conflict" << std::endl;
 135     d_conflict = true;
 136     return;
 137   }
 138
 139   if(!polarity && atom[0].getType().isSet()) {
 140     addToPending(atom);
 141   }
 142
 143 }/* TheorySetsPrivate::assertEquality() */
 144
 145
 146 void TheorySetsPrivate::assertMemebership(TNode fact, TNode reason, bool learnt)
 147 {
 148   Debug("sets-assert") << "\n[sets-assert] adding membership: " << fact
 149                        << ", " << reason
 150                        << ", " << learnt << std::endl;
 151
 152   bool polarity = fact.getKind() == kind::NOT ? false : true;
 153   TNode atom = polarity ? fact : fact[0];
 154
 155   // fact already holds
 156   if( holds(atom, polarity) ) {
 157     Debug("sets-assert") << "[sets-assert]   already present, skipping" << std::endl;
 158     return;
 159   }
 160
 161   // assert fact & check for conflict
 162   if(learnt) {
 163     registerReason(reason, true);
 164   }
 165   d_equalityEngine.assertPredicate(atom, polarity, reason);
 166
 167   if(!d_equalityEngine.consistent()) {
 168     Debug("sets-assert") << "[sets-assert]   running into a conflict" << std::endl;
 169     d_conflict = true;
 170     return;
 171   }
 172
 173   // update term info data structures
 174   d_termInfoManager->notifyMembership(fact);
 175
 176   // propagation
 177   TNode x = d_equalityEngine.getRepresentative(atom[0]);
 178   eq::EqClassIterator j(d_equalityEngine.getRepresentative(atom[1]),
 179                         &d_equalityEngine);
 180   TNode S = (*j);
 181   Node cur_atom = MEMBER(x, S);
 182
 183   /**
 184    * It is sufficient to do emptyset propagation outside the loop as
 185    * constant term is guaranteed to be class representative.
 186    */
 187   if(polarity && S.getKind() == kind::EMPTYSET) {
 188     Debug("sets-prop") << "[sets-prop]  something in empty set? conflict."
 189                        << std::endl;
 190     learnLiteral(cur_atom, false, cur_atom);
 191     Assert(d_conflict);
 192     return;
 193   }
 194
 195   /**
 196    * Disequality propagation if element type is set
 197    */
 198   if(x.getType().isSet()) {
 199     if(polarity) {
 200       const CDTNodeList* l = d_termInfoManager->getNonMembers(S);
 201       for(typeof(l->begin()) it = l->begin(); it != l->end(); ++it) {
 202         TNode n = *it;
 203         learnLiteral( /* atom = */ EQUAL(x, n),
 204                       /* polarity = */ false,
 205                       /* reason = */ AND( MEMBER(x, S), NOT( MEMBER(n, S)) ) );
 206       }
 207     } else {
 208       const CDTNodeList* l = d_termInfoManager->getMembers(S);
 209       for(typeof(l->begin()) it = l->begin(); it != l->end(); ++it) {
 210         TNode n = *it;
 211         learnLiteral( /* atom = */ EQUAL(x, n),
 212                       /* polarity = */ false,
 213                       /* reason = */ AND( NOT(MEMBER(x, S)), MEMBER(n, S)) );
 214       }
 215     }
 216   }
 217
 218   for(; !j.isFinished(); ++j) {
 219     TNode S = (*j);
 220     Node cur_atom = MEMBER(x, S);
 221
 222     // propagation : children
 223     Debug("sets-prop") << "[sets-prop] Propagating 'down' for "
 224                        << x << element_of_str << S << std::endl;
 225     if(S.getKind() == kind::UNION ||
 226        S.getKind() == kind::INTERSECTION ||
 227        S.getKind() == kind::SETMINUS ||
 228        S.getKind() == kind::SINGLETON) {
 229       doSettermPropagation(x, S);
 230       if(d_conflict) return;
 231     }// propagation: children
 232
 233
 234     // propagation : parents
 235     Debug("sets-prop") << "[sets-prop] Propagating 'up' for "
 236                        << x << element_of_str << S << std::endl;
 237     const CDTNodeList* parentList = d_termInfoManager->getParents(S);
 238     for(typeof(parentList->begin()) k = parentList->begin();
 239         k != parentList->end(); ++k) {
 240       doSettermPropagation(x, *k);
 241       if(d_conflict) return;
 242     }// propagation : parents
 243
 244
 245   }//j loop
 246
 247 }/* TheorySetsPrivate::assertMemebership() */
 248
 249
 250 void TheorySetsPrivate::doSettermPropagation(TNode x, TNode S)
 251 {
 252   Debug("sets-prop") << "[sets-prop] doSettermPropagation("
 253                      << x << ", " << S << std::endl;
 254
 255   Assert(S.getType().isSet() && S.getType().getSetElementType() == x.getType(),
 256          ( std::string("types of S and x are ") + S.getType().toString() +
 257            std::string(" and ") + x.getType().toString() +
 258            std::string(" respectively") ).c_str()  );
 259
 260   Node literal, left_literal, right_literal;
 261
 262   // axiom: literal <=> left_literal AND right_literal
 263   switch(S.getKind()) {
 264   case kind::INTERSECTION:
 265     literal       =       MEMBER(x, S)      ;
 266     left_literal  =       MEMBER(x, S[0])   ;
 267     right_literal =       MEMBER(x, S[1])   ;
 268     break;
 269   case kind::UNION:
 270     literal       = NOT(  MEMBER(x, S)     );
 271     left_literal  = NOT(  MEMBER(x, S[0])  );
 272     right_literal = NOT(  MEMBER(x, S[1])  );
 273     break;
 274   case kind::SETMINUS:
 275     literal       =       MEMBER(x, S)      ;
 276     left_literal  =       MEMBER(x, S[0])   ;
 277     right_literal = NOT(  MEMBER(x, S[1])  );
 278     break;
 279   case kind::SINGLETON: {
 280     Node atom = MEMBER(x, S);
 281     if(holds(atom, true)) {
 282       learnLiteral(EQUAL(x, S[0]), true, atom);
 283     } else if(holds(atom, false)) {
 284       learnLiteral(EQUAL(x, S[0]), false, NOT(atom));
 285     }
 286     return;
 287   }
 288   default:
 289     Unhandled();
 290   }
 291
 292   Debug("sets-prop-details")
 293     << "[sets-prop-details]   " << literal << " IFF " << left_literal
 294     << " AND " << right_literal << std::endl;
 295
 296   Debug("sets-prop-details")
 297     << "[sets-prop-details]   "
 298     << (holds(literal) ? "yes" : (holds(literal.negate()) ? " no" : " _ "))
 299     << " IFF "
 300     << (holds(left_literal) ? "yes" : (holds(left_literal.negate()) ? "no " : " _ "))
 301     << " AND "
 302     << (holds(right_literal) ? "yes" : (holds(right_literal.negate()) ? "no " : " _ "))
 303     << std::endl;
 304
 305   Assert( present( MEMBER(x, S)    ) ||
 306           present( MEMBER(x, S[0]) ) ||
 307           present( MEMBER(x, S[1]) ) );
 308
 309   if( holds(literal) ) {
 310     // 1a. literal => left_literal
 311     Debug("sets-prop") << "[sets-prop]  ... via case 1a. ..." << std::endl;
 312     learnLiteral(left_literal, literal);
 313     if(d_conflict) return;
 314
 315     // 1b. literal => right_literal
 316     Debug("sets-prop") << "[sets-prop]  ... via case 1b. ..." << std::endl;
 317     learnLiteral(right_literal, literal);
 318     if(d_conflict) return;
 319
 320     // subsumption requirement met, exit
 321     return;
 322   }
 323   else if( holds(literal.negate() ) ) {
 324     // 4. neg(literal), left_literal => neg(right_literal)
 325     if( holds(left_literal) ) {
 326       Debug("sets-prop") << "[sets-prop]  ... via case 4. ..." << std::endl;
 327       learnLiteral(right_literal.negate(), AND( literal.negate(),
 328                                                 left_literal) );
 329       if(d_conflict) return;
 330     }
 331
 332     // 5. neg(literal), right_literal => neg(left_literal)
 333     if( holds(right_literal) ) {
 334       Debug("sets-prop") << "[sets-prop]  ... via case 5. ..." << std::endl;
 335       learnLiteral(left_literal.negate(), AND( literal.negate(),
 336                                                right_literal) );
 337       if(d_conflict) return;
 338     }
 339   }
 340   else {
 341     // 2,3. neg(left_literal) v neg(right_literal) => neg(literal)
 342     if(holds(left_literal.negate())) {
 343       Debug("sets-prop") << "[sets-prop]  ... via case 2. ..." << std::endl;
 344       learnLiteral(literal.negate(), left_literal.negate());
 345       if(d_conflict) return;
 346     }
 347     else if(holds(right_literal.negate())) {
 348       Debug("sets-prop") << "[sets-prop]  ... via case 3. ..." << std::endl;
 349       learnLiteral(literal.negate(), right_literal.negate());
 350       if(d_conflict) return;
 351     }
 352
 353     // 6. the axiom itself:
 354     else if(holds(left_literal) && holds(right_literal)) {
 355       Debug("sets-prop") << "[sets-prop]  ... via case 6. ..." << std::endl;
 356       learnLiteral(literal, AND(left_literal, right_literal) );
 357       if(d_conflict) return;
 358     }
 359   }
 360
 361   // check fulfilling rule
 362   Node n;
 363   switch(S.getKind()) {
 364   case kind::UNION:
 365     if( holds(MEMBER(x, S)) &&
 366         !present( MEMBER(x, S[0]) ) )
 367       addToPending( MEMBER(x, S[0]) );
 368     break;
 369   case kind::SETMINUS: // intentional fallthrough
 370   case kind::INTERSECTION:
 371     if( holds(MEMBER(x, S[0])) &&
 372         !present( MEMBER(x, S[1]) ))
 373       addToPending( MEMBER(x, S[1]) );
 374     break;
 375   default:
 376     Assert(false, "MembershipEngine::doSettermPropagation");
 377   }
 378 }
 379
 380
 381 void TheorySetsPrivate::learnLiteral(TNode atom, bool polarity, Node reason) {
 382   Debug("sets-learn") << "[sets-learn] learnLiteral(" << atom
 383                       << ", " << polarity << ")" << std::endl;
 384
 385   if( holds(atom, polarity) ) {
 386     Debug("sets-learn") << "[sets-learn] \u2514 already known, skipping" << std::endl;
 387     return;
 388   }
 389
 390   if( holds(atom, !polarity) ) {
 391     Debug("sets-learn") << "[sets-learn] \u2514 conflict found" << std::endl;
 392
 393     registerReason(reason, /*save=*/ true);
 394
 395     if(atom.getKind() == kind::EQUAL) {
 396       d_equalityEngine.assertEquality(atom, polarity, reason);
 397     } else {
 398       d_equalityEngine.assertPredicate(atom, polarity, reason);
 399     }
 400     Assert(d_conflict);       // should be marked due to equality engine
 401     return;
 402   }
 403
 404   Assert(atom.getKind() == kind::EQUAL || atom.getKind() == kind::MEMBER);
 405
 406   Node learnt_literal = polarity ? Node(atom) : NOT(atom);
 407   d_propagationQueue.push_back( make_pair(learnt_literal, reason) );
 408 }/*TheorySetsPrivate::learnLiteral(...)*/
 409
 410
 411 /************************ Sharing ************************/
 412 /************************ Sharing ************************/
 413 /************************ Sharing ************************/
 414
 415 void TheorySetsPrivate::addSharedTerm(TNode n) {
 416   Debug("sets") << "[sets] ThoerySetsPrivate::addSharedTerm( " << n << ")" << std::endl;
 417   d_termInfoManager->addTerm(n);
 418   d_equalityEngine.addTriggerTerm(n, THEORY_SETS);
 419 }
 420
 421 void TheorySetsPrivate::dumpAssertionsHumanified() const
 422 {
 423     std::string tag = "sets-assertions";
 424
 425     if(Trace.isOn(tag)) { /* condition can't be !Trace.isOn, that's why this empty block */ }
 426     else { return; }
 427
 428     context::CDList<Assertion>::const_iterator it = d_external.facts_begin(), it_end = d_external.facts_end();
 429
 430     std::map<TNode, std::set<TNode> > equalities;
 431     std::set< pair<TNode, TNode> > disequalities;
 432     std::map<TNode, std::pair<std::set<TNode>, std::set<TNode> > > members;
 433     static std::map<TNode, int> numbering;
 434     static int number = 0;
 435
 436     for (unsigned i = 0; it != it_end; ++ it, ++i) {
 437       TNode ass = (*it).assertion;
 438       // Trace("sets-care-dump") << AssertCommand(ass.toExpr()) << endl;
 439       bool polarity = ass.getKind() != kind::NOT;
 440       ass = polarity ? ass : ass[0];
 441       Assert( ass.getNumChildren() == 2);
 442       TNode left = d_equalityEngine.getRepresentative(ass[0]);
 443       TNode right = d_equalityEngine.getRepresentative(ass[1]);
 444       if(numbering[left] == 0) numbering[left] = ++number;
 445       if(numbering[right] == 0) numbering[right] = ++number;
 446       equalities[left].insert(ass[0]);
 447       equalities[right].insert(ass[1]);
 448       if(ass.getKind() == kind::EQUAL) {
 449         if(polarity) {
 450           Assert(left == right);
 451         } else {
 452           if(left > right) std::swap(left, right);
 453           disequalities.insert(make_pair(left, right));
 454         }
 455       } else if(ass.getKind() == kind::MEMBER) {
 456         (polarity ? members[right].first : members[right].second).insert(left);
 457       }
 458     }
 459 #define FORIT(it, container) for(typeof((container).begin()) it=(container).begin(); (it) != (container).end(); ++(it))
 460     FORIT(kt, equalities) {
 461       Trace(tag) << " Eq class of t" << numbering[(*kt).first] << ": " << std::endl;
 462       FORIT(jt, (*kt).second) {
 463         TNode S = (*jt);
 464         if( S.getKind() != kind::UNION && S.getKind() != kind::INTERSECTION && S.getKind() != kind::SETMINUS) {
 465           Trace(tag) << "    " << *jt << ((*jt).getType().isSet() ? "\n": " ");
 466         } else {
 467           Trace(tag) << "    ";
 468           if(S[0].isConst() || numbering.find(d_equalityEngine.getRepresentative(S[0])) == numbering.end()) {
 469             Trace(tag) << S[0];
 470           } else {
 471             Trace(tag) << "t" << numbering[d_equalityEngine.getRepresentative(S[0])];
 472           }
 473           Trace(tag) << " " << (S.getKind() == kind::UNION ? "|" : (S.getKind() == kind::INTERSECTION ? "&" : "-")) << " ";
 474           if(S[1].isConst() || numbering.find(d_equalityEngine.getRepresentative(S[1])) == numbering.end()) {
 475             Trace(tag) << S[1];
 476           } else {
 477             Trace(tag) << "t" << numbering[d_equalityEngine.getRepresentative(S[1])];
 478           }
 479           Trace(tag) << std::endl;
 480         }
 481       }
 482       Trace(tag) << std::endl;
 483     }
 484     FORIT(kt, disequalities) Trace(tag) << "NOT(t"<<numbering[(*kt).first]<<" = t" <<numbering[(*kt).second] <<")"<< std::endl;
 485     FORIT(kt, members) {
 486       if( (*kt).second.first.size() > 0) {
 487         Trace(tag) << "IN t" << numbering[(*kt).first] << ": ";
 488         FORIT(jt, (*kt).second.first) {
 489           TNode x = (*jt);
 490           if(x.isConst() || numbering.find(d_equalityEngine.getRepresentative(x)) == numbering.end()) {
 491             Trace(tag) << x << ", ";
 492           } else {
 493             Trace(tag) << "t" << numbering[d_equalityEngine.getRepresentative(x)] << ", ";
 494           }
 495         }
 496         Trace(tag) << std::endl;
 497       }
 498       if( (*kt).second.second.size() > 0) {
 499         Trace(tag) << "NOT IN t" << numbering[(*kt).first] << ": ";
 500         FORIT(jt, (*kt).second.second) {
 501           TNode x = (*jt);
 502           if(x.isConst() || numbering.find(d_equalityEngine.getRepresentative(x)) == numbering.end()) {
 503             Trace(tag) << x << ", ";
 504           } else {
 505             Trace(tag) << "t" << numbering[d_equalityEngine.getRepresentative(x)] << ", ";
 506           }
 507         }
 508         Trace(tag) << std::endl;
 509       }
 510     }
 511     Trace(tag) << std::endl;
 512 #undef FORIT
 513 }
 514
 515 void TheorySetsPrivate::computeCareGraph() {
 516   Debug("sharing") << "Theory::computeCareGraph<" << d_external.identify() << ">()" << endl;
 517
 518   if(Trace.isOn("sets-assertions")) {
 519     // dump our understanding of assertions
 520     dumpAssertionsHumanified();
 521   }
 522
 523   CVC4_UNUSED unsigned edgesAddedCnt = 0;
 524
 525   unsigned i_st = 0;
 526   if(options::setsCare1()) { i_st = d_ccg_i; }
 527   for (unsigned i = i_st; i < d_external.d_sharedTerms.size(); ++ i) {
 528     TNode a = d_external.d_sharedTerms[i];
 529     TypeNode aType = a.getType();
 530
 531     unsigned j_st = i + 1;
 532     if(options::setsCare1()) { if(i == d_ccg_i) j_st = d_ccg_j + 1; }
 533
 534     for (unsigned j = j_st; j < d_external.d_sharedTerms.size(); ++ j) {
 535       TNode b = d_external.d_sharedTerms[j];
 536       if (b.getType() != aType) {
 537         // We don't care about the terms of different types
 538         continue;
 539       }
 540
 541       switch (d_external.d_valuation.getEqualityStatus(a, b)) {
 542       case EQUALITY_TRUE_AND_PROPAGATED:
 543         // If we know about it, we should have propagated it, so we can skip
 544         Trace("sets-care") << "[sets-care] Know: " << EQUAL(a, b) << std::endl;
 545         break;
 546       case EQUALITY_FALSE_AND_PROPAGATED:
 547         // If we know about it, we should have propagated it, so we can skip
 548         Trace("sets-care") << "[sets-care] Know: " << NOT(EQUAL(a, b)) << std::endl;
 549         break;
 550       case EQUALITY_FALSE:
 551       case EQUALITY_TRUE:
 552         Assert(false, "ERROR: Equality status true/false but not propagated (sets care graph computation).");
 553         break;
 554       case EQUALITY_TRUE_IN_MODEL:
 555         d_external.addCarePair(a, b);
 556         if(Trace.isOn("sharing")) {
 557           ++edgesAddedCnt;
 558         }
 559         if(Debug.isOn("sets-care")) {
 560           Debug("sets-care") << "[sets-care] Requesting split between" << a << " and "
 561                              << b << "." << std::endl << "[sets-care] "
 562                              << "  Both current have value "
 563                              << d_external.d_valuation.getModelValue(a) << std::endl;
 564         }
 565       case EQUALITY_FALSE_IN_MODEL:
 566         if(Trace.isOn("sets-care-performance-test")) {
 567           // TODO: delete these lines, only for performance testing for now
 568           d_external.addCarePair(a, b);
 569         }
 570         break;
 571       case EQUALITY_UNKNOWN:
 572         // Let's split on it
 573         d_external.addCarePair(a, b);
 574         if(options::setsCare1()) {
 575           d_ccg_i = i;
 576           d_ccg_j = j;
 577           return;
 578         }
 579         break;
 580       default:
 581         Unreachable();
 582       }
 583     }
 584   }
 585   Trace("sharing") << "TheorySetsPrivate::computeCareGraph(): size = " << edgesAddedCnt << std::endl;
 586 }
 587
 588 EqualityStatus TheorySetsPrivate::getEqualityStatus(TNode a, TNode b) {
 589   Assert(d_equalityEngine.hasTerm(a) && d_equalityEngine.hasTerm(b));
 590   if (d_equalityEngine.areEqual(a, b)) {
 591     // The terms are implied to be equal
 592     return EQUALITY_TRUE;
 593   }
 594   if (d_equalityEngine.areDisequal(a, b, false)) {
 595     // The terms are implied to be dis-equal
 596     return EQUALITY_FALSE;
 597   }
 598   if( d_external.d_valuation.getModelValue(a) == d_external.d_valuation.getModelValue(b) ) {
 599     // Ther term are true in current model
 600     return EQUALITY_TRUE_IN_MODEL;
 601   }
 602   return EQUALITY_FALSE_IN_MODEL;
 603   // }
 604   // //TODO: can we be more precise sometimes?
 605   // return EQUALITY_UNKNOWN;
 606 }
 607
 608 /******************** Model generation ********************/
 609 /******************** Model generation ********************/
 610 /******************** Model generation ********************/
 611
 612 const TheorySetsPrivate::Elements& TheorySetsPrivate::getElements
 613 (TNode setterm, SettermElementsMap& settermElementsMap) const {
 614   SettermElementsMap::const_iterator it = settermElementsMap.find(setterm);
 615   bool alreadyCalculated = (it != settermElementsMap.end());
 616   if( !alreadyCalculated ) {
 617
 618     Kind k = setterm.getKind();
 619     Elements cur;
 620
 621     switch(k) {
 622     case kind::UNION: {
 623       const Elements& left = getElements(setterm[0], settermElementsMap);
 624       const Elements& right = getElements(setterm[1], settermElementsMap);
 625       if(left.size() >= right.size()) {
 626         cur = left; cur.insert(right.begin(), right.end());
 627       } else {
 628         cur = right; cur.insert(left.begin(), left.end());
 629       }
 630       break;
 631     }
 632     case kind::INTERSECTION: {
 633       const Elements& left = getElements(setterm[0], settermElementsMap);
 634       const Elements& right = getElements(setterm[1], settermElementsMap);
 635       std::set_intersection(left.begin(), left.end(), right.begin(), right.end(),
 636                             std::inserter(cur, cur.begin()) );
 637       break;
 638     }
 639     case kind::SETMINUS: {
 640       const Elements& left = getElements(setterm[0], settermElementsMap);
 641       const Elements& right = getElements(setterm[1], settermElementsMap);
 642       std::set_difference(left.begin(), left.end(), right.begin(), right.end(),
 643                           std::inserter(cur, cur.begin()) );
 644       break;
 645     }
 646     default:
 647       Assert(theory::kindToTheoryId(k) != theory::THEORY_SETS,
 648              (std::string("Kind belonging to set theory not explicitly handled: ") + kindToString(k)).c_str());
 649       // Assert(k == kind::VARIABLE || k == kind::APPLY_UF || k == kind::SKOLEM,
 650       //        (std::string("Expect variable or UF got ") + kindToString(k)).c_str() );
 651       /* assign emptyset, which is default */
 652     }
 653
 654     it = settermElementsMap.insert(SettermElementsMap::value_type(setterm, cur)).first;
 655   }
 656   return it->second;
 657 }
 658
 659
 660 bool TheorySetsPrivate::checkModel(const SettermElementsMap& settermElementsMap, TNode S) const {
 661
 662   Debug("sets-model") << "[sets-model] checkModel(..., " << S << "): "
 663                       << std::endl;
 664
 665   Assert(S.getType().isSet());
 666
 667   const Elements emptySetOfElements;
 668   const Elements& saved =
 669     d_equalityEngine.getRepresentative(S).getKind() == kind::EMPTYSET ||
 670     settermElementsMap.find(d_equalityEngine.getRepresentative(S)) == settermElementsMap.end() ?
 671     emptySetOfElements :
 672     settermElementsMap.find(d_equalityEngine.getRepresentative(S))->second;
 673   Debug("sets-model") << "[sets-model] saved :  { ";
 674   BOOST_FOREACH(TNode element, saved) { Debug("sets-model") << element << ", "; }
 675   Debug("sets-model") << " }" << std::endl;
 676
 677   if(theory::kindToTheoryId(S.getKind()) == THEORY_SETS && S.getNumChildren() == 2) {
 678
 679     Elements cur;
 680
 681     const Elements& left =
 682       d_equalityEngine.getRepresentative(S[0]).getKind() == kind::EMPTYSET ||
 683       settermElementsMap.find(d_equalityEngine.getRepresentative(S[0])) == settermElementsMap.end() ?
 684       emptySetOfElements :
 685       settermElementsMap.find(d_equalityEngine.getRepresentative(S[0]))->second;
 686
 687     const Elements&  right =
 688       d_equalityEngine.getRepresentative(S[1]).getKind() == kind::EMPTYSET ||
 689       settermElementsMap.find(d_equalityEngine.getRepresentative(S[1])) == settermElementsMap.end() ?
 690       emptySetOfElements :
 691       settermElementsMap.find(d_equalityEngine.getRepresentative(S[1]))->second;
 692
 693     switch(S.getKind()) {
 694     case kind::UNION:
 695       if(left.size() >= right.size()) {
 696         cur = left; cur.insert(right.begin(), right.end());
 697       } else {
 698         cur = right; cur.insert(left.begin(), left.end());
 699       }
 700       break;
 701     case kind::INTERSECTION:
 702       std::set_intersection(left.begin(), left.end(), right.begin(), right.end(),
 703                             std::inserter(cur, cur.begin()) );
 704       break;
 705     case kind::SETMINUS:
 706       std::set_difference(left.begin(), left.end(), right.begin(), right.end(),
 707                           std::inserter(cur, cur.begin()) );
 708       break;
 709     default:
 710       Unhandled();
 711     }
 712
 713     Debug("sets-model") << "[sets-model] cur :  { ";
 714     BOOST_FOREACH(TNode element, cur) { Debug("sets-model") << element << ", "; }
 715     Debug("sets-model") << " }" << std::endl;
 716
 717     if(saved != cur) {
 718       Debug("sets-model") << "[sets-model] *** ERROR *** cur != saved "
 719                           << std::endl;
 720       Debug("sets-model")
 721         << "[sets-model]   FYI: "
 722         << "  [" << S << "] = " << d_equalityEngine.getRepresentative(S) << ", "
 723         << "  [" << S[0] << "] = " << d_equalityEngine.getRepresentative(S[0]) << ", "
 724         << "  [" << S[1] << "] = " << d_equalityEngine.getRepresentative(S[1]) << "\n";
 725
 726       return false;
 727     }
 728   }
 729   return true;
 730 }
 731
 732 Node TheorySetsPrivate::elementsToShape(Elements elements, TypeNode setType) const
 733 {
 734   NodeManager* nm = NodeManager::currentNM();
 735
 736   if(elements.size() == 0) {
 737     return nm->mkConst(EmptySet(nm->toType(setType)));
 738   } else {
 739     Elements::iterator it = elements.begin();
 740     Node cur = SINGLETON(*it);
 741     while( ++it != elements.end() ) {
 742       cur = nm->mkNode(kind::UNION, cur, SINGLETON(*it));
 743     }
 744     return cur;
 745   }
 746 }
 747 Node TheorySetsPrivate::elementsToShape(set<Node> elements, TypeNode setType) const
 748 {
 749   NodeManager* nm = NodeManager::currentNM();
 750
 751   if(elements.size() == 0) {
 752     return nm->mkConst(EmptySet(nm->toType(setType)));
 753   } else {
 754     typeof(elements.begin()) it = elements.begin();
 755     Node cur = SINGLETON(*it);
 756     while( ++it != elements.end() ) {
 757       cur = nm->mkNode(kind::UNION, cur, SINGLETON(*it));
 758     }
 759     return cur;
 760   }
 761 }
 762
 763 void TheorySetsPrivate::collectModelInfo(TheoryModel* m, bool fullModel)
 764 {
 765   Debug("sets-model") << "[sets-model] collectModelInfo(..., fullModel="
 766                       << (fullModel ? "true)" : "false)") << std::endl;
 767
 768   set<Node> terms;
 769
 770   // Compute terms appearing assertions and shared terms
 771   d_external.computeRelevantTerms(terms);
 772
 773   // Compute for each setterm elements that it contains
 774   SettermElementsMap settermElementsMap;
 775   TNode true_atom = NodeManager::currentNM()->mkConst<bool>(true);
 776   TNode false_atom = NodeManager::currentNM()->mkConst<bool>(false);
 777   for(eq::EqClassIterator it_eqclasses(true_atom, &d_equalityEngine);
 778       ! it_eqclasses.isFinished() ; ++it_eqclasses) {
 779     TNode n = (*it_eqclasses);
 780     if(n.getKind() == kind::MEMBER) {
 781       Assert(d_equalityEngine.areEqual(n, true_atom));
 782       TNode x = d_equalityEngine.getRepresentative(n[0]);
 783       TNode S = d_equalityEngine.getRepresentative(n[1]);
 784       settermElementsMap[S].insert(x);
 785     }
 786     if(Debug.isOn("sets-model-details")) {
 787       vector<TNode> explanation;
 788       d_equalityEngine.explainPredicate(n, true, explanation);
 789       Debug("sets-model-details")
 790         << "[sets-model-details]  >  node: " << n << ", explanation:" << std::endl;
 791       BOOST_FOREACH(TNode m, explanation) {
 792         Debug("sets-model-details") << "[sets-model-details]  >>  " << m << std::endl;
 793       }
 794     }
 795   }
 796
 797   if(Debug.isOn("sets-model-details")) {
 798     for(eq::EqClassIterator it_eqclasses(false_atom, &d_equalityEngine);
 799         ! it_eqclasses.isFinished() ; ++it_eqclasses) {
 800       TNode n = (*it_eqclasses);
 801       vector<TNode> explanation;
 802       d_equalityEngine.explainPredicate(n, false, explanation);
 803       Debug("sets-model-details")
 804         << "[sets-model-details]  >  node: not: " << n << ", explanation:" << std::endl;
 805       BOOST_FOREACH(TNode m, explanation) {
 806         Debug("sets-model-details") << "[sets-model-details]  >>  " << m << std::endl;
 807       }
 808     }
 809   }
 810
 811   // Assert equalities and disequalities to the model
 812   m->assertEqualityEngine(&d_equalityEngine, &terms);
 813
 814   // Loop over terms to collect set-terms for which we generate models
 815   set<Node> settermsModEq;
 816   BOOST_FOREACH(TNode term, terms) {
 817     TNode n = term.getKind() == kind::NOT ? term[0] : term;
 818
 819     Debug("sets-model-details") << "[sets-model-details]  >   " << n << std::endl;
 820
 821     if(n.getType().isSet()) {
 822       n = d_equalityEngine.getRepresentative(n);
 823       if( !n.isConst() ) {
 824         settermsModEq.insert(n);
 825       }
 826     }
 827
 828   }
 829
 830   if(Debug.isOn("sets-model")) {
 831     BOOST_FOREACH( TNode node, settermsModEq ) {
 832       Debug("sets-model") << "[sets-model]   " << node << std::endl;
 833     }
 834   }
 835
 836   BOOST_FOREACH( SettermElementsMap::value_type &it, settermElementsMap ) {
 837     BOOST_FOREACH( TNode element, it.second /* elements */ ) {
 838       Debug("sets-model-details") << "[sets-model-details]  >   " <<
 839         (it.first /* setterm */) << ": " << element << std::endl;
 840     }
 841   }
 842
 843   // assign representatives to equivalence class
 844   BOOST_FOREACH( TNode setterm, settermsModEq ) {
 845     Elements elements = getElements(setterm, settermElementsMap);
 846     Node shape = elementsToShape(elements, setterm.getType());
 847     shape = theory::Rewriter::rewrite(shape);
 848     m->assertEquality(shape, setterm, true);
 849     m->assertRepresentative(shape);
 850   }
 851
 852 #ifdef CVC4_ASSERTIONS
 853   bool checkPassed = true;
 854   BOOST_FOREACH(TNode term, terms) {
 855     if( term.getType().isSet() ) {
 856       checkPassed &= checkModel(settermElementsMap, term);
 857     }
 858   }
 859   if(Debug.isOn("sets-checkmodel-ignore")) {
 860     Debug("sets-checkmodel-ignore") << "[sets-checkmodel-ignore] checkPassed value was " << checkPassed << std::endl;
 861   } else {
 862     Assert( checkPassed,
 863             "THEORY_SETS check-model failed. Run with -d sets-model for details." );
 864   }
 865 #endif
 866 }
 867
 868 Node TheorySetsPrivate::getModelValue(TNode n)
 869 {
 870   CodeTimer codeTimer(d_statistics.d_getModelValueTime);
 871   return d_termInfoManager->getModelValue(n);
 872 }
 873
 874 /********************** Helper functions ***************************/
 875 /********************** Helper functions ***************************/
 876 /********************** Helper functions ***************************/
 877
 878 Node mkAnd(const std::vector<TNode>& conjunctions) {
 879   Assert(conjunctions.size() > 0);
 880
 881   std::set<TNode> all;
 882
 883   for (unsigned i = 0; i < conjunctions.size(); ++i) {
 884     TNode t = conjunctions[i];
 885
 886     if (t.getKind() == kind::AND) {
 887       for(TNode::iterator child_it = t.begin();
 888           child_it != t.end(); ++child_it) {
 889         Assert((*child_it).getKind() != kind::AND);
 890         all.insert(*child_it);
 891       }
 892     }
 893     else {
 894       all.insert(t);
 895     }
 896
 897   }
 898
 899   Assert(all.size() > 0);
 900
 901   if (all.size() == 1) {
 902     // All the same, or just one
 903     return conjunctions[0];
 904   }
 905
 906   NodeBuilder<> conjunction(kind::AND);
 907   std::set<TNode>::const_iterator it = all.begin();
 908   std::set<TNode>::const_iterator it_end = all.end();
 909   while (it != it_end) {
 910     conjunction << *it;
 911     ++ it;
 912   }
 913
 914   return conjunction;
 915 }/* mkAnd() */
 916
 917
 918 TheorySetsPrivate::Statistics::Statistics() :
 919   d_checkTime("theory::sets::time")
 920   , d_getModelValueTime("theory::sets::getModelValueTime")
 921   , d_memberLemmas("theory::sets::lemmas::member", 0)
 922   , d_disequalityLemmas("theory::sets::lemmas::disequality", 0)
 923 {
 924   StatisticsRegistry::registerStat(&d_checkTime);
 925   StatisticsRegistry::registerStat(&d_getModelValueTime);
 926   StatisticsRegistry::registerStat(&d_memberLemmas);
 927   StatisticsRegistry::registerStat(&d_disequalityLemmas);
 928 }
 929
 930
 931 TheorySetsPrivate::Statistics::~Statistics() {
 932   StatisticsRegistry::unregisterStat(&d_checkTime);
 933   StatisticsRegistry::unregisterStat(&d_getModelValueTime);
 934   StatisticsRegistry::unregisterStat(&d_memberLemmas);
 935   StatisticsRegistry::unregisterStat(&d_disequalityLemmas);
 936 }
 937
 938
 939 bool TheorySetsPrivate::present(TNode atom) {
 940   return holds(atom) || holds(atom.notNode());
 941 }
 942
 943
 944 bool TheorySetsPrivate::holds(TNode atom, bool polarity) {
 945   Node polarity_atom = NodeManager::currentNM()->mkConst<bool>(polarity);
 946
 947   Node atomModEq = NodeManager::currentNM()->mkNode
 948     (atom.getKind(), d_equalityEngine.getRepresentative(atom[0]),
 949      d_equalityEngine.getRepresentative(atom[1]) );
 950
 951   d_equalityEngine.addTerm(atomModEq);
 952
 953   return d_equalityEngine.areEqual(atomModEq, polarity_atom);
 954 }
 955
 956
 957 void TheorySetsPrivate::registerReason(TNode reason, bool save)
 958 {
 959   if(save) d_nodeSaver.insert(reason);
 960
 961   if(reason.getKind() == kind::AND) {
 962     Assert(reason.getNumChildren() == 2);
 963     registerReason(reason[0], false);
 964     registerReason(reason[1], false);
 965   } else if(reason.getKind() == kind::NOT) {
 966     registerReason(reason[0], false);
 967   } else if(reason.getKind() == kind::MEMBER) {
 968     d_equalityEngine.addTerm(reason);
 969     Assert(present(reason));
 970   } else if(reason.getKind() == kind::EQUAL) {
 971     d_equalityEngine.addTerm(reason);
 972     Assert(present(reason));
 973   } else if(reason.getKind() == kind::CONST_BOOLEAN) {
 974     // That's OK, already in EqEngine
 975   } else {
 976     Unhandled();
 977   }
 978 }
 979
 980 void TheorySetsPrivate::finishPropagation()
 981 {
 982   while(!d_conflict && !d_settermPropagationQueue.empty()) {
 983     std::pair<TNode,TNode> np = d_settermPropagationQueue.front();
 984     d_settermPropagationQueue.pop();
 985     doSettermPropagation(np.first, np.second);
 986   }
 987   while(!d_conflict && !d_propagationQueue.empty()) {
 988     std::pair<Node,Node> np = d_propagationQueue.front();
 989     d_propagationQueue.pop();
 990     TNode atom = np.first.getKind() == kind::NOT ? np.first[0] : np.first;
 991     if(atom.getKind() == kind::MEMBER) {
 992       assertMemebership(np.first, np.second, /* learnt = */ true);
 993     } else {
 994       assertEquality(np.first, np.second, /* learnt = */ true);
 995     }
 996   }
 997 }
 998
 999 void TheorySetsPrivate::addToPending(Node n) {
1000   Debug("sets-pending") << "[sets-pending] addToPending " << n << std::endl;
1001   if(d_pendingEverInserted.find(n) == d_pendingEverInserted.end()) {
1002     if(n.getKind() == kind::MEMBER) {
1003       Debug("sets-pending") << "[sets-pending] \u2514 added to member queue"
1004                             << std::endl;
1005       ++d_statistics.d_memberLemmas;
1006       d_pending.push(n);
1007     } else {
1008       Debug("sets-pending") << "[sets-pending] \u2514 added to equality queue"
1009                             << std::endl;
1010       Assert(n.getKind() == kind::EQUAL);
1011       ++d_statistics.d_disequalityLemmas;
1012       d_pendingDisequal.push(n);
1013     }
1014     d_external.d_out->lemma(getLemma());
1015     Assert(isComplete());
1016   }
1017 }
1018
1019 bool TheorySetsPrivate::isComplete() {
1020   // while(!d_pending.empty() &&
1021   //       (d_pendingEverInserted.find(d_pending.front()) != d_pendingEverInserted.end()
1022   //        || present(d_pending.front()) ) ) {
1023   //   Debug("sets-pending") << "[sets-pending] removing as already present: "
1024   //                         << d_pending.front() << std::endl;
1025   //   d_pending.pop();
1026   // }
1027   return d_pending.empty() && d_pendingDisequal.empty();
1028 }
1029
1030 Node TheorySetsPrivate::getLemma() {
1031   Assert(!d_pending.empty() || !d_pendingDisequal.empty());
1032
1033   Node n, lemma;
1034
1035   if(!d_pending.empty()) {
1036     n = d_pending.front();
1037     d_pending.pop();
1038     d_pendingEverInserted.insert(n);
1039
1040     Assert(!present(n));
1041     Assert(n.getKind() == kind::MEMBER);
1042
1043     lemma = OR(n, NOT(n));
1044   } else {
1045     n = d_pendingDisequal.front();
1046     d_pendingDisequal.pop();
1047     d_pendingEverInserted.insert(n);
1048
1049     Assert(n.getKind() == kind::EQUAL && n[0].getType().isSet());
1050     Node x = NodeManager::currentNM()->mkSkolem("sde_", n[0].getType().getSetElementType() );
1051     Node l1 = MEMBER(x, n[0]), l2 = MEMBER(x, n[1]);
1052
1053     lemma = OR(n, AND(l1, NOT(l2)), AND(NOT(l1), l2));
1054   }
1055
1056   Debug("sets-lemma") << "[sets-lemma] Generating for " << n << ", lemma: " << lemma << std::endl;
1057
1058   return  lemma;
1059 }
1060
1061
1062 TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
1063                                      context::Context* c,
1064                                      context::UserContext* u):
1065   d_external(external),
1066   d_notify(*this),
1067   d_equalityEngine(d_notify, c, "theory::sets::TheorySetsPrivate"),
1068   d_conflict(c),
1069   d_termInfoManager(NULL),
1070   d_propagationQueue(c),
1071   d_settermPropagationQueue(c),
1072   d_nodeSaver(c),
1073   d_pending(c),
1074   d_pendingDisequal(c),
1075   d_pendingEverInserted(u),
1076   d_modelCache(c),
1077   d_ccg_i(c),
1078   d_ccg_j(c),
1079   d_scrutinize(NULL)
1080 {
1081   d_termInfoManager = new TermInfoManager(*this, c, &d_equalityEngine);
1082
1083   d_equalityEngine.addFunctionKind(kind::UNION);
1084   d_equalityEngine.addFunctionKind(kind::INTERSECTION);
1085   d_equalityEngine.addFunctionKind(kind::SETMINUS);
1086
1087   d_equalityEngine.addFunctionKind(kind::MEMBER);
1088   d_equalityEngine.addFunctionKind(kind::SUBSET);
1089
1090   if( Debug.isOn("sets-scrutinize") ) {
1091     d_scrutinize = new TheorySetsScrutinize(this);
1092   }
1093 }/* TheorySetsPrivate::TheorySetsPrivate() */
1094
1095
1096 TheorySetsPrivate::~TheorySetsPrivate()
1097 {
1098   delete d_termInfoManager;
1099   if( Debug.isOn("sets-scrutinize") ) {
1100     Assert(d_scrutinize != NULL);
1101     delete d_scrutinize;
1102   }
1103 }/* TheorySetsPrivate::~TheorySetsPrivate() */
1104
1105 void TheorySetsPrivate::propagate(Theory::Effort effort) {
1106   if(effort != Theory::EFFORT_FULL || !options::setsPropFull()) {
1107     return;
1108   }
1109
1110   // build a model
1111   Trace("sets-prop-full") << "[sets-prop-full] propagate(FULL_EFFORT)" << std::endl;
1112   if(Trace.isOn("sets-assertions")) {
1113     dumpAssertionsHumanified();
1114   }
1115
1116   const CDNodeSet& terms = (d_termInfoManager->d_terms);
1117   for(typeof(terms.begin()) it = terms.begin(); it != terms.end(); ++it) {
1118     Node node = (*it);
1119     Kind k = node.getKind();
1120     if(k == kind::UNION && node[0].getKind() == kind::SINGLETON ) {
1121
1122       if(holds(MEMBER(node[0][0], node[1]))) {
1123         Trace("sets-prop-full") << "[sets-prop-full] " << MEMBER(node[0][0], node[1])
1124                                 << " => " << EQUAL(node[1], node) << std::endl;
1125         learnLiteral(EQUAL(node[1], node), MEMBER(node[0][0], node[1]));
1126       }
1127
1128     } else if(k == kind::UNION && node[1].getKind() == kind::SINGLETON ) {
1129
1130       if(holds(MEMBER(node[1][0], node[0]))) {
1131         Trace("sets-prop-full") << "[sets-prop-full] " << MEMBER(node[1][0], node[0])
1132                                 << " => " << EQUAL(node[0], node) << std::endl;
1133         learnLiteral(EQUAL(node[0], node), MEMBER(node[1][0], node[0]));
1134       }
1135
1136     }
1137   }
1138
1139   finishPropagation();
1140 }
1141
1142 bool TheorySetsPrivate::propagate(TNode literal) {
1143   Debug("sets-prop") << " propagate(" << literal  << ")" << std::endl;
1144
1145   // If already in conflict, no more propagation
1146   if (d_conflict) {
1147     Debug("sets-prop") << "TheoryUF::propagate(" << literal << "): already in conflict" << std::endl;
1148     return false;
1149   }
1150
1151   // Propagate out
1152   bool ok = d_external.d_out->propagate(literal);
1153   if (!ok) {
1154     d_conflict = true;
1155   }
1156
1157   return ok;
1158 }/* TheorySetsPrivate::propagate(TNode) */
1159
1160
1161 void TheorySetsPrivate::setMasterEqualityEngine(eq::EqualityEngine* eq) {
1162   d_equalityEngine.setMasterEqualityEngine(eq);
1163 }
1164
1165
1166 void TheorySetsPrivate::conflict(TNode a, TNode b)
1167 {
1168   if (a.getKind() == kind::CONST_BOOLEAN) {
1169     d_conflictNode = explain(a.iffNode(b));
1170   } else {
1171     d_conflictNode = explain(a.eqNode(b));
1172   }
1173   d_external.d_out->conflict(d_conflictNode);
1174   Debug("sets") << "[sets] conflict: " << a << " iff " << b
1175                 << ", explaination " << d_conflictNode << std::endl;
1176   d_conflict = true;
1177 }
1178
1179 Node TheorySetsPrivate::explain(TNode literal)
1180 {
1181   Debug("sets") << "TheorySetsPrivate::explain(" << literal << ")"
1182                 << std::endl;
1183
1184   bool polarity = literal.getKind() != kind::NOT;
1185   TNode atom = polarity ? literal : literal[0];
1186   std::vector<TNode> assumptions;
1187
1188   if(atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
1189     d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
1190   } else if(atom.getKind() == kind::MEMBER) {
1191     if( !d_equalityEngine.hasTerm(atom)) {
1192       d_equalityEngine.addTerm(atom);
1193     }
1194     d_equalityEngine.explainPredicate(atom, polarity, assumptions);
1195   } else {
1196     Debug("sets") << "unhandled: " << literal << "; (" << atom << ", "
1197                   << polarity << "); kind" << atom.getKind() << std::endl;
1198     Unhandled();
1199   }
1200
1201   return mkAnd(assumptions);
1202 }
1203
1204
1205 void TheorySetsPrivate::preRegisterTerm(TNode node)
1206 {
1207   Debug("sets") << "TheorySetsPrivate::preRegisterTerm(" << node << ")"
1208                 << std::endl;
1209
1210   switch(node.getKind()) {
1211   case kind::EQUAL:
1212     // TODO: what's the point of this
1213     d_equalityEngine.addTriggerEquality(node);
1214     break;
1215   case kind::MEMBER:
1216     // TODO: what's the point of this
1217     d_equalityEngine.addTriggerPredicate(node);
1218     break;
1219   default:
1220     d_termInfoManager->addTerm(node);
1221     d_equalityEngine.addTriggerTerm(node, THEORY_SETS);
1222     // d_equalityEngine.addTerm(node);
1223   }
1224   if(node.getKind() == kind::SINGLETON) {
1225     Node true_node = NodeManager::currentNM()->mkConst<bool>(true);
1226     learnLiteral(MEMBER(node[0], node), true, true_node);
1227     //intentional fallthrough
1228   }
1229 }
1230
1231
1232
1233 /**************************** eq::NotifyClass *****************************/
1234 /**************************** eq::NotifyClass *****************************/
1235 /**************************** eq::NotifyClass *****************************/
1236
1237
1238 bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool value)
1239 {
1240   Debug("sets-eq") << "[sets-eq] eqNotifyTriggerEquality: equality = " << equality
1241                    << " value = " << value << std::endl;
1242   if (value) {
1243     return d_theory.propagate(equality);
1244   } else {
1245     // We use only literal triggers so taking not is safe
1246     return d_theory.propagate(equality.notNode());
1247   }
1248 }
1249
1250 bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value)
1251 {
1252   Debug("sets-eq") << "[sets-eq] eqNotifyTriggerPredicate: predicate = " << predicate
1253                    << " value = " << value << std::endl;
1254   if (value) {
1255     return d_theory.propagate(predicate);
1256   } else {
1257     return d_theory.propagate(predicate.notNode());
1258   }
1259 }
1260
1261 bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value)
1262 {
1263   Debug("sets-eq") << "[sets-eq] eqNotifyTriggerTermEquality: tag = " << tag
1264                    << " t1 = " << t1 << "  t2 = " << t2 << "  value = " << value << std::endl;
1265   if(value) {
1266     d_theory.d_termInfoManager->mergeTerms(t1, t2);
1267   }
1268   d_theory.propagate( value ? EQUAL(t1, t2) : NOT(EQUAL(t1, t2)) );
1269   return true;
1270 }
1271
1272 void TheorySetsPrivate::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2)
1273 {
1274   Debug("sets-eq") << "[sets-eq] eqNotifyConstantTermMerge " << " t1 = " << t1 << " t2 = " << t2 << std::endl;
1275   d_theory.conflict(t1, t2);
1276 }
1277
1278 // void TheorySetsPrivate::NotifyClass::eqNotifyNewClass(TNode t)
1279 // {
1280 //   Debug("sets-eq") << "[sets-eq] eqNotifyNewClass:" << " t = " << t << std::endl;
1281 // }
1282
1283 // void TheorySetsPrivate::NotifyClass::eqNotifyPreMerge(TNode t1, TNode t2)
1284 // {
1285 //   Debug("sets-eq") << "[sets-eq] eqNotifyPreMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl;
1286 // }
1287
1288 // void TheorySetsPrivate::NotifyClass::eqNotifyPostMerge(TNode t1, TNode t2)
1289 // {
1290 //   Debug("sets-eq") << "[sets-eq] eqNotifyPostMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl;
1291 // }
1292
1293 // void TheorySetsPrivate::NotifyClass::eqNotifyDisequal(TNode t1, TNode t2, TNode reason)
1294 // {
1295 //   Debug("sets-eq") << "[sets-eq] eqNotifyDisequal:" << " t1 = " << t1 << " t2 = " << t2 << " reason = " << reason << std::endl;
1296 // }
1297
1298
1299 /**************************** TermInfoManager *****************************/
1300 /**************************** TermInfoManager *****************************/
1301 /**************************** TermInfoManager *****************************/
1302
1303 void TheorySetsPrivate::TermInfoManager::mergeLists
1304 (CDTNodeList* la, const CDTNodeList* lb) const {
1305   // straight from theory/arrays/array_info.cpp
1306   std::set<TNode> temp;
1307   CDTNodeList::const_iterator it;
1308   for(it = la->begin() ; it != la->end(); it++ ) {
1309     temp.insert((*it));
1310   }
1311
1312   for(it = lb->begin() ; it!= lb->end(); it++ ) {
1313     if(temp.count(*it) == 0) {
1314       la->push_back(*it);
1315     }
1316   }
1317 }
1318
1319 TheorySetsPrivate::TermInfoManager::TermInfoManager
1320 (TheorySetsPrivate& theory, context::Context* satContext, eq::EqualityEngine* eq):
1321   d_theory(theory),
1322   d_context(satContext),
1323   d_eqEngine(eq),
1324   d_terms(satContext),
1325   d_info()
1326 { }
1327
1328 TheorySetsPrivate::TermInfoManager::~TermInfoManager() {
1329   for( typeof(d_info.begin()) it = d_info.begin();
1330        it != d_info.end(); ++it) {
1331     delete (*it).second;
1332   }
1333 }
1334
1335 void TheorySetsPrivate::TermInfoManager::notifyMembership(TNode fact) {
1336   bool polarity = fact.getKind() != kind::NOT;
1337   TNode atom = polarity ? fact : fact[0];
1338
1339   TNode x = d_eqEngine->getRepresentative(atom[0]);
1340   TNode S = d_eqEngine->getRepresentative(atom[1]);
1341
1342   Debug("sets-terminfo") << "[sets-terminfo] Adding membership " << x
1343                          << " in " << S << " " << polarity << std::endl;
1344
1345   d_info[S]->addToElementList(x, polarity);
1346   d_info[x]->addToSetList(S, polarity);
1347
1348   d_theory.d_modelCache.clear();
1349 }
1350
1351 const CDTNodeList* TheorySetsPrivate::TermInfoManager::getParents(TNode x) {
1352   return d_info[x]->parents;
1353 }
1354
1355 const CDTNodeList* TheorySetsPrivate::TermInfoManager::getMembers(TNode S) {
1356   return d_info[S]->elementsInThisSet;
1357 }
1358
1359 const CDTNodeList* TheorySetsPrivate::TermInfoManager::getNonMembers(TNode S) {
1360   return d_info[S]->elementsNotInThisSet;
1361 }
1362
1363 void TheorySetsPrivate::TermInfoManager::addTerm(TNode n) {
1364   unsigned numChild = n.getNumChildren();
1365
1366   if(!d_terms.contains(n)) {
1367     d_terms.insert(n);
1368     d_info[n] = new TheorySetsTermInfo(d_context);
1369   }
1370
1371   if(n.getKind() == kind::UNION ||
1372      n.getKind() == kind::INTERSECTION ||
1373      n.getKind() == kind::SETMINUS) {
1374
1375     for(unsigned i = 0; i < numChild; ++i) {
1376       if(d_terms.contains(n[i])) {
1377         Debug("sets-parent") << "Adding " << n << " to parent list of "
1378                              << n[i] << std::endl;
1379         d_info[n[i]]->parents->push_back(n);
1380       }
1381     }
1382
1383   }
1384 }
1385
1386 void TheorySetsPrivate::TermInfoManager::pushToSettermPropagationQueue
1387 (TNode x, TNode S, bool polarity)
1388 {
1389   Node cur_atom = MEMBER(x, S);
1390
1391   // propagation : empty set
1392   if(polarity && S.getKind() == kind::EMPTYSET) {
1393     Debug("sets-prop") << "[sets-prop]  something in empty set? conflict."
1394                        << std::endl;
1395     d_theory.learnLiteral(cur_atom, false, cur_atom);
1396     return;
1397   }// propagation: empty set
1398
1399   // propagation : children
1400   if(S.getKind() == kind::UNION ||
1401      S.getKind() == kind::INTERSECTION ||
1402      S.getKind() == kind::SETMINUS ||
1403      S.getKind() == kind::SINGLETON) {
1404     d_theory.d_settermPropagationQueue.push_back(std::make_pair(x, S));
1405   }// propagation: children
1406
1407   // propagation : parents
1408   const CDTNodeList* parentList = getParents(S);
1409   for(typeof(parentList->begin()) k = parentList->begin();
1410       k != parentList->end(); ++k) {
1411     d_theory.d_settermPropagationQueue.push_back(std::make_pair(x, *k));
1412   }// propagation : parents
1413
1414 }
1415
1416 void TheorySetsPrivate::TermInfoManager::pushToSettermPropagationQueue
1417 (TNode x, CDTNodeList* l, bool polarity)
1418 {
1419   set<TNode> alreadyProcessed;
1420
1421   BOOST_FOREACH(TNode S, (*l) ) {
1422     Debug("sets-prop") << "[sets-terminfo]  setterm todo: "
1423                        << MEMBER(x, d_eqEngine->getRepresentative(S))
1424                        << std::endl;
1425
1426     TNode repS = d_eqEngine->getRepresentative(S);
1427     if(alreadyProcessed.find(repS) != alreadyProcessed.end()) {
1428       continue;
1429     } else {
1430       alreadyProcessed.insert(repS);
1431     }
1432
1433     d_eqEngine->addTerm(MEMBER(d_eqEngine->getRepresentative(x), repS));
1434
1435     for(eq::EqClassIterator j(d_eqEngine->getRepresentative(S), d_eqEngine);
1436         !j.isFinished(); ++j) {
1437
1438       pushToSettermPropagationQueue(x, *j, polarity);
1439
1440     }//j loop
1441   }
1442 }
1443
1444 void TheorySetsPrivate::TermInfoManager::pushToSettermPropagationQueue
1445 (CDTNodeList* l, TNode S, bool polarity)
1446 {
1447   BOOST_FOREACH(TNode x, (*l) ) {
1448     Debug("sets-prop") << "[sets-terminfo]  setterm todo: "
1449                        << MEMBER(x, d_eqEngine->getRepresentative(S))
1450                        << std::endl;
1451
1452     d_eqEngine->addTerm(MEMBER(d_eqEngine->getRepresentative(x),
1453                                d_eqEngine->getRepresentative(S)));
1454
1455     for(eq::EqClassIterator j(d_eqEngine->getRepresentative(S), d_eqEngine);
1456         !j.isFinished(); ++j) {
1457
1458       pushToSettermPropagationQueue(x, *j, polarity);
1459
1460     }//j loop
1461
1462   }
1463
1464 }
1465
1466
1467
1468 void TheorySetsPrivate::TermInfoManager::mergeTerms(TNode a, TNode b) {
1469   // merge b into a
1470   Debug("sets-terminfo") << "[sets-terminfo] Merging (into) a = " << a
1471                          << ", b = " << b << std::endl;
1472   Debug("sets-terminfo") << "[sets-terminfo] reps"
1473                          << ", a: " << d_eqEngine->getRepresentative(a)
1474                          << ", b: " << d_eqEngine->getRepresentative(b)
1475                          << std::endl;
1476
1477   typeof(d_info.begin()) ita = d_info.find(a);
1478   typeof(d_info.begin()) itb = d_info.find(b);
1479
1480   Assert(ita != d_info.end());
1481   Assert(itb != d_info.end());
1482
1483   /* elements in this sets */
1484   pushToSettermPropagationQueue( (*ita).second->elementsInThisSet, b, true );
1485   pushToSettermPropagationQueue( (*ita).second->elementsNotInThisSet, b, false );
1486   pushToSettermPropagationQueue( (*itb).second->elementsNotInThisSet, a, false );
1487   pushToSettermPropagationQueue( (*itb).second->elementsInThisSet, a, true );
1488   mergeLists((*ita).second->elementsInThisSet,
1489              (*itb).second->elementsInThisSet);
1490   mergeLists((*ita).second->elementsNotInThisSet,
1491              (*itb).second->elementsNotInThisSet);
1492
1493   /* sets containing this element */
1494   // pushToSettermPropagationQueue( b, (*ita).second->setsContainingThisElement, true);
1495   // pushToSettermPropagationQueue( b, (*ita).second->setsNotContainingThisElement, false);
1496   pushToSettermPropagationQueue( a, (*itb).second->setsNotContainingThisElement, false);
1497   pushToSettermPropagationQueue( a, (*itb).second->setsContainingThisElement, true);
1498   mergeLists( (*ita).second->setsContainingThisElement,
1499               (*itb).second->setsContainingThisElement );
1500   mergeLists( (*ita).second->setsNotContainingThisElement,
1501               (*itb).second->setsNotContainingThisElement );
1502
1503   d_theory.d_modelCache.clear();
1504 }
1505
1506 Node TheorySetsPrivate::TermInfoManager::getModelValue(TNode n)
1507 {
1508   if(d_terms.find(n) == d_terms.end()) {
1509     return Node();
1510   }
1511   Assert(n.getType().isSet());
1512   set<Node> elements, elements_const;
1513   Node S = d_eqEngine->getRepresentative(n);
1514   typeof(d_theory.d_modelCache.begin()) it = d_theory.d_modelCache.find(S);
1515   if(it != d_theory.d_modelCache.end()) {
1516     return (*it).second;
1517   }
1518   const CDTNodeList* l = getMembers(S);
1519   for(typeof(l->begin()) it = l->begin(); it != l->end(); ++it) {
1520     TNode n = *it;
1521     elements.insert(d_eqEngine->getRepresentative(n));
1522   }
1523   BOOST_FOREACH(TNode e, elements) {
1524     if(e.isConst()) {
1525       elements_const.insert(e);
1526     } else {
1527       elements_const.insert(d_theory.d_external.d_valuation.getModelValue(e));
1528     }
1529   }
1530   Node v = d_theory.elementsToShape(elements_const, n.getType());
1531   d_theory.d_modelCache[n] = v;
1532   return v;
1533 }
1534
1535 }/* CVC4::theory::sets namespace */
1536 }/* CVC4::theory namespace */
1537 }/* CVC4 namespace */