src/theory/sets/theory_sets_private.cpp

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