src/theory/sets/theory_sets_private.cpp

   1 /*********************                                                        */
   2 /*! \file theory_sets_private.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Mudathir Mohamed, Kshitij Bansal
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Sets theory implementation.
  13  **
  14  ** Sets theory implementation.
  15  **/
  16
  17 #include "theory/sets/theory_sets_private.h"
  18
  19 #include <algorithm>
  20
  21 #include "expr/emptyset.h"
  22 #include "expr/node_algorithm.h"
  23 #include "options/sets_options.h"
  24 #include "smt/smt_statistics_registry.h"
  25 #include "theory/sets/normal_form.h"
  26 #include "theory/sets/theory_sets.h"
  27 #include "theory/theory_model.h"
  28 #include "util/result.h"
  29
  30 using namespace std;
  31 using namespace CVC4::kind;
  32
  33 namespace CVC4 {
  34 namespace theory {
  35 namespace sets {
  36
  37 TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
  38                                      context::Context* c,
  39                                      context::UserContext* u)
  40     : d_members(c),
  41       d_deq(c),
  42       d_termProcessed(u),
  43       d_keep(c),
  44       d_full_check_incomplete(false),
  45       d_external(external),
  46       d_state(*this, c, u),
  47       d_im(*this, d_state, c, u),
  48       d_rels(new TheorySetsRels(d_state, d_im, u)),
  49       d_cardSolver(new CardinalityExtension(d_state, d_im, c, u)),
  50       d_rels_enabled(false),
  51       d_card_enabled(false)
  52 {
  53   d_true = NodeManager::currentNM()->mkConst(true);
  54   d_false = NodeManager::currentNM()->mkConst(false);
  55   d_zero = NodeManager::currentNM()->mkConst(Rational(0));
  56 }
  57
  58 TheorySetsPrivate::~TheorySetsPrivate()
  59 {
  60   for (std::pair<const Node, EqcInfo*>& current_pair : d_eqc_info)
  61   {
  62     delete current_pair.second;
  63   }
  64 }
  65
  66 void TheorySetsPrivate::finishInit()
  67 {
  68   d_equalityEngine = d_external.getEqualityEngine();
  69   Assert(d_equalityEngine != nullptr);
  70   d_state.finishInit(d_equalityEngine);
  71 }
  72
  73 void TheorySetsPrivate::eqNotifyNewClass(TNode t)
  74 {
  75   if (t.getKind() == kind::SINGLETON || t.getKind() == kind::EMPTYSET)
  76   {
  77     EqcInfo* e = getOrMakeEqcInfo(t, true);
  78     e->d_singleton = t;
  79   }
  80 }
  81
  82 void TheorySetsPrivate::eqNotifyMerge(TNode t1, TNode t2)
  83 {
  84   if (!d_state.isInConflict())
  85   {
  86     Trace("sets-prop-debug")
  87         << "Merge " << t1 << " and " << t2 << "..." << std::endl;
  88     Node s1, s2;
  89     EqcInfo* e2 = getOrMakeEqcInfo(t2);
  90     if (e2)
  91     {
  92       s2 = e2->d_singleton;
  93       EqcInfo* e1 = getOrMakeEqcInfo(t1);
  94       Trace("sets-prop-debug") << "Merging singletons..." << std::endl;
  95       if (e1)
  96       {
  97         s1 = e1->d_singleton;
  98         if (!s1.isNull() && !s2.isNull())
  99         {
 100           if (s1.getKind() == s2.getKind())
 101           {
 102             Trace("sets-prop") << "Propagate eq inference : " << s1
 103                                << " == " << s2 << std::endl;
 104             // infer equality between elements of singleton
 105             Node exp = s1.eqNode(s2);
 106             Node eq = s1[0].eqNode(s2[0]);
 107             d_keep.insert(exp);
 108             d_keep.insert(eq);
 109             assertFact(eq, exp);
 110           }
 111           else
 112           {
 113             // singleton equal to emptyset, conflict
 114             Trace("sets-prop")
 115                 << "Propagate conflict : " << s1 << " == " << s2 << std::endl;
 116             conflict(s1, s2);
 117             return;
 118           }
 119         }
 120       }
 121       else
 122       {
 123         // copy information
 124         e1 = getOrMakeEqcInfo(t1, true);
 125         e1->d_singleton.set(e2->d_singleton);
 126       }
 127     }
 128     // merge membership list
 129     Trace("sets-prop-debug") << "Copying membership list..." << std::endl;
 130     NodeIntMap::iterator mem_i2 = d_members.find(t2);
 131     if (mem_i2 != d_members.end())
 132     {
 133       NodeIntMap::iterator mem_i1 = d_members.find(t1);
 134       int n_members = 0;
 135       if (mem_i1 != d_members.end())
 136       {
 137         n_members = (*mem_i1).second;
 138       }
 139       for (int i = 0; i < (*mem_i2).second; i++)
 140       {
 141         Assert(i < (int)d_members_data[t2].size()
 142                && d_members_data[t2][i].getKind() == kind::MEMBER);
 143         Node m2 = d_members_data[t2][i];
 144         // check if redundant
 145         bool add = true;
 146         for (int j = 0; j < n_members; j++)
 147         {
 148           Assert(j < (int)d_members_data[t1].size()
 149                  && d_members_data[t1][j].getKind() == kind::MEMBER);
 150           if (d_state.areEqual(m2[0], d_members_data[t1][j][0]))
 151           {
 152             add = false;
 153             break;
 154           }
 155         }
 156         if (add)
 157         {
 158           if (!s1.isNull() && s2.isNull())
 159           {
 160             Assert(m2[1].getType().isComparableTo(s1.getType()));
 161             Assert(d_state.areEqual(m2[1], s1));
 162             Node exp = NodeManager::currentNM()->mkNode(
 163                 kind::AND, m2[1].eqNode(s1), m2);
 164             if (s1.getKind() == kind::SINGLETON)
 165             {
 166               if (s1[0] != m2[0])
 167               {
 168                 Node eq = s1[0].eqNode(m2[0]);
 169                 d_keep.insert(exp);
 170                 d_keep.insert(eq);
 171                 Trace("sets-prop") << "Propagate eq-mem eq inference : " << exp
 172                                    << " => " << eq << std::endl;
 173                 assertFact(eq, exp);
 174               }
 175             }
 176             else
 177             {
 178               // conflict
 179               Trace("sets-prop")
 180                   << "Propagate eq-mem conflict : " << exp << std::endl;
 181               d_state.setConflict(exp);
 182               return;
 183             }
 184           }
 185           if (n_members < (int)d_members_data[t1].size())
 186           {
 187             d_members_data[t1][n_members] = m2;
 188           }
 189           else
 190           {
 191             d_members_data[t1].push_back(m2);
 192           }
 193           n_members++;
 194         }
 195       }
 196       d_members[t1] = n_members;
 197     }
 198   }
 199 }
 200
 201 void TheorySetsPrivate::eqNotifyDisequal(TNode t1, TNode t2, TNode reason)
 202 {
 203   if (t1.getType().isSet())
 204   {
 205     Node eq = t1.eqNode(t2);
 206     if (d_deq.find(eq) == d_deq.end())
 207     {
 208       d_deq[eq] = true;
 209     }
 210   }
 211 }
 212
 213 TheorySetsPrivate::EqcInfo::EqcInfo(context::Context* c) : d_singleton(c) {}
 214
 215 TheorySetsPrivate::EqcInfo* TheorySetsPrivate::getOrMakeEqcInfo(TNode n,
 216                                                                 bool doMake)
 217 {
 218   std::map<Node, EqcInfo*>::iterator eqc_i = d_eqc_info.find(n);
 219   if (eqc_i == d_eqc_info.end())
 220   {
 221     EqcInfo* ei = NULL;
 222     if (doMake)
 223     {
 224       ei = new EqcInfo(d_external.getSatContext());
 225       d_eqc_info[n] = ei;
 226     }
 227     return ei;
 228   }
 229   else
 230   {
 231     return eqc_i->second;
 232   }
 233 }
 234
 235 bool TheorySetsPrivate::areCareDisequal(Node a, Node b)
 236 {
 237   if (d_equalityEngine->isTriggerTerm(a, THEORY_SETS)
 238       && d_equalityEngine->isTriggerTerm(b, THEORY_SETS))
 239   {
 240     TNode a_shared =
 241         d_equalityEngine->getTriggerTermRepresentative(a, THEORY_SETS);
 242     TNode b_shared =
 243         d_equalityEngine->getTriggerTermRepresentative(b, THEORY_SETS);
 244     EqualityStatus eqStatus =
 245         d_external.d_valuation.getEqualityStatus(a_shared, b_shared);
 246     if (eqStatus == EQUALITY_FALSE_AND_PROPAGATED || eqStatus == EQUALITY_FALSE
 247         || eqStatus == EQUALITY_FALSE_IN_MODEL)
 248     {
 249       return true;
 250     }
 251   }
 252   return false;
 253 }
 254
 255 bool TheorySetsPrivate::isMember(Node x, Node s)
 256 {
 257   Assert(d_equalityEngine->hasTerm(s)
 258          && d_equalityEngine->getRepresentative(s) == s);
 259   NodeIntMap::iterator mem_i = d_members.find(s);
 260   if (mem_i != d_members.end())
 261   {
 262     for (int i = 0; i < (*mem_i).second; i++)
 263     {
 264       if (d_state.areEqual(d_members_data[s][i][0], x))
 265       {
 266         return true;
 267       }
 268     }
 269   }
 270   return false;
 271 }
 272
 273 bool TheorySetsPrivate::assertFact(Node fact, Node exp)
 274 {
 275   Trace("sets-assert") << "TheorySets::assertFact : " << fact
 276                        << ", exp = " << exp << std::endl;
 277   bool polarity = fact.getKind() != kind::NOT;
 278   TNode atom = polarity ? fact : fact[0];
 279   if (!d_state.isEntailed(atom, polarity))
 280   {
 281     if (atom.getKind() == kind::EQUAL)
 282     {
 283       d_equalityEngine->assertEquality(atom, polarity, exp);
 284     }
 285     else
 286     {
 287       d_equalityEngine->assertPredicate(atom, polarity, exp);
 288     }
 289     if (!d_state.isInConflict())
 290     {
 291       if (atom.getKind() == kind::MEMBER && polarity)
 292       {
 293         // check if set has a value, if so, we can propagate
 294         Node r = d_equalityEngine->getRepresentative(atom[1]);
 295         EqcInfo* e = getOrMakeEqcInfo(r, true);
 296         if (e)
 297         {
 298           Node s = e->d_singleton;
 299           if (!s.isNull())
 300           {
 301             Node pexp = NodeManager::currentNM()->mkNode(
 302                 kind::AND, atom, atom[1].eqNode(s));
 303             d_keep.insert(pexp);
 304             if (s.getKind() == kind::SINGLETON)
 305             {
 306               if (s[0] != atom[0])
 307               {
 308                 Trace("sets-prop")
 309                     << "Propagate mem-eq : " << pexp << std::endl;
 310                 Node eq = s[0].eqNode(atom[0]);
 311                 d_keep.insert(eq);
 312                 assertFact(eq, pexp);
 313               }
 314             }
 315             else
 316             {
 317               Trace("sets-prop")
 318                   << "Propagate mem-eq conflict : " << pexp << std::endl;
 319               d_state.setConflict(pexp);
 320             }
 321           }
 322         }
 323         // add to membership list
 324         NodeIntMap::iterator mem_i = d_members.find(r);
 325         int n_members = 0;
 326         if (mem_i != d_members.end())
 327         {
 328           n_members = (*mem_i).second;
 329         }
 330         d_members[r] = n_members + 1;
 331         if (n_members < (int)d_members_data[r].size())
 332         {
 333           d_members_data[r][n_members] = atom;
 334         }
 335         else
 336         {
 337           d_members_data[r].push_back(atom);
 338         }
 339       }
 340     }
 341     return true;
 342   }
 343   else
 344   {
 345     return false;
 346   }
 347 }
 348
 349 void TheorySetsPrivate::fullEffortReset()
 350 {
 351   Assert(d_equalityEngine->consistent());
 352   d_full_check_incomplete = false;
 353   d_most_common_type.clear();
 354   d_most_common_type_term.clear();
 355   d_card_enabled = false;
 356   d_rels_enabled = false;
 357   // reset the state object
 358   d_state.reset();
 359   // reset the inference manager
 360   d_im.reset();
 361   // reset the cardinality solver
 362   d_cardSolver->reset();
 363 }
 364
 365 void TheorySetsPrivate::fullEffortCheck()
 366 {
 367   Trace("sets") << "----- Full effort check ------" << std::endl;
 368   do
 369   {
 370     Assert(!d_im.hasPendingLemmas() || d_im.hasProcessed());
 371
 372     Trace("sets") << "...iterate full effort check..." << std::endl;
 373     fullEffortReset();
 374
 375     Trace("sets-eqc") << "Equality Engine:" << std::endl;
 376     std::map<TypeNode, unsigned> eqcTypeCount;
 377     eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(d_equalityEngine);
 378     while (!eqcs_i.isFinished())
 379     {
 380       Node eqc = (*eqcs_i);
 381       bool isSet = false;
 382       TypeNode tn = eqc.getType();
 383       d_state.registerEqc(tn, eqc);
 384       eqcTypeCount[tn]++;
 385       // common type node and term
 386       TypeNode tnc;
 387       Node tnct;
 388       if (tn.isSet())
 389       {
 390         isSet = true;
 391         tnc = tn.getSetElementType();
 392         tnct = eqc;
 393       }
 394       Trace("sets-eqc") << "[" << eqc << "] : ";
 395       eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, d_equalityEngine);
 396       while (!eqc_i.isFinished())
 397       {
 398         Node n = (*eqc_i);
 399         if (n != eqc)
 400         {
 401           Trace("sets-eqc") << n << " ";
 402         }
 403         TypeNode tnn = n.getType();
 404         if (isSet)
 405         {
 406           Assert(tnn.isSet());
 407           TypeNode tnnel = tnn.getSetElementType();
 408           tnc = TypeNode::mostCommonTypeNode(tnc, tnnel);
 409           Assert(!tnc.isNull());
 410           // update the common type term
 411           if (tnc == tnnel)
 412           {
 413             tnct = n;
 414           }
 415         }
 416         // register it with the state
 417         d_state.registerTerm(eqc, tnn, n);
 418         if (n.getKind() == kind::CARD)
 419         {
 420           d_card_enabled = true;
 421           // register it with the cardinality solver
 422           d_cardSolver->registerTerm(n);
 423           // if we do not handle the kind, set incomplete
 424           Kind nk = n[0].getKind();
 425           // some kinds of cardinality we cannot handle
 426           if (d_rels->isRelationKind(nk))
 427           {
 428             d_full_check_incomplete = true;
 429             Trace("sets-incomplete")
 430                 << "Sets : incomplete because of " << n << "." << std::endl;
 431             // TODO (#1124):  The issue can be divided into 4 parts
 432             // 1- Supporting the universe cardinality for finite types with
 433             // finite cardinality (done)
 434             // 2- Supporting the universe cardinality for uninterpreted sorts
 435             // with finite-model-find (pending) See the implementation of
 436             //    CardinalityExtension::checkCardinalityExtended
 437             // 3- Supporting the universe cardinality for non-finite types
 438             // (done)
 439             // 4- Supporting cardinality for relations (hard)
 440           }
 441         }
 442         else
 443         {
 444           if (d_rels->isRelationKind(n.getKind()))
 445           {
 446             d_rels_enabled = true;
 447           }
 448         }
 449         ++eqc_i;
 450       }
 451       if (isSet)
 452       {
 453         Assert(tnct.getType().getSetElementType() == tnc);
 454         d_most_common_type[eqc] = tnc;
 455         d_most_common_type_term[eqc] = tnct;
 456       }
 457       Trace("sets-eqc") << std::endl;
 458       ++eqcs_i;
 459     }
 460
 461     Trace("sets-eqc") << "...finished equality engine." << std::endl;
 462
 463     if (Trace.isOn("sets-state"))
 464     {
 465       Trace("sets-state") << "Equivalence class counters:" << std::endl;
 466       for (std::pair<const TypeNode, unsigned>& ec : eqcTypeCount)
 467       {
 468         Trace("sets-state")
 469             << "  " << ec.first << " -> " << ec.second << std::endl;
 470       }
 471     }
 472
 473     // We may have sent lemmas while registering the terms in the loop above,
 474     // e.g. the cardinality solver.
 475     if (d_im.hasProcessed())
 476     {
 477       continue;
 478     }
 479     if (Trace.isOn("sets-mem"))
 480     {
 481       const std::vector<Node>& sec = d_state.getSetsEqClasses();
 482       for (const Node& s : sec)
 483       {
 484         Trace("sets-mem") << "Eqc " << s << " : ";
 485         const std::map<Node, Node>& smem = d_state.getMembers(s);
 486         if (!smem.empty())
 487         {
 488           Trace("sets-mem") << "Memberships : ";
 489           for (const std::pair<const Node, Node>& it2 : smem)
 490           {
 491             Trace("sets-mem") << it2.first << " ";
 492           }
 493         }
 494         Node ss = d_state.getSingletonEqClass(s);
 495         if (!ss.isNull())
 496         {
 497           Trace("sets-mem") << " : Singleton : " << ss;
 498         }
 499         Trace("sets-mem") << std::endl;
 500       }
 501     }
 502     // check subtypes
 503     checkSubtypes();
 504     d_im.flushPendingLemmas(true);
 505     if (d_im.hasProcessed())
 506     {
 507       continue;
 508     }
 509     // check downwards closure
 510     checkDownwardsClosure();
 511     d_im.flushPendingLemmas();
 512     if (d_im.hasProcessed())
 513     {
 514       continue;
 515     }
 516     // check upwards closure
 517     checkUpwardsClosure();
 518     d_im.flushPendingLemmas();
 519     if (d_im.hasProcessed())
 520     {
 521       continue;
 522     }
 523     // check disequalities
 524     checkDisequalities();
 525     d_im.flushPendingLemmas();
 526     if (d_im.hasProcessed())
 527     {
 528       continue;
 529     }
 530     // check reduce comprehensions
 531     checkReduceComprehensions();
 532     d_im.flushPendingLemmas();
 533     if (d_im.hasProcessed())
 534     {
 535       continue;
 536     }
 537     if (d_card_enabled)
 538     {
 539       // call the check method of the cardinality solver
 540       d_cardSolver->check();
 541       if (d_im.hasProcessed())
 542       {
 543         continue;
 544       }
 545     }
 546     if (d_rels_enabled)
 547     {
 548       // call the check method of the relations solver
 549       d_rels->check(Theory::EFFORT_FULL);
 550     }
 551   } while (!d_im.hasSentLemma() && !d_state.isInConflict()
 552            && d_im.hasAddedFact());
 553   Assert(!d_im.hasPendingLemmas() || d_im.hasProcessed());
 554   Trace("sets") << "----- End full effort check, conflict="
 555                 << d_state.isInConflict() << ", lemma=" << d_im.hasSentLemma()
 556                 << std::endl;
 557 }
 558
 559 void TheorySetsPrivate::checkSubtypes()
 560 {
 561   Trace("sets") << "TheorySetsPrivate: check Subtypes..." << std::endl;
 562   const std::vector<Node>& sec = d_state.getSetsEqClasses();
 563   for (const Node& s : sec)
 564   {
 565     TypeNode mct = d_most_common_type[s];
 566     Assert(!mct.isNull());
 567     const std::map<Node, Node>& smems = d_state.getMembers(s);
 568     if (!smems.empty())
 569     {
 570       for (const std::pair<const Node, Node>& it2 : smems)
 571       {
 572         Trace("sets") << "  check subtype " << it2.first << " " << it2.second
 573                       << std::endl;
 574         Trace("sets") << "    types : " << it2.first.getType() << " " << mct
 575                       << std::endl;
 576         if (!it2.first.getType().isSubtypeOf(mct))
 577         {
 578           Node mctt = d_most_common_type_term[s];
 579           Assert(!mctt.isNull());
 580           Trace("sets") << "    most common type term is " << mctt << std::endl;
 581           std::vector<Node> exp;
 582           exp.push_back(it2.second);
 583           Assert(d_state.areEqual(mctt, it2.second[1]));
 584           exp.push_back(mctt.eqNode(it2.second[1]));
 585           Node tc_k = d_state.getTypeConstraintSkolem(it2.first, mct);
 586           if (!tc_k.isNull())
 587           {
 588             Node etc = tc_k.eqNode(it2.first);
 589             d_im.assertInference(etc, exp, "subtype-clash");
 590             if (d_state.isInConflict())
 591             {
 592               return;
 593             }
 594           }
 595         }
 596       }
 597     }
 598   }
 599   Trace("sets") << "TheorySetsPrivate: finished." << std::endl;
 600 }
 601
 602 void TheorySetsPrivate::checkDownwardsClosure()
 603 {
 604   Trace("sets") << "TheorySetsPrivate: check downwards closure..." << std::endl;
 605   // downwards closure
 606   const std::vector<Node>& sec = d_state.getSetsEqClasses();
 607   for (const Node& s : sec)
 608   {
 609     const std::vector<Node>& nvsets = d_state.getNonVariableSets(s);
 610     if (!nvsets.empty())
 611     {
 612       const std::map<Node, Node>& smem = d_state.getMembers(s);
 613       for (const Node& nv : nvsets)
 614       {
 615         if (!d_state.isCongruent(nv))
 616         {
 617           for (const std::pair<const Node, Node>& it2 : smem)
 618           {
 619             Node mem = it2.second;
 620             Node eq_set = nv;
 621             Assert(d_equalityEngine->areEqual(mem[1], eq_set));
 622             if (mem[1] != eq_set)
 623             {
 624               Trace("sets-debug") << "Downwards closure based on " << mem
 625                                   << ", eq_set = " << eq_set << std::endl;
 626               if (!options::setsProxyLemmas())
 627               {
 628                 Node nmem = NodeManager::currentNM()->mkNode(
 629                     kind::MEMBER, mem[0], eq_set);
 630                 nmem = Rewriter::rewrite(nmem);
 631                 std::vector<Node> exp;
 632                 exp.push_back(mem);
 633                 exp.push_back(mem[1].eqNode(eq_set));
 634                 d_im.assertInference(nmem, exp, "downc");
 635                 if (d_state.isInConflict())
 636                 {
 637                   return;
 638                 }
 639               }
 640               else
 641               {
 642                 // use proxy set
 643                 Node k = d_state.getProxy(eq_set);
 644                 Node pmem =
 645                     NodeManager::currentNM()->mkNode(kind::MEMBER, mem[0], k);
 646                 Node nmem = NodeManager::currentNM()->mkNode(
 647                     kind::MEMBER, mem[0], eq_set);
 648                 nmem = Rewriter::rewrite(nmem);
 649                 std::vector<Node> exp;
 650                 if (d_state.areEqual(mem, pmem))
 651                 {
 652                   exp.push_back(pmem);
 653                 }
 654                 else
 655                 {
 656                   nmem = NodeManager::currentNM()->mkNode(
 657                       kind::OR, pmem.negate(), nmem);
 658                 }
 659                 d_im.assertInference(nmem, exp, "downc");
 660               }
 661             }
 662           }
 663         }
 664       }
 665     }
 666   }
 667 }
 668
 669 void TheorySetsPrivate::checkUpwardsClosure()
 670 {
 671   // upwards closure
 672   NodeManager* nm = NodeManager::currentNM();
 673   const std::map<Kind, std::map<Node, std::map<Node, Node> > >& boi =
 674       d_state.getBinaryOpIndex();
 675   for (const std::pair<const Kind, std::map<Node, std::map<Node, Node> > >&
 676            itb : boi)
 677   {
 678     Kind k = itb.first;
 679     Trace("sets") << "TheorySetsPrivate: check upwards closure " << k << "..."
 680                   << std::endl;
 681     for (const std::pair<const Node, std::map<Node, Node> >& it : itb.second)
 682     {
 683       Node r1 = it.first;
 684       // see if there are members in first argument r1
 685       const std::map<Node, Node>& r1mem = d_state.getMembers(r1);
 686       if (!r1mem.empty() || k == kind::UNION)
 687       {
 688         for (const std::pair<const Node, Node>& it2 : it.second)
 689         {
 690           Node r2 = it2.first;
 691           Node term = it2.second;
 692           // see if there are members in second argument
 693           const std::map<Node, Node>& r2mem = d_state.getMembers(r2);
 694           const std::map<Node, Node>& r2nmem = d_state.getNegativeMembers(r2);
 695           if (!r2mem.empty() || k != kind::INTERSECTION)
 696           {
 697             Trace("sets-debug")
 698                 << "Checking " << term << ", members = " << (!r1mem.empty())
 699                 << ", " << (!r2mem.empty()) << std::endl;
 700             // for all members of r1
 701             if (!r1mem.empty())
 702             {
 703               for (const std::pair<const Node, Node>& itm1m : r1mem)
 704               {
 705                 Node xr = itm1m.first;
 706                 Node x = itm1m.second[0];
 707                 Trace("sets-debug") << "checking membership " << xr << " "
 708                                     << itm1m.second << std::endl;
 709                 std::vector<Node> exp;
 710                 exp.push_back(itm1m.second);
 711                 d_state.addEqualityToExp(term[0], itm1m.second[1], exp);
 712                 bool valid = false;
 713                 int inferType = 0;
 714                 if (k == kind::UNION)
 715                 {
 716                   valid = true;
 717                 }
 718                 else if (k == kind::INTERSECTION)
 719                 {
 720                   // conclude x is in term
 721                   // if also existing in members of r2
 722                   std::map<Node, Node>::const_iterator itm = r2mem.find(xr);
 723                   if (itm != r2mem.end())
 724                   {
 725                     exp.push_back(itm->second);
 726                     d_state.addEqualityToExp(term[1], itm->second[1], exp);
 727                     d_state.addEqualityToExp(x, itm->second[0], exp);
 728                     valid = true;
 729                   }
 730                   else
 731                   {
 732                     // if not, check whether it is definitely not a member, if
 733                     // unknown, split
 734                     if (r2nmem.find(xr) == r2nmem.end())
 735                     {
 736                       exp.push_back(nm->mkNode(kind::MEMBER, x, term[1]));
 737                       valid = true;
 738                       inferType = 1;
 739                     }
 740                   }
 741                 }
 742                 else
 743                 {
 744                   Assert(k == kind::SETMINUS);
 745                   std::map<Node, Node>::const_iterator itm = r2mem.find(xr);
 746                   if (itm == r2mem.end())
 747                   {
 748                     // must add lemma for set minus since non-membership in this
 749                     // case is not explained
 750                     exp.push_back(
 751                         nm->mkNode(kind::MEMBER, x, term[1]).negate());
 752                     valid = true;
 753                     inferType = 1;
 754                   }
 755                 }
 756                 if (valid)
 757                 {
 758                   Node rr = d_equalityEngine->getRepresentative(term);
 759                   if (!isMember(x, rr))
 760                   {
 761                     Node kk = d_state.getProxy(term);
 762                     Node fact = nm->mkNode(kind::MEMBER, x, kk);
 763                     d_im.assertInference(fact, exp, "upc", inferType);
 764                     if (d_state.isInConflict())
 765                     {
 766                       return;
 767                     }
 768                   }
 769                 }
 770                 Trace("sets-debug") << "done checking membership " << xr << " "
 771                                     << itm1m.second << std::endl;
 772               }
 773             }
 774             if (k == kind::UNION)
 775             {
 776               if (!r2mem.empty())
 777               {
 778                 // for all members of r2
 779                 for (const std::pair<const Node, Node>& itm2m : r2mem)
 780                 {
 781                   Node x = itm2m.second[0];
 782                   Node rr = d_equalityEngine->getRepresentative(term);
 783                   if (!isMember(x, rr))
 784                   {
 785                     std::vector<Node> exp;
 786                     exp.push_back(itm2m.second);
 787                     d_state.addEqualityToExp(term[1], itm2m.second[1], exp);
 788                     Node r = d_state.getProxy(term);
 789                     Node fact = nm->mkNode(kind::MEMBER, x, r);
 790                     d_im.assertInference(fact, exp, "upc2");
 791                     if (d_state.isInConflict())
 792                     {
 793                       return;
 794                     }
 795                   }
 796                 }
 797               }
 798             }
 799           }
 800         }
 801       }
 802     }
 803   }
 804   if (!d_im.hasProcessed())
 805   {
 806     if (options::setsExt())
 807     {
 808       // universal sets
 809       Trace("sets-debug") << "Check universe sets..." << std::endl;
 810       // all elements must be in universal set
 811       const std::vector<Node>& sec = d_state.getSetsEqClasses();
 812       for (const Node& s : sec)
 813       {
 814         // if equivalence class contains a variable
 815         Node v = d_state.getVariableSet(s);
 816         if (!v.isNull())
 817         {
 818           // the variable in the equivalence class
 819           std::map<TypeNode, Node> univ_set;
 820           const std::map<Node, Node>& smems = d_state.getMembers(s);
 821           for (const std::pair<const Node, Node>& it2 : smems)
 822           {
 823             Node e = it2.second[0];
 824             TypeNode tn = NodeManager::currentNM()->mkSetType(e.getType());
 825             Node u;
 826             std::map<TypeNode, Node>::iterator itu = univ_set.find(tn);
 827             if (itu == univ_set.end())
 828             {
 829               Node ueqc = d_state.getUnivSetEqClass(tn);
 830               // if the universe does not yet exist, or is not in this
 831               // equivalence class
 832               if (s != ueqc)
 833               {
 834                 u = d_state.getUnivSet(tn);
 835               }
 836               univ_set[tn] = u;
 837             }
 838             else
 839             {
 840               u = itu->second;
 841             }
 842             if (!u.isNull())
 843             {
 844               Assert(it2.second.getKind() == kind::MEMBER);
 845               std::vector<Node> exp;
 846               exp.push_back(it2.second);
 847               if (v != it2.second[1])
 848               {
 849                 exp.push_back(v.eqNode(it2.second[1]));
 850               }
 851               Node fact = nm->mkNode(kind::MEMBER, it2.second[0], u);
 852               d_im.assertInference(fact, exp, "upuniv");
 853               if (d_state.isInConflict())
 854               {
 855                 return;
 856               }
 857             }
 858           }
 859         }
 860       }
 861     }
 862   }
 863 }
 864
 865 void TheorySetsPrivate::checkDisequalities()
 866 {
 867   // disequalities
 868   Trace("sets") << "TheorySetsPrivate: check disequalities..." << std::endl;
 869   NodeManager* nm = NodeManager::currentNM();
 870   for (NodeBoolMap::const_iterator it = d_deq.begin(); it != d_deq.end(); ++it)
 871   {
 872     if (!(*it).second)
 873     {
 874       // not active
 875       continue;
 876     }
 877     Node deq = (*it).first;
 878     // check if it is already satisfied
 879     Assert(d_equalityEngine->hasTerm(deq[0])
 880            && d_equalityEngine->hasTerm(deq[1]));
 881     Node r1 = d_equalityEngine->getRepresentative(deq[0]);
 882     Node r2 = d_equalityEngine->getRepresentative(deq[1]);
 883     bool is_sat = d_state.isSetDisequalityEntailed(r1, r2);
 884     Trace("sets-debug") << "Check disequality " << deq
 885                         << ", is_sat = " << is_sat << std::endl;
 886     // will process regardless of sat/processed/unprocessed
 887     d_deq[deq] = false;
 888
 889     if (is_sat)
 890     {
 891       // already satisfied
 892       continue;
 893     }
 894     if (d_termProcessed.find(deq) != d_termProcessed.end())
 895     {
 896       // already added lemma
 897       continue;
 898     }
 899     d_termProcessed.insert(deq);
 900     d_termProcessed.insert(deq[1].eqNode(deq[0]));
 901     Trace("sets") << "Process Disequality : " << deq.negate() << std::endl;
 902     TypeNode elementType = deq[0].getType().getSetElementType();
 903     Node x = d_state.getSkolemCache().mkTypedSkolemCached(
 904         elementType, deq[0], deq[1], SkolemCache::SK_DISEQUAL, "sde");
 905     Node mem1 = nm->mkNode(MEMBER, x, deq[0]);
 906     Node mem2 = nm->mkNode(MEMBER, x, deq[1]);
 907     Node lem = nm->mkNode(OR, deq, nm->mkNode(EQUAL, mem1, mem2).negate());
 908     lem = Rewriter::rewrite(lem);
 909     d_im.assertInference(lem, d_true, "diseq", 1);
 910     d_im.flushPendingLemmas();
 911     if (d_im.hasProcessed())
 912     {
 913       return;
 914     }
 915   }
 916 }
 917
 918 void TheorySetsPrivate::checkReduceComprehensions()
 919 {
 920   NodeManager* nm = NodeManager::currentNM();
 921   const std::vector<Node>& comps = d_state.getComprehensionSets();
 922   for (const Node& n : comps)
 923   {
 924     if (d_termProcessed.find(n) != d_termProcessed.end())
 925     {
 926       // already reduced it
 927       continue;
 928     }
 929     d_termProcessed.insert(n);
 930     Node v = nm->mkBoundVar(n[2].getType());
 931     Node body = nm->mkNode(AND, n[1], v.eqNode(n[2]));
 932     // must do substitution
 933     std::vector<Node> vars;
 934     std::vector<Node> subs;
 935     for (const Node& cv : n[0])
 936     {
 937       vars.push_back(cv);
 938       Node cvs = nm->mkBoundVar(cv.getType());
 939       subs.push_back(cvs);
 940     }
 941     body = body.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
 942     Node bvl = nm->mkNode(BOUND_VAR_LIST, subs);
 943     body = nm->mkNode(EXISTS, bvl, body);
 944     Node mem = nm->mkNode(MEMBER, v, n);
 945     Node lem =
 946         nm->mkNode(FORALL, nm->mkNode(BOUND_VAR_LIST, v), body.eqNode(mem));
 947     Trace("sets-comprehension")
 948         << "Comprehension reduction: " << lem << std::endl;
 949     d_im.flushLemma(lem);
 950   }
 951 }
 952
 953 /**************************** TheorySetsPrivate *****************************/
 954 /**************************** TheorySetsPrivate *****************************/
 955 /**************************** TheorySetsPrivate *****************************/
 956
 957 void TheorySetsPrivate::check(Theory::Effort level)
 958 {
 959   Trace("sets-check") << "Sets check effort " << level << std::endl;
 960   if (level == Theory::EFFORT_LAST_CALL)
 961   {
 962     return;
 963   }
 964   while (!d_external.done() && !d_state.isInConflict())
 965   {
 966     // Get all the assertions
 967     Assertion assertion = d_external.get();
 968     TNode fact = assertion.d_assertion;
 969     Trace("sets-assert") << "Assert from input " << fact << std::endl;
 970     // assert the fact
 971     assertFact(fact, fact);
 972   }
 973   Trace("sets-check") << "Sets finished assertions effort " << level
 974                       << std::endl;
 975   // invoke full effort check, relations check
 976   if (!d_state.isInConflict())
 977   {
 978     if (level == Theory::EFFORT_FULL)
 979     {
 980       if (!d_external.d_valuation.needCheck())
 981       {
 982         fullEffortCheck();
 983         if (!d_state.isInConflict() && !d_im.hasSentLemma()
 984             && d_full_check_incomplete)
 985         {
 986           d_external.d_out->setIncomplete();
 987         }
 988       }
 989     }
 990   }
 991   Trace("sets-check") << "Sets finish Check effort " << level << std::endl;
 992 } /* TheorySetsPrivate::check() */
 993
 994 /************************ Sharing ************************/
 995 /************************ Sharing ************************/
 996 /************************ Sharing ************************/
 997
 998 void TheorySetsPrivate::addSharedTerm(TNode n)
 999 {
1000   Debug("sets") << "[sets] TheorySetsPrivate::addSharedTerm( " << n << ")"
1001                 << std::endl;
1002   d_equalityEngine->addTriggerTerm(n, THEORY_SETS);
1003 }
1004
1005 void TheorySetsPrivate::addCarePairs(TNodeTrie* t1,
1006                                      TNodeTrie* t2,
1007                                      unsigned arity,
1008                                      unsigned depth,
1009                                      unsigned& n_pairs)
1010 {
1011   if (depth == arity)
1012   {
1013     if (t2 != NULL)
1014     {
1015       Node f1 = t1->getData();
1016       Node f2 = t2->getData();
1017       if (!d_state.areEqual(f1, f2))
1018       {
1019         Trace("sets-cg") << "Check " << f1 << " and " << f2 << std::endl;
1020         vector<pair<TNode, TNode> > currentPairs;
1021         for (unsigned k = 0; k < f1.getNumChildren(); ++k)
1022         {
1023           TNode x = f1[k];
1024           TNode y = f2[k];
1025           Assert(d_equalityEngine->hasTerm(x));
1026           Assert(d_equalityEngine->hasTerm(y));
1027           Assert(!d_state.areDisequal(x, y));
1028           Assert(!areCareDisequal(x, y));
1029           if (!d_equalityEngine->areEqual(x, y))
1030           {
1031             Trace("sets-cg")
1032                 << "Arg #" << k << " is " << x << " " << y << std::endl;
1033             if (d_equalityEngine->isTriggerTerm(x, THEORY_SETS)
1034                 && d_equalityEngine->isTriggerTerm(y, THEORY_SETS))
1035             {
1036               TNode x_shared = d_equalityEngine->getTriggerTermRepresentative(
1037                   x, THEORY_SETS);
1038               TNode y_shared = d_equalityEngine->getTriggerTermRepresentative(
1039                   y, THEORY_SETS);
1040               currentPairs.push_back(make_pair(x_shared, y_shared));
1041             }
1042             else if (isCareArg(f1, k) && isCareArg(f2, k))
1043             {
1044               // splitting on sets (necessary for handling set of sets properly)
1045               if (x.getType().isSet())
1046               {
1047                 Assert(y.getType().isSet());
1048                 if (!d_state.areDisequal(x, y))
1049                 {
1050                   Trace("sets-cg-lemma")
1051                       << "Should split on : " << x << "==" << y << std::endl;
1052                   d_im.split(x.eqNode(y));
1053                 }
1054               }
1055             }
1056           }
1057         }
1058         for (unsigned c = 0; c < currentPairs.size(); ++c)
1059         {
1060           Trace("sets-cg-pair") << "Pair : " << currentPairs[c].first << " "
1061                                 << currentPairs[c].second << std::endl;
1062           d_external.addCarePair(currentPairs[c].first, currentPairs[c].second);
1063           n_pairs++;
1064         }
1065       }
1066     }
1067   }
1068   else
1069   {
1070     if (t2 == NULL)
1071     {
1072       if (depth < (arity - 1))
1073       {
1074         // add care pairs internal to each child
1075         for (std::pair<const TNode, TNodeTrie>& t : t1->d_data)
1076         {
1077           addCarePairs(&t.second, NULL, arity, depth + 1, n_pairs);
1078         }
1079       }
1080       // add care pairs based on each pair of non-disequal arguments
1081       for (std::map<TNode, TNodeTrie>::iterator it = t1->d_data.begin();
1082            it != t1->d_data.end();
1083            ++it)
1084       {
1085         std::map<TNode, TNodeTrie>::iterator it2 = it;
1086         ++it2;
1087         for (; it2 != t1->d_data.end(); ++it2)
1088         {
1089           if (!d_equalityEngine->areDisequal(it->first, it2->first, false))
1090           {
1091             if (!areCareDisequal(it->first, it2->first))
1092             {
1093               addCarePairs(
1094                   &it->second, &it2->second, arity, depth + 1, n_pairs);
1095             }
1096           }
1097         }
1098       }
1099     }
1100     else
1101     {
1102       // add care pairs based on product of indices, non-disequal arguments
1103       for (std::pair<const TNode, TNodeTrie>& tt1 : t1->d_data)
1104       {
1105         for (std::pair<const TNode, TNodeTrie>& tt2 : t2->d_data)
1106         {
1107           if (!d_equalityEngine->areDisequal(tt1.first, tt2.first, false))
1108           {
1109             if (!areCareDisequal(tt1.first, tt2.first))
1110             {
1111               addCarePairs(&tt1.second, &tt2.second, arity, depth + 1, n_pairs);
1112             }
1113           }
1114         }
1115       }
1116     }
1117   }
1118 }
1119
1120 void TheorySetsPrivate::computeCareGraph()
1121 {
1122   const std::map<Kind, std::vector<Node> >& ol = d_state.getOperatorList();
1123   for (const std::pair<const Kind, std::vector<Node> >& it : ol)
1124   {
1125     Kind k = it.first;
1126     if (k == kind::SINGLETON || k == kind::MEMBER)
1127     {
1128       unsigned n_pairs = 0;
1129       Trace("sets-cg-summary") << "Compute graph for sets, op=" << k << "..."
1130                                << it.second.size() << std::endl;
1131       Trace("sets-cg") << "Build index for " << k << "..." << std::endl;
1132       std::map<TypeNode, TNodeTrie> index;
1133       unsigned arity = 0;
1134       // populate indices
1135       for (TNode f1 : it.second)
1136       {
1137         Assert(d_equalityEngine->hasTerm(f1));
1138         Trace("sets-cg-debug") << "...build for " << f1 << std::endl;
1139         Assert(d_equalityEngine->hasTerm(f1));
1140         // break into index based on operator, and type of first argument (since
1141         // some operators are parametric)
1142         TypeNode tn = f1[0].getType();
1143         std::vector<TNode> reps;
1144         bool hasCareArg = false;
1145         for (unsigned j = 0; j < f1.getNumChildren(); j++)
1146         {
1147           reps.push_back(d_equalityEngine->getRepresentative(f1[j]));
1148           if (isCareArg(f1, j))
1149           {
1150             hasCareArg = true;
1151           }
1152         }
1153         if (hasCareArg)
1154         {
1155           Trace("sets-cg-debug") << "......adding." << std::endl;
1156           index[tn].addTerm(f1, reps);
1157           arity = reps.size();
1158         }
1159         else
1160         {
1161           Trace("sets-cg-debug") << "......skip." << std::endl;
1162         }
1163       }
1164       if (arity > 0)
1165       {
1166         // for each index
1167         for (std::pair<const TypeNode, TNodeTrie>& tt : index)
1168         {
1169           Trace("sets-cg") << "Process index " << tt.first << "..."
1170                            << std::endl;
1171           addCarePairs(&tt.second, nullptr, arity, 0, n_pairs);
1172         }
1173       }
1174       Trace("sets-cg-summary") << "...done, # pairs = " << n_pairs << std::endl;
1175     }
1176   }
1177 }
1178
1179 bool TheorySetsPrivate::isCareArg(Node n, unsigned a)
1180 {
1181   if (d_equalityEngine->isTriggerTerm(n[a], THEORY_SETS))
1182   {
1183     return true;
1184   }
1185   else if ((n.getKind() == kind::MEMBER || n.getKind() == kind::SINGLETON)
1186            && a == 0 && n[0].getType().isSet())
1187   {
1188     return true;
1189   }
1190   else
1191   {
1192     return false;
1193   }
1194 }
1195
1196 EqualityStatus TheorySetsPrivate::getEqualityStatus(TNode a, TNode b)
1197 {
1198   Assert(d_equalityEngine->hasTerm(a) && d_equalityEngine->hasTerm(b));
1199   if (d_equalityEngine->areEqual(a, b))
1200   {
1201     // The terms are implied to be equal
1202     return EQUALITY_TRUE;
1203   }
1204   if (d_equalityEngine->areDisequal(a, b, false))
1205   {
1206     // The terms are implied to be dis-equal
1207     return EQUALITY_FALSE;
1208   }
1209   return EQUALITY_UNKNOWN;
1210   /*
1211   Node aModelValue = d_external.d_valuation.getModelValue(a);
1212   if(aModelValue.isNull()) { return EQUALITY_UNKNOWN; }
1213   Node bModelValue = d_external.d_valuation.getModelValue(b);
1214   if(bModelValue.isNull()) { return EQUALITY_UNKNOWN; }
1215   if( aModelValue == bModelValue ) {
1216     // The term are true in current model
1217     return EQUALITY_TRUE_IN_MODEL;
1218   } else {
1219     return EQUALITY_FALSE_IN_MODEL;
1220   }
1221   */
1222   // }
1223   // //TODO: can we be more precise sometimes?
1224   // return EQUALITY_UNKNOWN;
1225 }
1226
1227 /******************** Model generation ********************/
1228 /******************** Model generation ********************/
1229 /******************** Model generation ********************/
1230
1231 namespace {
1232 /**
1233  * This function is a helper function to print sets as
1234  * Set A = { a0, a1, a2, }
1235  * instead of
1236  * (union (singleton a0) (union (singleton a1) (singleton a2)))
1237  */
1238 void traceSetElementsRecursively(stringstream& stream, const Node& set)
1239 {
1240   Assert(set.getType().isSet());
1241   if (set.getKind() == SINGLETON)
1242   {
1243     stream << set[0] << ", ";
1244   }
1245   if (set.getKind() == UNION)
1246   {
1247     traceSetElementsRecursively(stream, set[0]);
1248     traceSetElementsRecursively(stream, set[1]);
1249   }
1250 }
1251
1252 std::string traceElements(const Node& set)
1253 {
1254   std::stringstream stream;
1255   traceSetElementsRecursively(stream, set);
1256   return stream.str();
1257 }
1258
1259 }  // namespace
1260
1261 bool TheorySetsPrivate::collectModelInfo(TheoryModel* m)
1262 {
1263   Trace("sets-model") << "Set collect model info" << std::endl;
1264   set<Node> termSet;
1265   // Compute terms appearing in assertions and shared terms
1266   d_external.computeRelevantTerms(termSet);
1267
1268   // Assert equalities and disequalities to the model
1269   if (!m->assertEqualityEngine(d_equalityEngine, &termSet))
1270   {
1271     return false;
1272   }
1273
1274   NodeManager* nm = NodeManager::currentNM();
1275   std::map<Node, Node> mvals;
1276   // If cardinality is enabled, we need to use the ordered equivalence class
1277   // list computed by the cardinality solver, where sets equivalence classes
1278   // are assigned model values based on their position in the cardinality
1279   // graph.
1280   const std::vector<Node>& sec = d_card_enabled
1281                                      ? d_cardSolver->getOrderedSetsEqClasses()
1282                                      : d_state.getSetsEqClasses();
1283   Valuation& val = getValuation();
1284   for (int i = (int)(sec.size() - 1); i >= 0; i--)
1285   {
1286     Node eqc = sec[i];
1287     if (termSet.find(eqc) == termSet.end())
1288     {
1289       Trace("sets-model") << "* Do not assign value for " << eqc
1290                           << " since is not relevant." << std::endl;
1291     }
1292     else
1293     {
1294       std::vector<Node> els;
1295       bool is_base = !d_card_enabled || d_cardSolver->isModelValueBasic(eqc);
1296       if (is_base)
1297       {
1298         Trace("sets-model")
1299             << "Collect elements of base eqc " << eqc << std::endl;
1300         // members that must be in eqc
1301         const std::map<Node, Node>& emems = d_state.getMembers(eqc);
1302         if (!emems.empty())
1303         {
1304           for (const std::pair<const Node, Node>& itmm : emems)
1305           {
1306             Node t = nm->mkNode(kind::SINGLETON, itmm.first);
1307             els.push_back(t);
1308           }
1309         }
1310       }
1311       if (d_card_enabled)
1312       {
1313         // make the slack elements for the equivalence class based on set
1314         // cardinality
1315         d_cardSolver->mkModelValueElementsFor(val, eqc, els, mvals, m);
1316       }
1317       Node rep = NormalForm::mkBop(kind::UNION, els, eqc.getType());
1318       rep = Rewriter::rewrite(rep);
1319       Trace("sets-model") << "* Assign representative of " << eqc << " to "
1320                           << rep << std::endl;
1321       mvals[eqc] = rep;
1322       if (!m->assertEquality(eqc, rep, true))
1323       {
1324         return false;
1325       }
1326       m->assertSkeleton(rep);
1327
1328       Trace("sets-model") << "Set " << eqc << " = { " << traceElements(rep)
1329                           << " }" << std::endl;
1330     }
1331   }
1332
1333   // handle slack elements constraints for finite types
1334   if (d_card_enabled)
1335   {
1336     const std::map<TypeNode, std::vector<TNode> >& slackElements =
1337         d_cardSolver->getFiniteTypeSlackElements();
1338     for (const std::pair<TypeNode, std::vector<TNode> >& pair : slackElements)
1339     {
1340       const std::vector<Node>& members =
1341           d_cardSolver->getFiniteTypeMembers(pair.first);
1342       m->setAssignmentExclusionSetGroup(pair.second, members);
1343       Trace("sets-model") << "ExclusionSet: Group " << pair.second
1344                           << " is excluded from set" << members << std::endl;
1345     }
1346   }
1347   return true;
1348 }
1349
1350 /********************** Helper functions ***************************/
1351 /********************** Helper functions ***************************/
1352 /********************** Helper functions ***************************/
1353
1354 Node mkAnd(const std::vector<TNode>& conjunctions)
1355 {
1356   Assert(conjunctions.size() > 0);
1357
1358   std::set<TNode> all;
1359   for (unsigned i = 0; i < conjunctions.size(); ++i)
1360   {
1361     TNode t = conjunctions[i];
1362     if (t.getKind() == kind::AND)
1363     {
1364       for (TNode::iterator child_it = t.begin(); child_it != t.end();
1365            ++child_it)
1366       {
1367         Assert((*child_it).getKind() != kind::AND);
1368         all.insert(*child_it);
1369       }
1370     }
1371     else
1372     {
1373       all.insert(t);
1374     }
1375   }
1376
1377   Assert(all.size() > 0);
1378   if (all.size() == 1)
1379   {
1380     // All the same, or just one
1381     return conjunctions[0];
1382   }
1383
1384   NodeBuilder<> conjunction(kind::AND);
1385   std::set<TNode>::const_iterator it = all.begin();
1386   std::set<TNode>::const_iterator it_end = all.end();
1387   while (it != it_end)
1388   {
1389     conjunction << *it;
1390     ++it;
1391   }
1392   return conjunction;
1393 } /* mkAnd() */
1394
1395 void TheorySetsPrivate::propagate(Theory::Effort effort) {}
1396
1397 bool TheorySetsPrivate::propagate(TNode literal)
1398 {
1399   Debug("sets-prop") << " propagate(" << literal << ")" << std::endl;
1400
1401   // If already in conflict, no more propagation
1402   if (d_state.isInConflict())
1403   {
1404     Debug("sets-prop") << "TheoryUF::propagate(" << literal
1405                        << "): already in conflict" << std::endl;
1406     return false;
1407   }
1408
1409   // Propagate out
1410   bool ok = d_external.d_out->propagate(literal);
1411   if (!ok)
1412   {
1413     d_state.setConflict();
1414   }
1415
1416   return ok;
1417 } /* TheorySetsPrivate::propagate(TNode) */
1418
1419 OutputChannel* TheorySetsPrivate::getOutputChannel()
1420 {
1421   return d_external.d_out;
1422 }
1423
1424 Valuation& TheorySetsPrivate::getValuation() { return d_external.d_valuation; }
1425
1426 void TheorySetsPrivate::conflict(TNode a, TNode b)
1427 {
1428   Node conf = explain(a.eqNode(b));
1429   d_state.setConflict(conf);
1430   Debug("sets") << "[sets] conflict: " << a << " iff " << b << ", explanation "
1431                 << conf << std::endl;
1432   Trace("sets-lemma") << "Equality Conflict : " << conf << std::endl;
1433 }
1434
1435 Node TheorySetsPrivate::explain(TNode literal)
1436 {
1437   Debug("sets") << "TheorySetsPrivate::explain(" << literal << ")" << std::endl;
1438
1439   bool polarity = literal.getKind() != kind::NOT;
1440   TNode atom = polarity ? literal : literal[0];
1441   std::vector<TNode> assumptions;
1442
1443   if (atom.getKind() == kind::EQUAL)
1444   {
1445     d_equalityEngine->explainEquality(atom[0], atom[1], polarity, assumptions);
1446   }
1447   else if (atom.getKind() == kind::MEMBER)
1448   {
1449     d_equalityEngine->explainPredicate(atom, polarity, assumptions);
1450   }
1451   else
1452   {
1453     Debug("sets") << "unhandled: " << literal << "; (" << atom << ", "
1454                   << polarity << "); kind" << atom.getKind() << std::endl;
1455     Unhandled();
1456   }
1457
1458   return mkAnd(assumptions);
1459 }
1460
1461 void TheorySetsPrivate::preRegisterTerm(TNode node)
1462 {
1463   Debug("sets") << "TheorySetsPrivate::preRegisterTerm(" << node << ")"
1464                 << std::endl;
1465   switch (node.getKind())
1466   {
1467     case kind::EQUAL: d_equalityEngine->addTriggerEquality(node); break;
1468     case kind::MEMBER: d_equalityEngine->addTriggerPredicate(node); break;
1469     case kind::CARD: d_equalityEngine->addTriggerTerm(node, THEORY_SETS); break;
1470     default: d_equalityEngine->addTerm(node); break;
1471   }
1472 }
1473
1474 TrustNode TheorySetsPrivate::expandDefinition(Node node)
1475 {
1476   Debug("sets-proc") << "expandDefinition : " << node << std::endl;
1477
1478   if (node.getKind() == kind::CHOOSE)
1479   {
1480     // (choose A) is expanded as
1481     // (witness ((x elementType))
1482     //    (ite
1483     //      (= A (as emptyset setType))
1484     //      (= x chooseUf(A))
1485     //      (and (member x A) (= x chooseUf(A)))
1486
1487     NodeManager* nm = NodeManager::currentNM();
1488     Node set = node[0];
1489     TypeNode setType = set.getType();
1490     Node chooseSkolem = getChooseFunction(setType);
1491     Node apply = NodeManager::currentNM()->mkNode(APPLY_UF, chooseSkolem, set);
1492
1493     Node witnessVariable = nm->mkBoundVar(setType.getSetElementType());
1494
1495     Node equal = witnessVariable.eqNode(apply);
1496     Node emptySet = nm->mkConst(EmptySet(setType));
1497     Node isEmpty = set.eqNode(emptySet);
1498     Node member = nm->mkNode(MEMBER, witnessVariable, set);
1499     Node memberAndEqual = member.andNode(equal);
1500     Node ite = nm->mkNode(kind::ITE, isEmpty, equal, memberAndEqual);
1501     Node witnessVariables = nm->mkNode(BOUND_VAR_LIST, witnessVariable);
1502     Node witness = nm->mkNode(WITNESS, witnessVariables, ite);
1503     return TrustNode::mkTrustRewrite(node, witness, nullptr);
1504   }
1505
1506   return TrustNode::null();
1507 }
1508
1509 Node TheorySetsPrivate::getChooseFunction(const TypeNode& setType)
1510 {
1511   std::map<TypeNode, Node>::iterator it = d_chooseFunctions.find(setType);
1512   if (it != d_chooseFunctions.end())
1513   {
1514     return it->second;
1515   }
1516
1517   NodeManager* nm = NodeManager::currentNM();
1518   TypeNode chooseUf = nm->mkFunctionType(setType, setType.getSetElementType());
1519   stringstream stream;
1520   stream << "chooseUf" << setType.getId();
1521   string name = stream.str();
1522   Node chooseSkolem = nm->mkSkolem(
1523       name, chooseUf, "choose function", NodeManager::SKOLEM_EXACT_NAME);
1524   d_chooseFunctions[setType] = chooseSkolem;
1525   return chooseSkolem;
1526 }
1527
1528 void TheorySetsPrivate::presolve() { d_state.reset(); }
1529
1530 }  // namespace sets
1531 }  // namespace theory
1532 }  // namespace CVC4