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