src/theory/sets/cardinality_extension.cpp

   1 /*********************                                                        */
   2 /*! \file cardinality_extension.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2019 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 Implementation of an extension of the theory sets for handling
  13  ** cardinality constraints.
  14  **/
  15
  16 #include "theory/sets/cardinality_extension.h"
  17
  18 #include "expr/emptyset.h"
  19 #include "expr/node_algorithm.h"
  20 #include "options/sets_options.h"
  21 #include "theory/sets/normal_form.h"
  22 #include "theory/theory_model.h"
  23 #include "theory/valuation.h"
  24
  25 using namespace std;
  26 using namespace CVC4::kind;
  27
  28 namespace CVC4 {
  29 namespace theory {
  30 namespace sets {
  31
  32 CardinalityExtension::CardinalityExtension(SolverState& s,
  33                                            InferenceManager& im,
  34                                            eq::EqualityEngine& e,
  35                                            context::Context* c,
  36                                            context::UserContext* u)
  37     : d_state(s),
  38       d_im(im),
  39       d_ee(e),
  40       d_card_processed(u),
  41       d_finite_type_constants_processed(false)
  42 {
  43   d_true = NodeManager::currentNM()->mkConst(true);
  44   d_zero = NodeManager::currentNM()->mkConst(Rational(0));
  45   // we do congruence over cardinality
  46   d_ee.addFunctionKind(CARD);
  47 }
  48
  49 void CardinalityExtension::reset()
  50 {
  51   d_eqc_to_card_term.clear();
  52   d_t_card_enabled.clear();
  53   d_finite_type_elements.clear();
  54   d_finite_type_slack_elements.clear();
  55   d_univProxy.clear();
  56 }
  57 void CardinalityExtension::registerTerm(Node n)
  58 {
  59   Trace("sets-card-debug") << "Register term : " << n << std::endl;
  60   Assert(n.getKind() == CARD);
  61   TypeNode tnc = n[0].getType().getSetElementType();
  62   d_t_card_enabled[tnc] = true;
  63   Node r = d_ee.getRepresentative(n[0]);
  64   if (d_eqc_to_card_term.find(r) == d_eqc_to_card_term.end())
  65   {
  66     d_eqc_to_card_term[r] = n;
  67     registerCardinalityTerm(n[0]);
  68   }
  69   Trace("sets-card-debug") << "...finished register term" << std::endl;
  70 }
  71
  72 void CardinalityExtension::checkFiniteTypes()
  73 {
  74   for (std::pair<const TypeNode, bool>& pair : d_t_card_enabled)
  75   {
  76     TypeNode type = pair.first;
  77     if (pair.second && type.isInterpretedFinite())
  78     {
  79       checkFiniteType(type);
  80     }
  81   }
  82 }
  83
  84 void CardinalityExtension::checkFiniteType(TypeNode& t)
  85 {
  86   Assert(t.isInterpretedFinite());
  87
  88   // get the cardinality of the finite type t
  89   Cardinality card = t.getCardinality();
  90
  91   // cardinality of an interpreted finite type t is infinite when t
  92   // is infinite without --fmf
  93
  94   if (card.isInfinite())
  95   {
  96     // TODO (#1123): support uninterpreted sorts with --finite-model-find
  97     std::stringstream message;
  98     message << "The cardinality " << card << " of the finite type " << t
  99             << " is not supported yet.";
 100     throw LogicException(message.str());
 101   }
 102
 103   // get the universe set (as univset (Set t))
 104   NodeManager* nm = NodeManager::currentNM();
 105   Node univ = d_state.getUnivSet(nm->mkSetType(t));
 106   std::map<Node, Node>::iterator it = d_univProxy.find(univ);
 107
 108   Node proxy;
 109
 110   if (it == d_univProxy.end())
 111   {
 112     // Force cvc4 to build the cardinality graph for the universe set
 113     proxy = d_state.getProxy(univ);
 114     d_univProxy[univ] = proxy;
 115   }
 116   else
 117   {
 118     proxy = it->second;
 119   }
 120
 121   // get all equivalent classes of type t
 122   vector<Node> representatives = d_state.getSetsEqClasses(t);
 123
 124   Node typeCardinality = nm->mkConst(Rational(card.getFiniteCardinality()));
 125
 126   Node cardUniv = nm->mkNode(kind::CARD, proxy);
 127   Node leq = nm->mkNode(kind::LEQ, cardUniv, typeCardinality);
 128
 129   // (=> true (<= (card (as univset t)) cardUniv)
 130   if (!d_state.isEntailed(leq, true))
 131   {
 132     d_im.assertInference(leq, d_true, "finite type cardinality", 1);
 133   }
 134
 135   // add subset lemmas for sets, and membership lemmas for negative members
 136   for (Node& representative : representatives)
 137   {
 138     // the universe set is a subset of itself
 139     if (representative != d_ee.getRepresentative(univ))
 140     {
 141       // here we only add representatives with variables to avoid adding
 142       // infinite equivalent generated terms to the cardinality graph
 143       Node variable = d_state.getVariableSet(representative);
 144       if (variable.isNull())
 145       {
 146         continue;
 147       }
 148
 149       // (=> true (subset representative (as univset t))
 150       Node subset = nm->mkNode(kind::SUBSET, variable, proxy);
 151       // subset terms are rewritten as union terms: (subset A B) implies (=
 152       // (union A B) B)
 153       subset = Rewriter::rewrite(subset);
 154       if (!d_state.isEntailed(subset, true))
 155       {
 156         d_im.assertInference(subset, d_true, "univset is a super set", 1);
 157       }
 158
 159       // negative members are members in the universe set
 160       const std::map<Node, Node>& negativeMembers =
 161           d_state.getNegativeMembers(representative);
 162
 163       for (const std::pair<Node, Node>& negativeMember : negativeMembers)
 164       {
 165         Node member = nm->mkNode(MEMBER, negativeMember.first, univ);
 166         // negativeMember.second is the reason for the negative membership and
 167         // has kind MEMBER. So we specify the negation as the reason for the
 168         // negative membership lemma
 169         Node notMember = nm->mkNode(NOT, negativeMember.second);
 170         // (=>
 171         //    (not (member negativeMember representative)))
 172         //    (member negativeMember (as univset t)))
 173         d_im.assertInference(
 174             member, notMember, "negative members are in the universe", 1);
 175       }
 176     }
 177   }
 178 }
 179
 180 void CardinalityExtension::check()
 181 {
 182   checkFiniteTypes();
 183   checkRegister();
 184   if (d_im.hasProcessed())
 185   {
 186     return;
 187   }
 188   checkMinCard();
 189   if (d_im.hasProcessed())
 190   {
 191     return;
 192   }
 193   checkCardCycles();
 194   if (d_im.hasProcessed())
 195   {
 196     return;
 197   }
 198   // The last step will either do nothing (in which case we are SAT), or request
 199   // that a new set term is introduced.
 200   std::vector<Node> intro_sets;
 201   checkNormalForms(intro_sets);
 202   if (intro_sets.empty())
 203   {
 204     return;
 205   }
 206   Assert(intro_sets.size() == 1);
 207   Trace("sets-intro") << "Introduce term : " << intro_sets[0] << std::endl;
 208   Trace("sets-intro") << "  Actual Intro : ";
 209   d_state.debugPrintSet(intro_sets[0], "sets-nf");
 210   Trace("sets-nf") << std::endl;
 211   Node k = d_state.getProxy(intro_sets[0]);
 212   AlwaysAssert(!k.isNull());
 213 }
 214
 215 void CardinalityExtension::checkRegister()
 216 {
 217   Trace("sets") << "Cardinality graph..." << std::endl;
 218   NodeManager* nm = NodeManager::currentNM();
 219   // first, ensure cardinality relationships are added as lemmas for all
 220   // non-basic set terms
 221   const std::vector<Node>& setEqc = d_state.getSetsEqClasses();
 222   for (const Node& eqc : setEqc)
 223   {
 224     const std::vector<Node>& nvsets = d_state.getNonVariableSets(eqc);
 225     for (Node n : nvsets)
 226     {
 227       if (!d_state.isCongruent(n))
 228       {
 229         // if setminus, do for intersection instead
 230         if (n.getKind() == SETMINUS)
 231         {
 232           n = Rewriter::rewrite(nm->mkNode(INTERSECTION, n[0], n[1]));
 233         }
 234         registerCardinalityTerm(n);
 235       }
 236     }
 237   }
 238   Trace("sets") << "Done cardinality graph" << std::endl;
 239 }
 240
 241 void CardinalityExtension::registerCardinalityTerm(Node n)
 242 {
 243   TypeNode tnc = n.getType().getSetElementType();
 244   if (d_t_card_enabled.find(tnc) == d_t_card_enabled.end())
 245   {
 246     // if no cardinality constraints for sets of this type, we can ignore
 247     return;
 248   }
 249   if (d_card_processed.find(n) != d_card_processed.end())
 250   {
 251     // already processed
 252     return;
 253   }
 254   d_card_processed.insert(n);
 255   NodeManager* nm = NodeManager::currentNM();
 256   Trace("sets-card") << "Cardinality lemmas for " << n << " : " << std::endl;
 257   std::vector<Node> cterms;
 258   if (n.getKind() == INTERSECTION)
 259   {
 260     for (unsigned e = 0; e < 2; e++)
 261     {
 262       Node s = nm->mkNode(SETMINUS, n[e], n[1 - e]);
 263       cterms.push_back(s);
 264     }
 265     Node pos_lem = nm->mkNode(GEQ, nm->mkNode(CARD, n), d_zero);
 266     d_im.assertInference(pos_lem, d_emp_exp, "pcard", 1);
 267   }
 268   else
 269   {
 270     cterms.push_back(n);
 271   }
 272   for (unsigned k = 0, csize = cterms.size(); k < csize; k++)
 273   {
 274     Node nn = cterms[k];
 275     Node nk = d_state.getProxy(nn);
 276     Node pos_lem = nm->mkNode(GEQ, nm->mkNode(CARD, nk), d_zero);
 277     d_im.assertInference(pos_lem, d_emp_exp, "pcard", 1);
 278     if (nn != nk)
 279     {
 280       Node lem = nm->mkNode(EQUAL, nm->mkNode(CARD, nk), nm->mkNode(CARD, nn));
 281       lem = Rewriter::rewrite(lem);
 282       Trace("sets-card") << "  " << k << " : " << lem << std::endl;
 283       d_im.assertInference(lem, d_emp_exp, "card", 1);
 284     }
 285   }
 286   d_im.flushPendingLemmas();
 287 }
 288
 289 void CardinalityExtension::checkCardCycles()
 290 {
 291   Trace("sets") << "Check cardinality cycles..." << std::endl;
 292   // build order of equivalence classes, also build cardinality graph
 293   const std::vector<Node>& setEqc = d_state.getSetsEqClasses();
 294   d_oSetEqc.clear();
 295   d_card_parent.clear();
 296   for (const Node& s : setEqc)
 297   {
 298     std::vector<Node> curr;
 299     std::vector<Node> exp;
 300     checkCardCyclesRec(s, curr, exp);
 301     if (d_im.hasProcessed())
 302     {
 303       return;
 304     }
 305   }
 306   Trace("sets") << "Done check cardinality cycles" << std::endl;
 307 }
 308
 309 void CardinalityExtension::checkCardCyclesRec(Node eqc,
 310                                               std::vector<Node>& curr,
 311                                               std::vector<Node>& exp)
 312 {
 313   NodeManager* nm = NodeManager::currentNM();
 314   if (std::find(curr.begin(), curr.end(), eqc) != curr.end())
 315   {
 316     Trace("sets-debug") << "Found venn region loop..." << std::endl;
 317     if (curr.size() > 1)
 318     {
 319       // all regions must be equal
 320       std::vector<Node> conc;
 321       for (const Node& cc : curr)
 322       {
 323         conc.push_back(curr[0].eqNode(cc));
 324       }
 325       Node fact = conc.size() == 1 ? conc[0] : nm->mkNode(AND, conc);
 326       d_im.assertInference(fact, exp, "card_cycle");
 327       d_im.flushPendingLemmas();
 328     }
 329     else
 330     {
 331       // should be guaranteed based on not exploring equal parents
 332       Assert(false);
 333     }
 334     return;
 335   }
 336   if (std::find(d_oSetEqc.begin(), d_oSetEqc.end(), eqc) != d_oSetEqc.end())
 337   {
 338     // already processed
 339     return;
 340   }
 341   const std::vector<Node>& nvsets = d_state.getNonVariableSets(eqc);
 342   if (nvsets.empty())
 343   {
 344     // no non-variable sets, trivial
 345     d_oSetEqc.push_back(eqc);
 346     return;
 347   }
 348   curr.push_back(eqc);
 349   TypeNode tn = eqc.getType();
 350   bool is_empty = eqc == d_state.getEmptySetEqClass(tn);
 351   Node emp_set = d_state.getEmptySet(tn);
 352   for (const Node& n : nvsets)
 353   {
 354     Kind nk = n.getKind();
 355     if (nk != INTERSECTION && nk != SETMINUS)
 356     {
 357       continue;
 358     }
 359     Trace("sets-debug") << "Build cardinality parents for " << n << "..."
 360                         << std::endl;
 361     std::vector<Node> sib;
 362     unsigned true_sib = 0;
 363     if (n.getKind() == INTERSECTION)
 364     {
 365       d_localBase[n] = n;
 366       for (unsigned e = 0; e < 2; e++)
 367       {
 368         Node sm = Rewriter::rewrite(nm->mkNode(SETMINUS, n[e], n[1 - e]));
 369         sib.push_back(sm);
 370       }
 371       true_sib = 2;
 372     }
 373     else
 374     {
 375       Node si = Rewriter::rewrite(nm->mkNode(INTERSECTION, n[0], n[1]));
 376       sib.push_back(si);
 377       d_localBase[n] = si;
 378       Node osm = Rewriter::rewrite(nm->mkNode(SETMINUS, n[1], n[0]));
 379       sib.push_back(osm);
 380       true_sib = 1;
 381     }
 382     Node u = Rewriter::rewrite(nm->mkNode(UNION, n[0], n[1]));
 383     if (!d_ee.hasTerm(u))
 384     {
 385       u = Node::null();
 386     }
 387     unsigned n_parents = true_sib + (u.isNull() ? 0 : 1);
 388     // if this set is empty
 389     if (is_empty)
 390     {
 391       Assert(d_state.areEqual(n, emp_set));
 392       Trace("sets-debug") << "  empty, parents equal siblings" << std::endl;
 393       std::vector<Node> conc;
 394       // parent equal siblings
 395       for (unsigned e = 0; e < true_sib; e++)
 396       {
 397         if (d_ee.hasTerm(sib[e]) && !d_state.areEqual(n[e], sib[e]))
 398         {
 399           conc.push_back(n[e].eqNode(sib[e]));
 400         }
 401       }
 402       d_im.assertInference(conc, n.eqNode(emp_set), "cg_emp");
 403       d_im.flushPendingLemmas();
 404       if (d_im.hasProcessed())
 405       {
 406         return;
 407       }
 408       else
 409       {
 410         // justify why there is no edge to parents (necessary?)
 411         for (unsigned e = 0; e < n_parents; e++)
 412         {
 413           Node p = (e == true_sib) ? u : n[e];
 414         }
 415       }
 416       continue;
 417     }
 418     std::vector<Node> card_parents;
 419     std::vector<int> card_parent_ids;
 420     // check if equal to a parent
 421     for (unsigned e = 0; e < n_parents; e++)
 422     {
 423       Trace("sets-debug") << "  check parent " << e << "/" << n_parents
 424                           << std::endl;
 425       bool is_union = e == true_sib;
 426       Node p = (e == true_sib) ? u : n[e];
 427       Trace("sets-debug") << "  check relation to parent " << p
 428                           << ", isu=" << is_union << "..." << std::endl;
 429       // if parent is empty
 430       if (d_state.areEqual(p, emp_set))
 431       {
 432         Trace("sets-debug") << "  it is empty..." << std::endl;
 433         Assert(!d_state.areEqual(n, emp_set));
 434         d_im.assertInference(n.eqNode(emp_set), p.eqNode(emp_set), "cg_emppar");
 435         d_im.flushPendingLemmas();
 436         if (d_im.hasProcessed())
 437         {
 438           return;
 439         }
 440         // if we are equal to a parent
 441       }
 442       else if (d_state.areEqual(p, n))
 443       {
 444         Trace("sets-debug") << "  it is equal to this..." << std::endl;
 445         std::vector<Node> conc;
 446         std::vector<int> sib_emp_indices;
 447         if (is_union)
 448         {
 449           for (unsigned s = 0; s < sib.size(); s++)
 450           {
 451             sib_emp_indices.push_back(s);
 452           }
 453         }
 454         else
 455         {
 456           sib_emp_indices.push_back(e);
 457         }
 458         // sibling(s) are empty
 459         for (unsigned si : sib_emp_indices)
 460         {
 461           if (!d_state.areEqual(sib[si], emp_set))
 462           {
 463             conc.push_back(sib[si].eqNode(emp_set));
 464           }
 465           else
 466           {
 467             Trace("sets-debug")
 468                 << "Sibling " << sib[si] << " is already empty." << std::endl;
 469           }
 470         }
 471         if (!is_union && nk == INTERSECTION && !u.isNull())
 472         {
 473           // union is equal to other parent
 474           if (!d_state.areEqual(u, n[1 - e]))
 475           {
 476             conc.push_back(u.eqNode(n[1 - e]));
 477           }
 478         }
 479         Trace("sets-debug")
 480             << "...derived " << conc.size() << " conclusions" << std::endl;
 481         d_im.assertInference(conc, n.eqNode(p), "cg_eqpar");
 482         d_im.flushPendingLemmas();
 483         if (d_im.hasProcessed())
 484         {
 485           return;
 486         }
 487       }
 488       else
 489       {
 490         Trace("sets-cdg") << "Card graph : " << n << " -> " << p << std::endl;
 491         // otherwise, we a syntactic subset of p
 492         card_parents.push_back(p);
 493         card_parent_ids.push_back(is_union ? 2 : e);
 494       }
 495     }
 496     Assert(d_card_parent[n].empty());
 497     Trace("sets-debug") << "get parent representatives..." << std::endl;
 498     // for each parent, take their representatives
 499     for (unsigned k = 0, numcp = card_parents.size(); k < numcp; k++)
 500     {
 501       Node cpk = card_parents[k];
 502       Node eqcc = d_ee.getRepresentative(cpk);
 503       Trace("sets-debug") << "Check card parent " << k << "/"
 504                           << card_parents.size() << std::endl;
 505
 506       // if parent is singleton, then we should either be empty to equal to it
 507       Node eqccSingleton = d_state.getSingletonEqClass(eqcc);
 508       if (!eqccSingleton.isNull())
 509       {
 510         bool eq_parent = false;
 511         std::vector<Node> exps;
 512         d_state.addEqualityToExp(cpk, eqccSingleton, exps);
 513         if (d_state.areDisequal(n, emp_set))
 514         {
 515           exps.push_back(n.eqNode(emp_set).negate());
 516           eq_parent = true;
 517         }
 518         else
 519         {
 520           const std::map<Node, Node>& pmemsE = d_state.getMembers(eqc);
 521           if (!pmemsE.empty())
 522           {
 523             Node pmem = pmemsE.begin()->second;
 524             exps.push_back(pmem);
 525             d_state.addEqualityToExp(n, pmem[1], exps);
 526             eq_parent = true;
 527           }
 528         }
 529         // must be equal to parent
 530         if (eq_parent)
 531         {
 532           Node conc = n.eqNode(cpk);
 533           d_im.assertInference(conc, exps, "cg_par_sing");
 534           d_im.flushPendingLemmas();
 535         }
 536         else
 537         {
 538           // split on empty
 539           Trace("sets-nf") << "Split empty : " << n << std::endl;
 540           d_im.split(n.eqNode(emp_set), 1);
 541         }
 542         Assert(d_im.hasProcessed());
 543         return;
 544       }
 545       else
 546       {
 547         bool dup = false;
 548         for (unsigned l = 0, numcpn = d_card_parent[n].size(); l < numcpn; l++)
 549         {
 550           Node cpnl = d_card_parent[n][l];
 551           if (eqcc != cpnl)
 552           {
 553             continue;
 554           }
 555           Trace("sets-debug") << "  parents " << l << " and " << k
 556                               << " are equal, ids = " << card_parent_ids[l]
 557                               << " " << card_parent_ids[k] << std::endl;
 558           dup = true;
 559           if (n.getKind() != INTERSECTION)
 560           {
 561             continue;
 562           }
 563           Assert(card_parent_ids[l] != 2);
 564           std::vector<Node> conc;
 565           if (card_parent_ids[k] == 2)
 566           {
 567             // intersection is equal to other parent
 568             unsigned pid = 1 - card_parent_ids[l];
 569             if (!d_state.areEqual(n[pid], n))
 570             {
 571               Trace("sets-debug")
 572                   << "  one of them is union, make equal to other..."
 573                   << std::endl;
 574               conc.push_back(n[pid].eqNode(n));
 575             }
 576           }
 577           else
 578           {
 579             if (!d_state.areEqual(cpk, n))
 580             {
 581               Trace("sets-debug")
 582                   << "  neither is union, make equal to one parent..."
 583                   << std::endl;
 584               // intersection is equal to one of the parents
 585               conc.push_back(cpk.eqNode(n));
 586             }
 587           }
 588           d_im.assertInference(conc, cpk.eqNode(cpnl), "cg_pareq");
 589           d_im.flushPendingLemmas();
 590           if (d_im.hasProcessed())
 591           {
 592             return;
 593           }
 594         }
 595         if (!dup)
 596         {
 597           d_card_parent[n].push_back(eqcc);
 598         }
 599       }
 600     }
 601     // now recurse on parents (to ensure their normal will be computed after
 602     // this eqc)
 603     exp.push_back(eqc.eqNode(n));
 604     for (const Node& cpnc : d_card_parent[n])
 605     {
 606       checkCardCyclesRec(cpnc, curr, exp);
 607       if (d_im.hasProcessed())
 608       {
 609         return;
 610       }
 611     }
 612     exp.pop_back();
 613   }
 614   curr.pop_back();
 615   // parents now processed, can add to ordered list
 616   d_oSetEqc.push_back(eqc);
 617 }
 618
 619 void CardinalityExtension::checkNormalForms(std::vector<Node>& intro_sets)
 620 {
 621   Trace("sets") << "Check normal forms..." << std::endl;
 622   // now, build normal form for each equivalence class
 623   // d_oSetEqc is now sorted such that for each d_oSetEqc[i], d_oSetEqc[j],
 624   // if d_oSetEqc[i] is a strict syntactic subterm of d_oSetEqc[j], then i<j.
 625   d_ff.clear();
 626   d_nf.clear();
 627   for (int i = (int)(d_oSetEqc.size() - 1); i >= 0; i--)
 628   {
 629     checkNormalForm(d_oSetEqc[i], intro_sets);
 630     if (d_im.hasProcessed() || !intro_sets.empty())
 631     {
 632       return;
 633     }
 634   }
 635   Trace("sets") << "Done check normal forms" << std::endl;
 636 }
 637
 638 void CardinalityExtension::checkNormalForm(Node eqc,
 639                                            std::vector<Node>& intro_sets)
 640 {
 641   TypeNode tn = eqc.getType();
 642   Trace("sets") << "Compute normal form for " << eqc << std::endl;
 643   Trace("sets-nf") << "Compute N " << eqc << "..." << std::endl;
 644   if (eqc == d_state.getEmptySetEqClass(tn))
 645   {
 646     d_nf[eqc].clear();
 647     Trace("sets-nf") << "----> N " << eqc << " => {}" << std::endl;
 648     return;
 649   }
 650   // flat/normal forms are sets of equivalence classes
 651   Node base;
 652   std::vector<Node> comps;
 653   std::map<Node, std::map<Node, std::vector<Node> > >::iterator it =
 654       d_ff.find(eqc);
 655   if (it != d_ff.end())
 656   {
 657     for (std::pair<const Node, std::vector<Node> >& itf : it->second)
 658     {
 659       std::sort(itf.second.begin(), itf.second.end());
 660       if (base.isNull())
 661       {
 662         base = itf.first;
 663       }
 664       else
 665       {
 666         comps.push_back(itf.first);
 667       }
 668       Trace("sets-nf") << "  F " << itf.first << " : " << itf.second
 669                        << std::endl;
 670       Trace("sets-nf-debug") << " ...";
 671       d_state.debugPrintSet(itf.first, "sets-nf-debug");
 672       Trace("sets-nf-debug") << std::endl;
 673     }
 674   }
 675   else
 676   {
 677     Trace("sets-nf") << "(no flat forms)" << std::endl;
 678   }
 679   std::map<Node, std::vector<Node> >& ffeqc = d_ff[eqc];
 680   Assert(d_nf.find(eqc) == d_nf.end());
 681   std::vector<Node>& nfeqc = d_nf[eqc];
 682   NodeManager* nm = NodeManager::currentNM();
 683   bool success = true;
 684   Node emp_set = d_state.getEmptySet(tn);
 685   if (!base.isNull())
 686   {
 687     for (unsigned j = 0, csize = comps.size(); j < csize; j++)
 688     {
 689       // compare if equal
 690       std::vector<Node> c;
 691       c.push_back(base);
 692       c.push_back(comps[j]);
 693       std::vector<Node> only[2];
 694       std::vector<Node> common;
 695       Trace("sets-nf-debug") << "Compare venn regions of " << base << " vs "
 696                              << comps[j] << std::endl;
 697       unsigned k[2] = {0, 0};
 698       while (k[0] < ffeqc[c[0]].size() || k[1] < ffeqc[c[1]].size())
 699       {
 700         bool proc = true;
 701         for (unsigned e = 0; e < 2; e++)
 702         {
 703           if (k[e] == ffeqc[c[e]].size())
 704           {
 705             for (; k[1 - e] < ffeqc[c[1 - e]].size(); ++k[1 - e])
 706             {
 707               only[1 - e].push_back(ffeqc[c[1 - e]][k[1 - e]]);
 708             }
 709             proc = false;
 710           }
 711         }
 712         if (proc)
 713         {
 714           if (ffeqc[c[0]][k[0]] == ffeqc[c[1]][k[1]])
 715           {
 716             common.push_back(ffeqc[c[0]][k[0]]);
 717             k[0]++;
 718             k[1]++;
 719           }
 720           else if (ffeqc[c[0]][k[0]] < ffeqc[c[1]][k[1]])
 721           {
 722             only[0].push_back(ffeqc[c[0]][k[0]]);
 723             k[0]++;
 724           }
 725           else
 726           {
 727             only[1].push_back(ffeqc[c[1]][k[1]]);
 728             k[1]++;
 729           }
 730         }
 731       }
 732       if (!only[0].empty() || !only[1].empty())
 733       {
 734         if (Trace.isOn("sets-nf-debug"))
 735         {
 736           Trace("sets-nf-debug") << "Unique venn regions : " << std::endl;
 737           for (unsigned e = 0; e < 2; e++)
 738           {
 739             Trace("sets-nf-debug") << "  " << c[e] << " : { ";
 740             for (unsigned l = 0; l < only[e].size(); l++)
 741             {
 742               if (l > 0)
 743               {
 744                 Trace("sets-nf-debug") << ", ";
 745               }
 746               Trace("sets-nf-debug") << "[" << only[e][l] << "]";
 747             }
 748             Trace("sets-nf-debug") << " }" << std::endl;
 749           }
 750         }
 751         // try to make one empty, prefer the unique ones first
 752         for (unsigned e = 0; e < 3; e++)
 753         {
 754           unsigned sz = e == 2 ? common.size() : only[e].size();
 755           for (unsigned l = 0; l < sz; l++)
 756           {
 757             Node r = e == 2 ? common[l] : only[e][l];
 758             Trace("sets-nf-debug") << "Try split empty : " << r << std::endl;
 759             Trace("sets-nf-debug") << "         actual : ";
 760             d_state.debugPrintSet(r, "sets-nf-debug");
 761             Trace("sets-nf-debug") << std::endl;
 762             Assert(!d_state.areEqual(r, emp_set));
 763             if (!d_state.areDisequal(r, emp_set) && !d_state.hasMembers(r))
 764             {
 765               // guess that its equal empty if it has no explicit members
 766               Trace("sets-nf") << " Split empty : " << r << std::endl;
 767               Trace("sets-nf") << "Actual Split : ";
 768               d_state.debugPrintSet(r, "sets-nf");
 769               Trace("sets-nf") << std::endl;
 770               d_im.split(r.eqNode(emp_set), 1);
 771               Assert(d_im.hasProcessed());
 772               return;
 773             }
 774           }
 775         }
 776         for (const Node& o0 : only[0])
 777         {
 778           for (const Node& o1 : only[1])
 779           {
 780             bool disjoint = false;
 781             Trace("sets-nf-debug")
 782                 << "Try split " << o0 << " against " << o1 << std::endl;
 783             // split them
 784             for (unsigned e = 0; e < 2; e++)
 785             {
 786               Node r1 = e == 0 ? o0 : o1;
 787               Node r2 = e == 0 ? o1 : o0;
 788               // check if their intersection exists modulo equality
 789               Node r1r2i = d_state.getBinaryOpTerm(INTERSECTION, r1, r2);
 790               if (!r1r2i.isNull())
 791               {
 792                 Trace("sets-nf-debug")
 793                     << "Split term already exists, but not in cardinality "
 794                        "graph : "
 795                     << r1r2i << ", should be empty." << std::endl;
 796                 // their intersection is empty (probably?)
 797                 // e.g. these are two disjoint venn regions, proceed to next
 798                 // pair
 799                 Assert(d_state.areEqual(emp_set, r1r2i));
 800                 disjoint = true;
 801                 break;
 802               }
 803             }
 804             if (!disjoint)
 805             {
 806               // simply introduce their intersection
 807               Assert(o0 != o1);
 808               Node kca = d_state.getProxy(o0);
 809               Node kcb = d_state.getProxy(o1);
 810               Node intro =
 811                   Rewriter::rewrite(nm->mkNode(INTERSECTION, kca, kcb));
 812               Trace("sets-nf") << "   Intro split : " << o0 << " against " << o1
 813                                << ", term is " << intro << std::endl;
 814               intro_sets.push_back(intro);
 815               Assert(!d_ee.hasTerm(intro));
 816               return;
 817             }
 818           }
 819         }
 820         // should never get here
 821         success = false;
 822       }
 823     }
 824     if (success)
 825     {
 826       // normal form is flat form of base
 827       nfeqc.insert(nfeqc.end(), ffeqc[base].begin(), ffeqc[base].end());
 828       Trace("sets-nf") << "----> N " << eqc << " => F " << base << std::endl;
 829     }
 830     else
 831     {
 832       Trace("sets-nf") << "failed to build N " << eqc << std::endl;
 833     }
 834   }
 835   else
 836   {
 837     // must ensure disequal from empty
 838     if (!eqc.isConst() && !d_state.areDisequal(eqc, emp_set)
 839         && !d_state.hasMembers(eqc))
 840     {
 841       Trace("sets-nf-debug") << "Split on leaf " << eqc << std::endl;
 842       d_im.split(eqc.eqNode(emp_set));
 843       success = false;
 844     }
 845     else
 846     {
 847       // normal form is this equivalence class
 848       nfeqc.push_back(eqc);
 849       Trace("sets-nf") << "----> N " << eqc << " => { " << eqc << " }"
 850                        << std::endl;
 851     }
 852   }
 853   if (!success)
 854   {
 855     Assert(d_im.hasProcessed());
 856     return;
 857   }
 858   // Send to parents (a parent is a set that contains a term in this equivalence
 859   // class as a direct child).
 860   const std::vector<Node>& nvsets = d_state.getNonVariableSets(eqc);
 861   if (nvsets.empty())
 862   {
 863     // no non-variable sets
 864     return;
 865   }
 866   std::map<Node, std::map<Node, bool> > parents_proc;
 867   for (const Node& n : nvsets)
 868   {
 869     Trace("sets-nf-debug") << "Carry nf for term " << n << std::endl;
 870     if (d_card_parent[n].empty())
 871     {
 872       // nothing to do
 873       continue;
 874     }
 875     Assert(d_localBase.find(n) != d_localBase.end());
 876     Node cbase = d_localBase[n];
 877     Trace("sets-nf-debug") << "Card base is " << cbase << std::endl;
 878     for (const Node& p : d_card_parent[n])
 879     {
 880       Trace("sets-nf-debug") << "Check parent " << p << std::endl;
 881       if (parents_proc[cbase].find(p) != parents_proc[cbase].end())
 882       {
 883         Trace("sets-nf-debug") << "..already processed parent " << p << " for "
 884                                << cbase << std::endl;
 885         continue;
 886       }
 887       parents_proc[cbase][p] = true;
 888       Trace("sets-nf-debug") << "Carry nf to parent ( " << cbase << ", [" << p
 889                              << "] ), from " << n << "..." << std::endl;
 890
 891       std::vector<Node>& ffpc = d_ff[p][cbase];
 892       for (const Node& nfeqci : nfeqc)
 893       {
 894         if (std::find(ffpc.begin(), ffpc.end(), nfeqci) == ffpc.end())
 895         {
 896           ffpc.insert(ffpc.end(), nfeqc.begin(), nfeqc.end());
 897         }
 898         else
 899         {
 900           // if it is a duplicate venn region, it must be empty since it is
 901           // coming from syntactically disjoint siblings
 902         }
 903       }
 904     }
 905   }
 906 }
 907
 908 void CardinalityExtension::checkMinCard()
 909 {
 910   NodeManager* nm = NodeManager::currentNM();
 911   const std::vector<Node>& setEqc = d_state.getSetsEqClasses();
 912   for (int i = (int)(setEqc.size() - 1); i >= 0; i--)
 913   {
 914     Node eqc = setEqc[i];
 915     TypeNode tn = eqc.getType().getSetElementType();
 916     if (d_t_card_enabled.find(tn) == d_t_card_enabled.end())
 917     {
 918       // cardinality is not enabled for this type, skip
 919       continue;
 920     }
 921     // get members in class
 922     const std::map<Node, Node>& pmemsE = d_state.getMembers(eqc);
 923     if (pmemsE.empty())
 924     {
 925       // no members, trivial
 926       continue;
 927     }
 928     std::vector<Node> exp;
 929     std::vector<Node> members;
 930     Node cardTerm;
 931     std::map<Node, Node>::iterator it = d_eqc_to_card_term.find(eqc);
 932     if (it != d_eqc_to_card_term.end())
 933     {
 934       cardTerm = it->second;
 935     }
 936     else
 937     {
 938       cardTerm = nm->mkNode(CARD, eqc);
 939     }
 940     for (const std::pair<const Node, Node>& itmm : pmemsE)
 941     {
 942       members.push_back(itmm.first);
 943       exp.push_back(nm->mkNode(MEMBER, itmm.first, cardTerm[0]));
 944     }
 945     if (members.size() > 1)
 946     {
 947       exp.push_back(nm->mkNode(DISTINCT, members));
 948     }
 949     if (!members.empty())
 950     {
 951       Node conc =
 952           nm->mkNode(GEQ, cardTerm, nm->mkConst(Rational(members.size())));
 953       Node expn = exp.size() == 1 ? exp[0] : nm->mkNode(AND, exp);
 954       d_im.assertInference(conc, expn, "mincard", 1);
 955     }
 956   }
 957   // flush the lemmas
 958   d_im.flushPendingLemmas();
 959 }
 960
 961 bool CardinalityExtension::isModelValueBasic(Node eqc)
 962 {
 963   return d_nf[eqc].size() == 1 && d_nf[eqc][0] == eqc;
 964 }
 965
 966 void CardinalityExtension::mkModelValueElementsFor(
 967     Valuation& val,
 968     Node eqc,
 969     std::vector<Node>& els,
 970     const std::map<Node, Node>& mvals,
 971     TheoryModel* model)
 972 {
 973   TypeNode elementType = eqc.getType().getSetElementType();
 974   if (isModelValueBasic(eqc))
 975   {
 976     std::map<Node, Node>::iterator it = d_eqc_to_card_term.find(eqc);
 977     if (it != d_eqc_to_card_term.end())
 978     {
 979       // slack elements from cardinality value
 980       Node v = val.getModelValue(it->second);
 981       Trace("sets-model") << "Cardinality of " << eqc << " is " << v
 982                           << std::endl;
 983       Assert(v.getConst<Rational>() <= LONG_MAX)
 984           << "Exceeded LONG_MAX in sets model";
 985       unsigned vu = v.getConst<Rational>().getNumerator().toUnsignedInt();
 986       Assert(els.size() <= vu);
 987       NodeManager* nm = NodeManager::currentNM();
 988       if (elementType.isInterpretedFinite())
 989       {
 990         // get all members of this finite type
 991         collectFiniteTypeSetElements(model);
 992       }
 993       while (els.size() < vu)
 994       {
 995         if (elementType.isInterpretedFinite())
 996         {
 997           // At this point we are sure the formula is satisfiable and all
 998           // cardinality constraints are satisfied. Since this type is finite,
 999           // there is only one single cardinality graph for all sets of this
1000           // type because the universe cardinality constraint has been added by
1001           // CardinalityExtension::checkFiniteType. This means we have enough
1002           // slack elements of this finite type for all disjoint leaves in the
1003           // cardinality graph. Therefore we can safely add new distinct slack
1004           // elements for the leaves without worrying about conflicts with the
1005           // current members of this finite type.
1006
1007           Node slack = nm->mkSkolem("slack", elementType);
1008           Node singleton = nm->mkNode(SINGLETON, slack);
1009           els.push_back(singleton);
1010           d_finite_type_slack_elements[elementType].push_back(slack);
1011           Trace("sets-model") << "Added slack element " << slack << " to set "
1012                               << eqc << std::endl;
1013         }
1014         else
1015         {
1016           els.push_back(
1017               nm->mkNode(SINGLETON, nm->mkSkolem("msde", elementType)));
1018         }
1019       }
1020     }
1021     else
1022     {
1023       Trace("sets-model") << "No slack elements for " << eqc << std::endl;
1024     }
1025   }
1026   else
1027   {
1028     Trace("sets-model") << "Build value for " << eqc
1029                         << " based on normal form, size = " << d_nf[eqc].size()
1030                         << std::endl;
1031     // it is union of venn regions
1032     for (unsigned j = 0; j < d_nf[eqc].size(); j++)
1033     {
1034       std::map<Node, Node>::const_iterator itm = mvals.find(d_nf[eqc][j]);
1035       if (itm != mvals.end())
1036       {
1037         els.push_back(itm->second);
1038       }
1039       else
1040       {
1041         Assert(false);
1042       }
1043     }
1044   }
1045 }
1046
1047 void CardinalityExtension::collectFiniteTypeSetElements(TheoryModel* model)
1048 {
1049   if (d_finite_type_constants_processed)
1050   {
1051     return;
1052   }
1053   for (const Node& set : getOrderedSetsEqClasses())
1054   {
1055     if (!set.getType().isInterpretedFinite())
1056     {
1057       continue;
1058     }
1059     if (!isModelValueBasic(set))
1060     {
1061       // only consider leaves in the cardinality graph
1062       continue;
1063     }
1064     for (const std::pair<const Node, Node>& pair : d_state.getMembers(set))
1065     {
1066       Node member = pair.first;
1067       Node modelRepresentative = model->getRepresentative(member);
1068       std::vector<Node>& elements = d_finite_type_elements[member.getType()];
1069       if (std::find(elements.begin(), elements.end(), modelRepresentative)
1070           == elements.end())
1071       {
1072         elements.push_back(modelRepresentative);
1073       }
1074     }
1075   }
1076   d_finite_type_constants_processed = true;
1077 }
1078
1079 const std::vector<Node>& CardinalityExtension::getFiniteTypeMembers(
1080     TypeNode typeNode)
1081 {
1082   return d_finite_type_elements[typeNode];
1083 }
1084
1085 }  // namespace sets
1086 }  // namespace theory
1087 }  // namespace CVC4