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_equalityEngine.addTriggerTerm(n, THEORY_SETS);
 418 }
 419
 420 void TheorySetsPrivate::dumpAssertionsHumanified() const
 421 {
 422     std::string tag = "sets-assertions";
 423     context::CDList<Assertion>::const_iterator it = d_external.facts_begin(), it_end = d_external.facts_end();
 424
 425     std::map<TNode, std::set<TNode> > equalities;
 426     std::set< pair<TNode, TNode> > disequalities;
 427     std::map<TNode, std::pair<std::set<TNode>, std::set<TNode> > > members;
 428     static std::map<TNode, int> numbering;
 429     static int number = 0;
 430
 431     for (unsigned i = 0; it != it_end; ++ it, ++i) {
 432       TNode ass = (*it).assertion;
 433       // Trace("sets-care-dump") << AssertCommand(ass.toExpr()) << endl;
 434       bool polarity = ass.getKind() != kind::NOT;
 435       ass = polarity ? ass : ass[0];
 436       Assert( ass.getNumChildren() == 2);
 437       TNode left = d_equalityEngine.getRepresentative(ass[0]);
 438       TNode right = d_equalityEngine.getRepresentative(ass[1]);
 439       if(numbering[left] == 0) numbering[left] = ++number;
 440       if(numbering[right] == 0) numbering[right] = ++number;
 441       equalities[left].insert(ass[0]);
 442       equalities[right].insert(ass[1]);
 443       if(ass.getKind() == kind::EQUAL) {
 444         if(polarity) {
 445           Assert(left == right);
 446         } else {
 447           if(left > right) std::swap(left, right);
 448           disequalities.insert(make_pair(left, right));
 449         }
 450       } else if(ass.getKind() == kind::MEMBER) {
 451         (polarity ? members[right].first : members[right].second).insert(left);
 452       }
 453     }
 454 #define FORIT(it, container) for(typeof((container).begin()) it=(container).begin(); (it) != (container).end(); ++(it))
 455     FORIT(kt, equalities) {
 456       Trace(tag) << " Eq class of t" << numbering[(*kt).first] << ": " << std::endl;
 457       FORIT(jt, (*kt).second) {
 458         TNode S = (*jt);
 459         if( S.getKind() != kind::UNION && S.getKind() != kind::INTERSECTION && S.getKind() != kind::SETMINUS) {
 460           Trace(tag) << "    " << *jt << ((*jt).getType().isSet() ? "\n": " ");
 461         } else {
 462           Trace(tag) << "    ";
 463           if(S[0].isConst() || numbering.find(d_equalityEngine.getRepresentative(S[0])) == numbering.end()) {
 464             Trace(tag) << S[0];
 465           } else {
 466             Trace(tag) << "t" << numbering[d_equalityEngine.getRepresentative(S[0])];
 467           }
 468           Trace(tag) << " " << (S.getKind() == kind::UNION ? "|" : (S.getKind() == kind::INTERSECTION ? "&" : "-")) << " ";
 469           if(S[1].isConst() || numbering.find(d_equalityEngine.getRepresentative(S[1])) == numbering.end()) {
 470             Trace(tag) << S[1];
 471           } else {
 472             Trace(tag) << "t" << numbering[d_equalityEngine.getRepresentative(S[1])];
 473           }
 474           Trace(tag) << std::endl;
 475         }
 476       }
 477       Trace(tag) << std::endl;
 478     }
 479     FORIT(kt, disequalities) Trace(tag) << "NOT(t"<<numbering[(*kt).first]<<" = t" <<numbering[(*kt).second] <<")"<< std::endl;
 480     FORIT(kt, members) {
 481       if( (*kt).second.first.size() > 0) {
 482         Trace(tag) << "IN t" << numbering[(*kt).first] << ": ";
 483         FORIT(jt, (*kt).second.first) {
 484           TNode x = (*jt);
 485           if(x.isConst() || numbering.find(d_equalityEngine.getRepresentative(x)) == numbering.end()) {
 486             Trace(tag) << x;
 487           } else {
 488             Trace(tag) << "x" << numbering[d_equalityEngine.getRepresentative(x)] << ", ";
 489           }
 490         }
 491         Trace(tag) << std::endl;
 492       }
 493       if( (*kt).second.second.size() > 0) {
 494         Trace(tag) << "NOT IN t" << numbering[(*kt).first] << ": ";
 495         FORIT(jt, (*kt).second.second) {
 496           TNode x = (*jt);
 497           if(x.isConst() || numbering.find(d_equalityEngine.getRepresentative(x)) == numbering.end()) {
 498             Trace(tag) << x;
 499           } else {
 500             Trace(tag) << "x" << numbering[d_equalityEngine.getRepresentative(x)] << ", ";
 501           }
 502         }
 503         Trace(tag) << std::endl;
 504       }
 505     }
 506     Trace(tag) << std::endl;
 507 #undef FORIT
 508 }
 509
 510 void TheorySetsPrivate::computeCareGraph() {
 511   Debug("sharing") << "Theory::computeCareGraph<" << d_external.identify() << ">()" << endl;
 512
 513   if(Trace.isOn("sets-assertions")) {
 514     // dump our understanding of assertions
 515     dumpAssertionsHumanified();
 516   }
 517
 518   unsigned i_st = 0;
 519   if(options::setsCare1()) { i_st = d_ccg_i; }
 520   for (unsigned i = i_st; i < d_external.d_sharedTerms.size(); ++ i) {
 521     TNode a = d_external.d_sharedTerms[i];
 522     TypeNode aType = a.getType();
 523
 524     unsigned j_st = i + 1;
 525     if(options::setsCare1()) { if(i == d_ccg_i) j_st = d_ccg_j + 1; }
 526
 527     for (unsigned j = j_st; j < d_external.d_sharedTerms.size(); ++ j) {
 528       TNode b = d_external.d_sharedTerms[j];
 529       if (b.getType() != aType) {
 530         // We don't care about the terms of different types
 531         continue;
 532       }
 533
 534       switch (d_external.d_valuation.getEqualityStatus(a, b)) {
 535       case EQUALITY_TRUE_AND_PROPAGATED:
 536         // If we know about it, we should have propagated it, so we can skip
 537         Trace("sets-care") << "[sets-care] Know: " << EQUAL(a, b) << std::endl;
 538         break;
 539       case EQUALITY_FALSE_AND_PROPAGATED:
 540         // If we know about it, we should have propagated it, so we can skip
 541         Trace("sets-care") << "[sets-care] Know: " << NOT(EQUAL(a, b)) << std::endl;
 542         break;
 543       case EQUALITY_FALSE:
 544       case EQUALITY_TRUE:
 545         Assert(false, "ERROR: Equality status true/false but not propagated (sets care graph computation).");
 546         break;
 547       case EQUALITY_TRUE_IN_MODEL:
 548         d_external.addCarePair(a, b);
 549       case EQUALITY_FALSE_IN_MODEL:
 550         if(Trace.isOn("sets-care-performance-test")) {
 551           // TODO: delete these lines, only for performance testing for now
 552           d_external.addCarePair(a, b);
 553         }
 554         break;
 555       case EQUALITY_UNKNOWN:
 556         // Let's split on it
 557         d_external.addCarePair(a, b);
 558         if(options::setsCare1()) {
 559           d_ccg_i = i;
 560           d_ccg_j = j;
 561           return;
 562         }
 563         break;
 564       default:
 565         Unreachable();
 566       }
 567     }
 568   }
 569 }
 570
 571 EqualityStatus TheorySetsPrivate::getEqualityStatus(TNode a, TNode b) {
 572   Assert(d_equalityEngine.hasTerm(a) && d_equalityEngine.hasTerm(b));
 573   if (d_equalityEngine.areEqual(a, b)) {
 574     // The terms are implied to be equal
 575     return EQUALITY_TRUE;
 576   }
 577   if (d_equalityEngine.areDisequal(a, b, false)) {
 578     // The terms are implied to be dis-equal
 579     return EQUALITY_FALSE;
 580   }
 581   if( d_external.d_valuation.getModelValue(a) == d_external.d_valuation.getModelValue(b) ) {
 582     // Ther term are true in current model
 583     return EQUALITY_TRUE_IN_MODEL;
 584   }
 585   return EQUALITY_FALSE_IN_MODEL;
 586   // }
 587   // //TODO: can we be more precise sometimes?
 588   // return EQUALITY_UNKNOWN;
 589 }
 590
 591 /******************** Model generation ********************/
 592 /******************** Model generation ********************/
 593 /******************** Model generation ********************/
 594
 595 const TheorySetsPrivate::Elements& TheorySetsPrivate::getElements
 596 (TNode setterm, SettermElementsMap& settermElementsMap) const {
 597   SettermElementsMap::const_iterator it = settermElementsMap.find(setterm);
 598   bool alreadyCalculated = (it != settermElementsMap.end());
 599   if( !alreadyCalculated ) {
 600
 601     Kind k = setterm.getKind();
 602     unsigned numChildren = setterm.getNumChildren();
 603     Elements cur;
 604     if(numChildren == 2) {
 605       const Elements& left = getElements(setterm[0], settermElementsMap);
 606       const Elements& right = getElements(setterm[1], settermElementsMap);
 607       switch(k) {
 608       case kind::UNION:
 609         if(left.size() >= right.size()) {
 610           cur = left; cur.insert(right.begin(), right.end());
 611         } else {
 612           cur = right; cur.insert(left.begin(), left.end());
 613         }
 614         break;
 615       case kind::INTERSECTION:
 616         std::set_intersection(left.begin(), left.end(), right.begin(), right.end(),
 617                               std::inserter(cur, cur.begin()) );
 618         break;
 619       case kind::SETMINUS:
 620         std::set_difference(left.begin(), left.end(), right.begin(), right.end(),
 621                             std::inserter(cur, cur.begin()) );
 622         break;
 623       default:
 624         Unhandled();
 625       }
 626     } else {
 627       Assert(k == kind::VARIABLE || k == kind::APPLY_UF || k == kind::SKOLEM,
 628              (std::string("Expect variable or UF got ") + kindToString(k)).c_str() );
 629       /* assign emptyset, which is default */
 630     }
 631
 632     it = settermElementsMap.insert(SettermElementsMap::value_type(setterm, cur)).first;
 633   }
 634   return it->second;
 635 }
 636
 637
 638 bool TheorySetsPrivate::checkModel(const SettermElementsMap& settermElementsMap, TNode S) const {
 639
 640   Debug("sets-model") << "[sets-model] checkModel(..., " << S << "): "
 641                       << std::endl;
 642
 643   Assert(S.getType().isSet());
 644
 645   const Elements emptySetOfElements;
 646   const Elements& saved =
 647     d_equalityEngine.getRepresentative(S).getKind() == kind::EMPTYSET ||
 648     settermElementsMap.find(d_equalityEngine.getRepresentative(S)) == settermElementsMap.end() ?
 649     emptySetOfElements :
 650     settermElementsMap.find(d_equalityEngine.getRepresentative(S))->second;
 651   Debug("sets-model") << "[sets-model] saved :  { ";
 652   BOOST_FOREACH(TNode element, saved) { Debug("sets-model") << element << ", "; }
 653   Debug("sets-model") << " }" << std::endl;
 654
 655   if(S.getNumChildren() == 2) {
 656
 657     Elements cur;
 658
 659     const Elements& left =
 660       d_equalityEngine.getRepresentative(S[0]).getKind() == kind::EMPTYSET ||
 661       settermElementsMap.find(d_equalityEngine.getRepresentative(S[0])) == settermElementsMap.end() ?
 662       emptySetOfElements :
 663       settermElementsMap.find(d_equalityEngine.getRepresentative(S[0]))->second;
 664
 665     const Elements&  right =
 666       d_equalityEngine.getRepresentative(S[1]).getKind() == kind::EMPTYSET ||
 667       settermElementsMap.find(d_equalityEngine.getRepresentative(S[1])) == settermElementsMap.end() ?
 668       emptySetOfElements :
 669       settermElementsMap.find(d_equalityEngine.getRepresentative(S[1]))->second;
 670
 671     switch(S.getKind()) {
 672     case kind::UNION:
 673       if(left.size() >= right.size()) {
 674         cur = left; cur.insert(right.begin(), right.end());
 675       } else {
 676         cur = right; cur.insert(left.begin(), left.end());
 677       }
 678       break;
 679     case kind::INTERSECTION:
 680       std::set_intersection(left.begin(), left.end(), right.begin(), right.end(),
 681                             std::inserter(cur, cur.begin()) );
 682       break;
 683     case kind::SETMINUS:
 684       std::set_difference(left.begin(), left.end(), right.begin(), right.end(),
 685                           std::inserter(cur, cur.begin()) );
 686       break;
 687     default:
 688       Unhandled();
 689     }
 690
 691     Debug("sets-model") << "[sets-model] cur :  { ";
 692     BOOST_FOREACH(TNode element, cur) { Debug("sets-model") << element << ", "; }
 693     Debug("sets-model") << " }" << std::endl;
 694
 695     if(saved != cur) {
 696       Debug("sets-model") << "[sets-model] *** ERROR *** cur != saved "
 697                           << std::endl;
 698       Debug("sets-model")
 699         << "[sets-model]   FYI: "
 700         << "  [" << S << "] = " << d_equalityEngine.getRepresentative(S) << ", "
 701         << "  [" << S[0] << "] = " << d_equalityEngine.getRepresentative(S[0]) << ", "
 702         << "  [" << S[1] << "] = " << d_equalityEngine.getRepresentative(S[1]) << "\n";
 703
 704       return false;
 705     }
 706   }
 707   return true;
 708 }
 709
 710 Node TheorySetsPrivate::elementsToShape(Elements elements, TypeNode setType) const
 711 {
 712   NodeManager* nm = NodeManager::currentNM();
 713
 714   if(elements.size() == 0) {
 715     return nm->mkConst(EmptySet(nm->toType(setType)));
 716   } else {
 717     Elements::iterator it = elements.begin();
 718     Node cur = SINGLETON(*it);
 719     while( ++it != elements.end() ) {
 720       cur = nm->mkNode(kind::UNION, cur, SINGLETON(*it));
 721     }
 722     return cur;
 723   }
 724 }
 725 Node TheorySetsPrivate::elementsToShape(set<Node> elements, TypeNode setType) const
 726 {
 727   NodeManager* nm = NodeManager::currentNM();
 728
 729   if(elements.size() == 0) {
 730     return nm->mkConst(EmptySet(nm->toType(setType)));
 731   } else {
 732     typeof(elements.begin()) it = elements.begin();
 733     Node cur = SINGLETON(*it);
 734     while( ++it != elements.end() ) {
 735       cur = nm->mkNode(kind::UNION, cur, SINGLETON(*it));
 736     }
 737     return cur;
 738   }
 739 }
 740
 741 void TheorySetsPrivate::collectModelInfo(TheoryModel* m, bool fullModel)
 742 {
 743   Debug("sets-model") << "[sets-model] collectModelInfo(..., fullModel="
 744                       << (fullModel ? "true)" : "false)") << std::endl;
 745
 746   set<Node> terms;
 747
 748   // Compute terms appearing assertions and shared terms
 749   d_external.computeRelevantTerms(terms);
 750
 751   // Compute for each setterm elements that it contains
 752   SettermElementsMap settermElementsMap;
 753   TNode true_atom = NodeManager::currentNM()->mkConst<bool>(true);
 754   TNode false_atom = NodeManager::currentNM()->mkConst<bool>(false);
 755   for(eq::EqClassIterator it_eqclasses(true_atom, &d_equalityEngine);
 756       ! it_eqclasses.isFinished() ; ++it_eqclasses) {
 757     TNode n = (*it_eqclasses);
 758     if(n.getKind() == kind::MEMBER) {
 759       Assert(d_equalityEngine.areEqual(n, true_atom));
 760       TNode x = d_equalityEngine.getRepresentative(n[0]);
 761       TNode S = d_equalityEngine.getRepresentative(n[1]);
 762       settermElementsMap[S].insert(x);
 763     }
 764     if(Debug.isOn("sets-model-details")) {
 765       vector<TNode> explanation;
 766       d_equalityEngine.explainPredicate(n, true, explanation);
 767       Debug("sets-model-details")
 768         << "[sets-model-details]  >  node: " << n << ", explanation:" << std::endl;
 769       BOOST_FOREACH(TNode m, explanation) {
 770         Debug("sets-model-details") << "[sets-model-details]  >>  " << m << std::endl;
 771       }
 772     }
 773   }
 774
 775   if(Debug.isOn("sets-model-details")) {
 776     for(eq::EqClassIterator it_eqclasses(false_atom, &d_equalityEngine);
 777         ! it_eqclasses.isFinished() ; ++it_eqclasses) {
 778       TNode n = (*it_eqclasses);
 779       vector<TNode> explanation;
 780       d_equalityEngine.explainPredicate(n, false, explanation);
 781       Debug("sets-model-details")
 782         << "[sets-model-details]  >  node: not: " << n << ", explanation:" << std::endl;
 783       BOOST_FOREACH(TNode m, explanation) {
 784         Debug("sets-model-details") << "[sets-model-details]  >>  " << m << std::endl;
 785       }
 786     }
 787   }
 788
 789   // Assert equalities and disequalities to the model
 790   m->assertEqualityEngine(&d_equalityEngine, &terms);
 791
 792   // Loop over terms to collect set-terms for which we generate models
 793   set<Node> settermsModEq;
 794   BOOST_FOREACH(TNode term, terms) {
 795     TNode n = term.getKind() == kind::NOT ? term[0] : term;
 796
 797     Debug("sets-model-details") << "[sets-model-details]  >   " << n << std::endl;
 798
 799     if(n.getType().isSet()) {
 800       n = d_equalityEngine.getRepresentative(n);
 801       if( !n.isConst() ) {
 802         settermsModEq.insert(n);
 803       }
 804     }
 805
 806   }
 807
 808   if(Debug.isOn("sets-model")) {
 809     BOOST_FOREACH( TNode node, settermsModEq ) {
 810       Debug("sets-model") << "[sets-model]   " << node << std::endl;
 811     }
 812   }
 813
 814   BOOST_FOREACH( SettermElementsMap::value_type &it, settermElementsMap ) {
 815     BOOST_FOREACH( TNode element, it.second /* elements */ ) {
 816       Debug("sets-model-details") << "[sets-model-details]  >   " <<
 817         (it.first /* setterm */) << ": " << element << std::endl;
 818     }
 819   }
 820
 821   // assign representatives to equivalence class
 822   BOOST_FOREACH( TNode setterm, settermsModEq ) {
 823     Elements elements = getElements(setterm, settermElementsMap);
 824     Node shape = elementsToShape(elements, setterm.getType());
 825     shape = theory::Rewriter::rewrite(shape);
 826     m->assertEquality(shape, setterm, true);
 827     m->assertRepresentative(shape);
 828   }
 829
 830 #ifdef CVC4_ASSERTIONS
 831   bool checkPassed = true;
 832   BOOST_FOREACH(TNode term, terms) {
 833     if( term.getType().isSet() ) {
 834       checkPassed &= checkModel(settermElementsMap, term);
 835     }
 836   }
 837   if(Debug.isOn("sets-checkmodel-ignore")) {
 838     Debug("sets-checkmodel-ignore") << "[sets-checkmodel-ignore] checkPassed value was " << checkPassed << std::endl;
 839   } else {
 840     Assert( checkPassed,
 841             "THEORY_SETS check-model failed. Run with -d sets-model for details." );
 842   }
 843 #endif
 844 }
 845
 846 Node TheorySetsPrivate::getModelValue(TNode n)
 847 {
 848   CodeTimer codeTimer(d_statistics.d_getModelValueTime);
 849   return d_termInfoManager->getModelValue(n);
 850 }
 851
 852 /********************** Helper functions ***************************/
 853 /********************** Helper functions ***************************/
 854 /********************** Helper functions ***************************/
 855
 856 Node mkAnd(const std::vector<TNode>& conjunctions) {
 857   Assert(conjunctions.size() > 0);
 858
 859   std::set<TNode> all;
 860
 861   for (unsigned i = 0; i < conjunctions.size(); ++i) {
 862     TNode t = conjunctions[i];
 863
 864     if (t.getKind() == kind::AND) {
 865       for(TNode::iterator child_it = t.begin();
 866           child_it != t.end(); ++child_it) {
 867         Assert((*child_it).getKind() != kind::AND);
 868         all.insert(*child_it);
 869       }
 870     }
 871     else {
 872       all.insert(t);
 873     }
 874
 875   }
 876
 877   Assert(all.size() > 0);
 878
 879   if (all.size() == 1) {
 880     // All the same, or just one
 881     return conjunctions[0];
 882   }
 883
 884   NodeBuilder<> conjunction(kind::AND);
 885   std::set<TNode>::const_iterator it = all.begin();
 886   std::set<TNode>::const_iterator it_end = all.end();
 887   while (it != it_end) {
 888     conjunction << *it;
 889     ++ it;
 890   }
 891
 892   return conjunction;
 893 }/* mkAnd() */
 894
 895
 896 TheorySetsPrivate::Statistics::Statistics() :
 897   d_checkTime("theory::sets::time")
 898   , d_getModelValueTime("theory::sets::getModelValueTime")
 899 {
 900   StatisticsRegistry::registerStat(&d_checkTime);
 901   StatisticsRegistry::registerStat(&d_getModelValueTime);
 902 }
 903
 904
 905 TheorySetsPrivate::Statistics::~Statistics() {
 906   StatisticsRegistry::unregisterStat(&d_checkTime);
 907   StatisticsRegistry::unregisterStat(&d_getModelValueTime);
 908 }
 909
 910
 911 bool TheorySetsPrivate::present(TNode atom) {
 912   return holds(atom) || holds(atom.notNode());
 913 }
 914
 915
 916 bool TheorySetsPrivate::holds(TNode atom, bool polarity) {
 917   Node polarity_atom = NodeManager::currentNM()->mkConst<bool>(polarity);
 918
 919   Node atomModEq = NodeManager::currentNM()->mkNode
 920     (atom.getKind(), d_equalityEngine.getRepresentative(atom[0]),
 921      d_equalityEngine.getRepresentative(atom[1]) );
 922
 923   d_equalityEngine.addTerm(atomModEq);
 924
 925   return d_equalityEngine.areEqual(atomModEq, polarity_atom);
 926 }
 927
 928
 929 void TheorySetsPrivate::registerReason(TNode reason, bool save)
 930 {
 931   if(save) d_nodeSaver.insert(reason);
 932
 933   if(reason.getKind() == kind::AND) {
 934     Assert(reason.getNumChildren() == 2);
 935     registerReason(reason[0], false);
 936     registerReason(reason[1], false);
 937   } else if(reason.getKind() == kind::NOT) {
 938     registerReason(reason[0], false);
 939   } else if(reason.getKind() == kind::MEMBER) {
 940     d_equalityEngine.addTerm(reason);
 941     Assert(present(reason));
 942   } else if(reason.getKind() == kind::EQUAL) {
 943     d_equalityEngine.addTerm(reason);
 944     Assert(present(reason));
 945   } else if(reason.getKind() == kind::CONST_BOOLEAN) {
 946     // That's OK, already in EqEngine
 947   } else {
 948     Unhandled();
 949   }
 950 }
 951
 952 void TheorySetsPrivate::finishPropagation()
 953 {
 954   while(!d_conflict && !d_settermPropagationQueue.empty()) {
 955     std::pair<TNode,TNode> np = d_settermPropagationQueue.front();
 956     d_settermPropagationQueue.pop();
 957     doSettermPropagation(np.first, np.second);
 958   }
 959   while(!d_conflict && !d_propagationQueue.empty()) {
 960     std::pair<Node,Node> np = d_propagationQueue.front();
 961     d_propagationQueue.pop();
 962     TNode atom = np.first.getKind() == kind::NOT ? np.first[0] : np.first;
 963     if(atom.getKind() == kind::MEMBER) {
 964       assertMemebership(np.first, np.second, /* learnt = */ true);
 965     } else {
 966       assertEquality(np.first, np.second, /* learnt = */ true);
 967     }
 968   }
 969 }
 970
 971 void TheorySetsPrivate::addToPending(Node n) {
 972   Debug("sets-pending") << "[sets-pending] addToPending " << n << std::endl;
 973   if(d_pendingEverInserted.find(n) == d_pendingEverInserted.end()) {
 974     if(n.getKind() == kind::MEMBER) {
 975       Debug("sets-pending") << "[sets-pending] \u2514 added to member queue"
 976                             << std::endl;
 977       d_pending.push(n);
 978     } else {
 979       Debug("sets-pending") << "[sets-pending] \u2514 added to equality queue"
 980                             << std::endl;
 981       Assert(n.getKind() == kind::EQUAL);
 982       d_pendingDisequal.push(n);
 983     }
 984     d_external.d_out->lemma(getLemma());
 985     Assert(isComplete());
 986   }
 987 }
 988
 989 bool TheorySetsPrivate::isComplete() {
 990   // while(!d_pending.empty() &&
 991   //       (d_pendingEverInserted.find(d_pending.front()) != d_pendingEverInserted.end()
 992   //        || present(d_pending.front()) ) ) {
 993   //   Debug("sets-pending") << "[sets-pending] removing as already present: "
 994   //                         << d_pending.front() << std::endl;
 995   //   d_pending.pop();
 996   // }
 997   return d_pending.empty() && d_pendingDisequal.empty();
 998 }
 999
1000 Node TheorySetsPrivate::getLemma() {
1001   Assert(!d_pending.empty() || !d_pendingDisequal.empty());
1002
1003   Node n, lemma;
1004
1005   if(!d_pending.empty()) {
1006     n = d_pending.front();
1007     d_pending.pop();
1008     d_pendingEverInserted.insert(n);
1009
1010     Assert(!present(n));
1011     Assert(n.getKind() == kind::MEMBER);
1012
1013     lemma = OR(n, NOT(n));
1014   } else {
1015     n = d_pendingDisequal.front();
1016     d_pendingDisequal.pop();
1017     d_pendingEverInserted.insert(n);
1018
1019     Assert(n.getKind() == kind::EQUAL && n[0].getType().isSet());
1020     Node x = NodeManager::currentNM()->mkSkolem("sde_", n[0].getType().getSetElementType() );
1021     Node l1 = MEMBER(x, n[0]), l2 = MEMBER(x, n[1]);
1022
1023     lemma = OR(n, AND(l1, NOT(l2)), AND(NOT(l1), l2));
1024   }
1025
1026   Debug("sets-lemma") << "[sets-lemma] Generating for " << n << ", lemma: " << lemma << std::endl;
1027
1028   return  lemma;
1029 }
1030
1031
1032 TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
1033                                      context::Context* c,
1034                                      context::UserContext* u):
1035   d_external(external),
1036   d_notify(*this),
1037   d_equalityEngine(d_notify, c, "theory::sets::TheorySetsPrivate"),
1038   d_conflict(c),
1039   d_termInfoManager(NULL),
1040   d_propagationQueue(c),
1041   d_settermPropagationQueue(c),
1042   d_nodeSaver(c),
1043   d_pending(c),
1044   d_pendingDisequal(c),
1045   d_pendingEverInserted(u),
1046   d_modelCache(c),
1047   d_ccg_i(c),
1048   d_ccg_j(c),
1049   d_scrutinize(NULL)
1050 {
1051   d_termInfoManager = new TermInfoManager(*this, c, &d_equalityEngine);
1052
1053   d_equalityEngine.addFunctionKind(kind::UNION);
1054   d_equalityEngine.addFunctionKind(kind::INTERSECTION);
1055   d_equalityEngine.addFunctionKind(kind::SETMINUS);
1056
1057   d_equalityEngine.addFunctionKind(kind::MEMBER);
1058   d_equalityEngine.addFunctionKind(kind::SUBSET);
1059
1060   if( Debug.isOn("sets-scrutinize") ) {
1061     d_scrutinize = new TheorySetsScrutinize(this);
1062   }
1063 }/* TheorySetsPrivate::TheorySetsPrivate() */
1064
1065
1066 TheorySetsPrivate::~TheorySetsPrivate()
1067 {
1068   delete d_termInfoManager;
1069   if( Debug.isOn("sets-scrutinize") ) {
1070     Assert(d_scrutinize != NULL);
1071     delete d_scrutinize;
1072   }
1073 }
1074
1075
1076 bool TheorySetsPrivate::propagate(TNode literal) {
1077   Debug("sets-prop") << " propagate(" << literal  << ")" << std::endl;
1078
1079   // If already in conflict, no more propagation
1080   if (d_conflict) {
1081     Debug("sets-prop") << "TheoryUF::propagate(" << literal << "): already in conflict" << std::endl;
1082     return false;
1083   }
1084
1085   // Propagate out
1086   bool ok = d_external.d_out->propagate(literal);
1087   if (!ok) {
1088     d_conflict = true;
1089   }
1090
1091   return ok;
1092 }/* TheorySetsPropagate::propagate(TNode) */
1093
1094
1095 void TheorySetsPrivate::setMasterEqualityEngine(eq::EqualityEngine* eq) {
1096   d_equalityEngine.setMasterEqualityEngine(eq);
1097 }
1098
1099 void TheorySetsPrivate::conflict(TNode a, TNode b)
1100 {
1101   if (a.getKind() == kind::CONST_BOOLEAN) {
1102     d_conflictNode = explain(a.iffNode(b));
1103   } else {
1104     d_conflictNode = explain(a.eqNode(b));
1105   }
1106   d_external.d_out->conflict(d_conflictNode);
1107   Debug("sets") << "[sets] conflict: " << a << " iff " << b
1108                 << ", explaination " << d_conflictNode << std::endl;
1109   d_conflict = true;
1110 }
1111
1112 Node TheorySetsPrivate::explain(TNode literal)
1113 {
1114   Debug("sets") << "TheorySetsPrivate::explain(" << literal << ")"
1115                 << std::endl;
1116
1117   bool polarity = literal.getKind() != kind::NOT;
1118   TNode atom = polarity ? literal : literal[0];
1119   std::vector<TNode> assumptions;
1120
1121   if(atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
1122     d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
1123   } else if(atom.getKind() == kind::MEMBER) {
1124     if( !d_equalityEngine.hasTerm(atom)) {
1125       d_equalityEngine.addTerm(atom);
1126     }
1127     d_equalityEngine.explainPredicate(atom, polarity, assumptions);
1128   } else {
1129     Debug("sets") << "unhandled: " << literal << "; (" << atom << ", "
1130                   << polarity << "); kind" << atom.getKind() << std::endl;
1131     Unhandled();
1132   }
1133
1134   return mkAnd(assumptions);
1135 }
1136
1137 void TheorySetsPrivate::preRegisterTerm(TNode node)
1138 {
1139   Debug("sets") << "TheorySetsPrivate::preRegisterTerm(" << node << ")"
1140                 << std::endl;
1141
1142   switch(node.getKind()) {
1143   case kind::EQUAL:
1144     // TODO: what's the point of this
1145     d_equalityEngine.addTriggerEquality(node);
1146     break;
1147   case kind::MEMBER:
1148     // TODO: what's the point of this
1149     d_equalityEngine.addTriggerPredicate(node);
1150     break;
1151   default:
1152     d_termInfoManager->addTerm(node);
1153     d_equalityEngine.addTriggerTerm(node, THEORY_SETS);
1154     // d_equalityEngine.addTerm(node);
1155   }
1156   if(node.getKind() == kind::SINGLETON) {
1157     Node true_node = NodeManager::currentNM()->mkConst<bool>(true);
1158     learnLiteral(MEMBER(node[0], node), true, true_node);
1159     //intentional fallthrough
1160   }
1161 }
1162
1163
1164
1165 /**************************** eq::NotifyClass *****************************/
1166 /**************************** eq::NotifyClass *****************************/
1167 /**************************** eq::NotifyClass *****************************/
1168
1169
1170 bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool value)
1171 {
1172   Debug("sets-eq") << "[sets-eq] eqNotifyTriggerEquality: equality = " << equality
1173                    << " value = " << value << std::endl;
1174   if (value) {
1175     return d_theory.propagate(equality);
1176   } else {
1177     // We use only literal triggers so taking not is safe
1178     return d_theory.propagate(equality.notNode());
1179   }
1180 }
1181
1182 bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value)
1183 {
1184   Debug("sets-eq") << "[sets-eq] eqNotifyTriggerPredicate: predicate = " << predicate
1185                    << " value = " << value << std::endl;
1186   if (value) {
1187     return d_theory.propagate(predicate);
1188   } else {
1189     return d_theory.propagate(predicate.notNode());
1190   }
1191 }
1192
1193 bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value)
1194 {
1195   Debug("sets-eq") << "[sets-eq] eqNotifyTriggerTermEquality: tag = " << tag
1196                    << " t1 = " << t1 << "  t2 = " << t2 << "  value = " << value << std::endl;
1197   if(value) {
1198     d_theory.d_termInfoManager->mergeTerms(t1, t2);
1199   }
1200   d_theory.propagate( value ? EQUAL(t1, t2) : NOT(EQUAL(t1, t2)) );
1201   return true;
1202 }
1203
1204 void TheorySetsPrivate::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2)
1205 {
1206   Debug("sets-eq") << "[sets-eq] eqNotifyConstantTermMerge " << " t1 = " << t1 << " t2 = " << t2 << std::endl;
1207   d_theory.conflict(t1, t2);
1208 }
1209
1210 // void TheorySetsPrivate::NotifyClass::eqNotifyNewClass(TNode t)
1211 // {
1212 //   Debug("sets-eq") << "[sets-eq] eqNotifyNewClass:" << " t = " << t << std::endl;
1213 // }
1214
1215 // void TheorySetsPrivate::NotifyClass::eqNotifyPreMerge(TNode t1, TNode t2)
1216 // {
1217 //   Debug("sets-eq") << "[sets-eq] eqNotifyPreMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl;
1218 // }
1219
1220 // void TheorySetsPrivate::NotifyClass::eqNotifyPostMerge(TNode t1, TNode t2)
1221 // {
1222 //   Debug("sets-eq") << "[sets-eq] eqNotifyPostMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl;
1223 // }
1224
1225 // void TheorySetsPrivate::NotifyClass::eqNotifyDisequal(TNode t1, TNode t2, TNode reason)
1226 // {
1227 //   Debug("sets-eq") << "[sets-eq] eqNotifyDisequal:" << " t1 = " << t1 << " t2 = " << t2 << " reason = " << reason << std::endl;
1228 // }
1229
1230
1231 /**************************** TermInfoManager *****************************/
1232 /**************************** TermInfoManager *****************************/
1233 /**************************** TermInfoManager *****************************/
1234
1235 void TheorySetsPrivate::TermInfoManager::mergeLists
1236 (CDTNodeList* la, const CDTNodeList* lb) const {
1237   // straight from theory/arrays/array_info.cpp
1238   std::set<TNode> temp;
1239   CDTNodeList::const_iterator it;
1240   for(it = la->begin() ; it != la->end(); it++ ) {
1241     temp.insert((*it));
1242   }
1243
1244   for(it = lb->begin() ; it!= lb->end(); it++ ) {
1245     if(temp.count(*it) == 0) {
1246       la->push_back(*it);
1247     }
1248   }
1249 }
1250
1251 TheorySetsPrivate::TermInfoManager::TermInfoManager
1252 (TheorySetsPrivate& theory, context::Context* satContext, eq::EqualityEngine* eq):
1253   d_theory(theory),
1254   d_context(satContext),
1255   d_eqEngine(eq),
1256   d_terms(satContext),
1257   d_info()
1258 { }
1259
1260 TheorySetsPrivate::TermInfoManager::~TermInfoManager() {
1261   for( typeof(d_info.begin()) it = d_info.begin();
1262        it != d_info.end(); ++it) {
1263     delete (*it).second;
1264   }
1265 }
1266
1267 void TheorySetsPrivate::TermInfoManager::notifyMembership(TNode fact) {
1268   bool polarity = fact.getKind() != kind::NOT;
1269   TNode atom = polarity ? fact : fact[0];
1270
1271   TNode x = d_eqEngine->getRepresentative(atom[0]);
1272   TNode S = d_eqEngine->getRepresentative(atom[1]);
1273
1274   Debug("sets-terminfo") << "[sets-terminfo] Adding membership " << x
1275                          << " in " << S << " " << polarity << std::endl;
1276
1277   d_info[S]->addToElementList(x, polarity);
1278   d_info[x]->addToSetList(S, polarity);
1279
1280   d_theory.d_modelCache.clear();
1281 }
1282
1283 const CDTNodeList* TheorySetsPrivate::TermInfoManager::getParents(TNode x) {
1284   return d_info[x]->parents;
1285 }
1286
1287 const CDTNodeList* TheorySetsPrivate::TermInfoManager::getMembers(TNode S) {
1288   return d_info[S]->elementsInThisSet;
1289 }
1290
1291 const CDTNodeList* TheorySetsPrivate::TermInfoManager::getNonMembers(TNode S) {
1292   return d_info[S]->elementsNotInThisSet;
1293 }
1294
1295 void TheorySetsPrivate::TermInfoManager::addTerm(TNode n) {
1296   unsigned numChild = n.getNumChildren();
1297
1298   if(!d_terms.contains(n)) {
1299     d_terms.insert(n);
1300     d_info[n] = new TheorySetsTermInfo(d_context);
1301   }
1302
1303   if(n.getKind() == kind::UNION ||
1304      n.getKind() == kind::INTERSECTION ||
1305      n.getKind() == kind::SETMINUS) {
1306
1307     for(unsigned i = 0; i < numChild; ++i) {
1308       if(d_terms.contains(n[i])) {
1309         Debug("sets-parent") << "Adding " << n << " to parent list of "
1310                              << n[i] << std::endl;
1311         d_info[n[i]]->parents->push_back(n);
1312       }
1313     }
1314
1315   }
1316 }
1317
1318 void TheorySetsPrivate::TermInfoManager::pushToSettermPropagationQueue
1319 (TNode x, TNode S, bool polarity)
1320 {
1321   Node cur_atom = MEMBER(x, S);
1322
1323   // propagation : empty set
1324   if(polarity && S.getKind() == kind::EMPTYSET) {
1325     Debug("sets-prop") << "[sets-prop]  something in empty set? conflict."
1326                        << std::endl;
1327     d_theory.learnLiteral(cur_atom, false, cur_atom);
1328     return;
1329   }// propagation: empty set
1330
1331   // propagation : children
1332   if(S.getKind() == kind::UNION ||
1333      S.getKind() == kind::INTERSECTION ||
1334      S.getKind() == kind::SETMINUS ||
1335      S.getKind() == kind::SINGLETON) {
1336     d_theory.d_settermPropagationQueue.push_back(std::make_pair(x, S));
1337   }// propagation: children
1338
1339   // propagation : parents
1340   const CDTNodeList* parentList = getParents(S);
1341   for(typeof(parentList->begin()) k = parentList->begin();
1342       k != parentList->end(); ++k) {
1343     d_theory.d_settermPropagationQueue.push_back(std::make_pair(x, *k));
1344   }// propagation : parents
1345
1346 }
1347
1348 void TheorySetsPrivate::TermInfoManager::pushToSettermPropagationQueue
1349 (TNode x, CDTNodeList* l, bool polarity)
1350 {
1351   set<TNode> alreadyProcessed;
1352
1353   BOOST_FOREACH(TNode S, (*l) ) {
1354     Debug("sets-prop") << "[sets-terminfo]  setterm todo: "
1355                        << MEMBER(x, d_eqEngine->getRepresentative(S))
1356                        << std::endl;
1357
1358     TNode repS = d_eqEngine->getRepresentative(S);
1359     if(alreadyProcessed.find(repS) != alreadyProcessed.end()) {
1360       continue;
1361     } else {
1362       alreadyProcessed.insert(repS);
1363     }
1364
1365     d_eqEngine->addTerm(MEMBER(d_eqEngine->getRepresentative(x), repS));
1366
1367     for(eq::EqClassIterator j(d_eqEngine->getRepresentative(S), d_eqEngine);
1368         !j.isFinished(); ++j) {
1369
1370       pushToSettermPropagationQueue(x, *j, polarity);
1371
1372     }//j loop
1373   }
1374 }
1375
1376 void TheorySetsPrivate::TermInfoManager::pushToSettermPropagationQueue
1377 (CDTNodeList* l, TNode S, bool polarity)
1378 {
1379   BOOST_FOREACH(TNode x, (*l) ) {
1380     Debug("sets-prop") << "[sets-terminfo]  setterm todo: "
1381                        << MEMBER(x, d_eqEngine->getRepresentative(S))
1382                        << std::endl;
1383
1384     d_eqEngine->addTerm(MEMBER(d_eqEngine->getRepresentative(x),
1385                                d_eqEngine->getRepresentative(S)));
1386
1387     for(eq::EqClassIterator j(d_eqEngine->getRepresentative(S), d_eqEngine);
1388         !j.isFinished(); ++j) {
1389
1390       pushToSettermPropagationQueue(x, *j, polarity);
1391
1392     }//j loop
1393
1394   }
1395
1396 }
1397
1398
1399
1400 void TheorySetsPrivate::TermInfoManager::mergeTerms(TNode a, TNode b) {
1401   // merge b into a
1402   Debug("sets-terminfo") << "[sets-terminfo] Merging (into) a = " << a
1403                          << ", b = " << b << std::endl;
1404   Debug("sets-terminfo") << "[sets-terminfo] reps"
1405                          << ", a: " << d_eqEngine->getRepresentative(a)
1406                          << ", b: " << d_eqEngine->getRepresentative(b)
1407                          << std::endl;
1408
1409   typeof(d_info.begin()) ita = d_info.find(a);
1410   typeof(d_info.begin()) itb = d_info.find(b);
1411
1412   Assert(ita != d_info.end());
1413   Assert(itb != d_info.end());
1414
1415   /* elements in this sets */
1416   pushToSettermPropagationQueue( (*ita).second->elementsInThisSet, b, true );
1417   pushToSettermPropagationQueue( (*ita).second->elementsNotInThisSet, b, false );
1418   pushToSettermPropagationQueue( (*itb).second->elementsNotInThisSet, a, false );
1419   pushToSettermPropagationQueue( (*itb).second->elementsInThisSet, a, true );
1420   mergeLists((*ita).second->elementsInThisSet,
1421              (*itb).second->elementsInThisSet);
1422   mergeLists((*ita).second->elementsNotInThisSet,
1423              (*itb).second->elementsNotInThisSet);
1424
1425   /* sets containing this element */
1426   // pushToSettermPropagationQueue( b, (*ita).second->setsContainingThisElement, true);
1427   // pushToSettermPropagationQueue( b, (*ita).second->setsNotContainingThisElement, false);
1428   pushToSettermPropagationQueue( a, (*itb).second->setsNotContainingThisElement, false);
1429   pushToSettermPropagationQueue( a, (*itb).second->setsContainingThisElement, true);
1430   mergeLists( (*ita).second->setsContainingThisElement,
1431               (*itb).second->setsContainingThisElement );
1432   mergeLists( (*ita).second->setsNotContainingThisElement,
1433               (*itb).second->setsNotContainingThisElement );
1434
1435   d_theory.d_modelCache.clear();
1436 }
1437
1438 Node TheorySetsPrivate::TermInfoManager::getModelValue(TNode n)
1439 {
1440   Assert(n.getType().isSet());
1441   set<Node> elements, elements_const;
1442   Node S = d_eqEngine->getRepresentative(n);
1443   typeof(d_theory.d_modelCache.begin()) it = d_theory.d_modelCache.find(S);
1444   if(it != d_theory.d_modelCache.end()) {
1445     return (*it).second;
1446   }
1447   const CDTNodeList* l = getMembers(S);
1448   for(typeof(l->begin()) it = l->begin(); it != l->end(); ++it) {
1449     TNode n = *it;
1450     elements.insert(d_eqEngine->getRepresentative(n));
1451   }
1452   BOOST_FOREACH(TNode e, elements) {
1453     if(e.isConst()) {
1454       elements_const.insert(e);
1455     } else {
1456       elements_const.insert(d_theory.d_external.d_valuation.getModelValue(e));
1457     }
1458   }
1459   Node v = d_theory.elementsToShape(elements_const, n.getType());
1460   d_theory.d_modelCache[n] = v;
1461   return v;
1462 }
1463
1464 }/* CVC4::theory::sets namespace */
1465 }/* CVC4::theory namespace */
1466 }/* CVC4 namespace */