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::newSkolem(TypeNode t) {
 764   ostringstream oss;
 765   oss << "sde_" << (++d_skolemCounter);
 766   return NodeManager::currentNM()->mkSkolem(oss.str(), t, "", NodeManager::SKOLEM_EXACT_NAME);
 767 }
 768
 769 Node TheorySetsPrivate::getLemma() {
 770   Assert(!d_pending.empty() || !d_pendingDisequal.empty());
 771
 772   Node n, lemma;
 773
 774   if(!d_pending.empty()) {
 775     n = d_pending.front();
 776     d_pending.pop();
 777     d_pendingEverInserted.insert(n);
 778
 779     Assert(!present(n));
 780     Assert(n.getKind() == kind::MEMBER);
 781
 782     lemma = OR(n, NOT(n));
 783   } else {
 784     n = d_pendingDisequal.front();
 785     d_pendingDisequal.pop();
 786     d_pendingEverInserted.insert(n);
 787
 788     Assert(n.getKind() == kind::EQUAL && n[0].getType().isSet());
 789     Node x = newSkolem( n[0].getType().getSetElementType() );
 790     Node l1 = MEMBER(x, n[0]), l2 = MEMBER(x, n[1]);
 791
 792     lemma = OR(n, AND(l1, NOT(l2)), AND(NOT(l1), l2));
 793   }
 794
 795   Debug("sets-lemma") << "[sets-lemma] Generating for " << n << ", lemma: " << lemma << std::endl;
 796
 797   return  lemma;
 798 }
 799
 800
 801 TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
 802                                      context::Context* c,
 803                                      context::UserContext* u):
 804   d_external(external),
 805   d_notify(*this),
 806   d_equalityEngine(d_notify, c, "theory::sets::TheorySetsPrivate"),
 807   d_conflict(c),
 808   d_termInfoManager(NULL),
 809   d_propagationQueue(c),
 810   d_settermPropagationQueue(c),
 811   d_nodeSaver(c),
 812   d_pending(u),
 813   d_pendingDisequal(u),
 814   d_pendingEverInserted(u),
 815   d_skolemCounter(0),
 816   d_scrutinize(NULL)
 817 {
 818   d_termInfoManager = new TermInfoManager(*this, c, &d_equalityEngine);
 819
 820   d_equalityEngine.addFunctionKind(kind::UNION);
 821   d_equalityEngine.addFunctionKind(kind::INTERSECTION);
 822   d_equalityEngine.addFunctionKind(kind::SETMINUS);
 823
 824   d_equalityEngine.addFunctionKind(kind::MEMBER);
 825   d_equalityEngine.addFunctionKind(kind::SUBSET);
 826
 827   if( Debug.isOn("sets-scrutinize") ) {
 828     d_scrutinize = new TheorySetsScrutinize(this);
 829   }
 830 }/* TheorySetsPrivate::TheorySetsPrivate() */
 831
 832
 833 TheorySetsPrivate::~TheorySetsPrivate()
 834 {
 835   delete d_termInfoManager;
 836   if( Debug.isOn("sets-scrutinize") ) {
 837     Assert(d_scrutinize != NULL);
 838     delete d_scrutinize;
 839   }
 840 }
 841
 842
 843 bool TheorySetsPrivate::propagate(TNode literal) {
 844   Debug("sets-prop") << " propagate(" << literal  << ")" << std::endl;
 845
 846   // If already in conflict, no more propagation
 847   if (d_conflict) {
 848     Debug("sets-prop") << "TheoryUF::propagate(" << literal << "): already in conflict" << std::endl;
 849     return false;
 850   }
 851
 852   // Propagate out
 853   bool ok = d_external.d_out->propagate(literal);
 854   if (!ok) {
 855     d_conflict = true;
 856   }
 857
 858   return ok;
 859 }/* TheorySetsPropagate::propagate(TNode) */
 860
 861
 862 void TheorySetsPrivate::addSharedTerm(TNode n) {
 863   Debug("sets") << "[sets] ThoerySetsPrivate::addSharedTerm( " << n << ")" << std::endl;
 864   d_equalityEngine.addTriggerTerm(n, THEORY_SETS);
 865 }
 866
 867 void TheorySetsPrivate::conflict(TNode a, TNode b)
 868 {
 869   if (a.getKind() == kind::CONST_BOOLEAN) {
 870     d_conflictNode = explain(a.iffNode(b));
 871   } else {
 872     d_conflictNode = explain(a.eqNode(b));
 873   }
 874   d_external.d_out->conflict(d_conflictNode);
 875   Debug("sets") << "[sets] conflict: " << a << " iff " << b
 876                 << ", explaination " << d_conflictNode << std::endl;
 877   d_conflict = true;
 878 }
 879
 880 Node TheorySetsPrivate::explain(TNode literal)
 881 {
 882   Debug("sets") << "TheorySetsPrivate::explain(" << literal << ")"
 883                 << std::endl;
 884
 885   bool polarity = literal.getKind() != kind::NOT;
 886   TNode atom = polarity ? literal : literal[0];
 887   std::vector<TNode> assumptions;
 888
 889   if(atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
 890     d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
 891   } else if(atom.getKind() == kind::MEMBER) {
 892     if( !d_equalityEngine.hasTerm(atom)) {
 893       d_equalityEngine.addTerm(atom);
 894     }
 895     d_equalityEngine.explainPredicate(atom, polarity, assumptions);
 896   } else {
 897     Debug("sets") << "unhandled: " << literal << "; (" << atom << ", "
 898                   << polarity << "); kind" << atom.getKind() << std::endl;
 899     Unhandled();
 900   }
 901
 902   return mkAnd(assumptions);
 903 }
 904
 905 void TheorySetsPrivate::preRegisterTerm(TNode node)
 906 {
 907   Debug("sets") << "TheorySetsPrivate::preRegisterTerm(" << node << ")"
 908                 << std::endl;
 909
 910   switch(node.getKind()) {
 911   case kind::EQUAL:
 912     // TODO: what's the point of this
 913     d_equalityEngine.addTriggerEquality(node);
 914     break;
 915   case kind::MEMBER:
 916     // TODO: what's the point of this
 917     d_equalityEngine.addTriggerPredicate(node);
 918     break;
 919   default:
 920     d_termInfoManager->addTerm(node);
 921     d_equalityEngine.addTriggerTerm(node, THEORY_SETS);
 922     // d_equalityEngine.addTerm(node);
 923   }
 924   if(node.getKind() == kind::SET_SINGLETON) {
 925     Node true_node = NodeManager::currentNM()->mkConst<bool>(true);
 926     learnLiteral(MEMBER(node[0], node), true, true_node);
 927     //intentional fallthrough
 928   }
 929 }
 930
 931
 932
 933 /**************************** eq::NotifyClass *****************************/
 934 /**************************** eq::NotifyClass *****************************/
 935 /**************************** eq::NotifyClass *****************************/
 936
 937
 938 bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool value)
 939 {
 940   Debug("sets-eq") << "[sets-eq] eqNotifyTriggerEquality: equality = " << equality
 941                    << " value = " << value << std::endl;
 942   if (value) {
 943     return d_theory.propagate(equality);
 944   } else {
 945     // We use only literal triggers so taking not is safe
 946     return d_theory.propagate(equality.notNode());
 947   }
 948 }
 949
 950 bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value)
 951 {
 952   Debug("sets-eq") << "[sets-eq] eqNotifyTriggerPredicate: predicate = " << predicate
 953                    << " value = " << value << std::endl;
 954   if (value) {
 955     return d_theory.propagate(predicate);
 956   } else {
 957     return d_theory.propagate(predicate.notNode());
 958   }
 959 }
 960
 961 bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value)
 962 {
 963   Debug("sets-eq") << "[sets-eq] eqNotifyTriggerTermEquality: tag = " << tag
 964                    << " t1 = " << t1 << "  t2 = " << t2 << "  value = " << value << std::endl;
 965   if(value) {
 966     d_theory.d_termInfoManager->mergeTerms(t1, t2);
 967   }
 968   return true;
 969 }
 970
 971 void TheorySetsPrivate::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2)
 972 {
 973   Debug("sets-eq") << "[sets-eq] eqNotifyConstantTermMerge " << " t1 = " << t1 << " t2 = " << t2 << std::endl;
 974   d_theory.conflict(t1, t2);
 975 }
 976
 977 // void TheorySetsPrivate::NotifyClass::eqNotifyNewClass(TNode t)
 978 // {
 979 //   Debug("sets-eq") << "[sets-eq] eqNotifyNewClass:" << " t = " << t << std::endl;
 980 // }
 981
 982 // void TheorySetsPrivate::NotifyClass::eqNotifyPreMerge(TNode t1, TNode t2)
 983 // {
 984 //   Debug("sets-eq") << "[sets-eq] eqNotifyPreMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl;
 985 // }
 986
 987 // void TheorySetsPrivate::NotifyClass::eqNotifyPostMerge(TNode t1, TNode t2)
 988 // {
 989 //   Debug("sets-eq") << "[sets-eq] eqNotifyPostMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl;
 990 // }
 991
 992 // void TheorySetsPrivate::NotifyClass::eqNotifyDisequal(TNode t1, TNode t2, TNode reason)
 993 // {
 994 //   Debug("sets-eq") << "[sets-eq] eqNotifyDisequal:" << " t1 = " << t1 << " t2 = " << t2 << " reason = " << reason << std::endl;
 995 // }
 996
 997
 998 /**************************** TermInfoManager *****************************/
 999 /**************************** TermInfoManager *****************************/
1000 /**************************** TermInfoManager *****************************/
1001
1002 void TheorySetsPrivate::TermInfoManager::mergeLists
1003 (CDTNodeList* la, const CDTNodeList* lb) const {
1004   // straight from theory/arrays/array_info.cpp
1005   std::set<TNode> temp;
1006   CDTNodeList::const_iterator it;
1007   for(it = la->begin() ; it != la->end(); it++ ) {
1008     temp.insert((*it));
1009   }
1010
1011   for(it = lb->begin() ; it!= lb->end(); it++ ) {
1012     if(temp.count(*it) == 0) {
1013       la->push_back(*it);
1014     }
1015   }
1016 }
1017
1018 TheorySetsPrivate::TermInfoManager::TermInfoManager
1019 (TheorySetsPrivate& theory, context::Context* satContext, eq::EqualityEngine* eq):
1020   d_theory(theory),
1021   d_context(satContext),
1022   d_eqEngine(eq),
1023   d_terms(satContext),
1024   d_info()
1025 { }
1026
1027 TheorySetsPrivate::TermInfoManager::~TermInfoManager() {
1028   for( typeof(d_info.begin()) it = d_info.begin();
1029        it != d_info.end(); ++it) {
1030     delete (*it).second;
1031   }
1032 }
1033
1034 void TheorySetsPrivate::TermInfoManager::notifyMembership(TNode fact) {
1035   bool polarity = fact.getKind() != kind::NOT;
1036   TNode atom = polarity ? fact : fact[0];
1037
1038   TNode x = d_eqEngine->getRepresentative(atom[0]);
1039   TNode S = d_eqEngine->getRepresentative(atom[1]);
1040
1041   Debug("sets-terminfo") << "[sets-terminfo] Adding membership " << x
1042                          << " in " << S << " " << polarity << std::endl;
1043
1044   d_info[S]->addToElementList(x, polarity);
1045   d_info[x]->addToSetList(S, polarity);
1046 }
1047
1048 const CDTNodeList* TheorySetsPrivate::TermInfoManager::getParents(TNode x) {
1049   return d_info[x]->parents;
1050 }
1051
1052 void TheorySetsPrivate::TermInfoManager::addTerm(TNode n) {
1053   unsigned numChild = n.getNumChildren();
1054
1055   if(!d_terms.contains(n)) {
1056     d_terms.insert(n);
1057     d_info[n] = new TheorySetsTermInfo(d_context);
1058   }
1059
1060   if(n.getKind() == kind::UNION ||
1061      n.getKind() == kind::INTERSECTION ||
1062      n.getKind() == kind::SETMINUS ||
1063      n.getKind() == kind::SET_SINGLETON) {
1064
1065     for(unsigned i = 0; i < numChild; ++i) {
1066       if(d_terms.contains(n[i])) {
1067         Debug("sets-parent") << "Adding " << n << " to parent list of "
1068                              << n[i] << std::endl;
1069         d_info[n[i]]->parents->push_back(n);
1070       }
1071     }
1072
1073   }
1074 }
1075
1076 void TheorySetsPrivate::TermInfoManager::pushToSettermPropagationQueue
1077 (TNode x, TNode S, bool polarity)
1078 {
1079   Node cur_atom = MEMBER(x, S);
1080
1081   // propagation : empty set
1082   if(polarity && S.getKind() == kind::EMPTYSET) {
1083     Debug("sets-prop") << "[sets-prop]  something in empty set? conflict."
1084                        << std::endl;
1085     d_theory.learnLiteral(cur_atom, false, cur_atom);
1086     return;
1087   }// propagation: empty set
1088
1089   // propagation : children
1090   if(S.getKind() == kind::UNION ||
1091      S.getKind() == kind::INTERSECTION ||
1092      S.getKind() == kind::SETMINUS ||
1093      S.getKind() == kind::SET_SINGLETON) {
1094     d_theory.d_settermPropagationQueue.push_back(std::make_pair(x, S));
1095   }// propagation: children
1096
1097   // propagation : parents
1098   const CDTNodeList* parentList = getParents(S);
1099   for(typeof(parentList->begin()) k = parentList->begin();
1100       k != parentList->end(); ++k) {
1101     d_theory.d_settermPropagationQueue.push_back(std::make_pair(x, *k));
1102   }// propagation : parents
1103
1104 }
1105
1106 void TheorySetsPrivate::TermInfoManager::pushToSettermPropagationQueue
1107 (TNode x, CDTNodeList* l, bool polarity)
1108 {
1109   set<TNode> alreadyProcessed;
1110
1111   BOOST_FOREACH(TNode S, (*l) ) {
1112     Debug("sets-prop") << "[sets-terminfo]  setterm todo: "
1113                        << MEMBER(x, d_eqEngine->getRepresentative(S))
1114                        << std::endl;
1115
1116     TNode repS = d_eqEngine->getRepresentative(S);
1117     if(alreadyProcessed.find(repS) != alreadyProcessed.end()) {
1118       continue;
1119     } else {
1120       alreadyProcessed.insert(repS);
1121     }
1122
1123     d_eqEngine->addTerm(MEMBER(d_eqEngine->getRepresentative(x), repS));
1124
1125     for(eq::EqClassIterator j(d_eqEngine->getRepresentative(S), d_eqEngine);
1126         !j.isFinished(); ++j) {
1127
1128       pushToSettermPropagationQueue(x, *j, polarity);
1129
1130     }//j loop
1131   }
1132 }
1133
1134 void TheorySetsPrivate::TermInfoManager::pushToSettermPropagationQueue
1135 (CDTNodeList* l, TNode S, bool polarity)
1136 {
1137   BOOST_FOREACH(TNode x, (*l) ) {
1138     Debug("sets-prop") << "[sets-terminfo]  setterm todo: "
1139                        << MEMBER(x, d_eqEngine->getRepresentative(S))
1140                        << std::endl;
1141
1142     d_eqEngine->addTerm(MEMBER(d_eqEngine->getRepresentative(x),
1143                                d_eqEngine->getRepresentative(S)));
1144
1145     for(eq::EqClassIterator j(d_eqEngine->getRepresentative(S), d_eqEngine);
1146         !j.isFinished(); ++j) {
1147
1148       pushToSettermPropagationQueue(x, *j, polarity);
1149
1150     }//j loop
1151
1152   }
1153
1154 }
1155
1156
1157
1158 void TheorySetsPrivate::TermInfoManager::mergeTerms(TNode a, TNode b) {
1159   // merge b into a
1160   Debug("sets-terminfo") << "[sets-terminfo] Merging (into) a = " << a
1161                          << ", b = " << b << std::endl;
1162   Debug("sets-terminfo") << "[sets-terminfo] reps"
1163                          << ", a: " << d_eqEngine->getRepresentative(a)
1164                          << ", b: " << d_eqEngine->getRepresentative(b)
1165                          << std::endl;
1166
1167   typeof(d_info.begin()) ita = d_info.find(a);
1168   typeof(d_info.begin()) itb = d_info.find(b);
1169
1170   Assert(ita != d_info.end());
1171   Assert(itb != d_info.end());
1172
1173   /* elements in this sets */
1174   pushToSettermPropagationQueue( (*ita).second->elementsInThisSet, b, true );
1175   pushToSettermPropagationQueue( (*ita).second->elementsNotInThisSet, b, false );
1176   pushToSettermPropagationQueue( (*itb).second->elementsNotInThisSet, a, false );
1177   pushToSettermPropagationQueue( (*itb).second->elementsInThisSet, a, true );
1178   mergeLists((*ita).second->elementsInThisSet,
1179              (*itb).second->elementsInThisSet);
1180   mergeLists((*ita).second->elementsNotInThisSet,
1181              (*itb).second->elementsNotInThisSet);
1182
1183   /* sets containing this element */
1184   // pushToSettermPropagationQueue( b, (*ita).second->setsContainingThisElement, true);
1185   // pushToSettermPropagationQueue( b, (*ita).second->setsNotContainingThisElement, false);
1186   pushToSettermPropagationQueue( a, (*itb).second->setsNotContainingThisElement, false);
1187   pushToSettermPropagationQueue( a, (*itb).second->setsContainingThisElement, true);
1188   mergeLists( (*ita).second->setsContainingThisElement,
1189               (*itb).second->setsContainingThisElement );
1190   mergeLists( (*ita).second->setsNotContainingThisElement,
1191               (*itb).second->setsNotContainingThisElement );
1192 }
1193
1194
1195 }/* CVC4::theory::sets namespace */
1196 }/* CVC4::theory namespace */
1197 }/* CVC4 namespace */