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 "theory/sets/theory_sets.h"
  18 #include "theory/sets/theory_sets_private.h"
  19
  20 #include "theory/sets/options.h"
  21 #include "theory/sets/expr_patterns.h" // ONLY included here
  22
  23 #include "util/result.h"
  24
  25 using namespace std;
  26 using namespace CVC4::expr::pattern;
  27
  28 namespace CVC4 {
  29 namespace theory {
  30 namespace sets {
  31
  32 const char* element_of_str = " \u2208 ";
  33
  34 /**************************** TheorySetsPrivate *****************************/
  35 /**************************** TheorySetsPrivate *****************************/
  36 /**************************** TheorySetsPrivate *****************************/
  37
  38 void TheorySetsPrivate::check(Theory::Effort level) {
  39
  40   CodeTimer checkCodeTimer(d_statistics.d_checkTime);
  41
  42   while(!d_external.done() && !d_conflict) {
  43     // Get all the assertions
  44     Assertion assertion = d_external.get();
  45     TNode fact = assertion.assertion;
  46
  47     Debug("sets") << "\n\n[sets] TheorySetsPrivate::check(): processing "
  48                   << fact << std::endl;
  49
  50     bool polarity = fact.getKind() != kind::NOT;
  51     TNode atom = polarity ? fact : fact[0];
  52
  53     // Solve each
  54     switch(atom.getKind()) {
  55     case kind::EQUAL:
  56       Debug("sets") << atom[0] << " should " << (polarity ? "":"NOT ")
  57                     << "be equal to " << atom[1] << std::endl;
  58       assertEquality(fact, fact, /* learnt = */ false);
  59       break;
  60
  61     case kind::IN:
  62       Debug("sets") << atom[0] << " should " << (polarity ? "":"NOT ")
  63                     << "be in " << atom[1] << std::endl;
  64       assertMemebership(fact, fact, /* learnt = */ false);
  65       break;
  66
  67     default:
  68       Unhandled(fact.getKind());
  69     }
  70     finishPropagation();
  71
  72     Debug("sets") << "[sets]  in conflict = " << d_conflict << std::endl;
  73
  74     if(d_conflict && !d_equalityEngine.consistent()) return;
  75     Assert(!d_conflict);
  76     Assert(d_equalityEngine.consistent());
  77   }
  78
  79   Debug("sets") << "[sets]  is complete = " << isComplete() << std::endl;
  80
  81   if( (Theory::EFFORT_FULL || options::setsEagerLemmas() ) && !isComplete()) {
  82     d_external.d_out->lemma(getLemma());
  83   }
  84
  85   return;
  86 }/* TheorySetsPrivate::check() */
  87
  88
  89 void TheorySetsPrivate::assertEquality(TNode fact, TNode reason, bool learnt)
  90 {
  91   Debug("sets-assert") << "\n[sets-assert] adding equality: " << fact
  92                     << ", " << reason
  93                     << ", " << learnt << std::endl;
  94
  95   bool polarity = fact.getKind() != kind::NOT;
  96   TNode atom = polarity ? fact : fact[0];
  97
  98   // fact already holds
  99   if( holds(atom, polarity) ) {
 100     Debug("sets-assert") << "[sets-assert]   already present, skipping" << std::endl;
 101     return;
 102   }
 103
 104   // assert fact & check for conflict
 105   if(learnt) {
 106     registerReason(reason, /*save=*/ true);
 107   }
 108   d_equalityEngine.assertEquality(atom, polarity, reason);
 109
 110   if(!d_equalityEngine.consistent()) {
 111     Debug("sets-assert") << "[sets-assert]   running into a conflict" << std::endl;
 112     d_conflict = true;
 113     return;
 114   }
 115
 116   if(!polarity && atom[0].getType().isSet()) {
 117     addToPending(atom);
 118   }
 119
 120 }/* TheorySetsPrivate::assertEquality() */
 121
 122
 123 void TheorySetsPrivate::assertMemebership(TNode fact, TNode reason, bool learnt)
 124 {
 125   Debug("sets-assert") << "\n[sets-assert] adding membership: " << fact
 126                        << ", " << reason
 127                        << ", " << learnt << std::endl;
 128
 129   bool polarity = fact.getKind() == kind::NOT ? false : true;
 130   TNode atom = polarity ? fact : fact[0];
 131
 132   // fact already holds
 133   if( holds(atom, polarity) ) {
 134     Debug("sets-assert") << "[sets-assert]   already present, skipping" << std::endl;
 135     return;
 136   }
 137
 138   // assert fact & check for conflict
 139   if(learnt) {
 140     registerReason(reason, true);
 141   }
 142   d_equalityEngine.assertPredicate(atom, polarity, reason);
 143
 144   if(!d_equalityEngine.consistent()) {
 145     Debug("sets-assert") << "[sets-assert]   running into a conflict" << std::endl;
 146     d_conflict = true;
 147     return;
 148   }
 149
 150   // update term info data structures
 151   d_termInfoManager->notifyMembership(fact);
 152
 153   // propagation
 154   TNode x = d_equalityEngine.getRepresentative(atom[0]);
 155   eq::EqClassIterator j(d_equalityEngine.getRepresentative(atom[1]),
 156                         &d_equalityEngine);
 157   TNode S = (*j);
 158   Node cur_atom = IN(x, S);
 159
 160   /**
 161    * It is sufficient to do emptyset propagation outside the loop as
 162    * constant term is guaranteed to be class representative.
 163    */
 164   if(polarity && S.getKind() == kind::EMPTYSET) {
 165     Debug("sets-prop") << "[sets-prop]  something in empty set? conflict."
 166                        << std::endl;
 167     learnLiteral(cur_atom, false, cur_atom);
 168     Assert(d_conflict);
 169     return;
 170   }
 171
 172   for(; !j.isFinished(); ++j) {
 173     TNode S = (*j);
 174     Node cur_atom = IN(x, S);
 175
 176     // propagation : children
 177     Debug("sets-prop") << "[sets-prop] Propagating 'down' for "
 178                        << x << element_of_str << S << std::endl;
 179     if(S.getKind() == kind::UNION ||
 180        S.getKind() == kind::INTERSECTION ||
 181        S.getKind() == kind::SETMINUS ||
 182        S.getKind() == kind::SET_SINGLETON) {
 183       doSettermPropagation(x, S);
 184       if(d_conflict) return;
 185     }// propagation: children
 186
 187
 188     // propagation : parents
 189     Debug("sets-prop") << "[sets-prop] Propagating 'up' for "
 190                        << x << element_of_str << S << std::endl;
 191     const CDTNodeList* parentList = d_termInfoManager->getParents(S);
 192     for(typeof(parentList->begin()) k = parentList->begin();
 193         k != parentList->end(); ++k) {
 194       doSettermPropagation(x, *k);
 195       if(d_conflict) return;
 196     }// propagation : parents
 197
 198
 199   }//j loop
 200
 201 }/* TheorySetsPrivate::assertMemebership() */
 202
 203
 204 void TheorySetsPrivate::doSettermPropagation(TNode x, TNode S)
 205 {
 206   Debug("sets-prop") << "[sets-prop] doSettermPropagation("
 207                      << x << ", " << S << std::endl;
 208
 209   Assert(S.getType().isSet() && S.getType().getSetElementType() == x.getType());
 210
 211   Node literal, left_literal, right_literal;
 212
 213   // axiom: literal <=> left_literal AND right_literal
 214   switch(S.getKind()) {
 215   case kind::INTERSECTION:
 216     literal       =       IN(x, S)      ;
 217     left_literal  =       IN(x, S[0])   ;
 218     right_literal =       IN(x, S[1])   ;
 219     break;
 220   case kind::UNION:
 221     literal       = NOT(  IN(x, S)     );
 222     left_literal  = NOT(  IN(x, S[0])  );
 223     right_literal = NOT(  IN(x, S[1])  );
 224     break;
 225   case kind::SETMINUS:
 226     literal       =       IN(x, S)      ;
 227     left_literal  =       IN(x, S[0])   ;
 228     right_literal = NOT(  IN(x, S[1])  );
 229     break;
 230   case kind::SET_SINGLETON: {
 231     Node atom = IN(x, S);
 232     if(holds(atom, true)) {
 233       learnLiteral(EQUAL(x, S[0]), true, atom);
 234     } else if(holds(atom, false)) {
 235       learnLiteral(EQUAL(x, S[0]), false, NOT(atom));
 236     }
 237     return;
 238   }
 239   default:
 240     Unhandled();
 241   }
 242
 243   Debug("sets-prop-details")
 244     << "[sets-prop-details]   " << literal << " IFF " << left_literal
 245     << " AND " << right_literal << std::endl;
 246
 247   Debug("sets-prop-details")
 248     << "[sets-prop-details]   "
 249     << (holds(literal) ? "yes" : (holds(literal.negate()) ? " no" : " _ "))
 250     << " IFF "
 251     << (holds(left_literal) ? "yes" : (holds(left_literal.negate()) ? "no " : " _ "))
 252     << " AND "
 253     << (holds(right_literal) ? "yes" : (holds(right_literal.negate()) ? "no " : " _ "))
 254     << std::endl;
 255
 256   Assert( present( IN(x, S)    ) ||
 257           present( IN(x, S[0]) ) ||
 258           present( IN(x, S[1]) ) );
 259
 260   if( holds(literal) ) {
 261     // 1a. literal => left_literal
 262     Debug("sets-prop") << "[sets-prop]  ... via case 1a. ..." << std::endl;
 263     learnLiteral(left_literal, literal);
 264     if(d_conflict) return;
 265
 266     // 1b. literal => right_literal
 267     Debug("sets-prop") << "[sets-prop]  ... via case 1b. ..." << std::endl;
 268     learnLiteral(right_literal, literal);
 269     if(d_conflict) return;
 270
 271     // subsumption requirement met, exit
 272     return;
 273   }
 274   else if( holds(literal.negate() ) ) {
 275     // 4. neg(literal), left_literal => neg(right_literal)
 276     if( holds(left_literal) ) {
 277       Debug("sets-prop") << "[sets-prop]  ... via case 4. ..." << std::endl;
 278       learnLiteral(right_literal.negate(), AND( literal.negate(),
 279                                                 left_literal) );
 280       if(d_conflict) return;
 281     }
 282
 283     // 5. neg(literal), right_literal => neg(left_literal)
 284     if( holds(right_literal) ) {
 285       Debug("sets-prop") << "[sets-prop]  ... via case 5. ..." << std::endl;
 286       learnLiteral(left_literal.negate(), AND( literal.negate(),
 287                                                right_literal) );
 288       if(d_conflict) return;
 289     }
 290   }
 291   else {
 292     // 2,3. neg(left_literal) v neg(right_literal) => neg(literal)
 293     if(holds(left_literal.negate())) {
 294       Debug("sets-prop") << "[sets-prop]  ... via case 2. ..." << std::endl;
 295       learnLiteral(literal.negate(), left_literal.negate());
 296       if(d_conflict) return;
 297     }
 298     else if(holds(right_literal.negate())) {
 299       Debug("sets-prop") << "[sets-prop]  ... via case 3. ..." << std::endl;
 300       learnLiteral(literal.negate(), right_literal.negate());
 301       if(d_conflict) return;
 302     }
 303
 304     // 6. the axiom itself:
 305     else if(holds(left_literal) && holds(right_literal)) {
 306       Debug("sets-prop") << "[sets-prop]  ... via case 6. ..." << std::endl;
 307       learnLiteral(literal, AND(left_literal, right_literal) );
 308       if(d_conflict) return;
 309     }
 310   }
 311
 312   // check fulfilling rule
 313   Node n;
 314   switch(S.getKind()) {
 315   case kind::UNION:
 316     if( holds(IN(x, S)) &&
 317         !present( IN(x, S[0]) ) )
 318       addToPending( IN(x, S[0]) );
 319     break;
 320   case kind::SETMINUS: // intentional fallthrough
 321   case kind::INTERSECTION:
 322     if( holds(IN(x, S[0])) &&
 323         !present( IN(x, S[1]) ))
 324       addToPending( IN(x, S[1]) );
 325     break;
 326   default:
 327     Assert(false, "MembershipEngine::doSettermPropagation");
 328   }
 329 }
 330
 331
 332 void TheorySetsPrivate::learnLiteral(TNode atom, bool polarity, Node reason) {
 333   Debug("sets-learn") << "[sets-learn] learnLiteral(" << atom
 334                       << ", " << polarity << ")" << std::endl;
 335
 336   if( holds(atom, polarity) ) {
 337     Debug("sets-learn") << "[sets-learn] \u2514 already known, skipping" << std::endl;
 338     return;
 339   }
 340
 341   if( holds(atom, !polarity) ) {
 342     Debug("sets-learn") << "[sets-learn] \u2514 conflict found" << std::endl;
 343
 344     registerReason(reason, /*save=*/ true);
 345
 346     if(atom.getKind() == kind::EQUAL) {
 347       d_equalityEngine.assertEquality(atom, polarity, reason);
 348     } else {
 349       d_equalityEngine.assertPredicate(atom, polarity, reason);
 350     }
 351     Assert(d_conflict);       // should be marked due to equality engine
 352     return;
 353   }
 354
 355   Assert(atom.getKind() == kind::EQUAL || atom.getKind() == kind::IN);
 356
 357   Node learnt_literal = polarity ? Node(atom) : NOT(atom);
 358   d_propagationQueue.push_back( make_pair(learnt_literal, reason) );
 359 }
 360
 361 /********************** Helper functions ***************************/
 362 /********************** Helper functions ***************************/
 363 /********************** Helper functions ***************************/
 364
 365 Node mkAnd(const std::vector<TNode>& conjunctions) {
 366   Assert(conjunctions.size() > 0);
 367
 368   std::set<TNode> all;
 369
 370   for (unsigned i = 0; i < conjunctions.size(); ++i) {
 371     TNode t = conjunctions[i];
 372
 373     if (t.getKind() == kind::AND) {
 374       for(TNode::iterator child_it = t.begin();
 375           child_it != t.end(); ++child_it) {
 376         Assert((*child_it).getKind() != kind::AND);
 377         all.insert(*child_it);
 378       }
 379     }
 380     else {
 381       all.insert(t);
 382     }
 383
 384   }
 385
 386   Assert(all.size() > 0);
 387
 388   if (all.size() == 1) {
 389     // All the same, or just one
 390     return conjunctions[0];
 391   }
 392
 393   NodeBuilder<> conjunction(kind::AND);
 394   std::set<TNode>::const_iterator it = all.begin();
 395   std::set<TNode>::const_iterator it_end = all.end();
 396   while (it != it_end) {
 397     conjunction << *it;
 398     ++ it;
 399   }
 400
 401   return conjunction;
 402 }/* mkAnd() */
 403
 404
 405 TheorySetsPrivate::Statistics::Statistics() :
 406   d_checkTime("theory::sets::time") {
 407   StatisticsRegistry::registerStat(&d_checkTime);
 408 }
 409
 410
 411 TheorySetsPrivate::Statistics::~Statistics() {
 412   StatisticsRegistry::unregisterStat(&d_checkTime);
 413 }
 414
 415
 416 bool TheorySetsPrivate::present(TNode atom) {
 417   return holds(atom) || holds(atom.notNode());
 418 }
 419
 420
 421 bool TheorySetsPrivate::holds(TNode atom, bool polarity) {
 422   Node polarity_atom = NodeManager::currentNM()->mkConst<bool>(polarity);
 423
 424   Node atomModEq = NodeManager::currentNM()->mkNode
 425     (atom.getKind(), d_equalityEngine.getRepresentative(atom[0]),
 426      d_equalityEngine.getRepresentative(atom[1]) );
 427
 428   d_equalityEngine.addTerm(atomModEq);
 429
 430   return d_equalityEngine.areEqual(atomModEq, polarity_atom);
 431 }
 432
 433
 434 void TheorySetsPrivate::registerReason(TNode reason, bool save)
 435 {
 436   if(save) d_nodeSaver.insert(reason);
 437
 438   if(reason.getKind() == kind::AND) {
 439     Assert(reason.getNumChildren() == 2);
 440     registerReason(reason[0], false);
 441     registerReason(reason[1], false);
 442   } else if(reason.getKind() == kind::NOT) {
 443     registerReason(reason[0], false);
 444   } else if(reason.getKind() == kind::IN) {
 445     d_equalityEngine.addTerm(reason);
 446     Assert(present(reason));
 447   } else if(reason.getKind() == kind::EQUAL) {
 448     d_equalityEngine.addTerm(reason);
 449     Assert(present(reason));
 450   } else if(reason.getKind() == kind::CONST_BOOLEAN) {
 451     // That's OK, already in EqEngine
 452   } else {
 453     Unhandled();
 454   }
 455 }
 456
 457 void TheorySetsPrivate::finishPropagation()
 458 {
 459   while(!d_conflict && !d_settermPropagationQueue.empty()) {
 460     std::pair<TNode,TNode> np = d_settermPropagationQueue.front();
 461     d_settermPropagationQueue.pop();
 462     doSettermPropagation(np.first, np.second);
 463   }
 464   while(!d_conflict && !d_propagationQueue.empty()) {
 465     std::pair<Node,Node> np = d_propagationQueue.front();
 466     d_propagationQueue.pop();
 467     TNode atom = np.first.getKind() == kind::NOT ? np.first[0] : np.first;
 468     if(atom.getKind() == kind::IN) {
 469       assertMemebership(np.first, np.second, /* learnt = */ true);
 470     } else {
 471       assertEquality(np.first, np.second, /* learnt = */ true);
 472     }
 473   }
 474 }
 475
 476 void TheorySetsPrivate::addToPending(Node n) {
 477   if(d_pendingEverInserted.find(n) == d_pendingEverInserted.end()) {
 478     if(n.getKind() == kind::IN) {
 479       d_pending.push(n);
 480     } else {
 481       Assert(n.getKind() == kind::EQUAL);
 482       d_pendingDisequal.push(n);
 483     }
 484     d_pendingEverInserted.insert(n);
 485   }
 486 }
 487
 488 bool TheorySetsPrivate::isComplete() {
 489   while(!d_pending.empty() && present(d_pending.front()))
 490     d_pending.pop();
 491   return d_pending.empty() && d_pendingDisequal.empty();
 492 }
 493
 494 Node TheorySetsPrivate::getLemma() {
 495   Assert(!d_pending.empty() || !d_pendingDisequal.empty());
 496
 497   Node lemma;
 498
 499   if(!d_pending.empty()) {
 500     Node n = d_pending.front();
 501     d_pending.pop();
 502
 503     Assert(!present(n));
 504     Assert(n.getKind() == kind::IN);
 505
 506     lemma = OR(n, NOT(n));
 507   } else {
 508     Node n = d_pendingDisequal.front();
 509     d_pendingDisequal.pop();
 510
 511     Assert(n.getKind() == kind::EQUAL && n[0].getType().isSet());
 512     Node x = NodeManager::currentNM()->mkSkolem("sde_$$", n[0].getType().getSetElementType());
 513     Node l1 = IN(x, n[0]), l2 = IN(x, n[1]);
 514
 515     // d_equalityEngine.addTerm(x);
 516     // d_equalityEngine.addTerm(l1);
 517     // d_equalityEngine.addTerm(l2);
 518     // d_terms.insert(x);
 519
 520     lemma = OR(n, AND(l1, NOT(l2)), AND(NOT(l1), l2));
 521   }
 522
 523   Debug("sets-lemma") << "[sets-lemma] " << lemma << std::endl;
 524
 525   return  lemma;
 526 }
 527
 528
 529 TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
 530                                      context::Context* c,
 531                                      context::UserContext* u):
 532   d_external(external),
 533   d_notify(*this),
 534   d_equalityEngine(d_notify, c, "theory::sets::TheorySetsPrivate"),
 535   d_conflict(c),
 536   d_termInfoManager(NULL),
 537   d_propagationQueue(c),
 538   d_settermPropagationQueue(c),
 539   d_nodeSaver(c),
 540   d_pending(u),
 541   d_pendingDisequal(u),
 542   d_pendingEverInserted(u)
 543 {
 544   d_termInfoManager = new TermInfoManager(*this, c, &d_equalityEngine);
 545
 546   d_equalityEngine.addFunctionKind(kind::UNION);
 547   d_equalityEngine.addFunctionKind(kind::INTERSECTION);
 548   d_equalityEngine.addFunctionKind(kind::SETMINUS);
 549
 550   d_equalityEngine.addFunctionKind(kind::IN);
 551   d_equalityEngine.addFunctionKind(kind::SUBSET);
 552 }/* TheorySetsPrivate::TheorySetsPrivate() */
 553
 554 TheorySetsPrivate::~TheorySetsPrivate()
 555 {
 556   delete d_termInfoManager;
 557 }
 558
 559
 560
 561 void TheorySetsPrivate::propagate(Theory::Effort e)
 562 {
 563   return;
 564 }
 565
 566 bool TheorySetsPrivate::propagate(TNode literal) {
 567   Debug("sets-prop") << " propagate(" << literal  << ")" << std::endl;
 568
 569   // If already in conflict, no more propagation
 570   if (d_conflict) {
 571     Debug("sets-prop") << "TheoryUF::propagate(" << literal << "): already in conflict" << std::endl;
 572     return false;
 573   }
 574
 575   // Propagate out
 576   bool ok = d_external.d_out->propagate(literal);
 577   if (!ok) {
 578     d_conflict = true;
 579   }
 580
 581   return ok;
 582 }/* TheorySetsPropagate::propagate(TNode) */
 583
 584
 585 void TheorySetsPrivate::conflict(TNode a, TNode b)
 586 {
 587   if (a.getKind() == kind::CONST_BOOLEAN) {
 588     d_conflictNode = explain(a.iffNode(b));
 589   } else {
 590     d_conflictNode = explain(a.eqNode(b));
 591   }
 592   d_external.d_out->conflict(d_conflictNode);
 593   Debug("sets") << "[sets] conflict: " << a << " iff " << b
 594                 << ", explaination " << d_conflictNode << std::endl;
 595   d_conflict = true;
 596 }
 597
 598 Node TheorySetsPrivate::explain(TNode literal)
 599 {
 600   Debug("sets") << "TheorySetsPrivate::explain(" << literal << ")"
 601                 << std::endl;
 602
 603   bool polarity = literal.getKind() != kind::NOT;
 604   TNode atom = polarity ? literal : literal[0];
 605   std::vector<TNode> assumptions;
 606
 607   if(atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
 608      d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
 609   } else if(atom.getKind() == kind::IN) {
 610     if( !d_equalityEngine.hasTerm(atom)) {
 611       d_equalityEngine.addTerm(atom);
 612     }
 613     d_equalityEngine.explainPredicate(atom, polarity, assumptions);
 614   } else {
 615     Debug("sets") << "unhandled: " << literal << "; (" << atom << ", "
 616                   << polarity << "); kind" << atom.getKind() << std::endl;
 617     Unhandled();
 618   }
 619
 620   return mkAnd(assumptions);
 621 }
 622
 623 void TheorySetsPrivate::preRegisterTerm(TNode node)
 624 {
 625   Debug("sets") << "TheorySetsPrivate::preRegisterTerm(" << node << ")"
 626                 << std::endl;
 627
 628   switch(node.getKind()) {
 629   case kind::EQUAL:
 630     // TODO: what's the point of this
 631     d_equalityEngine.addTriggerEquality(node);
 632     break;
 633   case kind::IN:
 634     // TODO: what's the point of this
 635     d_equalityEngine.addTriggerPredicate(node);
 636     break;
 637   default:
 638     d_termInfoManager->addTerm(node);
 639     d_equalityEngine.addTriggerTerm(node, THEORY_SETS);
 640     // d_equalityEngine.addTerm(node);
 641   }
 642   if(node.getKind() == kind::SET_SINGLETON) {
 643     Node true_node = NodeManager::currentNM()->mkConst<bool>(true);
 644     learnLiteral(IN(node[0], node), true, true_node);
 645     //intentional fallthrough
 646   }
 647 }
 648
 649
 650
 651 /**************************** eq::NotifyClass *****************************/
 652 /**************************** eq::NotifyClass *****************************/
 653 /**************************** eq::NotifyClass *****************************/
 654
 655
 656 bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool value)
 657 {
 658   Debug("sets-eq") << "[sets-eq] eqNotifyTriggerEquality: equality = " << equality << " value = " << value << std::endl;
 659   if (value) {
 660     return d_theory.propagate(equality);
 661   } else {
 662     // We use only literal triggers so taking not is safe
 663     return d_theory.propagate(equality.notNode());
 664   }
 665 }
 666
 667 bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value)
 668 {
 669   Debug("sets-eq") << "[sets-eq] eqNotifyTriggerPredicate: predicate = " << predicate << " value = " << value << std::endl;
 670   if (value) {
 671     return d_theory.propagate(predicate);
 672   } else {
 673     return d_theory.propagate(predicate.notNode());
 674   }
 675 }
 676
 677 bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value)
 678 {
 679   Debug("sets-eq") << "[sets-eq] eqNotifyTriggerTermEquality: tag = " << tag << " t1 = " << t1 << "  t2 = " << t2 << "  value = " << value << std::endl;
 680   if(value) {
 681     d_theory.d_termInfoManager->mergeTerms(t1, t2);
 682   }
 683   return true;
 684 }
 685
 686 void TheorySetsPrivate::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2)
 687 {
 688   Debug("sets-eq") << "[sets-eq] eqNotifyConstantTermMerge " << " t1 = " << t1 << " t2 = " << t2 << std::endl;
 689   d_theory.conflict(t1, t2);
 690 }
 691
 692 void TheorySetsPrivate::NotifyClass::eqNotifyNewClass(TNode t)
 693 {
 694   Debug("sets-eq") << "[sets-eq] eqNotifyNewClass:" << " t = " << t << std::endl;
 695 }
 696
 697 void TheorySetsPrivate::NotifyClass::eqNotifyPreMerge(TNode t1, TNode t2)
 698 {
 699   Debug("sets-eq") << "[sets-eq] eqNotifyPreMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl;
 700 }
 701
 702 void TheorySetsPrivate::NotifyClass::eqNotifyPostMerge(TNode t1, TNode t2)
 703 {
 704   Debug("sets-eq") << "[sets-eq] eqNotifyPostMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl;
 705 }
 706
 707 void TheorySetsPrivate::NotifyClass::eqNotifyDisequal(TNode t1, TNode t2, TNode reason)
 708 {
 709   Debug("sets-eq") << "[sets-eq] eqNotifyDisequal:" << " t1 = " << t1 << " t2 = " << t2 << " reason = " << reason << std::endl;
 710 }
 711
 712
 713 /**************************** TermInfoManager *****************************/
 714 /**************************** TermInfoManager *****************************/
 715 /**************************** TermInfoManager *****************************/
 716
 717 void TheorySetsPrivate::TermInfoManager::mergeLists
 718 (CDTNodeList* la, const CDTNodeList* lb) const {
 719   // straight from theory/arrays/array_info.cpp
 720   std::set<TNode> temp;
 721   CDTNodeList::const_iterator it;
 722   for(it = la->begin() ; it != la->end(); it++ ) {
 723     temp.insert((*it));
 724   }
 725
 726   for(it = lb->begin() ; it!= lb->end(); it++ ) {
 727     if(temp.count(*it) == 0) {
 728       la->push_back(*it);
 729     }
 730   }
 731 }
 732
 733 TheorySetsPrivate::TermInfoManager::TermInfoManager
 734 (TheorySetsPrivate& theory, context::Context* satContext, eq::EqualityEngine* eq):
 735   d_theory(theory),
 736   d_context(satContext),
 737   d_eqEngine(eq),
 738   d_terms(satContext),
 739   d_info()
 740 { }
 741
 742 TheorySetsPrivate::TermInfoManager::~TermInfoManager() {
 743   for( typeof(d_info.begin()) it = d_info.begin();
 744        it != d_info.end(); ++it) {
 745     delete (*it).second;
 746   }
 747 }
 748
 749 void TheorySetsPrivate::TermInfoManager::notifyMembership(TNode fact) {
 750   bool polarity = fact.getKind() != kind::NOT;
 751   TNode atom = polarity ? fact : fact[0];
 752
 753   TNode x = d_eqEngine->getRepresentative(atom[0]);
 754   TNode S = d_eqEngine->getRepresentative(atom[1]);
 755
 756   Debug("sets-terminfo") << "[sets-terminfo] Adding membership " << x
 757                          << " in " << S << " " << polarity << std::endl;
 758
 759   d_info[S]->addToElementList(x, polarity);
 760 }
 761
 762 const CDTNodeList* TheorySetsPrivate::TermInfoManager::getParents(TNode x) {
 763   return d_info[x]->parents;
 764 }
 765
 766 void TheorySetsPrivate::TermInfoManager::addTerm(TNode n) {
 767   unsigned numChild = n.getNumChildren();
 768
 769   if(!d_terms.contains(n)) {
 770     d_terms.insert(n);
 771     d_info[n] = new TheorySetsTermInfo(d_context);
 772   }
 773
 774   if(n.getKind() == kind::UNION ||
 775      n.getKind() == kind::INTERSECTION ||
 776      n.getKind() == kind::SETMINUS ||
 777      n.getKind() == kind::SET_SINGLETON) {
 778
 779     for(unsigned i = 0; i < numChild; ++i) {
 780       if(d_terms.contains(n[i])) {
 781         Debug("sets-parent") << "Adding " << n << " to parent list of "
 782                              << n[i] << std::endl;
 783         d_info[n[i]]->parents->push_back(n);
 784       }
 785     }
 786
 787   }
 788 }
 789
 790 void TheorySetsPrivate::TermInfoManager::pushToSettermPropagationQueue
 791 (CDTNodeList* l, TNode S, bool polarity)
 792 {
 793   for(typeof(l->begin()) i = l->begin(); i != l->end(); ++i) {
 794     Debug("sets-prop") << "[sets-terminfo]  setterm todo: "
 795                        << IN(*i, d_eqEngine->getRepresentative(S))
 796                        << std::endl;
 797
 798     d_eqEngine->addTerm(IN(d_eqEngine->getRepresentative(*i),
 799                            d_eqEngine->getRepresentative(S)));
 800
 801     for(eq::EqClassIterator j(d_eqEngine->getRepresentative(S), d_eqEngine);
 802         !j.isFinished(); ++j) {
 803
 804       TNode x = (*i);
 805       TNode S = (*j);
 806       Node cur_atom = IN(x, S);
 807
 808       // propagation : empty set
 809       if(polarity && S.getKind() == kind::EMPTYSET) {
 810         Debug("sets-prop") << "[sets-prop]  something in empty set? conflict."
 811                            << std::endl;
 812         d_theory.learnLiteral(cur_atom, false, cur_atom);
 813         return;
 814       }// propagation: empty set
 815
 816       // propagation : children
 817       if(S.getKind() == kind::UNION ||
 818          S.getKind() == kind::INTERSECTION ||
 819          S.getKind() == kind::SETMINUS ||
 820          S.getKind() == kind::SET_SINGLETON) {
 821         d_theory.d_settermPropagationQueue.push_back(std::make_pair(x, S));
 822       }// propagation: children
 823
 824       // propagation : parents
 825       const CDTNodeList* parentList = getParents(S);
 826       for(typeof(parentList->begin()) k = parentList->begin();
 827           k != parentList->end(); ++k) {
 828         d_theory.d_settermPropagationQueue.push_back(std::make_pair(x, *k));
 829       }// propagation : parents
 830
 831
 832     }//j loop
 833
 834   }
 835
 836 }
 837
 838 void TheorySetsPrivate::TermInfoManager::mergeTerms(TNode a, TNode b) {
 839   // merge b into a
 840
 841   if(!a.getType().isSet()) return;
 842
 843   Debug("sets-terminfo") << "[sets-terminfo] Merging (into) a = " << a
 844                          << ", b = " << b << std::endl;
 845   Debug("sets-terminfo") << "[sets-terminfo] reps"
 846                          << ", a: " << d_eqEngine->getRepresentative(a)
 847                          << ", b: " << d_eqEngine->getRepresentative(b)
 848                          << std::endl;
 849
 850   typeof(d_info.begin()) ita = d_info.find(a);
 851   typeof(d_info.begin()) itb = d_info.find(b);
 852
 853   Assert(ita != d_info.end());
 854   Assert(itb != d_info.end());
 855
 856   pushToSettermPropagationQueue( (*ita).second->elementsInThisSet, b, true );
 857   pushToSettermPropagationQueue( (*ita).second->elementsNotInThisSet, b, false );
 858   pushToSettermPropagationQueue( (*itb).second->elementsNotInThisSet, a, false );
 859   pushToSettermPropagationQueue( (*itb).second->elementsInThisSet, a, true );
 860
 861   mergeLists((*ita).second->elementsInThisSet,
 862              (*itb).second->elementsInThisSet);
 863
 864   mergeLists((*ita).second->elementsNotInThisSet,
 865              (*itb).second->elementsNotInThisSet);
 866 }
 867
 868
 869 }/* CVC4::theory::sets namespace */
 870 }/* CVC4::theory namespace */
 871 }/* CVC4 namespace */