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::initializeCandidate(
 470     QuantifiersEngine* qe,
 471     Node f,
 472     std::vector<Node>& enums,
 473     std::map<Node, std::vector<Node>>& strategy_lemmas)
 474 {
 475   d_examples.clear();
 476   d_examples_out.clear();
 477   d_ecache.clear();
 478   d_candidate = f;
 479   SygusUnif::initializeCandidate(qe, f, enums, strategy_lemmas);
 480   // learn redundant operators based on the strategy
 481   d_strategy[f].staticLearnRedundantOps(strategy_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                                     std::vector<Node>& lemmas)
 685 {
 686   Node sol = constructSolutionNode(lemmas);
 687   if (!sol.isNull())
 688   {
 689     sols.push_back(sol);
 690     return true;
 691   }
 692   return false;
 693 }
 694
 695 Node SygusUnifIo::constructSolutionNode(std::vector<Node>& lemmas)
 696 {
 697   Node c = d_candidate;
 698   if (!d_solution.isNull())
 699   {
 700     // already has a solution
 701     return d_solution;
 702   }
 703   // only check if an enumerator updated
 704   if (d_check_sol)
 705   {
 706     Trace("sygus-pbe") << "Construct solution, #iterations = " << d_cond_count
 707                        << std::endl;
 708     d_check_sol = false;
 709     // try multiple times if we have done multiple conditions, due to
 710     // non-determinism
 711     Node vc;
 712     for (unsigned i = 0; i <= d_cond_count; i++)
 713     {
 714       Trace("sygus-pbe-dt") << "ConstructPBE for candidate: " << c << std::endl;
 715       // initialize a call to construct solution
 716       initializeConstructSol();
 717       initializeConstructSolFor(c);
 718       // call the virtual construct solution method
 719       Node e = d_strategy[c].getRootEnumerator();
 720       Node vcc = constructSol(c, e, role_equal, 1, lemmas);
 721       // if we constructed the solution, and we either did not previously have
 722       // a solution, or the new solution is better (smaller).
 723       if (!vcc.isNull()
 724           && (vc.isNull() || (!vc.isNull()
 725                               && d_tds->getSygusTermSize(vcc)
 726                                      < d_tds->getSygusTermSize(vc))))
 727       {
 728         Trace("sygus-pbe") << "**** SygusUnif SOLVED : " << c << " = " << vcc
 729                            << std::endl;
 730         Trace("sygus-pbe") << "...solved at iteration " << i << std::endl;
 731         vc = vcc;
 732       }
 733     }
 734     if (!vc.isNull())
 735     {
 736       d_solution = vc;
 737       return vc;
 738     }
 739     Trace("sygus-pbe") << "...failed to solve." << std::endl;
 740   }
 741   return Node::null();
 742 }
 743
 744 // ------------------------------------ solution construction from enumeration
 745
 746 bool SygusUnifIo::useStrContainsEnumeratorExclude(Node e)
 747 {
 748   TypeNode xbt = d_tds->sygusToBuiltinType(e.getType());
 749   if (xbt.isString())
 750   {
 751     std::map<Node, bool>::iterator itx = d_use_str_contains_eexc.find(e);
 752     if (itx != d_use_str_contains_eexc.end())
 753     {
 754       return itx->second;
 755     }
 756     Trace("sygus-sui-enum-debug")
 757         << "Is " << e << " is str.contains exclusion?" << std::endl;
 758     d_use_str_contains_eexc[e] = true;
 759     Node c = d_candidate;
 760     EnumInfo& ei = d_strategy[c].getEnumInfo(e);
 761     for (const Node& sn : ei.d_enum_slave)
 762     {
 763       EnumInfo& eis = d_strategy[c].getEnumInfo(sn);
 764       EnumRole er = eis.getRole();
 765       if (er != enum_io && er != enum_concat_term)
 766       {
 767         Trace("sygus-sui-enum-debug") << "  incompatible slave : " << sn
 768                                       << ", role = " << er << std::endl;
 769         d_use_str_contains_eexc[e] = false;
 770         return false;
 771       }
 772       if (eis.isConditional())
 773       {
 774         Trace("sygus-sui-enum-debug")
 775             << "  conditional slave : " << sn << std::endl;
 776         d_use_str_contains_eexc[e] = false;
 777         return false;
 778       }
 779     }
 780     Trace("sygus-sui-enum-debug")
 781         << "...can use str.contains exclusion." << std::endl;
 782     return d_use_str_contains_eexc[e];
 783   }
 784   return false;
 785 }
 786
 787 bool SygusUnifIo::getExplanationForEnumeratorExclude(Node e,
 788                                                      Node v,
 789                                                      std::vector<Node>& results,
 790                                                      std::vector<Node>& exp)
 791 {
 792   if (useStrContainsEnumeratorExclude(e))
 793   {
 794     NodeManager* nm = NodeManager::currentNM();
 795     // This check whether the example evaluates to something that is larger than
 796     // the output for some input/output pair. If so, then this term is never
 797     // useful. We generalize its explanation below.
 798
 799     if (Trace.isOn("sygus-sui-cterm-debug"))
 800     {
 801       Trace("sygus-sui-enum") << std::endl;
 802     }
 803     // check if all examples had longer length that the output
 804     Assert(d_examples_out.size() == results.size());
 805     Trace("sygus-sui-cterm-debug")
 806         << "Check enumerator exclusion for " << e << " -> "
 807         << d_tds->sygusToBuiltin(v) << " based on str.contains." << std::endl;
 808     std::vector<unsigned> cmp_indices;
 809     for (unsigned i = 0, size = results.size(); i < size; i++)
 810     {
 811       Assert(results[i].isConst());
 812       Assert(d_examples_out[i].isConst());
 813       Trace("sygus-sui-cterm-debug")
 814           << "  " << results[i] << " <> " << d_examples_out[i];
 815       Node cont = nm->mkNode(STRING_STRCTN, d_examples_out[i], results[i]);
 816       Node contr = Rewriter::rewrite(cont);
 817       if (contr == d_false)
 818       {
 819         cmp_indices.push_back(i);
 820         Trace("sygus-sui-cterm-debug") << "...not contained." << std::endl;
 821       }
 822       else
 823       {
 824         Trace("sygus-sui-cterm-debug") << "...contained." << std::endl;
 825       }
 826     }
 827     if (!cmp_indices.empty())
 828     {
 829       // we check invariance with respect to a negative contains test
 830       NegContainsSygusInvarianceTest ncset;
 831       ncset.init(e, d_examples, d_examples_out, cmp_indices);
 832       // construct the generalized explanation
 833       d_tds->getExplain()->getExplanationFor(e, v, exp, ncset);
 834       Trace("sygus-sui-cterm")
 835           << "PBE-cterm : enumerator exclude " << d_tds->sygusToBuiltin(v)
 836           << " due to negative containment." << std::endl;
 837       return true;
 838     }
 839   }
 840   return false;
 841 }
 842
 843 void SygusUnifIo::EnumCache::addEnumValue(Node v, std::vector<Node>& results)
 844 {
 845   // should not have been enumerated before
 846   Assert(d_enum_val_to_index.find(v) == d_enum_val_to_index.end());
 847   d_enum_val_to_index[v] = d_enum_vals.size();
 848   d_enum_vals.push_back(v);
 849   d_enum_vals_res.push_back(results);
 850 }
 851
 852 void SygusUnifIo::initializeConstructSol() { d_context.initialize(this); }
 853 void SygusUnifIo::initializeConstructSolFor(Node f)
 854 {
 855   Assert(d_candidate == f);
 856 }
 857
 858 Node SygusUnifIo::constructSol(
 859     Node f, Node e, NodeRole nrole, int ind, std::vector<Node>& lemmas)
 860 {
 861   Assert(d_candidate == f);
 862   UnifContextIo& x = d_context;
 863   TypeNode etn = e.getType();
 864   if (Trace.isOn("sygus-sui-dt-debug"))
 865   {
 866     indent("sygus-sui-dt-debug", ind);
 867     Trace("sygus-sui-dt-debug") << "ConstructPBE: (" << e << ", " << nrole
 868                                 << ") for type " << etn << " in context ";
 869     print_val("sygus-sui-dt-debug", x.d_vals);
 870     NodeRole ctx_role = x.getCurrentRole();
 871     Trace("sygus-sui-dt-debug") << ", context role [" << ctx_role;
 872     if (ctx_role == role_string_prefix || ctx_role == role_string_suffix)
 873     {
 874       Trace("sygus-sui-dt-debug") << ", string pos : ";
 875       for (unsigned i = 0, size = x.d_str_pos.size(); i < size; i++)
 876       {
 877         Trace("sygus-sui-dt-debug") << " " << x.d_str_pos[i];
 878       }
 879     }
 880     Trace("sygus-sui-dt-debug") << "]";
 881     Trace("sygus-sui-dt-debug") << std::endl;
 882   }
 883   // enumerator type info
 884   EnumTypeInfo& tinfo = d_strategy[f].getEnumTypeInfo(etn);
 885
 886   // get the enumerator information
 887   EnumInfo& einfo = d_strategy[f].getEnumInfo(e);
 888
 889   EnumCache& ecache = d_ecache[e];
 890
 891   Node ret_dt;
 892   if (nrole == role_equal)
 893   {
 894     if (!x.isReturnValueModified())
 895     {
 896       if (ecache.isSolved())
 897       {
 898         // this type has a complete solution
 899         ret_dt = ecache.getSolved();
 900         indent("sygus-sui-dt", ind);
 901         Trace("sygus-sui-dt") << "return PBE: success : solved "
 902                               << d_tds->sygusToBuiltin(ret_dt) << std::endl;
 903         Assert(!ret_dt.isNull());
 904       }
 905       else
 906       {
 907         // could be conditionally solved
 908         std::vector<Node> subsumed_by;
 909         ecache.d_term_trie.getSubsumedBy(x.d_vals, true, subsumed_by);
 910         if (!subsumed_by.empty())
 911         {
 912           ret_dt = constructBestSolvedTerm(subsumed_by);
 913           indent("sygus-sui-dt", ind);
 914           Trace("sygus-sui-dt") << "return PBE: success : conditionally solved"
 915                                 << d_tds->sygusToBuiltin(ret_dt) << std::endl;
 916         }
 917         else
 918         {
 919           indent("sygus-sui-dt-debug", ind);
 920           Trace("sygus-sui-dt-debug")
 921               << "  ...not currently conditionally solved." << std::endl;
 922         }
 923       }
 924     }
 925     if (ret_dt.isNull())
 926     {
 927       if (d_tds->sygusToBuiltinType(e.getType()).isString())
 928       {
 929         // check if a current value that closes all examples
 930         // get the term enumerator for this type
 931         std::map<EnumRole, Node>::iterator itnt =
 932             tinfo.d_enum.find(enum_concat_term);
 933         if (itnt != tinfo.d_enum.end())
 934         {
 935           Node et = itnt->second;
 936
 937           EnumCache& ecachet = d_ecache[et];
 938           // get the current examples
 939           std::vector<String> ex_vals;
 940           x.getCurrentStrings(this, d_examples_out, ex_vals);
 941           Assert(ecache.d_enum_vals.size() == ecache.d_enum_vals_res.size());
 942
 943           // test each example in the term enumerator for the type
 944           std::vector<Node> str_solved;
 945           for (unsigned i = 0, size = ecachet.d_enum_vals.size(); i < size; i++)
 946           {
 947             if (x.isStringSolved(this, ex_vals, ecachet.d_enum_vals_res[i]))
 948             {
 949               str_solved.push_back(ecachet.d_enum_vals[i]);
 950             }
 951           }
 952           if (!str_solved.empty())
 953           {
 954             ret_dt = constructBestStringSolvedTerm(str_solved);
 955             indent("sygus-sui-dt", ind);
 956             Trace("sygus-sui-dt") << "return PBE: success : string solved "
 957                                   << d_tds->sygusToBuiltin(ret_dt) << std::endl;
 958           }
 959           else
 960           {
 961             indent("sygus-sui-dt-debug", ind);
 962             Trace("sygus-sui-dt-debug")
 963                 << "  ...not currently string solved." << std::endl;
 964           }
 965         }
 966       }
 967     }
 968   }
 969   else if (nrole == role_string_prefix || nrole == role_string_suffix)
 970   {
 971     // check if each return value is a prefix/suffix of all open examples
 972     if (!x.isReturnValueModified() || x.getCurrentRole() == nrole)
 973     {
 974       std::map<Node, std::vector<unsigned> > incr;
 975       bool isPrefix = nrole == role_string_prefix;
 976       std::map<Node, unsigned> total_inc;
 977       std::vector<Node> inc_strs;
 978       // make the value of the examples
 979       std::vector<String> ex_vals;
 980       x.getCurrentStrings(this, d_examples_out, ex_vals);
 981       if (Trace.isOn("sygus-sui-dt-debug"))
 982       {
 983         indent("sygus-sui-dt-debug", ind);
 984         Trace("sygus-sui-dt-debug") << "current strings : " << std::endl;
 985         for (unsigned i = 0, size = ex_vals.size(); i < size; i++)
 986         {
 987           indent("sygus-sui-dt-debug", ind + 1);
 988           Trace("sygus-sui-dt-debug") << ex_vals[i] << std::endl;
 989         }
 990       }
 991
 992       // check if there is a value for which is a prefix/suffix of all active
 993       // examples
 994       Assert(ecache.d_enum_vals.size() == ecache.d_enum_vals_res.size());
 995
 996       for (unsigned i = 0, size = ecache.d_enum_vals.size(); i < size; i++)
 997       {
 998         Node val_t = ecache.d_enum_vals[i];
 999         Assert(incr.find(val_t) == incr.end());
1000         indent("sygus-sui-dt-debug", ind);
1001         Trace("sygus-sui-dt-debug")
1002             << "increment string values : " << val_t << " : ";
1003         Assert(ecache.d_enum_vals_res[i].size() == d_examples_out.size());
1004         unsigned tot = 0;
1005         bool exsuccess = x.getStringIncrement(this,
1006                                               isPrefix,
1007                                               ex_vals,
1008                                               ecache.d_enum_vals_res[i],
1009                                               incr[val_t],
1010                                               tot);
1011         if (!exsuccess)
1012         {
1013           incr.erase(val_t);
1014           Trace("sygus-sui-dt-debug") << "...fail" << std::endl;
1015         }
1016         else
1017         {
1018           total_inc[val_t] = tot;
1019           inc_strs.push_back(val_t);
1020           Trace("sygus-sui-dt-debug")
1021               << "...success, total increment = " << tot << std::endl;
1022         }
1023       }
1024
1025       if (!incr.empty())
1026       {
1027         ret_dt = constructBestStringToConcat(inc_strs, total_inc, incr);
1028         Assert(!ret_dt.isNull());
1029         indent("sygus-sui-dt", ind);
1030         Trace("sygus-sui-dt")
1031             << "PBE: CONCAT strategy : choose " << (isPrefix ? "pre" : "suf")
1032             << "fix value " << d_tds->sygusToBuiltin(ret_dt) << std::endl;
1033         // update the context
1034         bool ret = x.updateStringPosition(this, incr[ret_dt], nrole);
1035         AlwaysAssert(ret == (total_inc[ret_dt] > 0));
1036       }
1037       else
1038       {
1039         indent("sygus-sui-dt", ind);
1040         Trace("sygus-sui-dt") << "PBE: failed CONCAT strategy, no values are "
1041                               << (isPrefix ? "pre" : "suf")
1042                               << "fix of all examples." << std::endl;
1043       }
1044     }
1045     else
1046     {
1047       indent("sygus-sui-dt", ind);
1048       Trace("sygus-sui-dt")
1049           << "PBE: failed CONCAT strategy, prefix/suffix mismatch."
1050           << std::endl;
1051     }
1052   }
1053   if (ret_dt.isNull() && !einfo.isTemplated())
1054   {
1055     // we will try a single strategy
1056     EnumTypeInfoStrat* etis = nullptr;
1057     std::map<NodeRole, StrategyNode>::iterator itsn =
1058         tinfo.d_snodes.find(nrole);
1059     if (itsn != tinfo.d_snodes.end())
1060     {
1061       // strategy info
1062       StrategyNode& snode = itsn->second;
1063       if (x.d_visit_role[e].find(nrole) == x.d_visit_role[e].end())
1064       {
1065         x.d_visit_role[e][nrole] = true;
1066         // try a random strategy
1067         if (snode.d_strats.size() > 1)
1068         {
1069           std::random_shuffle(snode.d_strats.begin(), snode.d_strats.end());
1070         }
1071         // get an eligible strategy index
1072         unsigned sindex = 0;
1073         while (sindex < snode.d_strats.size()
1074                && !snode.d_strats[sindex]->isValid(x))
1075         {
1076           sindex++;
1077         }
1078         // if we found a eligible strategy
1079         if (sindex < snode.d_strats.size())
1080         {
1081           etis = snode.d_strats[sindex];
1082         }
1083       }
1084     }
1085     if (etis != nullptr)
1086     {
1087       StrategyType strat = etis->d_this;
1088       indent("sygus-sui-dt", ind + 1);
1089       Trace("sygus-sui-dt")
1090           << "...try STRATEGY " << strat << "..." << std::endl;
1091
1092       std::map<unsigned, Node> look_ahead_solved_children;
1093       std::vector<Node> dt_children_cons;
1094       bool success = true;
1095
1096       // for ITE
1097       Node split_cond_enum;
1098       int split_cond_res_index = -1;
1099
1100       for (unsigned sc = 0, size = etis->d_cenum.size(); sc < size; sc++)
1101       {
1102         indent("sygus-sui-dt", ind + 1);
1103         Trace("sygus-sui-dt")
1104             << "construct PBE child #" << sc << "..." << std::endl;
1105         Node rec_c;
1106         std::map<unsigned, Node>::iterator itla =
1107             look_ahead_solved_children.find(sc);
1108         if (itla != look_ahead_solved_children.end())
1109         {
1110           rec_c = itla->second;
1111           indent("sygus-sui-dt-debug", ind + 1);
1112           Trace("sygus-sui-dt-debug")
1113               << "ConstructPBE: look ahead solved : "
1114               << d_tds->sygusToBuiltin(rec_c) << std::endl;
1115         }
1116         else
1117         {
1118           std::pair<Node, NodeRole>& cenum = etis->d_cenum[sc];
1119
1120           // update the context
1121           std::vector<Node> prev;
1122           if (strat == strat_ITE && sc > 0)
1123           {
1124             EnumCache& ecache_cond = d_ecache[split_cond_enum];
1125             Assert(split_cond_res_index >= 0);
1126             Assert(split_cond_res_index
1127                    < (int)ecache_cond.d_enum_vals_res.size());
1128             prev = x.d_vals;
1129             bool ret = x.updateContext(
1130                 this,
1131                 ecache_cond.d_enum_vals_res[split_cond_res_index],
1132                 sc == 1);
1133             AlwaysAssert(ret);
1134           }
1135
1136           // recurse
1137           if (strat == strat_ITE && sc == 0)
1138           {
1139             Node ce = cenum.first;
1140
1141             EnumCache& ecache_child = d_ecache[ce];
1142
1143             // only used if the return value is not modified
1144             if (!x.isReturnValueModified())
1145             {
1146               if (x.d_uinfo.find(ce) == x.d_uinfo.end())
1147               {
1148                 Trace("sygus-sui-dt-debug2")
1149                     << "  reg : PBE: Look for direct solutions for conditional "
1150                        "enumerator "
1151                     << ce << " ... " << std::endl;
1152                 Assert(ecache_child.d_enum_vals.size()
1153                        == ecache_child.d_enum_vals_res.size());
1154                 for (unsigned i = 1; i <= 2; i++)
1155                 {
1156                   std::pair<Node, NodeRole>& te_pair = etis->d_cenum[i];
1157                   Node te = te_pair.first;
1158                   EnumCache& ecache_te = d_ecache[te];
1159                   bool branch_pol = (i == 1);
1160                   // for each condition, get terms that satisfy it in this
1161                   // branch
1162                   for (unsigned k = 0, size = ecache_child.d_enum_vals.size();
1163                        k < size;
1164                        k++)
1165                   {
1166                     Node cond = ecache_child.d_enum_vals[k];
1167                     std::vector<Node> solved;
1168                     ecache_te.d_term_trie.getSubsumedBy(
1169                         ecache_child.d_enum_vals_res[k], branch_pol, solved);
1170                     Trace("sygus-sui-dt-debug2")
1171                         << "  reg : PBE: " << d_tds->sygusToBuiltin(cond)
1172                         << " has " << solved.size() << " solutions in branch "
1173                         << i << std::endl;
1174                     if (!solved.empty())
1175                     {
1176                       Node slv = constructBestSolvedTerm(solved);
1177                       Trace("sygus-sui-dt-debug2")
1178                           << "  reg : PBE: ..." << d_tds->sygusToBuiltin(slv)
1179                           << " is a solution under branch " << i;
1180                       Trace("sygus-sui-dt-debug2")
1181                           << " of condition " << d_tds->sygusToBuiltin(cond)
1182                           << std::endl;
1183                       x.d_uinfo[ce].d_look_ahead_sols[cond][i] = slv;
1184                     }
1185                   }
1186                 }
1187               }
1188             }
1189
1190             // get the conditionals in the current context : they must be
1191             // distinguishable
1192             std::map<int, std::vector<Node> > possible_cond;
1193             std::map<Node, int> solved_cond;  // stores branch
1194             ecache_child.d_term_trie.getLeaves(x.d_vals, true, possible_cond);
1195
1196             std::map<int, std::vector<Node> >::iterator itpc =
1197                 possible_cond.find(0);
1198             if (itpc != possible_cond.end())
1199             {
1200               if (Trace.isOn("sygus-sui-dt-debug"))
1201               {
1202                 indent("sygus-sui-dt-debug", ind + 1);
1203                 Trace("sygus-sui-dt-debug")
1204                     << "PBE : We have " << itpc->second.size()
1205                     << " distinguishable conditionals:" << std::endl;
1206                 for (Node& cond : itpc->second)
1207                 {
1208                   indent("sygus-sui-dt-debug", ind + 2);
1209                   Trace("sygus-sui-dt-debug")
1210                       << d_tds->sygusToBuiltin(cond) << std::endl;
1211                 }
1212               }
1213
1214               // static look ahead conditional : choose conditionals that have
1215               // solved terms in at least one branch
1216               //    only applicable if we have not modified the return value
1217               std::map<int, std::vector<Node> > solved_cond;
1218               if (!x.isReturnValueModified())
1219               {
1220                 Assert(x.d_uinfo.find(ce) != x.d_uinfo.end());
1221                 int solve_max = 0;
1222                 for (Node& cond : itpc->second)
1223                 {
1224                   std::map<Node, std::map<unsigned, Node> >::iterator itla =
1225                       x.d_uinfo[ce].d_look_ahead_sols.find(cond);
1226                   if (itla != x.d_uinfo[ce].d_look_ahead_sols.end())
1227                   {
1228                     int nsolved = itla->second.size();
1229                     solve_max = nsolved > solve_max ? nsolved : solve_max;
1230                     solved_cond[nsolved].push_back(cond);
1231                   }
1232                 }
1233                 int n = solve_max;
1234                 while (n > 0)
1235                 {
1236                   if (!solved_cond[n].empty())
1237                   {
1238                     rec_c = constructBestSolvedConditional(solved_cond[n]);
1239                     indent("sygus-sui-dt", ind + 1);
1240                     Trace("sygus-sui-dt")
1241                         << "PBE: ITE strategy : choose solved conditional "
1242                         << d_tds->sygusToBuiltin(rec_c) << " with " << n
1243                         << " solved children..." << std::endl;
1244                     std::map<Node, std::map<unsigned, Node> >::iterator itla =
1245                         x.d_uinfo[ce].d_look_ahead_sols.find(rec_c);
1246                     Assert(itla != x.d_uinfo[ce].d_look_ahead_sols.end());
1247                     for (std::pair<const unsigned, Node>& las : itla->second)
1248                     {
1249                       look_ahead_solved_children[las.first] = las.second;
1250                     }
1251                     break;
1252                   }
1253                   n--;
1254                 }
1255               }
1256
1257               // otherwise, guess a conditional
1258               if (rec_c.isNull())
1259               {
1260                 rec_c = constructBestConditional(itpc->second);
1261                 Assert(!rec_c.isNull());
1262                 indent("sygus-sui-dt", ind);
1263                 Trace("sygus-sui-dt")
1264                     << "PBE: ITE strategy : choose random conditional "
1265                     << d_tds->sygusToBuiltin(rec_c) << std::endl;
1266               }
1267             }
1268             else
1269             {
1270               // TODO (#1250) : degenerate case where children have different
1271               // types?
1272               indent("sygus-sui-dt", ind);
1273               Trace("sygus-sui-dt") << "return PBE: failed ITE strategy, "
1274                                        "cannot find a distinguishable condition"
1275                                     << std::endl;
1276             }
1277             if (!rec_c.isNull())
1278             {
1279               Assert(ecache_child.d_enum_val_to_index.find(rec_c)
1280                      != ecache_child.d_enum_val_to_index.end());
1281               split_cond_res_index = ecache_child.d_enum_val_to_index[rec_c];
1282               split_cond_enum = ce;
1283               Assert(split_cond_res_index >= 0);
1284               Assert(split_cond_res_index
1285                      < (int)ecache_child.d_enum_vals_res.size());
1286             }
1287           }
1288           else
1289           {
1290             rec_c = constructSol(f, cenum.first, cenum.second, ind + 2, lemmas);
1291           }
1292
1293           // undo update the context
1294           if (strat == strat_ITE && sc > 0)
1295           {
1296             x.d_vals = prev;
1297           }
1298         }
1299         if (!rec_c.isNull())
1300         {
1301           dt_children_cons.push_back(rec_c);
1302         }
1303         else
1304         {
1305           success = false;
1306           break;
1307         }
1308       }
1309       if (success)
1310       {
1311         Assert(dt_children_cons.size() == etis->d_sol_templ_args.size());
1312         // ret_dt = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR,
1313         // dt_children );
1314         ret_dt = etis->d_sol_templ;
1315         ret_dt = ret_dt.substitute(etis->d_sol_templ_args.begin(),
1316                                    etis->d_sol_templ_args.end(),
1317                                    dt_children_cons.begin(),
1318                                    dt_children_cons.end());
1319         indent("sygus-sui-dt-debug", ind);
1320         Trace("sygus-sui-dt-debug")
1321             << "PBE: success : constructed for strategy " << strat << std::endl;
1322       }
1323       else
1324       {
1325         indent("sygus-sui-dt-debug", ind);
1326         Trace("sygus-sui-dt-debug")
1327             << "PBE: failed for strategy " << strat << std::endl;
1328       }
1329     }
1330   }
1331
1332   if (!ret_dt.isNull())
1333   {
1334     Assert(ret_dt.getType() == e.getType());
1335   }
1336   indent("sygus-sui-dt", ind);
1337   Trace("sygus-sui-dt") << "ConstructPBE: returned " << ret_dt << std::endl;
1338   return ret_dt;
1339 }
1340
1341 } /* CVC4::theory::quantifiers namespace */
1342 } /* CVC4::theory namespace */
1343 } /* CVC4 namespace */