src/theory/quantifiers/sygus/sygus_unif_strat.cpp

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