src/theory/sets/theory_sets_private.cpp

   1 /*********************                                                        */
   2 /*! \file theory_sets_private.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Kshitij Bansal, Tim King, Andrew Reynolds
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Sets theory implementation.
  13  **
  14  ** Sets theory implementation.
  15  **/
  16
  17 #include <algorithm>
  18 #include "theory/sets/theory_sets_private.h"
  19
  20 #include <boost/foreach.hpp>
  21
  22 #include "expr/emptyset.h"
  23 #include "options/sets_options.h"
  24 #include "smt/smt_statistics_registry.h"
  25 #include "theory/sets/expr_patterns.h" // ONLY included here
  26 #include "theory/sets/scrutinize.h"
  27 #include "theory/sets/theory_sets.h"
  28 #include "theory/theory_model.h"
  29 #include "util/result.h"
  30
  31 using namespace std;
  32 using namespace CVC4::expr::pattern;
  33
  34 namespace CVC4 {
  35 namespace theory {
  36 namespace sets {
  37
  38 const char* element_of_str = " \u2208 ";
  39
  40 // Declaration of functions defined later in this CPP file
  41 const std::set<TNode> getLeaves(map<TNode, set<TNode> >& edges, TNode node);
  42
  43 /**************************** TheorySetsPrivate *****************************/
  44 /**************************** TheorySetsPrivate *****************************/
  45 /**************************** TheorySetsPrivate *****************************/
  46
  47 void TheorySetsPrivate::check(Theory::Effort level) {
  48   d_newLemmaGenerated = false;
  49   while(!d_external.done() && !d_conflict) {
  50     // Get all the assertions
  51     Assertion assertion = d_external.get();
  52     TNode fact = assertion.assertion;
  53
  54     Debug("sets") << "\n\n[sets] TheorySetsPrivate::check(): processing "
  55                   << fact << std::endl;
  56
  57     bool polarity = fact.getKind() != kind::NOT;
  58     TNode atom = polarity ? fact : fact[0];
  59
  60     if (!assertion.isPreregistered) {
  61       if (atom.getKind() == kind::EQUAL) {
  62         if (!d_equalityEngine.hasTerm(atom[0])) {
  63           Assert(atom[0].isConst());
  64           d_equalityEngine.addTerm(atom[0]);
  65           d_termInfoManager->addTerm(atom[0]);
  66         }
  67         if (!d_equalityEngine.hasTerm(atom[1])) {
  68           Assert(atom[1].isConst());
  69           d_equalityEngine.addTerm(atom[1]);
  70           d_termInfoManager->addTerm(atom[1]);
  71         }
  72       }
  73     }
  74
  75     // Solve each
  76     switch(atom.getKind()) {
  77     case kind::EQUAL:
  78       Debug("sets") << atom[0] << " should " << (polarity ? "":"NOT ")
  79                     << "be equal to " << atom[1] << std::endl;
  80       assertEquality(fact, fact, /* learnt = */ false);
  81       break;
  82
  83     case kind::MEMBER:
  84       Debug("sets") << atom[0] << " should " << (polarity ? "":"NOT ")
  85                     << "be in " << atom[1] << std::endl;
  86       assertMemebership(fact, fact, /* learnt = */ false);
  87       break;
  88
  89     default:
  90       Unhandled(fact.getKind());
  91     }
  92     finishPropagation();
  93
  94     Debug("sets") << "[sets]  in conflict = " << d_conflict << std::endl;
  95     // Assert( d_conflict ^ d_equalityEngine.consistent() );
  96     // ^ doesn't hold when we propagate equality/disequality between shared terms
  97     // and that leads to conflict (externally).
  98     if(d_conflict) { return; }
  99     Debug("sets") << "[sets]  is complete = " << isComplete() << std::endl;
 100   }
 101
 102   if( (level == Theory::EFFORT_FULL || options::setsEagerLemmas() ) && !isComplete()) {
 103     lemma(getLemma(), SETS_LEMMA_OTHER);
 104     return;
 105   }
 106
 107   //processCard(level);
 108
 109   processCard2(level);
 110
 111   // if we are here, there is no conflict and we are complete
 112   if(Debug.isOn("sets-scrutinize")) { d_scrutinize->postCheckInvariants(); }
 113
 114   return;
 115 }/* TheorySetsPrivate::check() */
 116
 117
 118 void TheorySetsPrivate::assertEquality(TNode fact, TNode reason, bool learnt)
 119 {
 120   Debug("sets-assert") << "\n[sets-assert] adding equality: " << fact
 121                        << ", " << reason
 122                        << ", " << learnt << std::endl;
 123
 124   bool polarity = fact.getKind() != kind::NOT;
 125   TNode atom = polarity ? fact : fact[0];
 126
 127   // fact already holds
 128   if( holds(atom, polarity) ) {
 129     Debug("sets-assert") << "[sets-assert]   already present, skipping" << std::endl;
 130     return;
 131   }
 132
 133   // assert fact & check for conflict
 134   if(learnt) {
 135     registerReason(reason, /*save=*/ true);
 136   }
 137   d_equalityEngine.assertEquality(atom, polarity, reason);
 138
 139   if(!d_equalityEngine.consistent()) {
 140     Debug("sets-assert") << "[sets-assert]   running into a conflict" << std::endl;
 141     d_conflict = true;
 142     return;
 143   }
 144
 145   if(atom[0].getKind() == kind::CARD && isCardVar(atom[0])) {
 146     NodeManager* nm = NodeManager::currentNM();
 147     Node emptySet = nm->mkConst<EmptySet>(EmptySet(nm->toType(atom[0].getType())));
 148     Node newFact = nm->mkNode(kind::EQUAL, getCardVar(atom[0]), emptySet);
 149     if(!polarity) newFact = nm->mkNode(kind::NOT, newFact);
 150     learnLiteral(newFact, fact);
 151   }
 152
 153   // disequality lemma
 154   if(!polarity && atom[0].getType().isSet()) {
 155     addToPending(atom);
 156   }
 157
 158   // for cardinality
 159   if(polarity && atom[0].getType().isSet()) {
 160     d_graphMergesPending.push(make_pair(atom[0], atom[1]));
 161   }
 162 }/* TheorySetsPrivate::assertEquality() */
 163
 164
 165 void TheorySetsPrivate::assertMemebership(TNode fact, TNode reason, bool learnt)
 166 {
 167   Debug("sets-assert") << "\n[sets-assert] adding membership: " << fact
 168                        << ", " << reason
 169                        << ", " << learnt << std::endl;
 170
 171   bool polarity = fact.getKind() == kind::NOT ? false : true;
 172   TNode atom = polarity ? fact : fact[0];
 173
 174   // fact already holds
 175   if( holds(atom, polarity) ) {
 176     Debug("sets-assert") << "[sets-assert]   already present, skipping" << std::endl;
 177     return;
 178   }
 179
 180   // assert fact & check for conflict
 181   if(learnt) {
 182     registerReason(reason, true);
 183   }
 184   d_equalityEngine.assertPredicate(atom, polarity, reason);
 185
 186   if(!d_equalityEngine.consistent()) {
 187     Debug("sets-assert") << "[sets-assert]   running into a conflict" << std::endl;
 188     d_conflict = true;
 189     return;
 190   }
 191
 192   // update term info data structures
 193   d_termInfoManager->notifyMembership(fact);
 194
 195   // propagation
 196   TNode x = d_equalityEngine.getRepresentative(atom[0]);
 197   eq::EqClassIterator j(d_equalityEngine.getRepresentative(atom[1]),
 198                         &d_equalityEngine);
 199   TNode S = (*j);
 200   Node cur_atom = MEMBER(x, S);
 201
 202   /**
 203    * It is sufficient to do emptyset propagation outside the loop as
 204    * constant term is guaranteed to be class representative.
 205    */
 206   if(polarity && S.getKind() == kind::EMPTYSET) {
 207     Debug("sets-prop") << "[sets-prop]  something in empty set? conflict."
 208                        << std::endl;
 209     learnLiteral(cur_atom, false, cur_atom);
 210     Assert(d_conflict);
 211     return;
 212   }
 213
 214   /**
 215    * Disequality propagation if element type is set
 216    */
 217   if(x.getType().isSet()) {
 218     if(polarity) {
 219       const CDTNodeList* l = d_termInfoManager->getNonMembers(S);
 220       for(typeof(l->begin()) it = l->begin(); it != l->end(); ++it) {
 221         TNode n = *it;
 222         learnLiteral( /* atom = */ EQUAL(x, n),
 223                       /* polarity = */ false,
 224                       /* reason = */ AND( MEMBER(x, S), NOT( MEMBER(n, S)) ) );
 225       }
 226     } else {
 227       const CDTNodeList* l = d_termInfoManager->getMembers(S);
 228       for(typeof(l->begin()) it = l->begin(); it != l->end(); ++it) {
 229         TNode n = *it;
 230         learnLiteral( /* atom = */ EQUAL(x, n),
 231                       /* polarity = */ false,
 232                       /* reason = */ AND( NOT(MEMBER(x, S)), MEMBER(n, S)) );
 233       }
 234     }
 235   }
 236
 237   for(; !j.isFinished(); ++j) {
 238     TNode S = (*j);
 239     Node cur_atom = MEMBER(x, S);
 240
 241     // propagation : children
 242     Debug("sets-prop") << "[sets-prop] Propagating 'down' for "
 243                        << x << element_of_str << S << std::endl;
 244     if(S.getKind() == kind::UNION ||
 245        S.getKind() == kind::INTERSECTION ||
 246        S.getKind() == kind::SETMINUS ||
 247        S.getKind() == kind::SINGLETON) {
 248       doSettermPropagation(x, S);
 249       if(d_conflict) return;
 250     }// propagation: children
 251
 252
 253     // propagation : parents
 254     Debug("sets-prop") << "[sets-prop] Propagating 'up' for "
 255                        << x << element_of_str << S << std::endl;
 256     const CDTNodeList* parentList = d_termInfoManager->getParents(S);
 257     for(typeof(parentList->begin()) k = parentList->begin();
 258         k != parentList->end(); ++k) {
 259       doSettermPropagation(x, *k);
 260       if(d_conflict) return;
 261     }// propagation : parents
 262
 263
 264   }//j loop
 265
 266 }/* TheorySetsPrivate::assertMemebership() */
 267
 268
 269 void TheorySetsPrivate::doSettermPropagation(TNode x, TNode S)
 270 {
 271   Debug("sets-prop") << "[sets-prop] doSettermPropagation("
 272                      << x << ", " << S << std::endl;
 273
 274   Assert(S.getType().isSet() && S.getType().getSetElementType() == x.getType(),
 275          ( std::string("types of S and x are ") + S.getType().toString() +
 276            std::string(" and ") + x.getType().toString() +
 277            std::string(" respectively") ).c_str()  );
 278
 279   Node literal, left_literal, right_literal;
 280
 281   // axiom: literal <=> left_literal AND right_literal
 282   switch(S.getKind()) {
 283   case kind::INTERSECTION:
 284     literal       =       MEMBER(x, S)      ;
 285     left_literal  =       MEMBER(x, S[0])   ;
 286     right_literal =       MEMBER(x, S[1])   ;
 287     break;
 288   case kind::UNION:
 289     literal       = NOT(  MEMBER(x, S)     );
 290     left_literal  = NOT(  MEMBER(x, S[0])  );
 291     right_literal = NOT(  MEMBER(x, S[1])  );
 292     break;
 293   case kind::SETMINUS:
 294     literal       =       MEMBER(x, S)      ;
 295     left_literal  =       MEMBER(x, S[0])   ;
 296     right_literal = NOT(  MEMBER(x, S[1])  );
 297     break;
 298   case kind::SINGLETON: {
 299     Node atom = MEMBER(x, S);
 300     if(holds(atom, true)) {
 301       learnLiteral(EQUAL(x, S[0]), true, atom);
 302     } else if(holds(atom, false)) {
 303       learnLiteral(EQUAL(x, S[0]), false, NOT(atom));
 304     }
 305     return;
 306   }
 307   default:
 308     Unhandled();
 309   }
 310
 311   Debug("sets-prop-details")
 312     << "[sets-prop-details]   " << literal << " IFF " << left_literal
 313     << " AND " << right_literal << std::endl;
 314
 315   Debug("sets-prop-details")
 316     << "[sets-prop-details]   "
 317     << (holds(literal) ? "yes" : (holds(literal.negate()) ? " no" : " _ "))
 318     << " IFF "
 319     << (holds(left_literal) ? "yes" : (holds(left_literal.negate()) ? "no " : " _ "))
 320     << " AND "
 321     << (holds(right_literal) ? "yes" : (holds(right_literal.negate()) ? "no " : " _ "))
 322     << std::endl;
 323
 324   Assert( present( MEMBER(x, S)    ) ||
 325           present( MEMBER(x, S[0]) ) ||
 326           present( MEMBER(x, S[1]) ) );
 327
 328   if( holds(literal) ) {
 329     // 1a. literal => left_literal
 330     Debug("sets-prop") << "[sets-prop]  ... via case 1a. ..." << std::endl;
 331     learnLiteral(left_literal, literal);
 332     if(d_conflict) return;
 333
 334     // 1b. literal => right_literal
 335     Debug("sets-prop") << "[sets-prop]  ... via case 1b. ..." << std::endl;
 336     learnLiteral(right_literal, literal);
 337     if(d_conflict) return;
 338
 339     // subsumption requirement met, exit
 340     return;
 341   }
 342   else if( holds(literal.negate() ) ) {
 343     // 4. neg(literal), left_literal => neg(right_literal)
 344     if( holds(left_literal) ) {
 345       Debug("sets-prop") << "[sets-prop]  ... via case 4. ..." << std::endl;
 346       learnLiteral(right_literal.negate(), AND( literal.negate(),
 347                                                 left_literal) );
 348       if(d_conflict) return;
 349     }
 350
 351     // 5. neg(literal), right_literal => neg(left_literal)
 352     if( holds(right_literal) ) {
 353       Debug("sets-prop") << "[sets-prop]  ... via case 5. ..." << std::endl;
 354       learnLiteral(left_literal.negate(), AND( literal.negate(),
 355                                                right_literal) );
 356       if(d_conflict) return;
 357     }
 358   }
 359   else {
 360     // 2,3. neg(left_literal) v neg(right_literal) => neg(literal)
 361     if(holds(left_literal.negate())) {
 362       Debug("sets-prop") << "[sets-prop]  ... via case 2. ..." << std::endl;
 363       learnLiteral(literal.negate(), left_literal.negate());
 364       if(d_conflict) return;
 365     }
 366     else if(holds(right_literal.negate())) {
 367       Debug("sets-prop") << "[sets-prop]  ... via case 3. ..." << std::endl;
 368       learnLiteral(literal.negate(), right_literal.negate());
 369       if(d_conflict) return;
 370     }
 371
 372     // 6. the axiom itself:
 373     else if(holds(left_literal) && holds(right_literal)) {
 374       Debug("sets-prop") << "[sets-prop]  ... via case 6. ..." << std::endl;
 375       learnLiteral(literal, AND(left_literal, right_literal) );
 376       if(d_conflict) return;
 377     }
 378   }
 379
 380   // check fulfilling rule
 381   Node n;
 382   switch(S.getKind()) {
 383   case kind::UNION:
 384     if( holds(MEMBER(x, S)) &&
 385         !present( MEMBER(x, S[0]) ) )
 386       addToPending( MEMBER(x, S[0]) );
 387     break;
 388   case kind::SETMINUS: // intentional fallthrough
 389     if( holds(MEMBER(x, S[0])) &&
 390         !present( MEMBER(x, S[1]) ))
 391       addToPending( MEMBER(x, S[1]) );
 392     break;
 393   case kind::INTERSECTION:
 394     return;
 395   default:
 396     Assert(false, "MembershipEngine::doSettermPropagation");
 397   }
 398 }
 399
 400
 401 void TheorySetsPrivate::learnLiteral(TNode atom, bool polarity, Node reason) {
 402   Debug("sets-learn") << "[sets-learn] learnLiteral(" << atom
 403                       << ", " << polarity << ")" << std::endl;
 404
 405   if( holds(atom, polarity) ) {
 406     Debug("sets-learn") << "[sets-learn] \u2514 already known, skipping" << std::endl;
 407     return;
 408   }
 409
 410   if( holds(atom, !polarity) ) {
 411     Debug("sets-learn") << "[sets-learn] \u2514 conflict found" << std::endl;
 412
 413     registerReason(reason, /*save=*/ true);
 414
 415     if(atom.getKind() == kind::EQUAL) {
 416       d_equalityEngine.assertEquality(atom, polarity, reason);
 417     } else {
 418       d_equalityEngine.assertPredicate(atom, polarity, reason);
 419     }
 420     Assert(d_conflict);       // should be marked due to equality engine
 421     return;
 422   }
 423
 424   Assert(atom.getKind() == kind::EQUAL || atom.getKind() == kind::MEMBER);
 425
 426   Node learnt_literal = polarity ? Node(atom) : NOT(atom);
 427   d_propagationQueue.push_back( make_pair(learnt_literal, reason) );
 428 }/*TheorySetsPrivate::learnLiteral(...)*/
 429
 430
 431 /************************ CardVar ************************/
 432
 433 Node TheorySetsPrivate::getCardVar(TNode n) {
 434   NodeNodeHashMap::iterator it = d_setTermToCardVar.find(n);
 435   if(it == d_setTermToCardVar.end()) {
 436     return it->second;
 437   } else {
 438     NodeManager* nm = NodeManager::currentNM();
 439     Node cardVar = nm->mkSkolem("scv_",  n.getType());
 440     d_setTermToCardVar[n] = cardVar;
 441     d_cardVarToSetTerm[cardVar] = n;
 442     return cardVar;
 443   }
 444 }
 445
 446 Node TheorySetsPrivate::newCardVar(TNode n) {
 447   NodeNodeHashMap::iterator it = d_cardVarToSetTerm.find(n);
 448   Assert(it != d_cardVarToSetTerm.end());
 449   return it->second;
 450 }
 451
 452 bool TheorySetsPrivate::isCardVar(TNode n) {
 453   NodeNodeHashMap::iterator it = d_cardVarToSetTerm.find(n);
 454   return it != d_cardVarToSetTerm.end();
 455 }
 456
 457
 458 /************************ Sharing ************************/
 459 /************************ Sharing ************************/
 460 /************************ Sharing ************************/
 461
 462 void TheorySetsPrivate::addSharedTerm(TNode n) {
 463   Debug("sets") << "[sets] ThoerySetsPrivate::addSharedTerm( " << n << ")" << std::endl;
 464   d_termInfoManager->addTerm(n);
 465   d_equalityEngine.addTriggerTerm(n, THEORY_SETS);
 466 }
 467
 468 void TheorySetsPrivate::dumpAssertionsHumanified() const
 469 {
 470     std::string tag = "sets-assertions";
 471
 472     if(Trace.isOn(tag)) { /* condition can't be !Trace.isOn, that's why this empty block */ }
 473     else { return; }
 474
 475     context::CDList<Assertion>::const_iterator it = d_external.facts_begin(), it_end = d_external.facts_end();
 476
 477     std::map<TNode, std::set<TNode> > equalities;
 478     std::set< pair<TNode, TNode> > disequalities;
 479     std::map<TNode, std::pair<std::set<TNode>, std::set<TNode> > > members;
 480     static std::map<TNode, int> numbering;
 481     static int number = 0;
 482
 483     for (unsigned i = 0; it != it_end; ++ it, ++i) {
 484       TNode ass = (*it).assertion;
 485       // Trace("sets-care-dump") << AssertCommand(ass.toExpr()) << endl;
 486       bool polarity = ass.getKind() != kind::NOT;
 487       ass = polarity ? ass : ass[0];
 488       Assert( ass.getNumChildren() == 2);
 489       TNode left = d_equalityEngine.getRepresentative(ass[0]);
 490       TNode right = d_equalityEngine.getRepresentative(ass[1]);
 491       if(numbering[left] == 0) numbering[left] = ++number;
 492       if(numbering[right] == 0) numbering[right] = ++number;
 493       equalities[left].insert(ass[0]);
 494       equalities[right].insert(ass[1]);
 495       if(ass.getKind() == kind::EQUAL) {
 496         if(polarity) {
 497           Assert(left == right);
 498         } else {
 499           if(left > right) std::swap(left, right);
 500           disequalities.insert(make_pair(left, right));
 501         }
 502       } else if(ass.getKind() == kind::MEMBER) {
 503         (polarity ? members[right].first : members[right].second).insert(left);
 504       }
 505     }
 506 #define FORIT(it, container) for(typeof((container).begin()) it=(container).begin(); (it) != (container).end(); ++(it))
 507     FORIT(kt, equalities) {
 508       Trace(tag) << " Eq class of t" << numbering[(*kt).first] << ": " << std::endl;
 509       FORIT(jt, (*kt).second) {
 510         TNode S = (*jt);
 511         if( S.getKind() != kind::UNION && S.getKind() != kind::INTERSECTION && S.getKind() != kind::SETMINUS) {
 512           Trace(tag) << "    " << *jt << ((*jt).getType().isSet() ? "\n": " ");
 513         } else {
 514           Trace(tag) << "    ";
 515           if(S[0].isConst() || numbering.find(d_equalityEngine.getRepresentative(S[0])) == numbering.end()) {
 516             Trace(tag) << S[0];
 517           } else {
 518             Trace(tag) << "t" << numbering[d_equalityEngine.getRepresentative(S[0])];
 519           }
 520           Trace(tag) << " " << (S.getKind() == kind::UNION ? "|" : (S.getKind() == kind::INTERSECTION ? "&" : "-")) << " ";
 521           if(S[1].isConst() || numbering.find(d_equalityEngine.getRepresentative(S[1])) == numbering.end()) {
 522             Trace(tag) << S[1];
 523           } else {
 524             Trace(tag) << "t" << numbering[d_equalityEngine.getRepresentative(S[1])];
 525           }
 526           Trace(tag) << std::endl;
 527         }
 528       }
 529       Trace(tag) << std::endl;
 530     }
 531     FORIT(kt, disequalities) Trace(tag) << "NOT(t"<<numbering[(*kt).first]<<" = t" <<numbering[(*kt).second] <<")"<< std::endl;
 532     FORIT(kt, members) {
 533       if( (*kt).second.first.size() > 0) {
 534         Trace(tag) << "IN t" << numbering[(*kt).first] << ": ";
 535         FORIT(jt, (*kt).second.first) {
 536           TNode x = (*jt);
 537           if(x.isConst() || numbering.find(d_equalityEngine.getRepresentative(x)) == numbering.end()) {
 538             Trace(tag) << x << ", ";
 539           } else {
 540             Trace(tag) << "t" << numbering[d_equalityEngine.getRepresentative(x)] << ", ";
 541           }
 542         }
 543         Trace(tag) << std::endl;
 544       }
 545       if( (*kt).second.second.size() > 0) {
 546         Trace(tag) << "NOT IN t" << numbering[(*kt).first] << ": ";
 547         FORIT(jt, (*kt).second.second) {
 548           TNode x = (*jt);
 549           if(x.isConst() || numbering.find(d_equalityEngine.getRepresentative(x)) == numbering.end()) {
 550             Trace(tag) << x << ", ";
 551           } else {
 552             Trace(tag) << "t" << numbering[d_equalityEngine.getRepresentative(x)] << ", ";
 553           }
 554         }
 555         Trace(tag) << std::endl;
 556       }
 557     }
 558     Trace(tag) << std::endl;
 559 #undef FORIT
 560 }
 561
 562 void TheorySetsPrivate::computeCareGraph() {
 563   Debug("sharing") << "Theory::computeCareGraph<" << d_external.identify() << ">()" << endl;
 564
 565   if(Trace.isOn("sets-assertions")) {
 566     // dump our understanding of assertions
 567     dumpAssertionsHumanified();
 568   }
 569
 570   CVC4_UNUSED unsigned edgesAddedCnt = 0;
 571
 572   unsigned i_st = 0;
 573   if(options::setsCare1()) { i_st = d_ccg_i; }
 574   for (unsigned i = i_st; i < d_external.d_sharedTerms.size(); ++ i) {
 575     TNode a = d_external.d_sharedTerms[i];
 576     TypeNode aType = a.getType();
 577
 578     unsigned j_st = i + 1;
 579     if(options::setsCare1()) { if(i == d_ccg_i) j_st = d_ccg_j + 1; }
 580
 581     for (unsigned j = j_st; j < d_external.d_sharedTerms.size(); ++ j) {
 582       TNode b = d_external.d_sharedTerms[j];
 583       if (b.getType() != aType) {
 584         // We don't care about the terms of different types
 585         continue;
 586       }
 587
 588       switch (d_external.d_valuation.getEqualityStatus(a, b)) {
 589       case EQUALITY_TRUE_AND_PROPAGATED:
 590         // If we know about it, we should have propagated it, so we can skip
 591         Trace("sets-care") << "[sets-care] Know: " << EQUAL(a, b) << std::endl;
 592         break;
 593       case EQUALITY_FALSE_AND_PROPAGATED:
 594         // If we know about it, we should have propagated it, so we can skip
 595         Trace("sets-care") << "[sets-care] Know: " << NOT(EQUAL(a, b)) << std::endl;
 596         break;
 597       case EQUALITY_FALSE:
 598       case EQUALITY_TRUE:
 599         Assert(false, "ERROR: Equality status true/false but not propagated (sets care graph computation).");
 600         break;
 601       case EQUALITY_TRUE_IN_MODEL:
 602         d_external.addCarePair(a, b);
 603         if(Trace.isOn("sharing")) {
 604           ++edgesAddedCnt;
 605         }
 606         if(Debug.isOn("sets-care")) {
 607           Debug("sets-care") << "[sets-care] Requesting split between" << a << " and "
 608                              << b << "." << std::endl << "[sets-care] "
 609                              << "  Both current have value "
 610                              << d_external.d_valuation.getModelValue(a) << std::endl;
 611         }
 612       case EQUALITY_FALSE_IN_MODEL:
 613         if(Trace.isOn("sets-care-performance-test")) {
 614           // TODO: delete these lines, only for performance testing for now
 615           d_external.addCarePair(a, b);
 616         }
 617         break;
 618       case EQUALITY_UNKNOWN:
 619         // Let's split on it
 620         d_external.addCarePair(a, b);
 621         if(options::setsCare1()) {
 622           d_ccg_i = i;
 623           d_ccg_j = j;
 624           return;
 625         }
 626         break;
 627       default:
 628         Unreachable();
 629       }
 630     }
 631   }
 632   Trace("sharing") << "TheorySetsPrivate::computeCareGraph(): size = " << edgesAddedCnt << std::endl;
 633 }
 634
 635 EqualityStatus TheorySetsPrivate::getEqualityStatus(TNode a, TNode b) {
 636   Assert(d_equalityEngine.hasTerm(a) && d_equalityEngine.hasTerm(b));
 637   if (d_equalityEngine.areEqual(a, b)) {
 638     // The terms are implied to be equal
 639     return EQUALITY_TRUE;
 640   }
 641   if (d_equalityEngine.areDisequal(a, b, false)) {
 642     // The terms are implied to be dis-equal
 643     return EQUALITY_FALSE;
 644   }
 645   Node aModelValue = d_external.d_valuation.getModelValue(a);
 646   if(aModelValue.isNull()) { return EQUALITY_UNKNOWN; }
 647   Node bModelValue = d_external.d_valuation.getModelValue(b);
 648   if(bModelValue.isNull()) { return EQUALITY_UNKNOWN; }
 649   if( aModelValue == bModelValue ) {
 650     // The term are true in current model
 651     return EQUALITY_TRUE_IN_MODEL;
 652   } else {
 653     return EQUALITY_FALSE_IN_MODEL;
 654   }
 655   // }
 656   // //TODO: can we be more precise sometimes?
 657   // return EQUALITY_UNKNOWN;
 658 }
 659
 660 /******************** Model generation ********************/
 661 /******************** Model generation ********************/
 662 /******************** Model generation ********************/
 663
 664 const TheorySetsPrivate::Elements& TheorySetsPrivate::getElements
 665 (TNode setterm, SettermElementsMap& settermElementsMap) const {
 666   SettermElementsMap::const_iterator it = settermElementsMap.find(setterm);
 667   bool alreadyCalculated = (it != settermElementsMap.end());
 668   if( !alreadyCalculated ) {
 669
 670     Kind k = setterm.getKind();
 671     Elements cur;
 672
 673     switch(k) {
 674     case kind::UNION: {
 675       const Elements& left = getElements(setterm[0], settermElementsMap);
 676       const Elements& right = getElements(setterm[1], settermElementsMap);
 677       if(left.size() >= right.size()) {
 678         cur = left; cur.insert(right.begin(), right.end());
 679       } else {
 680         cur = right; cur.insert(left.begin(), left.end());
 681       }
 682       break;
 683     }
 684     case kind::INTERSECTION: {
 685       const Elements& left = getElements(setterm[0], settermElementsMap);
 686       const Elements& right = getElements(setterm[1], settermElementsMap);
 687       std::set_intersection(left.begin(), left.end(), right.begin(), right.end(),
 688                             std::inserter(cur, cur.begin()) );
 689       break;
 690     }
 691     case kind::SETMINUS: {
 692       const Elements& left = getElements(setterm[0], settermElementsMap);
 693       const Elements& right = getElements(setterm[1], settermElementsMap);
 694       std::set_difference(left.begin(), left.end(), right.begin(), right.end(),
 695                           std::inserter(cur, cur.begin()) );
 696       break;
 697     }
 698     default:
 699       Assert(theory::kindToTheoryId(k) != theory::THEORY_SETS,
 700              (std::string("Kind belonging to set theory not explicitly handled: ") + kindToString(k)).c_str());
 701       // Assert(k == kind::VARIABLE || k == kind::APPLY_UF || k == kind::SKOLEM,
 702       //        (std::string("Expect variable or UF got ") + kindToString(k)).c_str() );
 703       /* assign emptyset, which is default */
 704     }
 705
 706     it = settermElementsMap.insert(SettermElementsMap::value_type(setterm, cur)).first;
 707   }
 708   return it->second;
 709 }
 710
 711
 712 bool TheorySetsPrivate::checkModel(const SettermElementsMap& settermElementsMap, TNode S) const {
 713
 714   Debug("sets-model") << "[sets-model] checkModel(..., " << S << "): "
 715                       << std::endl;
 716
 717   Assert(S.getType().isSet());
 718
 719   const Elements emptySetOfElements;
 720   const Elements& saved =
 721     d_equalityEngine.getRepresentative(S).getKind() == kind::EMPTYSET ||
 722     settermElementsMap.find(d_equalityEngine.getRepresentative(S)) == settermElementsMap.end() ?
 723     emptySetOfElements :
 724     settermElementsMap.find(d_equalityEngine.getRepresentative(S))->second;
 725   Debug("sets-model") << "[sets-model] saved :  { ";
 726   BOOST_FOREACH(TNode element, saved) { Debug("sets-model") << element << ", "; }
 727   Debug("sets-model") << " }" << std::endl;
 728
 729   if(theory::kindToTheoryId(S.getKind()) == THEORY_SETS && S.getNumChildren() == 2) {
 730
 731     Elements cur;
 732
 733     const Elements& left =
 734       d_equalityEngine.getRepresentative(S[0]).getKind() == kind::EMPTYSET ||
 735       settermElementsMap.find(d_equalityEngine.getRepresentative(S[0])) == settermElementsMap.end() ?
 736       emptySetOfElements :
 737       settermElementsMap.find(d_equalityEngine.getRepresentative(S[0]))->second;
 738
 739     const Elements&  right =
 740       d_equalityEngine.getRepresentative(S[1]).getKind() == kind::EMPTYSET ||
 741       settermElementsMap.find(d_equalityEngine.getRepresentative(S[1])) == settermElementsMap.end() ?
 742       emptySetOfElements :
 743       settermElementsMap.find(d_equalityEngine.getRepresentative(S[1]))->second;
 744
 745     switch(S.getKind()) {
 746     case kind::UNION:
 747       if(left.size() >= right.size()) {
 748         cur = left; cur.insert(right.begin(), right.end());
 749       } else {
 750         cur = right; cur.insert(left.begin(), left.end());
 751       }
 752       break;
 753     case kind::INTERSECTION:
 754       std::set_intersection(left.begin(), left.end(), right.begin(), right.end(),
 755                             std::inserter(cur, cur.begin()) );
 756       break;
 757     case kind::SETMINUS:
 758       std::set_difference(left.begin(), left.end(), right.begin(), right.end(),
 759                           std::inserter(cur, cur.begin()) );
 760       break;
 761     default:
 762       Unhandled();
 763     }
 764
 765     Debug("sets-model") << "[sets-model] cur :  { ";
 766     BOOST_FOREACH(TNode element, cur) { Debug("sets-model") << element << ", "; }
 767     Debug("sets-model") << " }" << std::endl;
 768
 769     if(saved != cur) {
 770       Debug("sets-model") << "[sets-model] *** ERROR *** cur != saved "
 771                           << std::endl;
 772       Debug("sets-model")
 773         << "[sets-model]   FYI: "
 774         << "  [" << S << "] = " << d_equalityEngine.getRepresentative(S) << ", "
 775         << "  [" << S[0] << "] = " << d_equalityEngine.getRepresentative(S[0]) << ", "
 776         << "  [" << S[1] << "] = " << d_equalityEngine.getRepresentative(S[1]) << "\n";
 777
 778       return false;
 779     }
 780   }
 781   return true;
 782 }
 783
 784 Node TheorySetsPrivate::elementsToShape(Elements elements, TypeNode setType) const
 785 {
 786   NodeManager* nm = NodeManager::currentNM();
 787
 788   if(elements.size() == 0) {
 789     return nm->mkConst<EmptySet>(EmptySet(nm->toType(setType)));
 790   } else {
 791     Elements::iterator it = elements.begin();
 792     Node cur = SINGLETON(*it);
 793     while( ++it != elements.end() ) {
 794       cur = nm->mkNode(kind::UNION, cur, SINGLETON(*it));
 795     }
 796     return cur;
 797   }
 798 }
 799 Node TheorySetsPrivate::elementsToShape(set<Node> elements, TypeNode setType) const
 800 {
 801   NodeManager* nm = NodeManager::currentNM();
 802
 803   if(elements.size() == 0) {
 804     return nm->mkConst<EmptySet>(EmptySet(nm->toType(setType)));
 805   } else {
 806     typeof(elements.begin()) it = elements.begin();
 807     Node cur = SINGLETON(*it);
 808     while( ++it != elements.end() ) {
 809       cur = nm->mkNode(kind::UNION, cur, SINGLETON(*it));
 810     }
 811     return cur;
 812   }
 813 }
 814
 815 void TheorySetsPrivate::collectModelInfo(TheoryModel* m, bool fullModel)
 816 {
 817   Trace("sets-model") << "[sets-model] collectModelInfo(..., fullModel="
 818                       << (fullModel ? "true)" : "false)") << std::endl;
 819
 820   set<Node> terms;
 821
 822   NodeManager* nm = NodeManager::currentNM();
 823
 824   // // this is for processCard -- commenting out for now
 825   // if(Debug.isOn("sets-card")) {
 826   //   for(typeof(d_cardTerms.begin()) it = d_cardTerms.begin();
 827   //       it != d_cardTerms.end(); ++it) {
 828   //     Debug("sets-card") << "[sets-card] " << *it << " = "
 829   //                        << d_external.d_valuation.getModelValue(*it)
 830   //                        << std::endl;
 831   //   }
 832   // }
 833
 834   if(Trace.isOn("sets-assertions")) {
 835     dumpAssertionsHumanified();
 836   }
 837
 838   // Compute terms appearing assertions and shared terms
 839   d_external.computeRelevantTerms(terms);
 840
 841   //processCard2 begin
 842   if(Debug.isOn("sets-card")) {
 843     for(typeof(d_V.begin()) it = d_V.begin(); it != d_V.end(); ++it) {
 844       Node n = nm->mkNode(kind::CARD, *it);
 845       Debug("sets-card") << "[sets-card] " << n << " = ";
 846       // if(d_external.d_sharedTerms.find(n) == d_external.d_sharedTerms.end()) continue;
 847       if((Rewriter::rewrite(n)).isConst()) {
 848         Debug("sets-card") << (Rewriter::rewrite(n))
 849                            << std::endl;
 850       } else {
 851         Debug("sets-card") << d_external.d_valuation.getModelValue(n)
 852                            << std::endl;
 853       }
 854     }
 855   }
 856   //processCard2 end
 857
 858   // Compute for each setterm elements that it contains
 859   SettermElementsMap settermElementsMap;
 860   for(eq::EqClassIterator it_eqclasses(d_trueNode, &d_equalityEngine);
 861       ! it_eqclasses.isFinished() ; ++it_eqclasses) {
 862     TNode n = (*it_eqclasses);
 863     if(n.getKind() == kind::MEMBER) {
 864       Assert(d_equalityEngine.areEqual(n, d_trueNode));
 865       TNode x = d_equalityEngine.getRepresentative(n[0]);
 866       TNode S = d_equalityEngine.getRepresentative(n[1]);
 867       settermElementsMap[S].insert(x);
 868     }
 869     if(Debug.isOn("sets-model-details")) {
 870       Debug("sets-model-details")
 871         << "[sets-model-details]  >  node: " << n << ", explanation:" << std::endl;
 872       vector<TNode> explanation;
 873       d_equalityEngine.explainPredicate(n, true, explanation);
 874       BOOST_FOREACH(TNode m, explanation) {
 875         Debug("sets-model-details") << "[sets-model-details]  >>  " << m << std::endl;
 876       }
 877     }
 878   }
 879
 880   if(Debug.isOn("sets-model-details")) {
 881     for(eq::EqClassIterator it_eqclasses(d_trueNode, &d_equalityEngine);
 882         ! it_eqclasses.isFinished() ; ++it_eqclasses) {
 883       TNode n = (*it_eqclasses);
 884       vector<TNode> explanation;
 885       Debug("sets-model-details")
 886         << "[sets-model-details]  >  node: not: " << n << ", explanation:" << std::endl;
 887       d_equalityEngine.explainPredicate(n, false, explanation);
 888       BOOST_FOREACH(TNode m, explanation) {
 889         Debug("sets-model-details") << "[sets-model-details]  >>  " << m << std::endl;
 890       }
 891     }
 892   }
 893
 894   // Assert equalities and disequalities to the model
 895   m->assertEqualityEngine(&d_equalityEngine, &terms);
 896
 897   // Loop over terms to collect set-terms for which we generate models
 898   set<Node> settermsModEq;
 899   BOOST_FOREACH(TNode term, terms) {
 900     TNode n = term.getKind() == kind::NOT ? term[0] : term;
 901
 902     Debug("sets-model-details") << "[sets-model-details]  >   " << n << std::endl;
 903
 904     if(n.getType().isSet()) {
 905       n = d_equalityEngine.getRepresentative(n);
 906       if( !n.isConst() ) {
 907         settermsModEq.insert(n);
 908       }
 909     }
 910
 911   }
 912
 913   if(Debug.isOn("sets-model")) {
 914     BOOST_FOREACH( TNode node, settermsModEq ) {
 915       Debug("sets-model") << "[sets-model]   " << node << std::endl;
 916     }
 917   }
 918
 919   if(Debug.isOn("sets-model-details")) {
 920     BOOST_FOREACH( SettermElementsMap::value_type &it, settermElementsMap ) {
 921       BOOST_FOREACH( TNode element, it.second /* elements */ ) {
 922         Debug("sets-model-details") << "[sets-model-details]  >   " <<
 923           (it.first /* setterm */) << ": " << element << std::endl;
 924       }
 925     }
 926   }
 927
 928   // build graph, and create sufficient number of skolems
 929   // buildGraph(); // this is for processCard
 930
 931   //processCard2 begin
 932   leaves.clear();
 933   for(typeof(d_V.begin()) it = d_V.begin(); it != d_V.end(); ++it)
 934     if(d_E.find(*it) == d_E.end())
 935       leaves.insert(*it);
 936   d_statistics.d_numLeaves.setData(leaves.size());
 937   d_statistics.d_numLeavesMax.maxAssign(leaves.size());
 938   //processCard2 end
 939
 940   std::hash_map<TNode, std::vector<TNode>, TNodeHashFunction> slackElements;
 941   BOOST_FOREACH( TNode setterm, leaves ) {
 942     if(setterm.getKind() == kind::EMPTYSET) { continue; }
 943     // Assert(d_cardTerms.find(nm->mkNode(kind::CARD,setterm)) != d_cardTerms.end()); // for processCard
 944     Assert(d_V.find(setterm) != d_V.end());
 945     Node cardValNode = d_external.d_valuation.getModelValue(nm->mkNode(kind::CARD,setterm));
 946     Rational cardValRational = cardValNode.getConst<Rational>();
 947     Assert(cardValRational.isIntegral());
 948     Integer cardValInteger = cardValRational.getNumerator();
 949     Assert(cardValInteger.fitsSignedInt(), "Can't build models that big.");
 950     int cardValInt = cardValInteger.getSignedInt();
 951     Assert(cardValInt >= 0);
 952     int numElems = getElements(setterm, settermElementsMap).size();
 953     Trace("sets-model-card") << "[sets-model-card] cardValInt = " << cardValInt << std::endl
 954                              << "                  numElems = " << numElems << std::endl;
 955     Trace("sets-model-card") << "[sets-model-card] Creating " << cardValInt-numElems
 956                              << " slack variables for " << setterm << std::endl;
 957     Assert(cardValInt >= numElems, "Run with -d sets-model-card for details");
 958
 959     TypeNode elementType = setterm.getType().getSetElementType();
 960     std::vector<TNode>& cur = slackElements[setterm];
 961     for(int i = numElems; i < cardValInt; ++i) {
 962       // slk = slack
 963       cur.push_back(nm->mkSkolem("slk_",  elementType));
 964     }
 965   }
 966
 967   // assign representatives to equivalence class
 968   BOOST_FOREACH( TNode setterm, settermsModEq ) {
 969     Elements elements = getElements(setterm, settermElementsMap);
 970     if(d_E.find(setterm) != d_E.end()) {
 971       Trace("sets-model-card") << "[sets-model-card] " << setterm << " (before slacks): " << elements.size() << std::endl;
 972       std::set<TNode> leafChildren = get_leaves(setterm);
 973       BOOST_FOREACH( TNode leafChild, leafChildren ) {
 974         if(leaves.find(leafChild) == leaves.end()) { continue; }
 975         BOOST_FOREACH( TNode slackVar, slackElements[leafChild] ) {
 976           elements.insert(slackVar);
 977         }
 978       }
 979       Trace("sets-model-card") << "[sets-model-card] " << setterm << " (after slacks): " << elements.size() << std::endl;
 980     } else if(d_V.find(setterm) != d_V.end()) {
 981       Trace("sets-model-card") << "[sets-model-card] " << setterm << " (before slacks): " << elements.size() << std::endl;
 982       BOOST_FOREACH( TNode slackVar, slackElements[setterm] ) {
 983         elements.insert(slackVar);
 984       }
 985       Trace("sets-model-card") << "[sets-model-card] " << setterm << " (after slacks): " << elements.size() << std::endl;
 986     }
 987     Node shape = elementsToShape(elements, setterm.getType());
 988     shape = theory::Rewriter::rewrite(shape);
 989     m->assertEquality(shape, setterm, true);
 990     m->assertRepresentative(shape);
 991   }
 992
 993 #ifdef CVC4_ASSERTIONS
 994   bool checkPassed = true;
 995   BOOST_FOREACH(TNode term, terms) {
 996     if( term.getType().isSet() ) {
 997       checkPassed &= checkModel(settermElementsMap, term);
 998     }
 999   }
1000   if(Trace.isOn("sets-checkmodel-ignore")) {
1001     Trace("sets-checkmodel-ignore") << "[sets-checkmodel-ignore] checkPassed value was " << checkPassed << std::endl;
1002   } else {
1003     Assert( checkPassed,
1004             "THEORY_SETS check-model failed. Run with -d sets-model for details." );
1005   }
1006 #endif
1007 }
1008
1009 Node TheorySetsPrivate::getModelValue(TNode n)
1010 {
1011   CodeTimer codeTimer(d_statistics.d_getModelValueTime);
1012   return d_termInfoManager->getModelValue(n);
1013 }
1014
1015 /********************** Helper functions ***************************/
1016 /********************** Helper functions ***************************/
1017 /********************** Helper functions ***************************/
1018
1019 Node mkAnd(const std::vector<TNode>& conjunctions) {
1020   Assert(conjunctions.size() > 0);
1021
1022   std::set<TNode> all;
1023
1024   for (unsigned i = 0; i < conjunctions.size(); ++i) {
1025     TNode t = conjunctions[i];
1026
1027     if (t.getKind() == kind::AND) {
1028       for(TNode::iterator child_it = t.begin();
1029           child_it != t.end(); ++child_it) {
1030         Assert((*child_it).getKind() != kind::AND);
1031         all.insert(*child_it);
1032       }
1033     }
1034     else {
1035       all.insert(t);
1036     }
1037
1038   }
1039
1040   Assert(all.size() > 0);
1041
1042   if (all.size() == 1) {
1043     // All the same, or just one
1044     return conjunctions[0];
1045   }
1046
1047   NodeBuilder<> conjunction(kind::AND);
1048   std::set<TNode>::const_iterator it = all.begin();
1049   std::set<TNode>::const_iterator it_end = all.end();
1050   while (it != it_end) {
1051     conjunction << *it;
1052     ++ it;
1053   }
1054
1055   return conjunction;
1056 }/* mkAnd() */
1057
1058
1059 TheorySetsPrivate::Statistics::Statistics() :
1060   d_getModelValueTime("theory::sets::getModelValueTime")
1061   , d_mergeTime("theory::sets::merge_nodes::time")
1062   , d_processCard2Time("theory::sets::processCard2::time")
1063   , d_memberLemmas("theory::sets::lemmas::member", 0)
1064   , d_disequalityLemmas("theory::sets::lemmas::disequality", 0)
1065   , d_numVertices("theory::sets::vertices", 0)
1066   , d_numVerticesMax("theory::sets::vertices-max", 0)
1067   , d_numMergeEq1or2("theory::sets::merge1or2", 0)
1068   , d_numMergeEq3("theory::sets::merge3", 0)
1069   , d_numLeaves("theory::sets::leaves", 0)
1070   , d_numLeavesMax("theory::sets::leaves-max", 0)
1071 {
1072   smtStatisticsRegistry()->registerStat(&d_getModelValueTime);
1073   smtStatisticsRegistry()->registerStat(&d_mergeTime);
1074   smtStatisticsRegistry()->registerStat(&d_processCard2Time);
1075   smtStatisticsRegistry()->registerStat(&d_memberLemmas);
1076   smtStatisticsRegistry()->registerStat(&d_disequalityLemmas);
1077   smtStatisticsRegistry()->registerStat(&d_numVertices);
1078   smtStatisticsRegistry()->registerStat(&d_numVerticesMax);
1079   smtStatisticsRegistry()->registerStat(&d_numMergeEq1or2);
1080   smtStatisticsRegistry()->registerStat(&d_numMergeEq3);
1081   smtStatisticsRegistry()->registerStat(&d_numLeaves);
1082   smtStatisticsRegistry()->registerStat(&d_numLeavesMax);
1083 }
1084
1085
1086 TheorySetsPrivate::Statistics::~Statistics() {
1087   smtStatisticsRegistry()->unregisterStat(&d_getModelValueTime);
1088   smtStatisticsRegistry()->unregisterStat(&d_mergeTime);
1089   smtStatisticsRegistry()->unregisterStat(&d_processCard2Time);
1090   smtStatisticsRegistry()->unregisterStat(&d_memberLemmas);
1091   smtStatisticsRegistry()->unregisterStat(&d_disequalityLemmas);
1092   smtStatisticsRegistry()->unregisterStat(&d_numVertices);
1093   smtStatisticsRegistry()->unregisterStat(&d_numVerticesMax);
1094   smtStatisticsRegistry()->unregisterStat(&d_numMergeEq1or2);
1095   smtStatisticsRegistry()->unregisterStat(&d_numMergeEq3);
1096   smtStatisticsRegistry()->unregisterStat(&d_numLeaves);
1097   smtStatisticsRegistry()->unregisterStat(&d_numLeavesMax);
1098 }
1099
1100
1101 bool TheorySetsPrivate::present(TNode atom) {
1102   return holds(atom) || holds(atom.notNode());
1103 }
1104
1105
1106 bool TheorySetsPrivate::holds(TNode atom, bool polarity) {
1107   TNode polarity_atom = polarity ? d_trueNode : d_falseNode;
1108
1109   Node atomModEq = NodeManager::currentNM()->mkNode
1110     (atom.getKind(), d_equalityEngine.getRepresentative(atom[0]),
1111      d_equalityEngine.getRepresentative(atom[1]) );
1112
1113   d_equalityEngine.addTerm(atomModEq);
1114
1115   return d_equalityEngine.areEqual(atomModEq, polarity_atom);
1116 }
1117
1118
1119 void TheorySetsPrivate::registerReason(TNode reason, bool save)
1120 {
1121   if(save) d_nodeSaver.insert(reason);
1122
1123   if(reason.getKind() == kind::AND) {
1124     //Assert(reason.getNumChildren() == 2);
1125     for(unsigned i = 0; i < reason.getNumChildren(); ++i) {
1126       registerReason(reason[i], false);
1127     }
1128   } else if(reason.getKind() == kind::NOT) {
1129     registerReason(reason[0], false);
1130   } else if(reason.getKind() == kind::MEMBER) {
1131     d_equalityEngine.addTerm(reason);
1132     Assert(present(reason));
1133   } else if(reason.getKind() == kind::EQUAL) {
1134     d_equalityEngine.addTerm(reason);
1135     Assert(present(reason));
1136   } else if(reason.getKind() == kind::CONST_BOOLEAN) {
1137     // That's OK, already in EqEngine
1138   } else {
1139     Unhandled();
1140   }
1141 }
1142
1143 void TheorySetsPrivate::finishPropagation()
1144 {
1145   while(!d_conflict && !d_settermPropagationQueue.empty()) {
1146     std::pair<TNode,TNode> np = d_settermPropagationQueue.front();
1147     d_settermPropagationQueue.pop();
1148     doSettermPropagation(np.first, np.second);
1149   }
1150   while(!d_conflict && !d_propagationQueue.empty()) {
1151     std::pair<Node,Node> np = d_propagationQueue.front();
1152     d_propagationQueue.pop();
1153     TNode atom = np.first.getKind() == kind::NOT ? np.first[0] : np.first;
1154     if(atom.getKind() == kind::MEMBER) {
1155       assertMemebership(np.first, np.second, /* learnt = */ true);
1156     } else {
1157       assertEquality(np.first, np.second, /* learnt = */ true);
1158     }
1159   }
1160 }
1161
1162 void TheorySetsPrivate::addToPending(Node n) {
1163   Debug("sets-pending") << "[sets-pending] addToPending " << n << std::endl;
1164
1165   if(d_pendingEverInserted.find(n) != d_pendingEverInserted.end()) {
1166     Debug("sets-pending") << "[sets-pending] \u2514 skipping " << n
1167                           << " as lemma already generated." << std::endl;
1168     return;
1169   }
1170
1171   if(n.getKind() == kind::MEMBER) {
1172
1173     Node nRewritten = theory::Rewriter::rewrite(n);
1174
1175     if(nRewritten.isConst()) {
1176       Debug("sets-pending") << "[sets-pending] \u2514 skipping " << n
1177                             << " as we can learn one of the sides." << std::endl;
1178       Assert(nRewritten == d_trueNode || nRewritten == d_falseNode);
1179
1180       bool polarity = (nRewritten == d_trueNode);
1181       learnLiteral(n, polarity, d_trueNode);
1182       return;
1183     }
1184
1185     Debug("sets-pending") << "[sets-pending] \u2514 added to member queue"
1186                           << std::endl;
1187     ++d_statistics.d_memberLemmas;
1188     d_pending.push(n);
1189     lemma(getLemma(), SETS_LEMMA_MEMBER);
1190     // d_external.d_out->splitLemma();
1191     Assert(isComplete());
1192
1193   } else {
1194
1195     Debug("sets-pending") << "[sets-pending] \u2514 added to equality queue"
1196                           << std::endl;
1197     Assert(n.getKind() == kind::EQUAL);
1198     ++d_statistics.d_disequalityLemmas;
1199     d_pendingDisequal.push(n);
1200     lemma(getLemma(), SETS_LEMMA_DISEQUAL);
1201     // d_external.d_out->splitLemma();
1202     Assert(isComplete());
1203
1204   }
1205 }
1206
1207 bool TheorySetsPrivate::isComplete() {
1208   // while(!d_pending.empty() &&
1209   //       (d_pendingEverInserted.find(d_pending.front()) != d_pendingEverInserted.end()
1210   //        || present(d_pending.front()) ) ) {
1211   //   Debug("sets-pending") << "[sets-pending] removing as already present: "
1212   //                         << d_pending.front() << std::endl;
1213   //   d_pending.pop();
1214   // }
1215   return d_pending.empty() && d_pendingDisequal.empty();
1216 }
1217
1218 Node TheorySetsPrivate::getLemma() {
1219   Assert(!d_pending.empty() || !d_pendingDisequal.empty());
1220
1221   Node n, lemma;
1222
1223   if(!d_pending.empty()) {
1224     n = d_pending.front();
1225     d_pending.pop();
1226     d_pendingEverInserted.insert(n);
1227
1228     Assert(!present(n));
1229     Assert(n.getKind() == kind::MEMBER);
1230
1231     lemma = OR(n, NOT(n));
1232   } else {
1233     n = d_pendingDisequal.front();
1234     d_pendingDisequal.pop();
1235     d_pendingEverInserted.insert(n);
1236
1237     Assert(n.getKind() == kind::EQUAL && n[0].getType().isSet());
1238     TypeNode elementType = n[0].getType().getSetElementType();
1239     Node x = NodeManager::currentNM()->mkSkolem("sde_",  elementType);
1240     Node l1 = MEMBER(x, n[0]), l2 = MEMBER(x, n[1]);
1241
1242     if(n[0].getKind() == kind::EMPTYSET) {
1243       lemma = OR(n, l2);
1244     } else if(n[1].getKind() == kind::EMPTYSET) {
1245       lemma = OR(n, l1);
1246     } else {
1247       lemma = OR(n, AND(l1, NOT(l2)), AND(NOT(l1), l2));
1248     }
1249   }
1250
1251   Debug("sets-lemma") << "[sets-lemma] Generating for " << n
1252                       << ", lemma: " << lemma << std::endl;
1253
1254   return  lemma;
1255 }
1256
1257
1258 TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
1259                                      context::Context* c,
1260                                      context::UserContext* u):
1261   d_external(external),
1262   d_notify(*this),
1263   d_equalityEngine(d_notify, c, "theory::sets::TheorySetsPrivate", true),
1264   d_trueNode(NodeManager::currentNM()->mkConst<bool>(true)),
1265   d_falseNode(NodeManager::currentNM()->mkConst<bool>(false)),
1266   d_conflict(c),
1267   d_termInfoManager(NULL),
1268   d_setTermToCardVar(),
1269   d_cardVarToSetTerm(),
1270   d_propagationQueue(c),
1271   d_settermPropagationQueue(c),
1272   d_nodeSaver(c),
1273   d_pending(c),
1274   d_pendingDisequal(c),
1275   d_pendingEverInserted(u),
1276   d_modelCache(c),
1277   d_ccg_i(c),
1278   d_ccg_j(c),
1279   d_scrutinize(NULL),
1280   d_cardEnabled(false),
1281   d_cardTerms(c),
1282   d_typesAdded(),
1283   d_processedCardTerms(c),
1284   d_processedCardPairs(),
1285   d_cardLowerLemmaCache(u),
1286   edgesFd(),
1287   edgesBk(),
1288   disjoint(),
1289   leaves(),
1290   d_V(c),
1291   d_E(c),
1292   d_graphMergesPending(c),
1293   d_allSetEqualitiesSoFar(c),
1294   d_lemmasGenerated(u),
1295   d_newLemmaGenerated(false),
1296   d_relTerms(u)
1297 {
1298   d_termInfoManager = new TermInfoManager(*this, c, &d_equalityEngine);
1299
1300   d_equalityEngine.addFunctionKind(kind::UNION);
1301   d_equalityEngine.addFunctionKind(kind::INTERSECTION);
1302   d_equalityEngine.addFunctionKind(kind::SETMINUS);
1303
1304   d_equalityEngine.addFunctionKind(kind::MEMBER);
1305   d_equalityEngine.addFunctionKind(kind::SUBSET);
1306
1307   // If cardinality is on.
1308   d_equalityEngine.addFunctionKind(kind::CARD);
1309
1310   if( Debug.isOn("sets-scrutinize") ) {
1311     d_scrutinize = new TheorySetsScrutinize(this);
1312   }
1313 }/* TheorySetsPrivate::TheorySetsPrivate() */
1314
1315
1316 TheorySetsPrivate::~TheorySetsPrivate()
1317 {
1318   delete d_termInfoManager;
1319   if( Debug.isOn("sets-scrutinize") ) {
1320     Assert(d_scrutinize != NULL);
1321     delete d_scrutinize;
1322   }
1323 }/* TheorySetsPrivate::~TheorySetsPrivate() */
1324
1325 void TheorySetsPrivate::propagate(Theory::Effort effort) {
1326   if(effort != Theory::EFFORT_FULL || !options::setsPropFull()) {
1327     return;
1328   }
1329
1330   // build a model
1331   Trace("sets-prop-full") << "[sets-prop-full] propagate(FULL_EFFORT)" << std::endl;
1332   if(Trace.isOn("sets-assertions")) {
1333     dumpAssertionsHumanified();
1334   }
1335
1336   const CDNodeSet& terms = (d_termInfoManager->d_terms);
1337   for(typeof(terms.key_begin()) it = terms.key_begin(); it != terms.key_end(); ++it) {
1338     Node node = (*it);
1339     Kind k = node.getKind();
1340     if(k == kind::UNION && node[0].getKind() == kind::SINGLETON ) {
1341
1342       if(holds(MEMBER(node[0][0], node[1]))) {
1343         Trace("sets-prop-full") << "[sets-prop-full] " << MEMBER(node[0][0], node[1])
1344                                 << " => " << EQUAL(node[1], node) << std::endl;
1345         learnLiteral(EQUAL(node[1], node), MEMBER(node[0][0], node[1]));
1346       }
1347
1348     } else if(k == kind::UNION && node[1].getKind() == kind::SINGLETON ) {
1349
1350       if(holds(MEMBER(node[1][0], node[0]))) {
1351         Trace("sets-prop-full") << "[sets-prop-full] " << MEMBER(node[1][0], node[0])
1352                                 << " => " << EQUAL(node[0], node) << std::endl;
1353         learnLiteral(EQUAL(node[0], node), MEMBER(node[1][0], node[0]));
1354       }
1355
1356     }
1357   }
1358
1359   finishPropagation();
1360 }
1361
1362 bool TheorySetsPrivate::propagate(TNode literal) {
1363   Debug("sets-prop") << " propagate(" << literal  << ")" << std::endl;
1364
1365   // If already in conflict, no more propagation
1366   if (d_conflict) {
1367     Debug("sets-prop") << "TheoryUF::propagate(" << literal << "): already in conflict" << std::endl;
1368     return false;
1369   }
1370
1371   // Propagate out
1372   bool ok = d_external.d_out->propagate(literal);
1373   if (!ok) {
1374     d_conflict = true;
1375   }
1376
1377   return ok;
1378 }/* TheorySetsPrivate::propagate(TNode) */
1379
1380
1381 void TheorySetsPrivate::setMasterEqualityEngine(eq::EqualityEngine* eq) {
1382   d_equalityEngine.setMasterEqualityEngine(eq);
1383 }
1384
1385
1386 void TheorySetsPrivate::conflict(TNode a, TNode b)
1387 {
1388   if (a.getKind() == kind::CONST_BOOLEAN) {
1389     d_conflictNode = explain(a.iffNode(b));
1390   } else {
1391     d_conflictNode = explain(a.eqNode(b));
1392   }
1393   d_external.d_out->conflict(d_conflictNode);
1394   Debug("sets") << "[sets] conflict: " << a << " iff " << b
1395                 << ", explaination " << d_conflictNode << std::endl;
1396   d_conflict = true;
1397 }
1398
1399 Node TheorySetsPrivate::explain(TNode literal)
1400 {
1401   Debug("sets") << "TheorySetsPrivate::explain(" << literal << ")"
1402                 << std::endl;
1403
1404   bool polarity = literal.getKind() != kind::NOT;
1405   TNode atom = polarity ? literal : literal[0];
1406   std::vector<TNode> assumptions;
1407
1408   if(atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
1409     d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
1410   } else if(atom.getKind() == kind::MEMBER) {
1411     if( !d_equalityEngine.hasTerm(atom)) {
1412       d_equalityEngine.addTerm(atom);
1413     }
1414     d_equalityEngine.explainPredicate(atom, polarity, assumptions);
1415   } else {
1416     Debug("sets") << "unhandled: " << literal << "; (" << atom << ", "
1417                   << polarity << "); kind" << atom.getKind() << std::endl;
1418     Unhandled();
1419   }
1420
1421   return mkAnd(assumptions);
1422 }
1423
1424 bool TheorySetsPrivate::lemma(Node n, SetsLemmaTag t)
1425 {
1426   if(d_lemmasGenerated.find(n) != d_lemmasGenerated.end()) {
1427     return false;
1428   }
1429   d_lemmasGenerated.insert(n);
1430   d_newLemmaGenerated = true;
1431   switch(t) {
1432   case SETS_LEMMA_DISEQUAL:
1433   case SETS_LEMMA_MEMBER: {
1434     d_external.d_out->splitLemma(n);
1435     break;
1436   }
1437   case SETS_LEMMA_GRAPH://  {
1438   //   d_external.d_out->preservedLemma(n, false, false);
1439   //   break;
1440   // }
1441   case SETS_LEMMA_OTHER: {
1442     d_external.d_out->lemma(n);
1443     break;
1444   }
1445   }
1446   return true;
1447 }
1448
1449 void TheorySetsPrivate::preRegisterTerm(TNode node)
1450 {
1451   Debug("sets") << "TheorySetsPrivate::preRegisterTerm(" << node << ")"
1452                 << std::endl;
1453
1454   switch(node.getKind()) {
1455   case kind::EQUAL:
1456     // TODO: what's the point of this
1457     d_equalityEngine.addTriggerEquality(node);
1458     break;
1459   case kind::MEMBER:
1460     // TODO: what's the point of this
1461     d_equalityEngine.addTriggerPredicate(node);
1462     break;
1463   case kind::CARD:
1464     if(!d_cardEnabled) { enableCard(); }
1465     registerCard(node);
1466     d_equalityEngine.addTriggerTerm(node, THEORY_SETS);
1467     break;
1468   default:
1469     d_termInfoManager->addTerm(node);
1470     d_equalityEngine.addTriggerTerm(node, THEORY_SETS);
1471   }
1472
1473   if(node.getKind() == kind::SINGLETON) {
1474     learnLiteral(MEMBER(node[0], node), true, d_trueNode);
1475   }
1476
1477   // ** For cardinality reasoning **
1478   if(node.getType().isSet() && d_typesAdded.find(node.getType()) == d_typesAdded.end()) {
1479     d_typesAdded.insert(node.getType());
1480
1481     if(d_cardEnabled)  {
1482       cardCreateEmptysetSkolem(node.getType());
1483     }
1484   }
1485   if(d_cardEnabled && node.getKind() == kind::SINGLETON) {
1486     registerCard(NodeManager::currentNM()->mkNode(kind::CARD, node));
1487   }
1488 }
1489
1490
1491 void TheorySetsPrivate::presolve() {
1492
1493   for(typeof(d_termInfoManager->d_terms.begin()) it = d_termInfoManager->d_terms.begin();
1494       it !=  d_termInfoManager->d_terms.end(); ++it) {
1495     d_relTerms.insert(*it);
1496   }
1497
1498   if(Trace.isOn("sets-relterms")) {
1499     Trace("sets-relterms") << "[sets-relterms] ";
1500     for(typeof(d_relTerms.begin()) it = d_relTerms.begin();
1501         it != d_relTerms.end(); ++it ) {
1502       Trace("sets-relterms") << (*it) << ", ";
1503     }
1504     Trace("sets-relterms") << "\n";
1505   }
1506
1507 }
1508
1509 /**************************** eq::NotifyClass *****************************/
1510 /**************************** eq::NotifyClass *****************************/
1511 /**************************** eq::NotifyClass *****************************/
1512
1513
1514 bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool value)
1515 {
1516   Debug("sets-eq") << "[sets-eq] eqNotifyTriggerEquality: equality = " << equality
1517                    << " value = " << value << std::endl;
1518   if (value) {
1519     return d_theory.propagate(equality);
1520   } else {
1521     // We use only literal triggers so taking not is safe
1522     return d_theory.propagate(equality.notNode());
1523   }
1524 }
1525
1526 bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value)
1527 {
1528   Debug("sets-eq") << "[sets-eq] eqNotifyTriggerPredicate: predicate = " << predicate
1529                    << " value = " << value << std::endl;
1530   if (value) {
1531     return d_theory.propagate(predicate);
1532   } else {
1533     return d_theory.propagate(predicate.notNode());
1534   }
1535 }
1536
1537 bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value)
1538 {
1539   Debug("sets-eq") << "[sets-eq] eqNotifyTriggerTermEquality: tag = " << tag
1540                    << " t1 = " << t1 << "  t2 = " << t2 << "  value = " << value << std::endl;
1541   if(value && t1.getKind() != kind::CARD && t2.getKind() != kind::CARD) {
1542     d_theory.d_termInfoManager->mergeTerms(t1, t2);
1543   }
1544   d_theory.propagate( value ? EQUAL(t1, t2) : NOT(EQUAL(t1, t2)) );
1545   return true;
1546 }
1547
1548 void TheorySetsPrivate::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2)
1549 {
1550   Debug("sets-eq") << "[sets-eq] eqNotifyConstantTermMerge " << " t1 = " << t1 << " t2 = " << t2 << std::endl;
1551   d_theory.conflict(t1, t2);
1552 }
1553
1554 // void TheorySetsPrivate::NotifyClass::eqNotifyNewClass(TNode t)
1555 // {
1556 //   Debug("sets-eq") << "[sets-eq] eqNotifyNewClass:" << " t = " << t << std::endl;
1557 // }
1558
1559 // void TheorySetsPrivate::NotifyClass::eqNotifyPreMerge(TNode t1, TNode t2)
1560 // {
1561 //   Debug("sets-eq") << "[sets-eq] eqNotifyPreMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl;
1562 // }
1563
1564 // void TheorySetsPrivate::NotifyClass::eqNotifyPostMerge(TNode t1, TNode t2)
1565 // {
1566 //   Debug("sets-eq") << "[sets-eq] eqNotifyPostMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl;
1567 // }
1568
1569 // void TheorySetsPrivate::NotifyClass::eqNotifyDisequal(TNode t1, TNode t2, TNode reason)
1570 // {
1571 //   Debug("sets-eq") << "[sets-eq] eqNotifyDisequal:" << " t1 = " << t1 << " t2 = " << t2 << " reason = " << reason << std::endl;
1572 // }
1573
1574
1575 /**************************** TermInfoManager *****************************/
1576 /**************************** TermInfoManager *****************************/
1577 /**************************** TermInfoManager *****************************/
1578
1579 void TheorySetsPrivate::TermInfoManager::mergeLists
1580 (CDTNodeList* la, const CDTNodeList* lb) const {
1581   // straight from theory/arrays/array_info.cpp
1582   std::set<TNode> temp;
1583   CDTNodeList::const_iterator it;
1584   for(it = la->begin() ; it != la->end(); it++ ) {
1585     temp.insert((*it));
1586   }
1587
1588   for(it = lb->begin() ; it!= lb->end(); it++ ) {
1589     if(temp.count(*it) == 0) {
1590       la->push_back(*it);
1591     }
1592   }
1593 }
1594
1595 TheorySetsPrivate::TermInfoManager::TermInfoManager
1596 (TheorySetsPrivate& theory, context::Context* satContext, eq::EqualityEngine* eq):
1597   d_theory(theory),
1598   d_context(satContext),
1599   d_eqEngine(eq),
1600   d_terms(satContext),
1601   d_info()
1602 { }
1603
1604 TheorySetsPrivate::TermInfoManager::~TermInfoManager() {
1605   for( typeof(d_info.begin()) it = d_info.begin();
1606        it != d_info.end(); ++it) {
1607     delete (*it).second;
1608   }
1609 }
1610
1611 void TheorySetsPrivate::TermInfoManager::notifyMembership(TNode fact) {
1612   bool polarity = fact.getKind() != kind::NOT;
1613   TNode atom = polarity ? fact : fact[0];
1614
1615   TNode x = d_eqEngine->getRepresentative(atom[0]);
1616   TNode S = d_eqEngine->getRepresentative(atom[1]);
1617
1618   Debug("sets-terminfo") << "[sets-terminfo] Adding membership " << x
1619                          << " in " << S << " " << polarity << std::endl;
1620
1621   d_info[S]->addToElementList(x, polarity);
1622   d_info[x]->addToSetList(S, polarity);
1623
1624   d_theory.d_modelCache.clear();
1625 }
1626
1627 const CDTNodeList* TheorySetsPrivate::TermInfoManager::getParents(TNode x) {
1628   return d_info[x]->parents;
1629 }
1630
1631 const CDTNodeList* TheorySetsPrivate::TermInfoManager::getMembers(TNode S) {
1632   return d_info[S]->elementsInThisSet;
1633 }
1634
1635 const CDTNodeList* TheorySetsPrivate::TermInfoManager::getNonMembers(TNode S) {
1636   return d_info[S]->elementsNotInThisSet;
1637 }
1638
1639 void TheorySetsPrivate::TermInfoManager::addTerm(TNode n) {
1640   if(d_terms.contains(n)) {
1641     return;
1642   }
1643   d_terms.insert(n);
1644
1645   if(d_info.find(n) == d_info.end()) {
1646     d_info.insert(make_pair(n, new TheorySetsTermInfo(d_context)));
1647   }
1648
1649   if(n.getKind() == kind::UNION ||
1650      n.getKind() == kind::INTERSECTION ||
1651      n.getKind() == kind::SETMINUS) {
1652
1653     unsigned numChild = n.getNumChildren();
1654
1655     for(unsigned i = 0; i < numChild; ++i) {
1656       Assert(d_terms.contains(n[i]));
1657       if(d_terms.contains(n[i])) {
1658         Debug("sets-parent") << "Adding " << n << " to parent list of "
1659                              << n[i] << std::endl;
1660
1661         // introduce cardinality of this set if a child's cardinality appears
1662         d_info[n[i]]->parents->push_back(n);
1663         if(d_theory.d_cardTerms.find(CARD(n[i])) != d_theory.d_cardTerms.end()) {
1664           d_theory.registerCard(CARD(n));
1665         }
1666
1667         typeof(d_info.begin()) ita = d_info.find(d_eqEngine->getRepresentative(n[i]));
1668         Assert(ita != d_info.end());
1669         CDTNodeList* l = (*ita).second->elementsNotInThisSet;
1670         for(typeof(l->begin()) it = l->begin(); it != l->end(); ++it) {
1671           d_theory.d_settermPropagationQueue.push_back( std::make_pair( (*it), n ) );
1672         }
1673         l = (*ita).second->elementsInThisSet;
1674         for(typeof(l->begin()) it = l->begin(); it != l->end(); ++it) {
1675           d_theory.d_settermPropagationQueue.push_back( std::make_pair( (*it), n ) );
1676         }
1677       }
1678     }
1679   }
1680 }
1681
1682 void TheorySetsPrivate::TermInfoManager::pushToSettermPropagationQueue
1683 (TNode x, TNode S, bool polarity)
1684 {
1685   Node cur_atom = MEMBER(x, S);
1686
1687   // propagation : empty set
1688   if(polarity && S.getKind() == kind::EMPTYSET) {
1689     Debug("sets-prop") << "[sets-prop]  something in empty set? conflict."
1690                        << std::endl;
1691     d_theory.learnLiteral(cur_atom, false, cur_atom);
1692     return;
1693   }// propagation: empty set
1694
1695   // propagation : children
1696   if(S.getKind() == kind::UNION ||
1697      S.getKind() == kind::INTERSECTION ||
1698      S.getKind() == kind::SETMINUS ||
1699      S.getKind() == kind::SINGLETON) {
1700     d_theory.d_settermPropagationQueue.push_back(std::make_pair(x, S));
1701   }// propagation: children
1702
1703   // propagation : parents
1704   const CDTNodeList* parentList = getParents(S);
1705   for(typeof(parentList->begin()) k = parentList->begin();
1706       k != parentList->end(); ++k) {
1707     d_theory.d_settermPropagationQueue.push_back(std::make_pair(x, *k));
1708   }// propagation : parents
1709
1710 }
1711
1712 void TheorySetsPrivate::TermInfoManager::pushToSettermPropagationQueue
1713 (TNode x, CDTNodeList* l, bool polarity)
1714 {
1715   set<TNode> alreadyProcessed;
1716
1717   BOOST_FOREACH(TNode S, (*l) ) {
1718     Debug("sets-prop") << "[sets-terminfo]  setterm todo: "
1719                        << MEMBER(x, d_eqEngine->getRepresentative(S))
1720                        << std::endl;
1721
1722     TNode repS = d_eqEngine->getRepresentative(S);
1723     if(alreadyProcessed.find(repS) != alreadyProcessed.end()) {
1724       continue;
1725     } else {
1726       alreadyProcessed.insert(repS);
1727     }
1728
1729     d_eqEngine->addTerm(MEMBER(d_eqEngine->getRepresentative(x), repS));
1730
1731     for(eq::EqClassIterator j(d_eqEngine->getRepresentative(S), d_eqEngine);
1732         !j.isFinished(); ++j) {
1733
1734       pushToSettermPropagationQueue(x, *j, polarity);
1735
1736     }//j loop
1737   }
1738 }
1739
1740 void TheorySetsPrivate::TermInfoManager::pushToSettermPropagationQueue
1741 (CDTNodeList* l, TNode S, bool polarity)
1742 {
1743   BOOST_FOREACH(TNode x, (*l) ) {
1744     Debug("sets-prop") << "[sets-terminfo]  setterm todo: "
1745                        << MEMBER(x, d_eqEngine->getRepresentative(S))
1746                        << std::endl;
1747
1748     d_eqEngine->addTerm(MEMBER(d_eqEngine->getRepresentative(x),
1749                                d_eqEngine->getRepresentative(S)));
1750
1751     for(eq::EqClassIterator j(d_eqEngine->getRepresentative(S), d_eqEngine);
1752         !j.isFinished(); ++j) {
1753
1754       pushToSettermPropagationQueue(x, *j, polarity);
1755
1756     }//j loop
1757
1758   }
1759
1760 }
1761
1762
1763
1764 void TheorySetsPrivate::TermInfoManager::mergeTerms(TNode a, TNode b) {
1765   // merge b into a
1766   Debug("sets-terminfo") << "[sets-terminfo] Merging (into) a = " << a
1767                          << ", b = " << b << std::endl;
1768   Debug("sets-terminfo") << "[sets-terminfo] reps"
1769                          << ", a: " << d_eqEngine->getRepresentative(a)
1770                          << ", b: " << d_eqEngine->getRepresentative(b)
1771                          << std::endl;
1772
1773   typeof(d_info.begin()) ita = d_info.find(a);
1774   typeof(d_info.begin()) itb = d_info.find(b);
1775
1776   Assert(ita != d_info.end());
1777   Assert(itb != d_info.end());
1778
1779   /* elements in this sets */
1780   pushToSettermPropagationQueue( (*ita).second->elementsInThisSet, b, true );
1781   pushToSettermPropagationQueue( (*ita).second->elementsNotInThisSet, b, false );
1782   pushToSettermPropagationQueue( (*itb).second->elementsNotInThisSet, a, false );
1783   pushToSettermPropagationQueue( (*itb).second->elementsInThisSet, a, true );
1784   mergeLists((*ita).second->elementsInThisSet,
1785              (*itb).second->elementsInThisSet);
1786   mergeLists((*ita).second->elementsNotInThisSet,
1787              (*itb).second->elementsNotInThisSet);
1788
1789   /* sets containing this element */
1790   // pushToSettermPropagationQueue( b, (*ita).second->setsContainingThisElement, true);
1791   // pushToSettermPropagationQueue( b, (*ita).second->setsNotContainingThisElement, false);
1792   pushToSettermPropagationQueue( a, (*itb).second->setsNotContainingThisElement, false);
1793   pushToSettermPropagationQueue( a, (*itb).second->setsContainingThisElement, true);
1794   mergeLists( (*ita).second->setsContainingThisElement,
1795               (*itb).second->setsContainingThisElement );
1796   mergeLists( (*ita).second->setsNotContainingThisElement,
1797               (*itb).second->setsNotContainingThisElement );
1798
1799   d_theory.d_modelCache.clear();
1800 }
1801
1802 Node TheorySetsPrivate::TermInfoManager::getModelValue(TNode n)
1803 {
1804   if(d_terms.find(n) == d_terms.end()) {
1805     return Node();
1806   }
1807   Assert(n.getType().isSet());
1808   set<Node> elements, elements_const;
1809   Node S = d_eqEngine->getRepresentative(n);
1810   typeof(d_theory.d_modelCache.begin()) it = d_theory.d_modelCache.find(S);
1811   if(it != d_theory.d_modelCache.end()) {
1812     return (*it).second;
1813   }
1814   const CDTNodeList* l = getMembers(S);
1815   for(typeof(l->begin()) it = l->begin(); it != l->end(); ++it) {
1816     TNode n = *it;
1817     elements.insert(d_eqEngine->getRepresentative(n));
1818   }
1819   BOOST_FOREACH(TNode e, elements) {
1820     if(e.isConst()) {
1821       elements_const.insert(e);
1822     } else {
1823       Node eModelValue = d_theory.d_external.d_valuation.getModelValue(e);
1824       if( eModelValue.isNull() ) return eModelValue;
1825       elements_const.insert(eModelValue);
1826     }
1827   }
1828   Node v = d_theory.elementsToShape(elements_const, n.getType());
1829   d_theory.d_modelCache[n] = v;
1830   return v;
1831 }
1832
1833
1834
1835
1836 /********************** Cardinality ***************************/
1837 /********************** Cardinality ***************************/
1838 /********************** Cardinality ***************************/
1839
1840 void TheorySetsPrivate::enableCard()
1841 {
1842   Assert(!d_cardEnabled);
1843   Trace("sets-card") << "[sets-card] Enabling cardinality reasoning" << std::endl;
1844   d_cardEnabled = true;
1845
1846   BOOST_FOREACH( TypeNode t, d_typesAdded ) {
1847     cardCreateEmptysetSkolem(t);
1848   }
1849
1850   for(typeof(d_termInfoManager->d_terms.begin()) it = d_termInfoManager->d_terms.begin();
1851       it !=  d_termInfoManager->d_terms.end(); ++it) {
1852     Node n = (*it);
1853     if(n.getKind() == kind::SINGLETON) {
1854       registerCard(NodeManager::currentNM()->mkNode(kind::CARD, n));
1855     }
1856   }
1857 }
1858
1859 void TheorySetsPrivate::registerCard(TNode node) {
1860   Trace("sets-card") << "[sets-card] registerCard( " << node << ")" << std::endl;
1861   if(d_cardTerms.find(node) == d_cardTerms.end()) {
1862     d_cardTerms.insert(node);
1863
1864     // introduce cardinality of any set-term containing this term
1865     NodeManager* nm = NodeManager::currentNM();
1866     const CDTNodeList* parentList = d_termInfoManager->getParents(node[0]);
1867     for(typeof(parentList->begin()) it = parentList->begin();
1868         it != parentList->end(); ++it) {
1869       registerCard(nm->mkNode(kind::CARD, *it));
1870     }
1871   }
1872 }
1873
1874
1875 void TheorySetsPrivate::cardCreateEmptysetSkolem(TypeNode t) {
1876   // set cardinality zero
1877   NodeManager* nm = NodeManager::currentNM();
1878   Debug("sets-card") << "Creating skolem for emptyset for type "
1879                      << t << std::endl;
1880   Node emptySet = nm->mkConst<EmptySet>(EmptySet(nm->toType(t)));
1881   Node sk = nm->mkSkolem("scz_",  t);
1882   lemma(nm->mkNode(kind::EQUAL, sk, emptySet), SETS_LEMMA_OTHER);
1883   lemma(nm->mkNode(kind::EQUAL, nm->mkConst(Rational(0)), nm->mkNode(kind::CARD, sk)), SETS_LEMMA_OTHER);
1884 }
1885
1886
1887 void TheorySetsPrivate::buildGraph() {
1888
1889   NodeManager* nm = NodeManager::currentNM();
1890
1891   edgesFd.clear();
1892   edgesBk.clear();
1893   disjoint.clear();
1894
1895   for(typeof(d_processedCardPairs.begin()) it = d_processedCardPairs.begin();
1896       it != d_processedCardPairs.end(); ++it) {
1897     Node s = (it->first).first;
1898     Assert(Rewriter::rewrite(s) == s);
1899     Node t = (it->first).second;
1900     Assert(Rewriter::rewrite(t) == t);
1901     bool hasUnion = (it->second);
1902
1903     Node sNt = nm->mkNode(kind::INTERSECTION, s, t);
1904     sNt = Rewriter::rewrite(sNt);
1905     Node sMt = nm->mkNode(kind::SETMINUS, s, t);
1906     sMt = Rewriter::rewrite(sMt);
1907     Node tMs = nm->mkNode(kind::SETMINUS, t, s);
1908     tMs = Rewriter::rewrite(tMs);
1909
1910     edgesFd[s].insert(sNt);
1911     edgesFd[s].insert(sMt);
1912     edgesBk[sNt].insert(s);
1913     edgesBk[sMt].insert(s);
1914
1915     edgesFd[t].insert(sNt);
1916     edgesFd[t].insert(tMs);
1917     edgesBk[sNt].insert(t);
1918     edgesBk[tMs].insert(t);
1919
1920     if(hasUnion) {
1921       Node sUt = nm->mkNode(kind::UNION, s, t);
1922       sUt = Rewriter::rewrite(sUt);
1923
1924       edgesFd[sUt].insert(sNt);
1925       edgesFd[sUt].insert(sMt);
1926       edgesFd[sUt].insert(tMs);
1927       edgesBk[sNt].insert(sUt);
1928       edgesBk[sMt].insert(sUt);
1929       edgesBk[tMs].insert(sUt);
1930     }
1931
1932     disjoint.insert(make_pair(sNt, sMt));
1933     disjoint.insert(make_pair(sMt, sNt));
1934     disjoint.insert(make_pair(sNt, tMs));
1935     disjoint.insert(make_pair(tMs, sNt));
1936     disjoint.insert(make_pair(tMs, sMt));
1937     disjoint.insert(make_pair(sMt, tMs));
1938   }
1939
1940   if(Debug.isOn("sets-card-graph")) {
1941     Debug("sets-card-graph") << "[sets-card-graph] Fd:" << std::endl;
1942     for(typeof(edgesFd.begin()) it = edgesFd.begin();
1943         it != edgesFd.end(); ++it) {
1944       Debug("sets-card-graph") << "[sets-card-graph]  " << (it->first) << std::endl;
1945       for(typeof( (it->second).begin()) jt = (it->second).begin();
1946           jt != (it->second).end(); ++jt) {
1947         Debug("sets-card-graph") << "[sets-card-graph]   " << (*jt) << std::endl;
1948       }
1949     }
1950     Debug("sets-card-graph") << "[sets-card-graph] Bk:" << std::endl;
1951     for(typeof(edgesBk.begin()) it = edgesBk.begin();
1952         it != edgesBk.end(); ++it) {
1953       Debug("sets-card-graph") << "[sets-card-graph]  " << (it->first) << std::endl;
1954       for(typeof( (it->second).begin()) jt = (it->second).begin();
1955           jt != (it->second).end(); ++jt) {
1956         Debug("sets-card-graph") << "[sets-card-graph]   " << (*jt) << std::endl;
1957       }
1958     }
1959   }
1960
1961
1962
1963   leaves.clear();
1964
1965   for(typeof(d_processedCardTerms.begin()) it = d_processedCardTerms.begin();
1966       it != d_processedCardTerms.end(); ++it) {
1967     Node n = (*it)[0];
1968     if( edgesFd.find(n) == edgesFd.end() ) {
1969       leaves.insert(n);
1970       Debug("sets-card-graph") << "[sets-card-graph] Leaf: " << n << std::endl;
1971     }
1972     // if( edgesBk.find(n) != edgesBk.end() ) {
1973     //   Assert(n.getKind() == kind::INTERSECTION ||
1974     //          n.getKind() == kind::SETMINUS);
1975     // }
1976   }
1977
1978 }
1979
1980 const std::set<TNode> getReachable(map<TNode, set<TNode> >& edges, TNode node) {
1981   Debug("sets-getreachable-debug") << "[sets-getreachable-debug] " << node << ":" << std::endl;
1982   queue<TNode> Q;
1983   std::set<TNode> ret;
1984   ret.insert(node);
1985   if(edges.find(node) != edges.end()) {
1986     Debug("sets-getreachable-debug") << "[sets-getreachable-debug]   " << node << ":" << std::endl;
1987     Q.push(node);
1988   }
1989   while(!Q.empty()) {
1990     TNode n = Q.front();
1991     Q.pop();
1992     for(set<TNode>::iterator it = edges[n].begin();
1993         it != edges[n].end(); ++it) {
1994       if(ret.find(*it) == ret.end()) {
1995         if(edges.find(*it) != edges.end()) {
1996           Debug("sets-getreachable-debug") << "[sets-getreachable-debug]   " << *it << ":" << std::endl;
1997           Q.push(*it);
1998         }
1999         ret.insert(*it);
2000       }
2001     }
2002   }
2003   return ret;
2004 }
2005
2006 const std::set<TNode> getLeaves(map<TNode, set<TNode> >& edges, TNode node) {
2007   Debug("sets-getreachable-debug") << "[sets-getreachable-debug] " << node << ":" << std::endl;
2008   queue<TNode> Q;
2009   std::set<TNode> ret;
2010   std::set<TNode> visited;
2011   visited.insert(node);
2012   if(edges.find(node) != edges.end()) {
2013     Q.push(node);
2014   } else {
2015     Debug("sets-getreachable-debug") << "[sets-getreachable-debug]   " << node << std::endl;
2016     ret.insert(node);
2017   }
2018   while(!Q.empty()) {
2019     TNode n = Q.front();
2020     Q.pop();
2021     for(set<TNode>::iterator it = edges[n].begin();
2022         it != edges[n].end(); ++it) {
2023       if(visited.find(*it) == visited.end()) {
2024         if(edges.find(*it) != edges.end()) {
2025           Q.push(*it);
2026         } else {
2027           Debug("sets-getreachable-debug") << "[sets-getreachable-debug]   " << *it << std::endl;
2028           ret.insert(*it);
2029         }
2030         visited.insert(*it);
2031       }
2032     }
2033   }
2034   return ret;
2035 }
2036
2037 /************ New cardinality implementation **************/
2038
2039
2040 /***
2041  * Data structures:
2042  * d_V : vertices in the graph (context dependent data structure)
2043  * d_E : edges between vertices in the graph
2044  *
2045  * Methods:
2046  *
2047  * merge(vector<int> a, vector<int> b)
2048  * get non empty leaves
2049  * of a & b, for each internal node, there will be two parent nodes
2050  *
2051  * Introduce
2052  *   <If a node already exists, merge with it>
2053  */
2054
2055 void TheorySetsPrivate::add_edges(TNode source, TNode dest) {
2056   vector<TNode> V;
2057   V.push_back(dest);
2058   add_edges(source, V);
2059 }
2060
2061 void TheorySetsPrivate::add_edges(TNode source, TNode dest1, TNode dest2) {
2062   vector<TNode> V;
2063   V.push_back(dest1);
2064   V.push_back(dest2);
2065   add_edges(source, V);
2066 }
2067
2068 void TheorySetsPrivate::add_edges(TNode source, TNode dest1, TNode dest2, TNode dest3) {
2069   vector<TNode> V;
2070   V.push_back(dest1);
2071   V.push_back(dest2);
2072   V.push_back(dest3);
2073   add_edges(source, V);
2074 }
2075
2076 void TheorySetsPrivate::add_edges(TNode source, const std::vector<TNode>& dests) {
2077
2078   if(Debug.isOn("sets-graph-details")) {
2079     Debug("sets-graph-details") << "[sets-graph-details] add_edges " << source
2080                                 << "  [";
2081     BOOST_FOREACH(TNode v, dests) {
2082       Debug("sets-graph-details") << v << ", ";
2083       Assert(d_V.find(v) != d_V.end());
2084     }
2085     Debug("sets-graph-details") << "]" << std::endl;
2086   }
2087
2088   Assert(d_E.find(source) == d_E.end());
2089   if(dests.size() == 1 && dests[0] == source) {
2090     return;
2091   }
2092   d_E.insert(source, dests);
2093 }
2094
2095
2096 void TheorySetsPrivate::add_node(TNode vertex) {
2097   NodeManager* nm = NodeManager::currentNM();
2098   Debug("sets-graph-details") << "[sets-graph-details] add_node " << vertex << std::endl;
2099   if(d_V.find(vertex) == d_V.end()) {
2100     d_V.insert(vertex);
2101     Kind k = vertex.getKind();
2102     if(k == kind::SINGLETON) {
2103       // newLemmaGenerated = true;
2104       lemma(nm->mkNode(kind::EQUAL,
2105                        nm->mkNode(kind::CARD, vertex),
2106                        nm->mkConst(Rational(1))),
2107             SETS_LEMMA_OTHER);
2108     } else if(k != kind::EMPTYSET) {
2109       // newLemmaGenerated = true;
2110       lemma(nm->mkNode(kind::GEQ,
2111                        nm->mkNode(kind::CARD, vertex),
2112                        nm->mkConst(Rational(0))),
2113             SETS_LEMMA_OTHER);
2114     }
2115     d_statistics.d_numVerticesMax.maxAssign(d_V.size());
2116   }
2117   d_equalityEngine.addTerm(vertex);
2118   d_termInfoManager->addTerm(vertex);
2119 }
2120
2121 std::set<TNode> TheorySetsPrivate::non_empty(std::set<TNode> vertices)
2122 {
2123   std::set<TNode> ret;
2124   NodeManager* nm = NodeManager::currentNM();
2125   BOOST_FOREACH(TNode vertex, vertices) {
2126     Node emptySet = nm->mkConst<EmptySet>(EmptySet(nm->toType(vertex.getType())));
2127     if(!d_equalityEngine.areEqual(vertex, emptySet)) {
2128       ret.insert(vertex);
2129     }
2130   }
2131   return ret;
2132 }
2133
2134 std::set<TNode> TheorySetsPrivate::get_leaves(Node vertex) {
2135   Debug("sets-graph-details") << "[sets-graph-details] get_leaves " << vertex << std::endl;
2136   std::set<TNode> a;
2137   Assert(d_V.find(vertex) != d_V.end());
2138   if(d_E.find(vertex) != d_E.end()) {
2139     Assert(d_E[vertex].get().size() > 0);
2140     BOOST_FOREACH(TNode v , d_E[vertex].get()) {
2141       std::set<TNode> s = get_leaves(v);
2142       a.insert(s.begin(), s.end());
2143     }
2144   } else {
2145     a.insert(vertex);
2146   }
2147   // a = non_empty(a);
2148   return a;
2149 }
2150
2151 std::set<TNode> TheorySetsPrivate::get_leaves(Node vertex1, Node vertex2) {
2152   std::set<TNode> s = get_leaves(vertex1);
2153   std::set<TNode> t = get_leaves(vertex2);
2154   t.insert(s.begin(), s.end());
2155   return t;
2156 }
2157
2158 std::set<TNode> TheorySetsPrivate::get_leaves(Node vertex1, Node vertex2, Node vertex3) {
2159   std::set<TNode> s = get_leaves(vertex1);
2160   std::set<TNode> t = get_leaves(vertex2);
2161   std::set<TNode> u = get_leaves(vertex3);
2162   t.insert(s.begin(), s.end());
2163   t.insert(u.begin(), u.end());
2164   return t;
2165 }
2166
2167 Node TheorySetsPrivate::eqemptySoFar() {
2168   std::vector<Node> V;
2169
2170   for(typeof(d_V.begin()) it = d_V.begin(); it != d_V.end(); ++it) {
2171     Node rep = d_equalityEngine.getRepresentative(*it);
2172     if(rep.getKind() == kind::EMPTYSET) {
2173       V.push_back(EQUAL(rep, (*it)));
2174     }
2175   }
2176
2177   if(V.size() == 0) {
2178     return d_trueNode;
2179   } else if(V.size() == 1) {
2180     return V[0];
2181   } else {
2182     NodeManager* nm = NodeManager::currentNM();
2183     return nm->mkNode(kind::AND, V);
2184   }
2185 }
2186
2187
2188 void TheorySetsPrivate::merge_nodes(std::set<TNode> leaves1, std::set<TNode> leaves2, Node reason) {
2189   CodeTimer codeTimer(d_statistics.d_mergeTime);
2190
2191   NodeManager* nm = NodeManager::currentNM();
2192
2193   // do non-empty reasoning stuff
2194   std::vector<TNode> leaves1_nonempty, leaves2_nonempty;
2195   BOOST_FOREACH(TNode l, leaves1) {
2196     Node emptySet = nm->mkConst<EmptySet>(EmptySet(nm->toType(l.getType())));
2197     if(d_equalityEngine.getRepresentative(l).getKind() != kind::EMPTYSET) {
2198       leaves1_nonempty.push_back(l);
2199     } else {
2200       // reason = nm->mkNode(kind::AND, reason, EQUAL(l, emptySet));
2201     }
2202   }
2203   BOOST_FOREACH(TNode l, leaves2) {
2204     Node emptySet = nm->mkConst<EmptySet>(EmptySet(nm->toType(l.getType())));
2205     if(d_equalityEngine.getRepresentative(l).getKind() != kind::EMPTYSET) {
2206       leaves2_nonempty.push_back(l);
2207     } else {
2208       // reason = nm->mkNode(kind::AND, reason, EQUAL(l, emptySet));
2209     }
2210   }
2211
2212   // last minute stuff
2213   reason = nm->mkNode(kind::AND, reason, eqemptySoFar());
2214
2215   Trace("sets-graph-merge") << "[sets-graph-merge] merge_nodes(..,.., " << reason << ")"
2216                             << std::endl;
2217   print_graph();
2218   Trace("sets-graph") << std::endl;
2219
2220   std::set<TNode> leaves3, leaves4;
2221   std::set_difference(leaves1_nonempty.begin(), leaves1_nonempty.end(),
2222                       leaves2_nonempty.begin(), leaves2_nonempty.end(),
2223                       std::inserter(leaves3, leaves3.begin()));
2224   std::set_difference(leaves2_nonempty.begin(), leaves2_nonempty.end(),
2225                       leaves1_nonempty.begin(), leaves1_nonempty.end(),
2226                       std::inserter(leaves4, leaves4.begin()));
2227
2228   if(leaves3.size() == 0) {
2229     Trace("sets-graph-merge") << "[sets-graph-merge]  Merge Equality 1" << std::endl;
2230     // make everything in leaves4 empty
2231     BOOST_FOREACH(TNode v , leaves4) {
2232       Node zero = nm->mkConst(Rational(0));
2233       if(!d_equalityEngine.hasTerm(zero)) {
2234         d_equalityEngine.addTerm(zero);
2235         d_termInfoManager->addTerm(zero);
2236       }
2237       learnLiteral( /* atom = */ EQUAL(nm->mkNode(kind::CARD, v), zero),
2238                     /* polarity = */ true,
2239                     /* reason = */  reason);
2240     }
2241     ++d_statistics.d_numMergeEq1or2;
2242   } else if(leaves4.size() == 0) {
2243     Trace("sets-graph-merge") << "[sets-graph-merge]  Merge Equality 2" << std::endl;
2244     // make everything in leaves3 empty
2245     BOOST_FOREACH(TNode v , leaves3) {
2246       Node zero = nm->mkConst(Rational(0));
2247       if(!d_equalityEngine.hasTerm(zero)) {
2248         d_equalityEngine.addTerm(zero);
2249         d_termInfoManager->addTerm(zero);
2250       }
2251       learnLiteral( /* atom = */ EQUAL(nm->mkNode(kind::CARD, v), zero),
2252                     /* polarity = */ true,
2253                     /* reason = */  reason);
2254     }
2255     ++d_statistics.d_numMergeEq1or2;
2256   } else {
2257     Trace("sets-graph-merge") << "[sets-graph-merge]  Merge Equality 3" << std::endl;
2258     Trace("sets-graph-merge") << "[sets-graph-merge]    #left= " << leaves1.size()
2259                               << " #right= " << leaves2.size()
2260                               << " #left non-empty= " << leaves1_nonempty.size()
2261                               << " #right non-empty= " << leaves2_nonempty.size()
2262                               << " #left-right= " << leaves3.size()
2263                               << " #right-left= " << leaves4.size() << std::endl;
2264
2265     std::map<TNode, vector<TNode> > children;
2266
2267     // Merge Equality 3
2268     BOOST_FOREACH(TNode l1 , leaves3) {
2269       BOOST_FOREACH(TNode l2 , leaves4) {
2270         Node l1_inter_l2 = nm->mkNode(kind::INTERSECTION, min(l1, l2), max(l1, l2));
2271         l1_inter_l2 = Rewriter::rewrite(l1_inter_l2);
2272         add_node(l1_inter_l2);
2273         children[l1].push_back(l1_inter_l2);
2274         children[l2].push_back(l1_inter_l2);
2275         // if(d_V.find(l1_inter_l2) != d_V.end()) {
2276         //   // This case needs to be handled, currently not
2277         //   Warning() << "This might create a loop. We need to handle this case. Probably merge the two nodes?" << std::endl;
2278         //   Unhandled();
2279         // }
2280       }
2281       ++d_statistics.d_numMergeEq3;
2282     }
2283
2284     for(std::map<TNode, vector<TNode> >::iterator it = children.begin();
2285             it != children.end(); ++it) {
2286       add_edges(it->first, it->second);
2287       Node rhs;
2288       if(it->second.size() == 1) {
2289         rhs = nm->mkNode(kind::CARD, it->second[0]);
2290       } else {
2291         NodeBuilder<> nb(kind::PLUS);
2292         BOOST_FOREACH(TNode n , it->second) {
2293           Node card_n = nm->mkNode(kind::CARD, n);
2294           nb << card_n;
2295         }
2296         rhs = Node(nb);
2297       }
2298       Node lem;
2299       lem = nm->mkNode(kind::EQUAL,
2300                        nm->mkNode(kind::CARD, it->first),
2301                        rhs);
2302       lem = nm->mkNode(kind::IMPLIES, reason, lem);
2303       lem = Rewriter::rewrite(lem);
2304       d_external.d_out->lemma(lem);
2305     }
2306   }
2307
2308   Trace("sets-graph") << std::endl;
2309   print_graph();
2310   Trace("sets-graph") << std::endl;
2311
2312 }
2313
2314 void  TheorySetsPrivate::print_graph() {
2315   std::string tag = "sets-graph";
2316   if(Trace.isOn("sets-graph")) {
2317     Trace(tag) << "[sets-graph] Graph : " << std::endl;
2318     for(typeof(d_V.begin()) it = d_V.begin(); it != d_V.end(); ++it) {
2319       TNode v = *it;
2320       // BOOST_FOREACH(TNode v, d_V) {
2321       Trace(tag) << "[" << tag << "]  " << v << " : ";
2322       // BOOST_FOREACH(TNode w, d_E[v].get()) {
2323       if(d_E.find(v) != d_E.end()) {
2324         BOOST_FOREACH(TNode w, d_E[v].get()) {
2325           Trace(tag) << w << ", ";
2326         }
2327       } else {
2328         Trace(tag) << " leaf. " ;
2329       }
2330       Trace(tag) << std::endl;
2331     }
2332   }
2333
2334   if(Trace.isOn("sets-graph-dot")) {
2335     std::ostringstream oss;
2336     oss << "digraph G { ";
2337     for(typeof(d_V.begin()) it = d_V.begin(); it != d_V.end(); ++it) {
2338       TNode v = *it;
2339       if(d_E.find(v) != d_E.end()) {
2340         BOOST_FOREACH(TNode w, d_E[v].get()) {
2341           //oss << v.getId() << " -> " << w.getId() << "; ";
2342           oss << "\"" << v << "\" -> \"" << w << "\"; ";
2343         }
2344       } else {
2345         oss << "\"" << v << "\";";
2346       }
2347     }
2348     oss << "}";
2349     Trace("sets-graph-dot") << "[sets-graph-dot] " << oss.str() << std::endl;
2350   }
2351 }
2352
2353 Node TheorySetsPrivate::eqSoFar() {
2354   std::vector<Node> V(d_allSetEqualitiesSoFar.begin(), d_allSetEqualitiesSoFar.end());
2355   if(V.size() == 0) {
2356     return d_trueNode;
2357   } else if(V.size() == 1) {
2358     return V[0];
2359   } else {
2360     NodeManager* nm = NodeManager::currentNM();
2361     return nm->mkNode(kind::AND, V);
2362   }
2363 }
2364
2365
2366 void TheorySetsPrivate::guessLeavesEmptyLemmas() {
2367
2368   // Guess leaf nodes being empty or non-empty
2369   NodeManager* nm = NodeManager::currentNM();
2370   leaves.clear();
2371   for(typeof(d_V.begin()) it = d_V.begin(); it != d_V.end(); ++it) {
2372     TNode v = *it;
2373     if(d_E.find(v) == d_E.end()) {
2374       leaves.insert(v);
2375     }
2376   }
2377   d_statistics.d_numLeaves.setData(leaves.size());
2378   d_statistics.d_numLeavesMax.maxAssign(leaves.size());
2379
2380   int
2381     numLeaves = leaves.size(),
2382     numLemmasGenerated = 0,
2383     numLeavesIsEmpty = 0,
2384     numLeavesIsNonEmpty = 0,
2385     numLeavesCurrentlyNonEmpty = 0,
2386     numLemmaAlreadyExisted = 0;
2387
2388   for(typeof(leaves.begin()) it = leaves.begin(); it != leaves.end(); ++it) {
2389     bool generateLemma = true;
2390     Node emptySet = nm->mkConst<EmptySet>(EmptySet(nm->toType((*it).getType())));
2391
2392     if(d_equalityEngine.hasTerm(*it)) {
2393       Node n = d_equalityEngine.getRepresentative(*it);
2394       if(n.getKind() == kind::EMPTYSET) {
2395         ++numLeavesIsEmpty;
2396         continue;
2397       }
2398       if(d_termInfoManager->getMembers(n)->size() > 0) {
2399         ++numLeavesCurrentlyNonEmpty;
2400         continue;
2401       }
2402       if(!d_equalityEngine.hasTerm(emptySet)) {
2403         d_equalityEngine.addTerm(emptySet);
2404       }
2405       if(d_equalityEngine.areDisequal(n, emptySet, false)) {
2406         ++numLeavesIsNonEmpty;
2407         generateLemma = false;
2408       }
2409     }
2410
2411     if(generateLemma) {
2412       Node n = nm->mkNode(kind::EQUAL, (*it), emptySet);
2413       Node lem = nm->mkNode(kind::OR, n, nm->mkNode(kind::NOT, n));
2414       bool lemmaGenerated =
2415         lemma(lem, SETS_LEMMA_GRAPH);
2416       if(lemmaGenerated) {
2417         ++numLemmasGenerated;
2418       } else {
2419         ++numLemmaAlreadyExisted;
2420       }
2421       n = d_external.d_valuation.ensureLiteral(n);
2422       d_external.d_out->requirePhase(n, true);
2423     }
2424
2425   }
2426   Trace("sets-guess-empty")
2427     << "[sets-guess-empty] numLeaves                      = " << numLeaves << std::endl
2428     << "                       numLemmasGenerated         = " << numLemmasGenerated << std::endl
2429     << "                       numLeavesIsEmpty           = " << numLeavesIsEmpty << std::endl
2430     << "                       numLeavesIsNonEmpty        = " << numLeavesIsNonEmpty << std::endl
2431     << "                       numLeavesCurrentlyNonEmpty = " << numLeavesCurrentlyNonEmpty << std::endl
2432     << "                       numLemmaAlreadyExisted     = " << numLemmaAlreadyExisted << std::endl;
2433
2434 }
2435
2436 void TheorySetsPrivate::processCard2(Theory::Effort level) {
2437   CodeTimer codeTimer(d_statistics.d_processCard2Time);
2438
2439   if(level != Theory::EFFORT_FULL) return;
2440
2441   d_statistics.d_numVertices.setData(d_V.size());
2442   d_statistics.d_numVerticesMax.maxAssign(d_V.size());
2443
2444   Trace("sets-card") << "[sets-card] processCard( " << level << ")" << std::endl;
2445   Trace("sets-card") << "[sets-card]   # vertices = " << d_V.size() << std::endl;
2446
2447   NodeManager* nm = NodeManager::currentNM();
2448
2449   // Introduce
2450   for(typeof(d_cardTerms.begin()) it = d_cardTerms.begin();
2451       it != d_cardTerms.end(); ++it) {
2452
2453     for(eq::EqClassIterator j(d_equalityEngine.getRepresentative((*it)[0]), &d_equalityEngine);
2454         !j.isFinished(); ++j) {
2455
2456       Node n = nm->mkNode(kind::CARD, (*j));
2457
2458       if(d_processedCardTerms.find(n) != d_processedCardTerms.end()) {
2459         continue;
2460       }
2461
2462       if(d_relTerms.find(n[0]) == d_relTerms.end()) {
2463         // not relevant, skip
2464         continue;
2465       }
2466
2467       Trace("sets-graph") << std::endl;
2468       print_graph();
2469       Trace("sets-graph") << std::endl;
2470
2471       add_node(n[0]);
2472
2473       Trace("sets-card") << "[sets-card]  Processing " << n << " in eq cl of " << (*it) << std::endl;
2474
2475       d_processedCardTerms.insert(n);
2476
2477       Kind k = n[0].getKind();
2478
2479       if(k == kind::SINGLETON) {
2480         Trace("sets-card") << "[sets-card]  Introduce Singleton " << n[0] << std::endl;
2481         continue;
2482       }
2483
2484       // rest of the processing is for compound terms
2485       if(k != kind::UNION && k != kind::INTERSECTION && k != kind::SETMINUS) {
2486         continue;
2487       }
2488
2489       Trace("sets-card") << "[sets-card]  Introduce Term " << n[0] << std::endl;
2490
2491       Node s = min(n[0][0], n[0][1]);
2492       Node t = max(n[0][0], n[0][1]);
2493       bool isUnion = (k == kind::UNION);
2494       Assert(Rewriter::rewrite(s) == s);
2495       Assert(Rewriter::rewrite(t) == t);
2496
2497       Node sNt = nm->mkNode(kind::INTERSECTION, s, t);
2498       sNt = Rewriter::rewrite(sNt);
2499       Node sMt = nm->mkNode(kind::SETMINUS, s, t);
2500       sMt = Rewriter::rewrite(sMt);
2501       Node tMs = nm->mkNode(kind::SETMINUS, t, s);
2502       tMs = Rewriter::rewrite(tMs);
2503
2504       Node card_s = nm->mkNode(kind::CARD, s);
2505       Node card_t = nm->mkNode(kind::CARD, t);
2506       Node card_sNt = nm->mkNode(kind::CARD, sNt);
2507       Node card_sMt = nm->mkNode(kind::CARD, sMt);
2508       Node card_tMs = nm->mkNode(kind::CARD, tMs);
2509
2510       Node lem;
2511
2512       add_node(sMt);
2513       add_node(sNt);
2514       add_node(tMs);
2515
2516
2517       // for union
2518       if(isUnion) {
2519         if(d_E.find(n[0]) != d_E.end()) {
2520           // do a merge of current leaves of d_E with
2521           // sNT sMT tMs
2522           Trace("sets-card") << "[sets-card] Already found in the graph, merging " << n[0] << std::endl;
2523           merge_nodes(get_leaves(n[0]), get_leaves(sMt, sNt, tMs), eqSoFar());
2524         } else {
2525           add_node(n[0]);
2526
2527           lem = nm->mkNode(kind::EQUAL,
2528                            n,     // card(s union t)
2529                            nm->mkNode(kind::PLUS, card_sNt, card_sMt, card_tMs));
2530           lemma(lem, SETS_LEMMA_GRAPH);
2531
2532           Assert(d_E.find(n[0]) == d_E.end());
2533           add_edges(n[0], sMt, sNt, tMs);
2534         }
2535       }
2536
2537       // for s
2538       if(d_E.find(s) == d_E.end()) {
2539         add_node(s);
2540         add_edges(s, sMt, sNt);
2541
2542         lem = nm->mkNode(kind::EQUAL,
2543                          card_s,
2544                          nm->mkNode(kind::PLUS, card_sNt, card_sMt));
2545         lemma(lem, SETS_LEMMA_GRAPH);
2546       } else {
2547         if(find(d_E[s].get().begin(), d_E[s].get().end(), sMt) != d_E[s].get().end()) {
2548           Assert( find(d_E[s].get().begin(), d_E[s].get().end(), sMt) != d_E[s].get().end() );
2549           Assert( find(d_E[s].get().begin(), d_E[s].get().end(), sNt) != d_E[s].get().end() );
2550           Assert( find(d_E[t].get().begin(), d_E[t].get().end(), tMs) != d_E[t].get().end() );
2551           Assert( find(d_E[t].get().begin(), d_E[t].get().end(), sNt) != d_E[t].get().end() );
2552           continue;
2553         }
2554
2555         Trace("sets-card") << "[sets-card] Already found in the graph, merging " << s << std::endl;
2556         merge_nodes(get_leaves(s), get_leaves(sMt, sNt), eqSoFar());
2557       }
2558
2559       // for t
2560       if(d_E.find(t) == d_E.end()) {
2561         Assert(d_E.find(t) == d_E.end());
2562         add_node(t);
2563         add_edges(t, sNt, tMs);
2564
2565         lem = nm->mkNode(kind::EQUAL,
2566                          card_t,
2567                          nm->mkNode(kind::PLUS, card_sNt, card_tMs));
2568         lemma(lem, SETS_LEMMA_GRAPH);
2569       } else {
2570         // Assert( find(d_E[s].get().begin(), d_E[s].get().end(), sMt) == d_E[s].get().end() );
2571         // Assert( find(d_E[s].get().begin(), d_E[s].get().end(), sNt) == d_E[s].get().end() );
2572         // Assert( find(d_E[t].get().begin(), d_E[t].get().end(), tMs) == d_E[t].get().end() );
2573         // Assert( find(d_E[t].get().begin(), d_E[t].get().end(), sNt) == d_E[t].get().end() );
2574
2575         Trace("sets-card") << "[sets-card] Already found in the graph, merging " << t << std::endl;
2576         merge_nodes(get_leaves(t), get_leaves(sNt, tMs), eqSoFar());
2577       }
2578
2579       if(options::setsSlowLemmas()) {
2580         if(d_newLemmaGenerated) {
2581           break;
2582         } else if(options::setsGuessEmpty() == 0) {
2583           guessLeavesEmptyLemmas();
2584           if(d_newLemmaGenerated) {
2585             return;
2586           }
2587         }
2588       }
2589
2590     }//equivalence class loop
2591
2592     if(options::setsSlowLemmas() && d_newLemmaGenerated) {
2593       break;
2594     }
2595
2596   }//d_cardTerms loop
2597
2598   print_graph();
2599
2600   if(d_newLemmaGenerated) {
2601     Trace("sets-card") << "[sets-card] New introduce done. Returning." << std::endl;
2602     return;
2603   }
2604
2605   if(options::setsGuessEmpty() == 1) {
2606     guessLeavesEmptyLemmas();
2607     if(d_newLemmaGenerated) {
2608       return;
2609     }
2610   }
2611
2612   // Merge equalities from input assertions
2613
2614   while(!d_graphMergesPending.empty()) {
2615     std::pair<TNode,TNode> np = d_graphMergesPending.front();
2616     d_graphMergesPending.pop();
2617
2618     Debug("sets-card") << "[sets-card] Equality " << np.first << " " << np.second << std::endl;
2619     if(np.first.getKind() == kind::EMPTYSET || np.second.getKind() == kind::EMPTYSET) {
2620       Debug("sets-card") << "[sets-card]    skipping merge as one side is empty set" << std::endl;
2621       continue;
2622     }
2623
2624     if(d_V.find(np.first) == d_V.end() || d_V.find(np.second) == d_V.end()) {
2625       Assert((d_V.find(np.first) == d_V.end()));
2626       Assert((d_V.find(np.second) == d_V.end()));
2627       continue;
2628     }
2629     d_allSetEqualitiesSoFar.push_back(EQUAL(np.first, np.second));
2630     // merge_nodes(get_leaves(np.first), get_leaves(np.second), EQUAL(np.first, np.second));
2631     merge_nodes(get_leaves(np.first), get_leaves(np.second), eqSoFar());
2632   }
2633
2634   if(d_newLemmaGenerated) {
2635     Trace("sets-card") << "[sets-card] New merge done. Returning." << std::endl;
2636     return;
2637   }
2638
2639   leaves.clear();
2640   for(typeof(d_V.begin()) it = d_V.begin(); it != d_V.end(); ++it) {
2641     TNode v = *it;
2642     if(d_E.find(v) == d_E.end()) {
2643       leaves.insert(v);
2644     }
2645   }
2646   Trace("sets-card") << "[sets-card] # leaves = " << leaves.size() << std::endl;
2647   d_statistics.d_numLeaves.setData(leaves.size());
2648   d_statistics.d_numLeavesMax.maxAssign(leaves.size());
2649
2650   Assert(!d_newLemmaGenerated);
2651
2652
2653   if(options::setsGuessEmpty() == 2) {
2654     guessLeavesEmptyLemmas();
2655     if(d_newLemmaGenerated) {
2656       return;
2657     }
2658   }
2659
2660   // Elements being either equal or disequal [Members Arrangement rule]
2661   Trace("sets-card") << "[sets-card] Processing elements equality/disequal to each other" << std::endl;
2662   for(typeof(leaves.begin()) it = leaves.begin();
2663       it != leaves.end(); ++it) {
2664     if(!d_equalityEngine.hasTerm(*it)) continue;
2665     Node n = d_equalityEngine.getRepresentative(*it);
2666     Assert(n.getKind() == kind::EMPTYSET || leaves.find(n) != leaves.end());
2667     if(n != *it) continue;
2668     const CDTNodeList* l = d_termInfoManager->getMembers(*it);
2669     std::set<TNode> elems;
2670     for(typeof(l->begin()) l_it = l->begin(); l_it != l->end(); ++l_it) {
2671       elems.insert(d_equalityEngine.getRepresentative(*l_it));
2672     }
2673     for(typeof(elems.begin()) e1_it = elems.begin(); e1_it != elems.end(); ++e1_it) {
2674       for(typeof(elems.begin()) e2_it = elems.begin(); e2_it != elems.end(); ++e2_it) {
2675         if(*e1_it == *e2_it) continue;
2676         if(!d_equalityEngine.areDisequal(*e1_it, *e2_it, false)) {
2677           Node lem = nm->mkNode(kind::EQUAL, *e1_it, *e2_it);
2678           lem = nm->mkNode(kind::OR, lem, nm->mkNode(kind::NOT, lem));
2679           lemma(lem, SETS_LEMMA_GRAPH);
2680         }
2681       }
2682     }
2683   }
2684
2685   if(d_newLemmaGenerated) {
2686     Trace("sets-card") << "[sets-card] Members arrangments lemmas. Returning." << std::endl;
2687     return;
2688   }
2689
2690   // Assert Lower bound
2691   Trace("sets-card") << "[sets-card] Processing assert lower bound" << std::endl;
2692   for(typeof(leaves.begin()) it = leaves.begin();
2693       it != leaves.end(); ++it) {
2694     Trace("sets-cardlower") << "[sets-cardlower] Card Lower: " << *it << std::endl;
2695     Assert(d_equalityEngine.hasTerm(*it));
2696     Node n = d_equalityEngine.getRepresentative(*it);
2697     // Node n = (*it);
2698     // if(!d_equalityEngine.hasTerm(n)) {
2699     //   Trace("sets-cardlower") << "[sets-cardlower]   not in EE" << std::endl;
2700     //   continue;
2701     // }
2702     // Assert(n.getKind() == kind::EMPTYSET || leaves.find(n) != leaves.end()); // ????
2703     // if(n != *it) continue;
2704     const CDTNodeList* l = d_termInfoManager->getMembers(n);
2705     std::set<TNode> elems;
2706     for(typeof(l->begin()) l_it = l->begin(); l_it != l->end(); ++l_it) {
2707       elems.insert(d_equalityEngine.getRepresentative(*l_it));
2708     }
2709     if(elems.size() == 0) continue;
2710     NodeBuilder<> nb(kind::OR);
2711     nb << ( nm->mkNode(kind::LEQ, nm->mkConst(Rational(elems.size())), nm->mkNode(kind::CARD, *it)) );
2712     if(elems.size() > 1) {
2713       for(typeof(elems.begin()) e1_it = elems.begin(); e1_it != elems.end(); ++e1_it) {
2714         for(typeof(elems.begin()) e2_it = elems.begin(); e2_it != elems.end(); ++e2_it) {
2715           if(*e1_it == *e2_it) continue;
2716           nb << (nm->mkNode(kind::EQUAL, *e1_it, *e2_it));
2717         }
2718       }
2719     }
2720     for(typeof(elems.begin()) e_it = elems.begin(); e_it != elems.end(); ++e_it) {
2721       nb << nm->mkNode(kind::NOT, nm->mkNode(kind::MEMBER, *e_it, *it));
2722     }
2723     Node lem = Node(nb);
2724     // if(d_cardLowerLemmaCache.find(lem) == d_cardLowerLemmaCache.end()) {
2725     Trace("sets-card") << "[sets-card] Card Lower: " << lem << std::endl;
2726     lemma(lem, SETS_LEMMA_GRAPH);
2727     // d_cardLowerLemmaCache.insert(lem);
2728     // }
2729   }
2730 }
2731
2732
2733
2734 }/* CVC4::theory::sets namespace */
2735 }/* CVC4::theory namespace */
2736 }/* CVC4 namespace */