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