src/theory/quantifiers/sygus/sygus_unif_io.cpp

   1 /*********************                                                        */
   2 /*! \file sygus_unif_io.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_io
  13  **/
  14
  15 #include "theory/quantifiers/sygus/sygus_unif_io.h"
  16
  17 #include "theory/datatypes/datatypes_rewriter.h"
  18 #include "theory/quantifiers/sygus/term_database_sygus.h"
  19 #include "theory/quantifiers/term_util.h"
  20 #include "util/random.h"
  21
  22 using namespace CVC4::kind;
  23
  24 namespace CVC4 {
  25 namespace theory {
  26 namespace quantifiers {
  27
  28 UnifContextIo::UnifContextIo() : d_curr_role(role_invalid)
  29 {
  30   d_true = NodeManager::currentNM()->mkConst(true);
  31   d_false = NodeManager::currentNM()->mkConst(false);
  32 }
  33
  34 NodeRole UnifContextIo::getCurrentRole() { return d_curr_role; }
  35
  36 bool UnifContextIo::updateContext(SygusUnifIo* sui,
  37                                   std::vector<Node>& vals,
  38                                   bool pol)
  39 {
  40   Assert(d_vals.size() == vals.size());
  41   bool changed = false;
  42   Node poln = pol ? d_true : d_false;
  43   for (unsigned i = 0; i < vals.size(); i++)
  44   {
  45     if (vals[i] != poln)
  46     {
  47       if (d_vals[i] == d_true)
  48       {
  49         d_vals[i] = d_false;
  50         changed = true;
  51       }
  52     }
  53   }
  54   if (changed)
  55   {
  56     d_visit_role.clear();
  57   }
  58   return changed;
  59 }
  60
  61 bool UnifContextIo::updateStringPosition(SygusUnifIo* sui,
  62                                          std::vector<unsigned>& pos,
  63                                          NodeRole nrole)
  64 {
  65   Assert(pos.size() == d_str_pos.size());
  66   bool changed = false;
  67   for (unsigned i = 0; i < pos.size(); i++)
  68   {
  69     if (pos[i] > 0)
  70     {
  71       d_str_pos[i] += pos[i];
  72       changed = true;
  73     }
  74   }
  75   if (changed)
  76   {
  77     d_visit_role.clear();
  78   }
  79   d_curr_role = nrole;
  80   return changed;
  81 }
  82
  83 void UnifContextIo::initialize(SygusUnifIo* sui)
  84 {
  85   // clear previous data
  86   d_vals.clear();
  87   d_str_pos.clear();
  88   d_curr_role = role_equal;
  89   d_visit_role.clear();
  90   d_uinfo.clear();
  91
  92   // initialize with #examples
  93   unsigned sz = sui->d_examples.size();
  94   for (unsigned i = 0; i < sz; i++)
  95   {
  96     d_vals.push_back(d_true);
  97   }
  98
  99   if (!sui->d_examples_out.empty())
 100   {
 101     // output type of the examples
 102     TypeNode exotn = sui->d_examples_out[0].getType();
 103
 104     if (exotn.isString())
 105     {
 106       for (unsigned i = 0; i < sz; i++)
 107       {
 108         d_str_pos.push_back(0);
 109       }
 110     }
 111   }
 112   d_visit_role.clear();
 113 }
 114
 115 void UnifContextIo::getCurrentStrings(SygusUnifIo* sui,
 116                                       const std::vector<Node>& vals,
 117                                       std::vector<String>& ex_vals)
 118 {
 119   bool isPrefix = d_curr_role == role_string_prefix;
 120   String dummy;
 121   for (unsigned i = 0; i < vals.size(); i++)
 122   {
 123     if (d_vals[i] == sui->d_true)
 124     {
 125       Assert(vals[i].isConst());
 126       unsigned pos_value = d_str_pos[i];
 127       if (pos_value > 0)
 128       {
 129         Assert(d_curr_role != role_invalid);
 130         String s = vals[i].getConst<String>();
 131         Assert(pos_value <= s.size());
 132         ex_vals.push_back(isPrefix ? s.suffix(s.size() - pos_value)
 133                                    : s.prefix(s.size() - pos_value));
 134       }
 135       else
 136       {
 137         ex_vals.push_back(vals[i].getConst<String>());
 138       }
 139     }
 140     else
 141     {
 142       // irrelevant, add dummy
 143       ex_vals.push_back(dummy);
 144     }
 145   }
 146 }
 147
 148 bool UnifContextIo::getStringIncrement(SygusUnifIo* sui,
 149                                        bool isPrefix,
 150                                        const std::vector<String>& ex_vals,
 151                                        const std::vector<Node>& vals,
 152                                        std::vector<unsigned>& inc,
 153                                        unsigned& tot)
 154 {
 155   for (unsigned j = 0; j < vals.size(); j++)
 156   {
 157     unsigned ival = 0;
 158     if (d_vals[j] == sui->d_true)
 159     {
 160       // example is active in this context
 161       Assert(vals[j].isConst());
 162       String mystr = vals[j].getConst<String>();
 163       ival = mystr.size();
 164       if (mystr.size() <= ex_vals[j].size())
 165       {
 166         if (!(isPrefix ? ex_vals[j].strncmp(mystr, ival)
 167                        : ex_vals[j].rstrncmp(mystr, ival)))
 168         {
 169           Trace("sygus-sui-dt-debug") << "X";
 170           return false;
 171         }
 172       }
 173       else
 174       {
 175         Trace("sygus-sui-dt-debug") << "X";
 176         return false;
 177       }
 178     }
 179     Trace("sygus-sui-dt-debug") << ival;
 180     tot += ival;
 181     inc.push_back(ival);
 182   }
 183   return true;
 184 }
 185 bool UnifContextIo::isStringSolved(SygusUnifIo* sui,
 186                                    const std::vector<String>& ex_vals,
 187                                    const std::vector<Node>& vals)
 188 {
 189   for (unsigned j = 0; j < vals.size(); j++)
 190   {
 191     if (d_vals[j] == sui->d_true)
 192     {
 193       // example is active in this context
 194       Assert(vals[j].isConst());
 195       String mystr = vals[j].getConst<String>();
 196       if (ex_vals[j] != mystr)
 197       {
 198         return false;
 199       }
 200     }
 201   }
 202   return true;
 203 }
 204
 205 // status : 0 : exact, -1 : vals is subset, 1 : vals is superset
 206 Node SubsumeTrie::addTermInternal(Node t,
 207                                   const std::vector<Node>& vals,
 208                                   bool pol,
 209                                   std::vector<Node>& subsumed,
 210                                   bool spol,
 211                                   unsigned index,
 212                                   int status,
 213                                   bool checkExistsOnly,
 214                                   bool checkSubsume)
 215 {
 216   if (index == vals.size())
 217   {
 218     if (status == 0)
 219     {
 220       // set the term if checkExistsOnly = false
 221       if (d_term.isNull() && !checkExistsOnly)
 222       {
 223         d_term = t;
 224       }
 225     }
 226     else if (status == 1)
 227     {
 228       Assert(checkSubsume);
 229       // found a subsumed term
 230       if (!d_term.isNull())
 231       {
 232         subsumed.push_back(d_term);
 233         if (!checkExistsOnly)
 234         {
 235           // remove it if checkExistsOnly = false
 236           d_term = Node::null();
 237         }
 238       }
 239     }
 240     else
 241     {
 242       Assert(!checkExistsOnly && checkSubsume);
 243     }
 244     return d_term;
 245   }
 246   NodeManager* nm = NodeManager::currentNM();
 247   // the current value
 248   Assert(pol || (vals[index].isConst() && vals[index].getType().isBoolean()));
 249   Node cv = pol ? vals[index] : nm->mkConst(!vals[index].getConst<bool>());
 250   // if checkExistsOnly = false, check if the current value is subsumed if
 251   // checkSubsume = true, if so, don't add
 252   if (!checkExistsOnly && checkSubsume)
 253   {
 254     Assert(cv.isConst() && cv.getType().isBoolean());
 255     std::vector<bool> check_subsumed_by;
 256     if (status == 0)
 257     {
 258       if (!cv.getConst<bool>())
 259       {
 260         check_subsumed_by.push_back(spol);
 261       }
 262     }
 263     else if (status == -1)
 264     {
 265       check_subsumed_by.push_back(spol);
 266       if (!cv.getConst<bool>())
 267       {
 268         check_subsumed_by.push_back(!spol);
 269       }
 270     }
 271     // check for subsumed nodes
 272     for (unsigned i = 0, size = check_subsumed_by.size(); i < size; i++)
 273     {
 274       bool csbi = check_subsumed_by[i];
 275       Node csval = nm->mkConst(csbi);
 276       // check if subsumed
 277       std::map<Node, SubsumeTrie>::iterator itc = d_children.find(csval);
 278       if (itc != d_children.end())
 279       {
 280         Node ret = itc->second.addTermInternal(t,
 281                                                vals,
 282                                                pol,
 283                                                subsumed,
 284                                                spol,
 285                                                index + 1,
 286                                                -1,
 287                                                checkExistsOnly,
 288                                                checkSubsume);
 289         // ret subsumes t
 290         if (!ret.isNull())
 291         {
 292           return ret;
 293         }
 294       }
 295     }
 296   }
 297   Node ret;
 298   std::vector<bool> check_subsume;
 299   if (status == 0)
 300   {
 301     if (checkExistsOnly)
 302     {
 303       std::map<Node, SubsumeTrie>::iterator itc = d_children.find(cv);
 304       if (itc != d_children.end())
 305       {
 306         ret = itc->second.addTermInternal(t,
 307                                           vals,
 308                                           pol,
 309                                           subsumed,
 310                                           spol,
 311                                           index + 1,
 312                                           0,
 313                                           checkExistsOnly,
 314                                           checkSubsume);
 315       }
 316     }
 317     else
 318     {
 319       Assert(spol);
 320       ret = d_children[cv].addTermInternal(t,
 321                                            vals,
 322                                            pol,
 323                                            subsumed,
 324                                            spol,
 325                                            index + 1,
 326                                            0,
 327                                            checkExistsOnly,
 328                                            checkSubsume);
 329       if (ret != t)
 330       {
 331         // we were subsumed by ret, return
 332         return ret;
 333       }
 334     }
 335     if (checkSubsume)
 336     {
 337       Assert(cv.isConst() && cv.getType().isBoolean());
 338       // check for subsuming
 339       if (cv.getConst<bool>())
 340       {
 341         check_subsume.push_back(!spol);
 342       }
 343     }
 344   }
 345   else if (status == 1)
 346   {
 347     Assert(checkSubsume);
 348     Assert(cv.isConst() && cv.getType().isBoolean());
 349     check_subsume.push_back(!spol);
 350     if (cv.getConst<bool>())
 351     {
 352       check_subsume.push_back(spol);
 353     }
 354   }
 355   if (checkSubsume)
 356   {
 357     // check for subsumed terms
 358     for (unsigned i = 0, size = check_subsume.size(); i < size; i++)
 359     {
 360       Node csval = nm->mkConst<bool>(check_subsume[i]);
 361       std::map<Node, SubsumeTrie>::iterator itc = d_children.find(csval);
 362       if (itc != d_children.end())
 363       {
 364         itc->second.addTermInternal(t,
 365                                     vals,
 366                                     pol,
 367                                     subsumed,
 368                                     spol,
 369                                     index + 1,
 370                                     1,
 371                                     checkExistsOnly,
 372                                     checkSubsume);
 373         // clean up
 374         if (itc->second.isEmpty())
 375         {
 376           Assert(!checkExistsOnly);
 377           d_children.erase(csval);
 378         }
 379       }
 380     }
 381   }
 382   return ret;
 383 }
 384
 385 Node SubsumeTrie::addTerm(Node t,
 386                           const std::vector<Node>& vals,
 387                           bool pol,
 388                           std::vector<Node>& subsumed)
 389 {
 390   return addTermInternal(t, vals, pol, subsumed, true, 0, 0, false, true);
 391 }
 392
 393 Node SubsumeTrie::addCond(Node c, const std::vector<Node>& vals, bool pol)
 394 {
 395   std::vector<Node> subsumed;
 396   return addTermInternal(c, vals, pol, subsumed, true, 0, 0, false, false);
 397 }
 398
 399 void SubsumeTrie::getSubsumed(const std::vector<Node>& vals,
 400                               bool pol,
 401                               std::vector<Node>& subsumed)
 402 {
 403   addTermInternal(Node::null(), vals, pol, subsumed, true, 0, 1, true, true);
 404 }
 405
 406 void SubsumeTrie::getSubsumedBy(const std::vector<Node>& vals,
 407                                 bool pol,
 408                                 std::vector<Node>& subsumed_by)
 409 {
 410   // flip polarities
 411   addTermInternal(
 412       Node::null(), vals, !pol, subsumed_by, false, 0, 1, true, true);
 413 }
 414
 415 void SubsumeTrie::getLeavesInternal(const std::vector<Node>& vals,
 416                                     bool pol,
 417                                     std::map<int, std::vector<Node> >& v,
 418                                     unsigned index,
 419                                     int status)
 420 {
 421   if (index == vals.size())
 422   {
 423     Assert(!d_term.isNull());
 424     Assert(std::find(v[status].begin(), v[status].end(), d_term)
 425            == v[status].end());
 426     v[status].push_back(d_term);
 427   }
 428   else
 429   {
 430     Assert(vals[index].isConst() && vals[index].getType().isBoolean());
 431     bool curr_val_true = vals[index].getConst<bool>() == pol;
 432     for (std::map<Node, SubsumeTrie>::iterator it = d_children.begin();
 433          it != d_children.end();
 434          ++it)
 435     {
 436       int new_status = status;
 437       // if the current value is true
 438       if (curr_val_true)
 439       {
 440         if (status != 0)
 441         {
 442           Assert(it->first.isConst() && it->first.getType().isBoolean());
 443           new_status = (it->first.getConst<bool>() ? 1 : -1);
 444           if (status != -2 && new_status != status)
 445           {
 446             new_status = 0;
 447           }
 448         }
 449       }
 450       it->second.getLeavesInternal(vals, pol, v, index + 1, new_status);
 451     }
 452   }
 453 }
 454
 455 void SubsumeTrie::getLeaves(const std::vector<Node>& vals,
 456                             bool pol,
 457                             std::map<int, std::vector<Node> >& v)
 458 {
 459   getLeavesInternal(vals, pol, v, 0, -2);
 460 }
 461
 462 SygusUnifIo::SygusUnifIo() : d_check_sol(false), d_cond_count(0)
 463 {
 464   d_true = NodeManager::currentNM()->mkConst(true);
 465   d_false = NodeManager::currentNM()->mkConst(false);
 466 }
 467
 468 SygusUnifIo::~SygusUnifIo() {}
 469 void SygusUnifIo::initialize(QuantifiersEngine* qe,
 470                              const std::vector<Node>& funs,
 471                              std::vector<Node>& enums,
 472                              std::vector<Node>& lemmas)
 473 {
 474   Assert(funs.size() == 1);
 475   d_examples.clear();
 476   d_examples_out.clear();
 477   d_ecache.clear();
 478   d_candidate = funs[0];
 479   SygusUnif::initialize(qe, funs, enums, lemmas);
 480   // learn redundant operators based on the strategy
 481   d_strategy[d_candidate].staticLearnRedundantOps(lemmas);
 482 }
 483
 484 void SygusUnifIo::addExample(const std::vector<Node>& input, Node output)
 485 {
 486   d_examples.push_back(input);
 487   d_examples_out.push_back(output);
 488 }
 489
 490 void SygusUnifIo::notifyEnumeration(Node e, Node v, std::vector<Node>& lemmas)
 491 {
 492   Trace("sygus-sui-enum") << "Notify enumeration for " << e << " : " << v
 493                           << std::endl;
 494   Node c = d_candidate;
 495   Assert(!d_examples.empty());
 496   Assert(d_examples.size() == d_examples_out.size());
 497
 498   EnumInfo& ei = d_strategy[c].getEnumInfo(e);
 499   // The explanation for why the current value should be excluded in future
 500   // iterations.
 501   Node exp_exc;
 502
 503   TypeNode xtn = e.getType();
 504   Node bv = d_tds->sygusToBuiltin(v, xtn);
 505   std::vector<Node> base_results;
 506   // compte the results
 507   for (unsigned j = 0, size = d_examples.size(); j < size; j++)
 508   {
 509     Node res = d_tds->evaluateBuiltin(xtn, bv, d_examples[j]);
 510     Trace("sygus-sui-enum-debug")
 511         << "...got res = " << res << " from " << bv << std::endl;
 512     base_results.push_back(res);
 513   }
 514   // is it excluded for domain-specific reason?
 515   std::vector<Node> exp_exc_vec;
 516   if (getExplanationForEnumeratorExclude(e, v, base_results, exp_exc_vec))
 517   {
 518     Assert(!exp_exc_vec.empty());
 519     exp_exc = exp_exc_vec.size() == 1
 520                   ? exp_exc_vec[0]
 521                   : NodeManager::currentNM()->mkNode(AND, exp_exc_vec);
 522     Trace("sygus-sui-enum")
 523         << "  ...fail : term is excluded (domain-specific)" << std::endl;
 524   }
 525   else
 526   {
 527     // notify all slaves
 528     Assert(!ei.d_enum_slave.empty());
 529     // explanation for why this value should be excluded
 530     for (unsigned s = 0; s < ei.d_enum_slave.size(); s++)
 531     {
 532       Node xs = ei.d_enum_slave[s];
 533
 534       EnumInfo& eiv = d_strategy[c].getEnumInfo(xs);
 535
 536       EnumCache& ecv = d_ecache[xs];
 537
 538       Trace("sygus-sui-enum") << "Process " << xs << " from " << s << std::endl;
 539       // bool prevIsCover = false;
 540       if (eiv.getRole() == enum_io)
 541       {
 542         Trace("sygus-sui-enum") << "   IO-Eval of ";
 543         // prevIsCover = eiv.isFeasible();
 544       }
 545       else
 546       {
 547         Trace("sygus-sui-enum") << "Evaluation of ";
 548       }
 549       Trace("sygus-sui-enum") << xs << " : ";
 550       // evaluate all input/output examples
 551       std::vector<Node> results;
 552       Node templ = eiv.d_template;
 553       TNode templ_var = eiv.d_template_arg;
 554       std::map<Node, bool> cond_vals;
 555       for (unsigned j = 0, size = base_results.size(); j < size; j++)
 556       {
 557         Node res = base_results[j];
 558         Assert(res.isConst());
 559         if (!templ.isNull())
 560         {
 561           TNode tres = res;
 562           res = templ.substitute(templ_var, res);
 563           res = Rewriter::rewrite(res);
 564           Assert(res.isConst());
 565         }
 566         Node resb;
 567         if (eiv.getRole() == enum_io)
 568         {
 569           Node out = d_examples_out[j];
 570           Assert(out.isConst());
 571           resb = res == out ? d_true : d_false;
 572         }
 573         else
 574         {
 575           resb = res;
 576         }
 577         cond_vals[resb] = true;
 578         results.push_back(resb);
 579         if (Trace.isOn("sygus-sui-enum"))
 580         {
 581           if (resb.getType().isBoolean())
 582           {
 583             Trace("sygus-sui-enum") << (resb == d_true ? "1" : "0");
 584           }
 585           else
 586           {
 587             Trace("sygus-sui-enum") << "?";
 588           }
 589         }
 590       }
 591       bool keep = false;
 592       if (eiv.getRole() == enum_io)
 593       {
 594         // latter is the degenerate case of no examples
 595         if (cond_vals.find(d_true) != cond_vals.end() || cond_vals.empty())
 596         {
 597           // check subsumbed/subsuming
 598           std::vector<Node> subsume;
 599           if (cond_vals.find(d_false) == cond_vals.end())
 600           {
 601             // it is the entire solution, we are done
 602             Trace("sygus-sui-enum")
 603                 << "  ...success, full solution added to PBE pool : "
 604                 << d_tds->sygusToBuiltin(v) << std::endl;
 605             if (!ecv.isSolved())
 606             {
 607               ecv.setSolved(v);
 608               // it subsumes everything
 609               ecv.d_term_trie.clear();
 610               ecv.d_term_trie.addTerm(v, results, true, subsume);
 611             }
 612             keep = true;
 613           }
 614           else
 615           {
 616             Node val = ecv.d_term_trie.addTerm(v, results, true, subsume);
 617             if (val == v)
 618             {
 619               Trace("sygus-sui-enum") << "  ...success";
 620               if (!subsume.empty())
 621               {
 622                 ecv.d_enum_subsume.insert(
 623                     ecv.d_enum_subsume.end(), subsume.begin(), subsume.end());
 624                 Trace("sygus-sui-enum")
 625                     << " and subsumed " << subsume.size() << " terms";
 626               }
 627               Trace("sygus-sui-enum")
 628                   << "!   add to PBE pool : " << d_tds->sygusToBuiltin(v)
 629                   << std::endl;
 630               keep = true;
 631             }
 632             else
 633             {
 634               Assert(subsume.empty());
 635               Trace("sygus-sui-enum") << "  ...fail : subsumed" << std::endl;
 636             }
 637           }
 638         }
 639         else
 640         {
 641           Trace("sygus-sui-enum")
 642               << "  ...fail : it does not satisfy examples." << std::endl;
 643         }
 644       }
 645       else
 646       {
 647         // must be unique up to examples
 648         Node val = ecv.d_term_trie.addCond(v, results, true);
 649         if (val == v)
 650         {
 651           Trace("sygus-sui-enum") << "  ...success!   add to PBE pool : "
 652                                   << d_tds->sygusToBuiltin(v) << std::endl;
 653           keep = true;
 654         }
 655         else
 656         {
 657           Trace("sygus-sui-enum")
 658               << "  ...fail : term is not unique" << std::endl;
 659         }
 660         d_cond_count++;
 661       }
 662       if (keep)
 663       {
 664         // notify to retry the build of solution
 665         d_check_sol = true;
 666         ecv.addEnumValue(v, results);
 667       }
 668     }
 669   }
 670
 671   // exclude this value on subsequent iterations
 672   if (exp_exc.isNull())
 673   {
 674     // if we did not already explain why this should be excluded, use default
 675     exp_exc = d_tds->getExplain()->getExplanationForEquality(e, v);
 676   }
 677   exp_exc = exp_exc.negate();
 678   Trace("sygus-sui-enum-lemma")
 679       << "SygusUnifIo : enumeration exclude lemma : " << exp_exc << std::endl;
 680   lemmas.push_back(exp_exc);
 681 }
 682
 683 bool SygusUnifIo::constructSolution(std::vector<Node>& sols)
 684 {
 685   Node sol = constructSolutionNode();
 686   if (!sol.isNull())
 687   {
 688     sols.push_back(sol);
 689     return true;
 690   }
 691   return false;
 692 }
 693
 694 Node SygusUnifIo::constructSolutionNode()
 695 {
 696   Node c = d_candidate;
 697   if (!d_solution.isNull())
 698   {
 699     // already has a solution
 700     return d_solution;
 701   }
 702   // only check if an enumerator updated
 703   if (d_check_sol)
 704   {
 705     Trace("sygus-pbe") << "Construct solution, #iterations = " << d_cond_count
 706                        << std::endl;
 707     d_check_sol = false;
 708     // try multiple times if we have done multiple conditions, due to
 709     // non-determinism
 710     Node vc;
 711     for (unsigned i = 0; i <= d_cond_count; i++)
 712     {
 713       Trace("sygus-pbe-dt") << "ConstructPBE for candidate: " << c << std::endl;
 714       // initialize a call to construct solution
 715       initializeConstructSol();
 716       initializeConstructSolFor(c);
 717       // call the virtual construct solution method
 718       Node e = d_strategy[c].getRootEnumerator();
 719       Node vcc = constructSol(c, e, role_equal, 1);
 720       // if we constructed the solution, and we either did not previously have
 721       // a solution, or the new solution is better (smaller).
 722       if (!vcc.isNull()
 723           && (vc.isNull() || (!vc.isNull()
 724                               && d_tds->getSygusTermSize(vcc)
 725                                      < d_tds->getSygusTermSize(vc))))
 726       {
 727         Trace("sygus-pbe") << "**** SygusUnif SOLVED : " << c << " = " << vcc
 728                            << std::endl;
 729         Trace("sygus-pbe") << "...solved at iteration " << i << std::endl;
 730         vc = vcc;
 731       }
 732     }
 733     if (!vc.isNull())
 734     {
 735       d_solution = vc;
 736       return vc;
 737     }
 738     Trace("sygus-pbe") << "...failed to solve." << std::endl;
 739   }
 740   return Node::null();
 741 }
 742
 743 // ------------------------------------ solution construction from enumeration
 744
 745 bool SygusUnifIo::useStrContainsEnumeratorExclude(Node e)
 746 {
 747   TypeNode xbt = d_tds->sygusToBuiltinType(e.getType());
 748   if (xbt.isString())
 749   {
 750     std::map<Node, bool>::iterator itx = d_use_str_contains_eexc.find(e);
 751     if (itx != d_use_str_contains_eexc.end())
 752     {
 753       return itx->second;
 754     }
 755     Trace("sygus-sui-enum-debug")
 756         << "Is " << e << " is str.contains exclusion?" << std::endl;
 757     d_use_str_contains_eexc[e] = true;
 758     Node c = d_candidate;
 759     EnumInfo& ei = d_strategy[c].getEnumInfo(e);
 760     for (const Node& sn : ei.d_enum_slave)
 761     {
 762       EnumInfo& eis = d_strategy[c].getEnumInfo(sn);
 763       EnumRole er = eis.getRole();
 764       if (er != enum_io && er != enum_concat_term)
 765       {
 766         Trace("sygus-sui-enum-debug") << "  incompatible slave : " << sn
 767                                       << ", role = " << er << std::endl;
 768         d_use_str_contains_eexc[e] = false;
 769         return false;
 770       }
 771       if (eis.isConditional())
 772       {
 773         Trace("sygus-sui-enum-debug")
 774             << "  conditional slave : " << sn << std::endl;
 775         d_use_str_contains_eexc[e] = false;
 776         return false;
 777       }
 778     }
 779     Trace("sygus-sui-enum-debug")
 780         << "...can use str.contains exclusion." << std::endl;
 781     return d_use_str_contains_eexc[e];
 782   }
 783   return false;
 784 }
 785
 786 bool SygusUnifIo::getExplanationForEnumeratorExclude(Node e,
 787                                                      Node v,
 788                                                      std::vector<Node>& results,
 789                                                      std::vector<Node>& exp)
 790 {
 791   if (useStrContainsEnumeratorExclude(e))
 792   {
 793     NodeManager* nm = NodeManager::currentNM();
 794     // This check whether the example evaluates to something that is larger than
 795     // the output for some input/output pair. If so, then this term is never
 796     // useful. We generalize its explanation below.
 797
 798     if (Trace.isOn("sygus-sui-cterm-debug"))
 799     {
 800       Trace("sygus-sui-enum") << std::endl;
 801     }
 802     // check if all examples had longer length that the output
 803     Assert(d_examples_out.size() == results.size());
 804     Trace("sygus-sui-cterm-debug")
 805         << "Check enumerator exclusion for " << e << " -> "
 806         << d_tds->sygusToBuiltin(v) << " based on str.contains." << std::endl;
 807     std::vector<unsigned> cmp_indices;
 808     for (unsigned i = 0, size = results.size(); i < size; i++)
 809     {
 810       Assert(results[i].isConst());
 811       Assert(d_examples_out[i].isConst());
 812       Trace("sygus-sui-cterm-debug")
 813           << "  " << results[i] << " <> " << d_examples_out[i];
 814       Node cont = nm->mkNode(STRING_STRCTN, d_examples_out[i], results[i]);
 815       Node contr = Rewriter::rewrite(cont);
 816       if (contr == d_false)
 817       {
 818         cmp_indices.push_back(i);
 819         Trace("sygus-sui-cterm-debug") << "...not contained." << std::endl;
 820       }
 821       else
 822       {
 823         Trace("sygus-sui-cterm-debug") << "...contained." << std::endl;
 824       }
 825     }
 826     if (!cmp_indices.empty())
 827     {
 828       // we check invariance with respect to a negative contains test
 829       NegContainsSygusInvarianceTest ncset;
 830       ncset.init(e, d_examples, d_examples_out, cmp_indices);
 831       // construct the generalized explanation
 832       d_tds->getExplain()->getExplanationFor(e, v, exp, ncset);
 833       Trace("sygus-sui-cterm")
 834           << "PBE-cterm : enumerator exclude " << d_tds->sygusToBuiltin(v)
 835           << " due to negative containment." << std::endl;
 836       return true;
 837     }
 838   }
 839   return false;
 840 }
 841
 842 void SygusUnifIo::EnumCache::addEnumValue(Node v, std::vector<Node>& results)
 843 {
 844   // should not have been enumerated before
 845   Assert(d_enum_val_to_index.find(v) == d_enum_val_to_index.end());
 846   d_enum_val_to_index[v] = d_enum_vals.size();
 847   d_enum_vals.push_back(v);
 848   d_enum_vals_res.push_back(results);
 849 }
 850
 851 void SygusUnifIo::initializeConstructSol() { d_context.initialize(this); }
 852 void SygusUnifIo::initializeConstructSolFor(Node f)
 853 {
 854   Assert(d_candidate == f);
 855 }
 856
 857 Node SygusUnifIo::constructSol(Node f, Node e, NodeRole nrole, int ind)
 858 {
 859   Assert(d_candidate == f);
 860   UnifContextIo& x = d_context;
 861   TypeNode etn = e.getType();
 862   if (Trace.isOn("sygus-sui-dt-debug"))
 863   {
 864     indent("sygus-sui-dt-debug", ind);
 865     Trace("sygus-sui-dt-debug") << "ConstructPBE: (" << e << ", " << nrole
 866                                 << ") for type " << etn << " in context ";
 867     print_val("sygus-sui-dt-debug", x.d_vals);
 868     NodeRole ctx_role = x.getCurrentRole();
 869     Trace("sygus-sui-dt-debug") << ", context role [" << ctx_role;
 870     if (ctx_role == role_string_prefix || ctx_role == role_string_suffix)
 871     {
 872       Trace("sygus-sui-dt-debug") << ", string pos : ";
 873       for (unsigned i = 0, size = x.d_str_pos.size(); i < size; i++)
 874       {
 875         Trace("sygus-sui-dt-debug") << " " << x.d_str_pos[i];
 876       }
 877     }
 878     Trace("sygus-sui-dt-debug") << "]";
 879     Trace("sygus-sui-dt-debug") << std::endl;
 880   }
 881   // enumerator type info
 882   EnumTypeInfo& tinfo = d_strategy[f].getEnumTypeInfo(etn);
 883
 884   // get the enumerator information
 885   EnumInfo& einfo = d_strategy[f].getEnumInfo(e);
 886
 887   EnumCache& ecache = d_ecache[e];
 888
 889   Node ret_dt;
 890   if (nrole == role_equal)
 891   {
 892     if (!x.isReturnValueModified())
 893     {
 894       if (ecache.isSolved())
 895       {
 896         // this type has a complete solution
 897         ret_dt = ecache.getSolved();
 898         indent("sygus-sui-dt", ind);
 899         Trace("sygus-sui-dt") << "return PBE: success : solved "
 900                               << d_tds->sygusToBuiltin(ret_dt) << std::endl;
 901         Assert(!ret_dt.isNull());
 902       }
 903       else
 904       {
 905         // could be conditionally solved
 906         std::vector<Node> subsumed_by;
 907         ecache.d_term_trie.getSubsumedBy(x.d_vals, true, subsumed_by);
 908         if (!subsumed_by.empty())
 909         {
 910           ret_dt = constructBestSolvedTerm(subsumed_by);
 911           indent("sygus-sui-dt", ind);
 912           Trace("sygus-sui-dt") << "return PBE: success : conditionally solved"
 913                                 << d_tds->sygusToBuiltin(ret_dt) << std::endl;
 914         }
 915         else
 916         {
 917           indent("sygus-sui-dt-debug", ind);
 918           Trace("sygus-sui-dt-debug")
 919               << "  ...not currently conditionally solved." << std::endl;
 920         }
 921       }
 922     }
 923     if (ret_dt.isNull())
 924     {
 925       if (d_tds->sygusToBuiltinType(e.getType()).isString())
 926       {
 927         // check if a current value that closes all examples
 928         // get the term enumerator for this type
 929         std::map<EnumRole, Node>::iterator itnt =
 930             tinfo.d_enum.find(enum_concat_term);
 931         if (itnt != tinfo.d_enum.end())
 932         {
 933           Node et = itnt->second;
 934
 935           EnumCache& ecachet = d_ecache[et];
 936           // get the current examples
 937           std::vector<String> ex_vals;
 938           x.getCurrentStrings(this, d_examples_out, ex_vals);
 939           Assert(ecache.d_enum_vals.size() == ecache.d_enum_vals_res.size());
 940
 941           // test each example in the term enumerator for the type
 942           std::vector<Node> str_solved;
 943           for (unsigned i = 0, size = ecachet.d_enum_vals.size(); i < size; i++)
 944           {
 945             if (x.isStringSolved(this, ex_vals, ecachet.d_enum_vals_res[i]))
 946             {
 947               str_solved.push_back(ecachet.d_enum_vals[i]);
 948             }
 949           }
 950           if (!str_solved.empty())
 951           {
 952             ret_dt = constructBestStringSolvedTerm(str_solved);
 953             indent("sygus-sui-dt", ind);
 954             Trace("sygus-sui-dt") << "return PBE: success : string solved "
 955                                   << d_tds->sygusToBuiltin(ret_dt) << std::endl;
 956           }
 957           else
 958           {
 959             indent("sygus-sui-dt-debug", ind);
 960             Trace("sygus-sui-dt-debug")
 961                 << "  ...not currently string solved." << std::endl;
 962           }
 963         }
 964       }
 965     }
 966   }
 967   else if (nrole == role_string_prefix || nrole == role_string_suffix)
 968   {
 969     // check if each return value is a prefix/suffix of all open examples
 970     if (!x.isReturnValueModified() || x.getCurrentRole() == nrole)
 971     {
 972       std::map<Node, std::vector<unsigned> > incr;
 973       bool isPrefix = nrole == role_string_prefix;
 974       std::map<Node, unsigned> total_inc;
 975       std::vector<Node> inc_strs;
 976       // make the value of the examples
 977       std::vector<String> ex_vals;
 978       x.getCurrentStrings(this, d_examples_out, ex_vals);
 979       if (Trace.isOn("sygus-sui-dt-debug"))
 980       {
 981         indent("sygus-sui-dt-debug", ind);
 982         Trace("sygus-sui-dt-debug") << "current strings : " << std::endl;
 983         for (unsigned i = 0, size = ex_vals.size(); i < size; i++)
 984         {
 985           indent("sygus-sui-dt-debug", ind + 1);
 986           Trace("sygus-sui-dt-debug") << ex_vals[i] << std::endl;
 987         }
 988       }
 989
 990       // check if there is a value for which is a prefix/suffix of all active
 991       // examples
 992       Assert(ecache.d_enum_vals.size() == ecache.d_enum_vals_res.size());
 993
 994       for (unsigned i = 0, size = ecache.d_enum_vals.size(); i < size; i++)
 995       {
 996         Node val_t = ecache.d_enum_vals[i];
 997         Assert(incr.find(val_t) == incr.end());
 998         indent("sygus-sui-dt-debug", ind);
 999         Trace("sygus-sui-dt-debug")
1000             << "increment string values : " << val_t << " : ";
1001         Assert(ecache.d_enum_vals_res[i].size() == d_examples_out.size());
1002         unsigned tot = 0;
1003         bool exsuccess = x.getStringIncrement(this,
1004                                               isPrefix,
1005                                               ex_vals,
1006                                               ecache.d_enum_vals_res[i],
1007                                               incr[val_t],
1008                                               tot);
1009         if (!exsuccess)
1010         {
1011           incr.erase(val_t);
1012           Trace("sygus-sui-dt-debug") << "...fail" << std::endl;
1013         }
1014         else
1015         {
1016           total_inc[val_t] = tot;
1017           inc_strs.push_back(val_t);
1018           Trace("sygus-sui-dt-debug")
1019               << "...success, total increment = " << tot << std::endl;
1020         }
1021       }
1022
1023       if (!incr.empty())
1024       {
1025         ret_dt = constructBestStringToConcat(inc_strs, total_inc, incr);
1026         Assert(!ret_dt.isNull());
1027         indent("sygus-sui-dt", ind);
1028         Trace("sygus-sui-dt")
1029             << "PBE: CONCAT strategy : choose " << (isPrefix ? "pre" : "suf")
1030             << "fix value " << d_tds->sygusToBuiltin(ret_dt) << std::endl;
1031         // update the context
1032         bool ret = x.updateStringPosition(this, incr[ret_dt], nrole);
1033         AlwaysAssert(ret == (total_inc[ret_dt] > 0));
1034       }
1035       else
1036       {
1037         indent("sygus-sui-dt", ind);
1038         Trace("sygus-sui-dt") << "PBE: failed CONCAT strategy, no values are "
1039                               << (isPrefix ? "pre" : "suf")
1040                               << "fix of all examples." << std::endl;
1041       }
1042     }
1043     else
1044     {
1045       indent("sygus-sui-dt", ind);
1046       Trace("sygus-sui-dt")
1047           << "PBE: failed CONCAT strategy, prefix/suffix mismatch."
1048           << std::endl;
1049     }
1050   }
1051   if (ret_dt.isNull() && !einfo.isTemplated())
1052   {
1053     // we will try a single strategy
1054     EnumTypeInfoStrat* etis = nullptr;
1055     std::map<NodeRole, StrategyNode>::iterator itsn =
1056         tinfo.d_snodes.find(nrole);
1057     if (itsn != tinfo.d_snodes.end())
1058     {
1059       // strategy info
1060       StrategyNode& snode = itsn->second;
1061       if (x.d_visit_role[e].find(nrole) == x.d_visit_role[e].end())
1062       {
1063         x.d_visit_role[e][nrole] = true;
1064         // try a random strategy
1065         if (snode.d_strats.size() > 1)
1066         {
1067           std::random_shuffle(snode.d_strats.begin(), snode.d_strats.end());
1068         }
1069         // get an eligible strategy index
1070         unsigned sindex = 0;
1071         while (sindex < snode.d_strats.size()
1072                && !snode.d_strats[sindex]->isValid(x))
1073         {
1074           sindex++;
1075         }
1076         // if we found a eligible strategy
1077         if (sindex < snode.d_strats.size())
1078         {
1079           etis = snode.d_strats[sindex];
1080         }
1081       }
1082     }
1083     if (etis != nullptr)
1084     {
1085       StrategyType strat = etis->d_this;
1086       indent("sygus-sui-dt", ind + 1);
1087       Trace("sygus-sui-dt")
1088           << "...try STRATEGY " << strat << "..." << std::endl;
1089
1090       std::map<unsigned, Node> look_ahead_solved_children;
1091       std::vector<Node> dt_children_cons;
1092       bool success = true;
1093
1094       // for ITE
1095       Node split_cond_enum;
1096       int split_cond_res_index = -1;
1097
1098       for (unsigned sc = 0, size = etis->d_cenum.size(); sc < size; sc++)
1099       {
1100         indent("sygus-sui-dt", ind + 1);
1101         Trace("sygus-sui-dt")
1102             << "construct PBE child #" << sc << "..." << std::endl;
1103         Node rec_c;
1104         std::map<unsigned, Node>::iterator itla =
1105             look_ahead_solved_children.find(sc);
1106         if (itla != look_ahead_solved_children.end())
1107         {
1108           rec_c = itla->second;
1109           indent("sygus-sui-dt-debug", ind + 1);
1110           Trace("sygus-sui-dt-debug")
1111               << "ConstructPBE: look ahead solved : "
1112               << d_tds->sygusToBuiltin(rec_c) << std::endl;
1113         }
1114         else
1115         {
1116           std::pair<Node, NodeRole>& cenum = etis->d_cenum[sc];
1117
1118           // update the context
1119           std::vector<Node> prev;
1120           if (strat == strat_ITE && sc > 0)
1121           {
1122             EnumCache& ecache_cond = d_ecache[split_cond_enum];
1123             Assert(split_cond_res_index >= 0);
1124             Assert(split_cond_res_index
1125                    < (int)ecache_cond.d_enum_vals_res.size());
1126             prev = x.d_vals;
1127             bool ret = x.updateContext(
1128                 this,
1129                 ecache_cond.d_enum_vals_res[split_cond_res_index],
1130                 sc == 1);
1131             AlwaysAssert(ret);
1132           }
1133
1134           // recurse
1135           if (strat == strat_ITE && sc == 0)
1136           {
1137             Node ce = cenum.first;
1138
1139             EnumCache& ecache_child = d_ecache[ce];
1140
1141             // only used if the return value is not modified
1142             if (!x.isReturnValueModified())
1143             {
1144               if (x.d_uinfo.find(ce) == x.d_uinfo.end())
1145               {
1146                 Trace("sygus-sui-dt-debug2")
1147                     << "  reg : PBE: Look for direct solutions for conditional "
1148                        "enumerator "
1149                     << ce << " ... " << std::endl;
1150                 Assert(ecache_child.d_enum_vals.size()
1151                        == ecache_child.d_enum_vals_res.size());
1152                 for (unsigned i = 1; i <= 2; i++)
1153                 {
1154                   std::pair<Node, NodeRole>& te_pair = etis->d_cenum[i];
1155                   Node te = te_pair.first;
1156                   EnumCache& ecache_te = d_ecache[te];
1157                   bool branch_pol = (i == 1);
1158                   // for each condition, get terms that satisfy it in this
1159                   // branch
1160                   for (unsigned k = 0, size = ecache_child.d_enum_vals.size();
1161                        k < size;
1162                        k++)
1163                   {
1164                     Node cond = ecache_child.d_enum_vals[k];
1165                     std::vector<Node> solved;
1166                     ecache_te.d_term_trie.getSubsumedBy(
1167                         ecache_child.d_enum_vals_res[k], branch_pol, solved);
1168                     Trace("sygus-sui-dt-debug2")
1169                         << "  reg : PBE: " << d_tds->sygusToBuiltin(cond)
1170                         << " has " << solved.size() << " solutions in branch "
1171                         << i << std::endl;
1172                     if (!solved.empty())
1173                     {
1174                       Node slv = constructBestSolvedTerm(solved);
1175                       Trace("sygus-sui-dt-debug2")
1176                           << "  reg : PBE: ..." << d_tds->sygusToBuiltin(slv)
1177                           << " is a solution under branch " << i;
1178                       Trace("sygus-sui-dt-debug2")
1179                           << " of condition " << d_tds->sygusToBuiltin(cond)
1180                           << std::endl;
1181                       x.d_uinfo[ce].d_look_ahead_sols[cond][i] = slv;
1182                     }
1183                   }
1184                 }
1185               }
1186             }
1187
1188             // get the conditionals in the current context : they must be
1189             // distinguishable
1190             std::map<int, std::vector<Node> > possible_cond;
1191             std::map<Node, int> solved_cond;  // stores branch
1192             ecache_child.d_term_trie.getLeaves(x.d_vals, true, possible_cond);
1193
1194             std::map<int, std::vector<Node> >::iterator itpc =
1195                 possible_cond.find(0);
1196             if (itpc != possible_cond.end())
1197             {
1198               if (Trace.isOn("sygus-sui-dt-debug"))
1199               {
1200                 indent("sygus-sui-dt-debug", ind + 1);
1201                 Trace("sygus-sui-dt-debug")
1202                     << "PBE : We have " << itpc->second.size()
1203                     << " distinguishable conditionals:" << std::endl;
1204                 for (Node& cond : itpc->second)
1205                 {
1206                   indent("sygus-sui-dt-debug", ind + 2);
1207                   Trace("sygus-sui-dt-debug")
1208                       << d_tds->sygusToBuiltin(cond) << std::endl;
1209                 }
1210               }
1211
1212               // static look ahead conditional : choose conditionals that have
1213               // solved terms in at least one branch
1214               //    only applicable if we have not modified the return value
1215               std::map<int, std::vector<Node> > solved_cond;
1216               if (!x.isReturnValueModified())
1217               {
1218                 Assert(x.d_uinfo.find(ce) != x.d_uinfo.end());
1219                 int solve_max = 0;
1220                 for (Node& cond : itpc->second)
1221                 {
1222                   std::map<Node, std::map<unsigned, Node> >::iterator itla =
1223                       x.d_uinfo[ce].d_look_ahead_sols.find(cond);
1224                   if (itla != x.d_uinfo[ce].d_look_ahead_sols.end())
1225                   {
1226                     int nsolved = itla->second.size();
1227                     solve_max = nsolved > solve_max ? nsolved : solve_max;
1228                     solved_cond[nsolved].push_back(cond);
1229                   }
1230                 }
1231                 int n = solve_max;
1232                 while (n > 0)
1233                 {
1234                   if (!solved_cond[n].empty())
1235                   {
1236                     rec_c = constructBestSolvedConditional(solved_cond[n]);
1237                     indent("sygus-sui-dt", ind + 1);
1238                     Trace("sygus-sui-dt")
1239                         << "PBE: ITE strategy : choose solved conditional "
1240                         << d_tds->sygusToBuiltin(rec_c) << " with " << n
1241                         << " solved children..." << std::endl;
1242                     std::map<Node, std::map<unsigned, Node> >::iterator itla =
1243                         x.d_uinfo[ce].d_look_ahead_sols.find(rec_c);
1244                     Assert(itla != x.d_uinfo[ce].d_look_ahead_sols.end());
1245                     for (std::pair<const unsigned, Node>& las : itla->second)
1246                     {
1247                       look_ahead_solved_children[las.first] = las.second;
1248                     }
1249                     break;
1250                   }
1251                   n--;
1252                 }
1253               }
1254
1255               // otherwise, guess a conditional
1256               if (rec_c.isNull())
1257               {
1258                 rec_c = constructBestConditional(itpc->second);
1259                 Assert(!rec_c.isNull());
1260                 indent("sygus-sui-dt", ind);
1261                 Trace("sygus-sui-dt")
1262                     << "PBE: ITE strategy : choose random conditional "
1263                     << d_tds->sygusToBuiltin(rec_c) << std::endl;
1264               }
1265             }
1266             else
1267             {
1268               // TODO (#1250) : degenerate case where children have different
1269               // types?
1270               indent("sygus-sui-dt", ind);
1271               Trace("sygus-sui-dt") << "return PBE: failed ITE strategy, "
1272                                        "cannot find a distinguishable condition"
1273                                     << std::endl;
1274             }
1275             if (!rec_c.isNull())
1276             {
1277               Assert(ecache_child.d_enum_val_to_index.find(rec_c)
1278                      != ecache_child.d_enum_val_to_index.end());
1279               split_cond_res_index = ecache_child.d_enum_val_to_index[rec_c];
1280               split_cond_enum = ce;
1281               Assert(split_cond_res_index >= 0);
1282               Assert(split_cond_res_index
1283                      < (int)ecache_child.d_enum_vals_res.size());
1284             }
1285           }
1286           else
1287           {
1288             rec_c = constructSol(f, cenum.first, cenum.second, ind + 2);
1289           }
1290
1291           // undo update the context
1292           if (strat == strat_ITE && sc > 0)
1293           {
1294             x.d_vals = prev;
1295           }
1296         }
1297         if (!rec_c.isNull())
1298         {
1299           dt_children_cons.push_back(rec_c);
1300         }
1301         else
1302         {
1303           success = false;
1304           break;
1305         }
1306       }
1307       if (success)
1308       {
1309         Assert(dt_children_cons.size() == etis->d_sol_templ_args.size());
1310         // ret_dt = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR,
1311         // dt_children );
1312         ret_dt = etis->d_sol_templ;
1313         ret_dt = ret_dt.substitute(etis->d_sol_templ_args.begin(),
1314                                    etis->d_sol_templ_args.end(),
1315                                    dt_children_cons.begin(),
1316                                    dt_children_cons.end());
1317         indent("sygus-sui-dt-debug", ind);
1318         Trace("sygus-sui-dt-debug")
1319             << "PBE: success : constructed for strategy " << strat << std::endl;
1320       }
1321       else
1322       {
1323         indent("sygus-sui-dt-debug", ind);
1324         Trace("sygus-sui-dt-debug")
1325             << "PBE: failed for strategy " << strat << std::endl;
1326       }
1327     }
1328   }
1329
1330   if (!ret_dt.isNull())
1331   {
1332     Assert(ret_dt.getType() == e.getType());
1333   }
1334   indent("sygus-sui-dt", ind);
1335   Trace("sygus-sui-dt") << "ConstructPBE: returned " << ret_dt << std::endl;
1336   return ret_dt;
1337 }
1338
1339 } /* CVC4::theory::quantifiers namespace */
1340 } /* CVC4::theory namespace */
1341 } /* CVC4 namespace */