src/theory/quantifiers/sygus/sygus_unif_strat.cpp

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds, Haniel Barbosa, Mathias Preiner
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   7  * Copyright (c) 2009-2021 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.
  11  * ****************************************************************************
  12  *
  13  * Implementation of sygus_unif_strat.
  14  */
  15
  16 #include "theory/quantifiers/sygus/sygus_unif_strat.h"
  17
  18 #include "expr/dtype.h"
  19 #include "expr/dtype_cons.h"
  20 #include "expr/skolem_manager.h"
  21 #include "theory/datatypes/theory_datatypes_utils.h"
  22 #include "theory/quantifiers/sygus/sygus_eval_unfold.h"
  23 #include "theory/quantifiers/sygus/sygus_unif.h"
  24 #include "theory/quantifiers/sygus/term_database_sygus.h"
  25 #include "theory/quantifiers/term_util.h"
  26
  27 using namespace std;
  28 using namespace cvc5::kind;
  29
  30 namespace cvc5 {
  31 namespace theory {
  32 namespace quantifiers {
  33
  34 std::ostream& operator<<(std::ostream& os, EnumRole r)
  35 {
  36   switch (r)
  37   {
  38     case enum_invalid: os << "INVALID"; break;
  39     case enum_io: os << "IO"; break;
  40     case enum_ite_condition: os << "CONDITION"; break;
  41     case enum_concat_term: os << "CTERM"; break;
  42     default: os << "enum_" << static_cast<unsigned>(r); break;
  43   }
  44   return os;
  45 }
  46
  47 std::ostream& operator<<(std::ostream& os, NodeRole r)
  48 {
  49   switch (r)
  50   {
  51     case role_equal: os << "equal"; break;
  52     case role_string_prefix: os << "string_prefix"; break;
  53     case role_string_suffix: os << "string_suffix"; break;
  54     case role_ite_condition: os << "ite_condition"; break;
  55     default: os << "role_" << static_cast<unsigned>(r); break;
  56   }
  57   return os;
  58 }
  59
  60 EnumRole getEnumeratorRoleForNodeRole(NodeRole r)
  61 {
  62   switch (r)
  63   {
  64     case role_equal: return enum_io; break;
  65     case role_string_prefix: return enum_concat_term; break;
  66     case role_string_suffix: return enum_concat_term; break;
  67     case role_ite_condition: return enum_ite_condition; break;
  68     default: break;
  69   }
  70   return enum_invalid;
  71 }
  72
  73 std::ostream& operator<<(std::ostream& os, StrategyType st)
  74 {
  75   switch (st)
  76   {
  77     case strat_ITE: os << "ITE"; break;
  78     case strat_CONCAT_PREFIX: os << "CONCAT_PREFIX"; break;
  79     case strat_CONCAT_SUFFIX: os << "CONCAT_SUFFIX"; break;
  80     case strat_ID: os << "ID"; break;
  81     default: os << "strat_" << static_cast<unsigned>(st); break;
  82   }
  83   return os;
  84 }
  85
  86 void SygusUnifStrategy::initialize(TermDbSygus* tds,
  87                                    Node f,
  88                                    std::vector<Node>& enums)
  89 {
  90   Assert(d_candidate.isNull());
  91   d_candidate = f;
  92   d_root = f.getType();
  93   d_tds = tds;
  94
  95   // collect the enumerator types and form the strategy
  96   buildStrategyGraph(d_root, role_equal);
  97   // add the enumerators
  98   enums.insert(enums.end(), d_esym_list.begin(), d_esym_list.end());
  99   // finish the initialization of the strategy
 100   // this computes if each node is conditional
 101   std::map<Node, std::map<NodeRole, bool> > visited;
 102   finishInit(getRootEnumerator(), role_equal, visited, false);
 103 }
 104
 105 void SygusUnifStrategy::initializeType(TypeNode tn)
 106 {
 107   Trace("sygus-unif") << "SygusUnifStrategy: initialize : " << tn << " for "
 108                       << d_candidate << std::endl;
 109   d_tinfo[tn].d_this_type = tn;
 110 }
 111
 112 Node SygusUnifStrategy::getRootEnumerator() const
 113 {
 114   std::map<TypeNode, EnumTypeInfo>::const_iterator itt = d_tinfo.find(d_root);
 115   Assert(itt != d_tinfo.end());
 116   std::map<EnumRole, Node>::const_iterator it =
 117       itt->second.d_enum.find(enum_io);
 118   Assert(it != itt->second.d_enum.end());
 119   return it->second;
 120 }
 121
 122 EnumInfo& SygusUnifStrategy::getEnumInfo(Node e)
 123 {
 124   std::map<Node, EnumInfo>::iterator it = d_einfo.find(e);
 125   Assert(it != d_einfo.end());
 126   return it->second;
 127 }
 128
 129 EnumTypeInfo& SygusUnifStrategy::getEnumTypeInfo(TypeNode tn)
 130 {
 131   Trace("sygus-unif") << "SygusUnifStrategy: get : " << tn << " for "
 132                       << d_candidate << std::endl;
 133   std::map<TypeNode, EnumTypeInfo>::iterator it = d_tinfo.find(tn);
 134   Assert(it != d_tinfo.end());
 135   return it->second;
 136 }
 137 // ----------------------------- establishing enumeration types
 138
 139 void SygusUnifStrategy::registerStrategyPoint(Node et,
 140                                            TypeNode tn,
 141                                            EnumRole enum_role,
 142                                            bool inSearch)
 143 {
 144   if (d_einfo.find(et) == d_einfo.end())
 145   {
 146     Trace("sygus-unif-debug")
 147         << "...register " << et << " for " << tn.getDType().getName();
 148     Trace("sygus-unif-debug") << ", role = " << enum_role
 149                               << ", in search = " << inSearch << std::endl;
 150     d_einfo[et].initialize(enum_role);
 151     // if we are actually enumerating this (could be a compound node in the
 152     // strategy)
 153     if (inSearch)
 154     {
 155       std::map<TypeNode, Node>::iterator itn = d_master_enum.find(tn);
 156       if (itn == d_master_enum.end())
 157       {
 158         // use this for the search
 159         d_master_enum[tn] = et;
 160         d_esym_list.push_back(et);
 161         d_einfo[et].d_enum_slave.push_back(et);
 162       }
 163       else
 164       {
 165         Trace("sygus-unif-debug") << "Make " << et << " a slave of "
 166                                   << itn->second << std::endl;
 167         d_einfo[itn->second].d_enum_slave.push_back(et);
 168       }
 169     }
 170   }
 171 }
 172
 173 void SygusUnifStrategy::buildStrategyGraph(TypeNode tn, NodeRole nrole)
 174 {
 175   NodeManager* nm = NodeManager::currentNM();
 176   SkolemManager* sm = nm->getSkolemManager();
 177   if (d_tinfo.find(tn) == d_tinfo.end())
 178   {
 179     // register type
 180     Trace("sygus-unif") << "Register enumerating type : " << tn << std::endl;
 181     initializeType(tn);
 182   }
 183   EnumTypeInfo& eti = d_tinfo[tn];
 184   std::map<NodeRole, StrategyNode>::iterator itsn = eti.d_snodes.find(nrole);
 185   if (itsn != eti.d_snodes.end())
 186   {
 187     // already initialized
 188     return;
 189   }
 190   StrategyNode& snode = eti.d_snodes[nrole];
 191
 192   // get the enumerator for this
 193   EnumRole erole = getEnumeratorRoleForNodeRole(nrole);
 194
 195   Node ee;
 196   std::map<EnumRole, Node>::iterator iten = eti.d_enum.find(erole);
 197   if (iten == eti.d_enum.end())
 198   {
 199     ee = sm->mkDummySkolem("ee", tn);
 200     eti.d_enum[erole] = ee;
 201     Trace("sygus-unif-debug")
 202         << "...enumerator " << ee << " for " << tn.getDType().getName()
 203         << ", role = " << erole << std::endl;
 204   }
 205   else
 206   {
 207     ee = iten->second;
 208   }
 209
 210   // roles that we do not recurse on
 211   if (nrole == role_ite_condition)
 212   {
 213     Trace("sygus-unif-debug") << "...this register (non-io)" << std::endl;
 214     registerStrategyPoint(ee, tn, erole, true);
 215     return;
 216   }
 217
 218   // look at information on how we will construct solutions for this type
 219   // we know this is a sygus datatype since it is either the top-level type
 220   // in the strategy graph, or was recursed by a strategy we inferred.
 221   Assert(tn.isDatatype());
 222   const DType& dt = tn.getDType();
 223   Assert(dt.isSygus());
 224
 225   std::map<Node, std::vector<StrategyType> > cop_to_strat;
 226   std::map<Node, unsigned> cop_to_cindex;
 227   std::map<Node, std::map<unsigned, Node> > cop_to_child_templ;
 228   std::map<Node, std::map<unsigned, Node> > cop_to_child_templ_arg;
 229   std::map<Node, std::vector<unsigned> > cop_to_carg_list;
 230   std::map<Node, std::vector<TypeNode> > cop_to_child_types;
 231   std::map<Node, std::vector<Node> > cop_to_sks;
 232
 233   // whether we will enumerate the current type
 234   bool search_this = false;
 235   for (unsigned j = 0, ncons = dt.getNumConstructors(); j < ncons; j++)
 236   {
 237     Node cop = dt[j].getConstructor();
 238     Node op = dt[j].getSygusOp();
 239     Trace("sygus-unif-debug") << "--- Infer strategy from " << cop
 240                               << " with sygus op " << op << "..." << std::endl;
 241
 242     // expand the evaluation to see if this constuctor induces a strategy
 243     std::vector<Node> utchildren;
 244     utchildren.push_back(cop);
 245     std::vector<Node> sks;
 246     std::vector<TypeNode> sktns;
 247     for (unsigned k = 0, nargs = dt[j].getNumArgs(); k < nargs; k++)
 248     {
 249       TypeNode ttn = dt[j][k].getRangeType();
 250       Node kv = sm->mkDummySkolem("ut", ttn);
 251       sks.push_back(kv);
 252       cop_to_sks[cop].push_back(kv);
 253       sktns.push_back(ttn);
 254       utchildren.push_back(kv);
 255     }
 256     Node ut = nm->mkNode(APPLY_CONSTRUCTOR, utchildren);
 257     std::vector<Node> echildren;
 258     echildren.push_back(ut);
 259     Node sbvl = dt.getSygusVarList();
 260     for (const Node& sbv : sbvl)
 261     {
 262       echildren.push_back(sbv);
 263     }
 264     Node eut = nm->mkNode(DT_SYGUS_EVAL, echildren);
 265     Trace("sygus-unif-debug2") << "  Test evaluation of " << eut << "..."
 266                                << std::endl;
 267     eut = d_tds->rewriteNode(eut);
 268     Trace("sygus-unif-debug2") << "  ...got " << eut;
 269     Trace("sygus-unif-debug2") << ", type : " << eut.getType() << std::endl;
 270
 271     // candidate strategy
 272     if (eut.getKind() == ITE)
 273     {
 274       cop_to_strat[cop].push_back(strat_ITE);
 275     }
 276     else if (eut.getKind() == STRING_CONCAT)
 277     {
 278       if (nrole != role_string_suffix)
 279       {
 280         cop_to_strat[cop].push_back(strat_CONCAT_PREFIX);
 281       }
 282       if (nrole != role_string_prefix)
 283       {
 284         cop_to_strat[cop].push_back(strat_CONCAT_SUFFIX);
 285       }
 286     }
 287     else if (dt[j].isSygusIdFunc())
 288     {
 289       cop_to_strat[cop].push_back(strat_ID);
 290     }
 291
 292     // the kinds for which there is a strategy
 293     if (cop_to_strat.find(cop) != cop_to_strat.end())
 294     {
 295       // infer an injection from the arguments of the datatype
 296       std::map<unsigned, unsigned> templ_injection;
 297       std::vector<Node> vs;
 298       std::vector<Node> ss;
 299       std::map<Node, unsigned> templ_var_index;
 300       for (unsigned k = 0, sksize = sks.size(); k < sksize; k++)
 301       {
 302         Assert(sks[k].getType().isDatatype());
 303         echildren[0] = sks[k];
 304         Trace("sygus-unif-debug2") << "...set eval dt to " << sks[k]
 305                                    << std::endl;
 306         Node esk = nm->mkNode(DT_SYGUS_EVAL, echildren);
 307         vs.push_back(esk);
 308         Node tvar = sm->mkDummySkolem("templ", esk.getType());
 309         templ_var_index[tvar] = k;
 310         Trace("sygus-unif-debug2") << "* template inference : looking for "
 311                                    << tvar << " for arg " << k << std::endl;
 312         ss.push_back(tvar);
 313         Trace("sygus-unif-debug2") << "* substitute : " << esk << " -> " << tvar
 314                                    << std::endl;
 315       }
 316       eut = eut.substitute(vs.begin(), vs.end(), ss.begin(), ss.end());
 317       Trace("sygus-unif-debug2") << "Constructor " << j << ", base term is "
 318                                  << eut << std::endl;
 319       std::map<unsigned, Node> test_args;
 320       if (dt[j].isSygusIdFunc())
 321       {
 322         test_args[0] = eut;
 323       }
 324       else
 325       {
 326         for (unsigned k = 0, size = eut.getNumChildren(); k < size; k++)
 327         {
 328           test_args[k] = eut[k];
 329         }
 330       }
 331
 332       // TODO : prefix grouping prefix/suffix
 333       bool isAssoc = TermUtil::isAssoc(eut.getKind());
 334       Trace("sygus-unif-debug2") << eut.getKind() << " isAssoc = " << isAssoc
 335                                  << std::endl;
 336       std::map<unsigned, std::vector<unsigned> > assoc_combine;
 337       std::vector<unsigned> assoc_waiting;
 338       int assoc_last_valid_index = -1;
 339       for (std::pair<const unsigned, Node>& ta : test_args)
 340       {
 341         unsigned k = ta.first;
 342         Node eut_c = ta.second;
 343         // success if we can find a injection from args to sygus args
 344         if (!inferTemplate(k, eut_c, templ_var_index, templ_injection))
 345         {
 346           Trace("sygus-unif-debug")
 347               << "...fail: could not find injection (range)." << std::endl;
 348           cop_to_strat.erase(cop);
 349           break;
 350         }
 351         std::map<unsigned, unsigned>::iterator itti = templ_injection.find(k);
 352         if (itti != templ_injection.end())
 353         {
 354           // if associative, combine arguments if it is the same variable
 355           if (isAssoc && assoc_last_valid_index >= 0
 356               && itti->second == templ_injection[assoc_last_valid_index])
 357           {
 358             templ_injection.erase(k);
 359             assoc_combine[assoc_last_valid_index].push_back(k);
 360           }
 361           else
 362           {
 363             assoc_last_valid_index = (int)k;
 364             if (!assoc_waiting.empty())
 365             {
 366               assoc_combine[k].insert(assoc_combine[k].end(),
 367                                       assoc_waiting.begin(),
 368                                       assoc_waiting.end());
 369               assoc_waiting.clear();
 370             }
 371             assoc_combine[k].push_back(k);
 372           }
 373         }
 374         else
 375         {
 376           // a ground argument
 377           if (!isAssoc)
 378           {
 379             Trace("sygus-unif-debug")
 380                 << "...fail: could not find injection (functional)."
 381                 << std::endl;
 382             cop_to_strat.erase(cop);
 383             break;
 384           }
 385           else
 386           {
 387             if (assoc_last_valid_index >= 0)
 388             {
 389               assoc_combine[assoc_last_valid_index].push_back(k);
 390             }
 391             else
 392             {
 393               assoc_waiting.push_back(k);
 394             }
 395           }
 396         }
 397       }
 398       if (cop_to_strat.find(cop) != cop_to_strat.end())
 399       {
 400         // construct the templates
 401         if (!assoc_waiting.empty())
 402         {
 403           // could not find a way to fit some arguments into injection
 404           cop_to_strat.erase(cop);
 405         }
 406         else
 407         {
 408           for (std::pair<const unsigned, Node>& ta : test_args)
 409           {
 410             unsigned k = ta.first;
 411             Trace("sygus-unif-debug2") << "- processing argument " << k << "..."
 412                                        << std::endl;
 413             if (templ_injection.find(k) != templ_injection.end())
 414             {
 415               unsigned sk_index = templ_injection[k];
 416               if (std::find(cop_to_carg_list[cop].begin(),
 417                             cop_to_carg_list[cop].end(),
 418                             sk_index)
 419                   == cop_to_carg_list[cop].end())
 420               {
 421                 cop_to_carg_list[cop].push_back(sk_index);
 422               }
 423               else
 424               {
 425                 Trace("sygus-unif-debug") << "...fail: duplicate argument used"
 426                                           << std::endl;
 427                 cop_to_strat.erase(cop);
 428                 break;
 429               }
 430               // also store the template information, if necessary
 431               Node teut;
 432               if (isAssoc)
 433               {
 434                 std::vector<unsigned>& ac = assoc_combine[k];
 435                 Assert(!ac.empty());
 436                 std::vector<Node> children;
 437                 for (unsigned ack = 0, size_ac = ac.size(); ack < size_ac;
 438                      ack++)
 439                 {
 440                   children.push_back(eut[ac[ack]]);
 441                 }
 442                 teut = children.size() == 1
 443                            ? children[0]
 444                            : nm->mkNode(eut.getKind(), children);
 445                 teut = rewrite(teut);
 446               }
 447               else
 448               {
 449                 teut = ta.second;
 450               }
 451
 452               if (!teut.isVar())
 453               {
 454                 cop_to_child_templ[cop][k] = teut;
 455                 cop_to_child_templ_arg[cop][k] = ss[sk_index];
 456                 Trace("sygus-unif-debug")
 457                     << "  Arg " << k << " (template : " << teut << " arg "
 458                     << ss[sk_index] << "), index " << sk_index << std::endl;
 459               }
 460               else
 461               {
 462                 Trace("sygus-unif-debug") << "  Arg " << k << ", index "
 463                                           << sk_index << std::endl;
 464                 Assert(teut == ss[sk_index]);
 465               }
 466             }
 467             else
 468             {
 469               Assert(isAssoc);
 470             }
 471           }
 472         }
 473       }
 474     }
 475
 476     std::map<Node, std::vector<StrategyType> >::iterator itcs = cop_to_strat.find(cop);
 477     if (itcs != cop_to_strat.end())
 478     {
 479       Trace("sygus-unif") << "-> constructor " << cop
 480                           << " matches strategy for " << eut.getKind() << "..."
 481                           << std::endl;
 482       // collect children types
 483       for (unsigned k = 0, size = cop_to_carg_list[cop].size(); k < size; k++)
 484       {
 485         TypeNode ctn = sktns[cop_to_carg_list[cop][k]];
 486         Trace("sygus-unif-debug") << "   Child type " << k << " : "
 487                                   << ctn.getDType().getName() << std::endl;
 488         cop_to_child_types[cop].push_back(ctn);
 489       }
 490       // if there are checks on the consistency of child types wrt strategies,
 491       // these should be enforced here. We currently have none.
 492     }
 493     if (cop_to_strat.find(cop) == cop_to_strat.end())
 494     {
 495       Trace("sygus-unif") << "...constructor " << cop
 496                           << " does not correspond to a strategy." << std::endl;
 497       search_this = true;
 498     }
 499   }
 500
 501   // check whether we should also enumerate the current type
 502   Trace("sygus-unif-debug2") << "  register this strategy ..." << std::endl;
 503   registerStrategyPoint(ee, tn, erole, search_this);
 504
 505   if (cop_to_strat.empty())
 506   {
 507     Trace("sygus-unif") << "...consider " << dt.getName() << " a basic type"
 508                         << std::endl;
 509   }
 510   else
 511   {
 512     for (std::pair<const Node, std::vector<StrategyType> >& cstr : cop_to_strat)
 513     {
 514       Node cop = cstr.first;
 515       Trace("sygus-unif-debug") << "Constructor " << cop << " has "
 516                                 << cstr.second.size() << " strategies..."
 517                                 << std::endl;
 518       for (unsigned s = 0, ssize = cstr.second.size(); s < ssize; s++)
 519       {
 520         EnumTypeInfoStrat* cons_strat = new EnumTypeInfoStrat;
 521         StrategyType strat = cstr.second[s];
 522
 523         cons_strat->d_this = strat;
 524         cons_strat->d_cons = cop;
 525         Trace("sygus-unif-debug") << "Process strategy #" << s
 526                                   << " for operator : " << cop << " : " << strat
 527                                   << std::endl;
 528         Assert(cop_to_child_types.find(cop) != cop_to_child_types.end());
 529         std::vector<TypeNode>& childTypes = cop_to_child_types[cop];
 530         Assert(cop_to_carg_list.find(cop) != cop_to_carg_list.end());
 531         std::vector<unsigned>& cargList = cop_to_carg_list[cop];
 532
 533         std::vector<Node> sol_templ_children;
 534         sol_templ_children.resize(cop_to_sks[cop].size());
 535
 536         for (unsigned j = 0, csize = childTypes.size(); j < csize; j++)
 537         {
 538           // calculate if we should allocate a new enumerator : should be true
 539           // if we have a new role
 540           NodeRole nrole_c = nrole;
 541           if (strat == strat_ITE)
 542           {
 543             if (j == 0)
 544             {
 545               nrole_c = role_ite_condition;
 546             }
 547           }
 548           else if (strat == strat_CONCAT_PREFIX)
 549           {
 550             if ((j + 1) < childTypes.size())
 551             {
 552               nrole_c = role_string_prefix;
 553             }
 554           }
 555           else if (strat == strat_CONCAT_SUFFIX)
 556           {
 557             if (j > 0)
 558             {
 559               nrole_c = role_string_suffix;
 560             }
 561           }
 562           // in all other cases, role is same as parent
 563
 564           // register the child type
 565           TypeNode ct = childTypes[j];
 566           Node csk = cop_to_sks[cop][cargList[j]];
 567           cons_strat->d_sol_templ_args.push_back(csk);
 568           sol_templ_children[cargList[j]] = csk;
 569
 570           EnumRole erole_c = getEnumeratorRoleForNodeRole(nrole_c);
 571           // make the enumerator
 572           Node et;
 573           // Build the strategy recursively, regardless of whether the
 574           // enumerator is templated.
 575           buildStrategyGraph(ct, nrole_c);
 576           if (cop_to_child_templ[cop].find(j) != cop_to_child_templ[cop].end())
 577           {
 578             // it is templated, allocate a fresh variable
 579             et = sm->mkDummySkolem("et", ct);
 580             Trace("sygus-unif-debug") << "...enumerate " << et << " of type "
 581                                       << ct.getDType().getName();
 582             Trace("sygus-unif-debug") << " for arg " << j << " of "
 583                                       << tn.getDType().getName() << std::endl;
 584             registerStrategyPoint(et, ct, erole_c, true);
 585             d_einfo[et].d_template = cop_to_child_templ[cop][j];
 586             d_einfo[et].d_template_arg = cop_to_child_templ_arg[cop][j];
 587             Assert(!d_einfo[et].d_template.isNull());
 588             Assert(!d_einfo[et].d_template_arg.isNull());
 589           }
 590           else
 591           {
 592             Trace("sygus-unif-debug")
 593                 << "...child type enumerate " << ct.getDType().getName()
 594                 << ", node role = " << nrole_c << std::endl;
 595             // otherwise use the previous
 596             Assert(d_tinfo[ct].d_enum.find(erole_c)
 597                    != d_tinfo[ct].d_enum.end());
 598             et = d_tinfo[ct].d_enum[erole_c];
 599           }
 600           Trace("sygus-unif-debug") << "Register child enumerator " << et
 601                                     << ", arg " << j << " of " << cop
 602                                     << ", role = " << erole_c << std::endl;
 603           Assert(!et.isNull());
 604           cons_strat->d_cenum.push_back(std::pair<Node, NodeRole>(et, nrole_c));
 605         }
 606         // children that are unused in the strategy can be arbitrary
 607         for (unsigned j = 0, stsize = sol_templ_children.size(); j < stsize;
 608              j++)
 609         {
 610           if (sol_templ_children[j].isNull())
 611           {
 612             sol_templ_children[j] = cop_to_sks[cop][j].getType().mkGroundTerm();
 613           }
 614         }
 615         sol_templ_children.insert(sol_templ_children.begin(), cop);
 616         cons_strat->d_sol_templ =
 617             nm->mkNode(APPLY_CONSTRUCTOR, sol_templ_children);
 618         if (strat == strat_CONCAT_SUFFIX)
 619         {
 620           std::reverse(cons_strat->d_cenum.begin(), cons_strat->d_cenum.end());
 621           std::reverse(cons_strat->d_sol_templ_args.begin(),
 622                        cons_strat->d_sol_templ_args.end());
 623         }
 624         if (Trace.isOn("sygus-unif"))
 625         {
 626           Trace("sygus-unif") << "Initialized strategy " << strat;
 627           Trace("sygus-unif")
 628               << " for " << tn.getDType().getName() << ", operator " << cop;
 629           Trace("sygus-unif") << ", #children = " << cons_strat->d_cenum.size()
 630                               << ", solution template = (lambda ( ";
 631           for (const Node& targ : cons_strat->d_sol_templ_args)
 632           {
 633             Trace("sygus-unif") << targ << " ";
 634           }
 635           Trace("sygus-unif") << ") " << cons_strat->d_sol_templ << ")";
 636           Trace("sygus-unif") << std::endl;
 637         }
 638         // make the strategy
 639         snode.d_strats.push_back(cons_strat);
 640       }
 641     }
 642   }
 643 }
 644
 645 bool SygusUnifStrategy::inferTemplate(
 646     unsigned k,
 647     Node n,
 648     std::map<Node, unsigned>& templ_var_index,
 649     std::map<unsigned, unsigned>& templ_injection)
 650 {
 651   if (n.getNumChildren() == 0)
 652   {
 653     std::map<Node, unsigned>::iterator itt = templ_var_index.find(n);
 654     if (itt != templ_var_index.end())
 655     {
 656       unsigned kk = itt->second;
 657       std::map<unsigned, unsigned>::iterator itti = templ_injection.find(k);
 658       if (itti == templ_injection.end())
 659       {
 660         Trace("sygus-unif-debug") << "...set template injection " << k << " -> "
 661                                   << kk << std::endl;
 662         templ_injection[k] = kk;
 663       }
 664       else if (itti->second != kk)
 665       {
 666         // two distinct variables in this term, we fail
 667         return false;
 668       }
 669     }
 670     return true;
 671   }
 672   else
 673   {
 674     for (unsigned i = 0; i < n.getNumChildren(); i++)
 675     {
 676       if (!inferTemplate(k, n[i], templ_var_index, templ_injection))
 677       {
 678         return false;
 679       }
 680     }
 681   }
 682   return true;
 683 }
 684
 685 void SygusUnifStrategy::staticLearnRedundantOps(
 686     std::map<Node, std::vector<Node>>& strategy_lemmas)
 687 {
 688   StrategyRestrictions restrictions;
 689   staticLearnRedundantOps(strategy_lemmas, restrictions);
 690 }
 691
 692 void SygusUnifStrategy::staticLearnRedundantOps(
 693     std::map<Node, std::vector<Node>>& strategy_lemmas,
 694     StrategyRestrictions& restrictions)
 695 {
 696   for (unsigned i = 0; i < d_esym_list.size(); i++)
 697   {
 698     Node e = d_esym_list[i];
 699     std::map<Node, EnumInfo>::iterator itn = d_einfo.find(e);
 700     Assert(itn != d_einfo.end());
 701     // see if there is anything we can eliminate
 702     Trace("sygus-unif") << "* Search enumerator #" << i << " : type "
 703                         << e.getType().getDType().getName() << " : ";
 704     Trace("sygus-unif") << e << " has " << itn->second.d_enum_slave.size()
 705                         << " slaves:" << std::endl;
 706     for (unsigned j = 0; j < itn->second.d_enum_slave.size(); j++)
 707     {
 708       Node es = itn->second.d_enum_slave[j];
 709       std::map<Node, EnumInfo>::iterator itns = d_einfo.find(es);
 710       Assert(itns != d_einfo.end());
 711       Trace("sygus-unif") << "  " << es << ", role = " << itns->second.getRole()
 712                           << std::endl;
 713     }
 714   }
 715   Trace("sygus-unif") << std::endl;
 716   Trace("sygus-unif") << "Strategy for candidate " << d_candidate
 717                       << " is : " << std::endl;
 718   debugPrint("sygus-unif");
 719   std::map<Node, std::map<NodeRole, bool> > visited;
 720   std::map<Node, std::map<unsigned, bool> > needs_cons;
 721   staticLearnRedundantOps(
 722       getRootEnumerator(), role_equal, visited, needs_cons, restrictions);
 723   // now, check the needs_cons map
 724   for (std::pair<const Node, std::map<unsigned, bool> >& nce : needs_cons)
 725   {
 726     Node em = nce.first;
 727     const DType& dt = em.getType().getDType();
 728     std::vector<Node> lemmas;
 729     for (std::pair<const unsigned, bool>& nc : nce.second)
 730     {
 731       Assert(nc.first < dt.getNumConstructors());
 732       if (!nc.second)
 733       {
 734         Node tst = datatypes::utils::mkTester(em, nc.first, dt).negate();
 735
 736         if (std::find(lemmas.begin(), lemmas.end(), tst) == lemmas.end())
 737         {
 738           Trace("sygus-unif") << "...can exclude based on  : " << tst
 739                               << std::endl;
 740           lemmas.push_back(tst);
 741         }
 742       }
 743     }
 744     if (!lemmas.empty())
 745     {
 746       strategy_lemmas[em] = lemmas;
 747     }
 748   }
 749 }
 750
 751 void SygusUnifStrategy::debugPrint(const char* c)
 752 {
 753   if (Trace.isOn(c))
 754   {
 755     std::map<Node, std::map<NodeRole, bool> > visited;
 756     debugPrint(c, getRootEnumerator(), role_equal, visited, 0);
 757   }
 758 }
 759
 760 void SygusUnifStrategy::staticLearnRedundantOps(
 761     Node e,
 762     NodeRole nrole,
 763     std::map<Node, std::map<NodeRole, bool>>& visited,
 764     std::map<Node, std::map<unsigned, bool>>& needs_cons,
 765     StrategyRestrictions& restrictions)
 766 {
 767   if (visited[e].find(nrole) != visited[e].end())
 768   {
 769     return;
 770   }
 771   Trace("sygus-strat-slearn") << "Learn redundant operators " << e << " "
 772                               << nrole << "..." << std::endl;
 773   visited[e][nrole] = true;
 774   EnumInfo& ei = getEnumInfo(e);
 775   if (ei.isTemplated())
 776   {
 777     return;
 778   }
 779   TypeNode etn = e.getType();
 780   EnumTypeInfo& tinfo = getEnumTypeInfo(etn);
 781   StrategyNode& snode = tinfo.getStrategyNode(nrole);
 782   // the constructors of the current strategy point we need
 783   std::map<unsigned, bool> needs_cons_curr;
 784   // get the unused strategies
 785   std::map<Node, std::unordered_set<unsigned>>::iterator itus =
 786       restrictions.d_unused_strategies.find(e);
 787   std::unordered_set<unsigned> unused_strats;
 788   if (itus != restrictions.d_unused_strategies.end())
 789   {
 790     unused_strats.insert(itus->second.begin(), itus->second.end());
 791   }
 792   for (unsigned j = 0, size = snode.d_strats.size(); j < size; j++)
 793   {
 794     // if we are not using this strategy, there is nothing to do
 795     if (unused_strats.find(j) != unused_strats.end())
 796     {
 797       continue;
 798     }
 799     EnumTypeInfoStrat* etis = snode.d_strats[j];
 800     unsigned cindex = datatypes::utils::indexOf(etis->d_cons);
 801     // constructors that correspond to strategies are not needed
 802     // the intuition is that the strategy itself is responsible for constructing
 803     // all terms that use the given constructor
 804     Trace("sygus-strat-slearn") << "...by strategy, can exclude operator "
 805                                 << etis->d_cons << std::endl;
 806     needs_cons_curr[cindex] = false;
 807     // try to eliminate from etn's datatype all operators except TRUE/FALSE if
 808     // arguments of ITE are the same BOOL type
 809     if (restrictions.d_iteReturnBoolConst)
 810     {
 811       const DType& dt = etn.getDType();
 812       Node op = dt[cindex].getSygusOp();
 813       TypeNode sygus_tn = dt.getSygusType();
 814       if (op.getKind() == kind::BUILTIN
 815           && NodeManager::operatorToKind(op) == ITE && sygus_tn.isBoolean()
 816           && (dt[cindex].getArgType(1) == dt[cindex].getArgType(2)))
 817       {
 818         unsigned ncons = dt.getNumConstructors(), indexT = ncons,
 819                  indexF = ncons;
 820         for (unsigned k = 0; k < ncons; ++k)
 821         {
 822           Node op_arg = dt[k].getSygusOp();
 823           if (dt[k].getNumArgs() > 0 || !op_arg.isConst())
 824           {
 825             continue;
 826           }
 827           if (op_arg.getConst<bool>())
 828           {
 829             indexT = k;
 830           }
 831           else
 832           {
 833             indexF = k;
 834           }
 835         }
 836         if (indexT < ncons && indexF < ncons)
 837         {
 838           Trace("sygus-strat-slearn")
 839               << "...for ite boolean arg, can exclude all operators but T/F\n";
 840           for (unsigned k = 0; k < ncons; ++k)
 841           {
 842             needs_cons_curr[k] = false;
 843           }
 844           needs_cons_curr[indexT] = true;
 845           needs_cons_curr[indexF] = true;
 846         }
 847       }
 848     }
 849     for (std::pair<Node, NodeRole>& cec : etis->d_cenum)
 850     {
 851       staticLearnRedundantOps(
 852           cec.first, cec.second, visited, needs_cons, restrictions);
 853     }
 854   }
 855   // get the current datatype
 856   const DType& dt = etn.getDType();
 857   // do not use recursive Boolean connectives for conditions of ITEs
 858   if (nrole == role_ite_condition && restrictions.d_iteCondOnlyAtoms)
 859   {
 860     TypeNode sygus_tn = dt.getSygusType();
 861     for (unsigned j = 0, size = dt.getNumConstructors(); j < size; j++)
 862     {
 863       Node op = dt[j].getSygusOp();
 864       Trace("sygus-strat-slearn")
 865           << "...for ite condition, look at operator : " << op << std::endl;
 866       if (op.isConst() && dt[j].getNumArgs() == 0)
 867       {
 868         Trace("sygus-strat-slearn")
 869             << "...for ite condition, can exclude Boolean constant " << op
 870             << std::endl;
 871         needs_cons_curr[j] = false;
 872         continue;
 873       }
 874       if (op.getKind() == kind::BUILTIN)
 875       {
 876         Kind kind = NodeManager::operatorToKind(op);
 877         if (kind == NOT || kind == OR || kind == AND || kind == ITE)
 878         {
 879           // can eliminate if their argument types are simple loops to this type
 880           bool type_ok = true;
 881           for (unsigned k = 0, nargs = dt[j].getNumArgs(); k < nargs; k++)
 882           {
 883             TypeNode tn = dt[j].getArgType(k);
 884             if (tn != etn)
 885             {
 886               type_ok = false;
 887               break;
 888             }
 889           }
 890           if (type_ok)
 891           {
 892             Trace("sygus-strat-slearn")
 893                 << "...for ite condition, can exclude Boolean connective : "
 894                 << op << std::endl;
 895             needs_cons_curr[j] = false;
 896           }
 897         }
 898       }
 899     }
 900   }
 901   // all other constructors are needed
 902   for (unsigned j = 0, size = dt.getNumConstructors(); j < size; j++)
 903   {
 904     if (needs_cons_curr.find(j) == needs_cons_curr.end())
 905     {
 906       needs_cons_curr[j] = true;
 907     }
 908   }
 909   // update the constructors that the master enumerator needs
 910   if (needs_cons.find(e) == needs_cons.end())
 911   {
 912     needs_cons[e] = needs_cons_curr;
 913   }
 914   else
 915   {
 916     for (unsigned j = 0, size = dt.getNumConstructors(); j < size; j++)
 917     {
 918       needs_cons[e][j] = needs_cons[e][j] || needs_cons_curr[j];
 919     }
 920   }
 921 }
 922
 923 void SygusUnifStrategy::finishInit(
 924     Node e,
 925     NodeRole nrole,
 926     std::map<Node, std::map<NodeRole, bool> >& visited,
 927     bool isCond)
 928 {
 929   EnumInfo& ei = getEnumInfo(e);
 930   if (visited[e].find(nrole) != visited[e].end()
 931       && (!isCond || ei.isConditional()))
 932   {
 933     return;
 934   }
 935   visited[e][nrole] = true;
 936   // set conditional
 937   if (isCond)
 938   {
 939     ei.setConditional();
 940   }
 941   if (ei.isTemplated())
 942   {
 943     return;
 944   }
 945   TypeNode etn = e.getType();
 946   EnumTypeInfo& tinfo = getEnumTypeInfo(etn);
 947   StrategyNode& snode = tinfo.getStrategyNode(nrole);
 948   for (unsigned j = 0, size = snode.d_strats.size(); j < size; j++)
 949   {
 950     EnumTypeInfoStrat* etis = snode.d_strats[j];
 951     StrategyType strat = etis->d_this;
 952     bool newIsCond = isCond || strat == strat_ITE;
 953     for (std::pair<Node, NodeRole>& cec : etis->d_cenum)
 954     {
 955       finishInit(cec.first, cec.second, visited, newIsCond);
 956     }
 957   }
 958 }
 959
 960 void SygusUnifStrategy::debugPrint(
 961     const char* c,
 962     Node e,
 963     NodeRole nrole,
 964     std::map<Node, std::map<NodeRole, bool> >& visited,
 965     int ind)
 966 {
 967   if (visited[e].find(nrole) != visited[e].end())
 968   {
 969     indent(c, ind);
 970     Trace(c) << e << " :: node role : " << nrole << std::endl;
 971     return;
 972   }
 973   visited[e][nrole] = true;
 974   EnumInfo& ei = getEnumInfo(e);
 975
 976   TypeNode etn = e.getType();
 977
 978   indent(c, ind);
 979   Trace(c) << e << " :: node role : " << nrole;
 980   Trace(c) << ", type : " << etn.getDType().getName();
 981   if (ei.isConditional())
 982   {
 983     Trace(c) << ", conditional";
 984   }
 985   Trace(c) << ", enum role : " << ei.getRole();
 986
 987   if (ei.isTemplated())
 988   {
 989     Trace(c) << ", templated : (lambda " << ei.d_template_arg << " "
 990              << ei.d_template << ")" << std::endl;
 991     return;
 992   }
 993   Trace(c) << std::endl;
 994
 995   EnumTypeInfo& tinfo = getEnumTypeInfo(etn);
 996   StrategyNode& snode = tinfo.getStrategyNode(nrole);
 997   for (unsigned j = 0, size = snode.d_strats.size(); j < size; j++)
 998   {
 999     EnumTypeInfoStrat* etis = snode.d_strats[j];
1000     StrategyType strat = etis->d_this;
1001     indent(c, ind + 1);
1002     Trace(c) << "Strategy : " << strat << ", from cons : " << etis->d_cons
1003              << std::endl;
1004     for (std::pair<Node, NodeRole>& cec : etis->d_cenum)
1005     {
1006       // recurse
1007       debugPrint(c, cec.first, cec.second, visited, ind + 2);
1008     }
1009   }
1010 }
1011
1012 void EnumInfo::initialize(EnumRole role) { d_role = role; }
1013
1014 StrategyNode& EnumTypeInfo::getStrategyNode(NodeRole nrole)
1015 {
1016   std::map<NodeRole, StrategyNode>::iterator it = d_snodes.find(nrole);
1017   Assert(it != d_snodes.end());
1018   return it->second;
1019 }
1020
1021 bool EnumTypeInfoStrat::isValid(UnifContext& x)
1022 {
1023   if ((x.getCurrentRole() == role_string_prefix
1024        && d_this == strat_CONCAT_SUFFIX)
1025       || (x.getCurrentRole() == role_string_suffix
1026           && d_this == strat_CONCAT_PREFIX))
1027   {
1028     return false;
1029   }
1030   return true;
1031 }
1032
1033 StrategyNode::~StrategyNode()
1034 {
1035   for (unsigned j = 0, size = d_strats.size(); j < size; j++)
1036   {
1037     delete d_strats[j];
1038   }
1039   d_strats.clear();
1040 }
1041
1042 void SygusUnifStrategy::indent(const char* c, int ind)
1043 {
1044   if (Trace.isOn(c))
1045   {
1046     for (int i = 0; i < ind; i++)
1047     {
1048       Trace(c) << "  ";
1049     }
1050   }
1051 }
1052
1053 }  // namespace quantifiers
1054 }  // namespace theory
1055 }  // namespace cvc5