src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp

   1 /*********************                                                        */
   2 /*! \file inst_strategy_e_matching.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Morgan Deters, Mathias Preiner
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 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 e matching instantiation strategies
  13  **/
  14
  15 #include "theory/quantifiers/ematching/inst_strategy_e_matching.h"
  16
  17 #include "theory/quantifiers/ematching/pattern_term_selector.h"
  18 #include "theory/quantifiers/quant_relevance.h"
  19 #include "theory/quantifiers_engine.h"
  20 #include "util/random.h"
  21
  22 using namespace CVC4::kind;
  23 using namespace CVC4::theory::inst;
  24
  25 namespace CVC4 {
  26 namespace theory {
  27 namespace quantifiers {
  28
  29 //priority levels :
  30 //1 : user patterns (when user-pat!={resort,ignore}), auto-gen patterns (for non-user pattern quantifiers, or when user-pat={resort,ignore})
  31 //2 : user patterns (when user-pat=resort), auto gen patterns (for user pattern quantifiers when user-pat=use)
  32
  33 // user-pat=interleave alternates between use and resort
  34
  35 struct sortQuantifiersForSymbol {
  36   QuantRelevance* d_quant_rel;
  37   std::map< Node, Node > d_op_map;
  38   bool operator() (Node i, Node j) {
  39     size_t nqfsi = d_quant_rel->getNumQuantifiersForSymbol(d_op_map[i]);
  40     size_t nqfsj = d_quant_rel->getNumQuantifiersForSymbol(d_op_map[j]);
  41     if( nqfsi<nqfsj ){
  42       return true;
  43     }else if( nqfsi>nqfsj ){
  44       return false;
  45     }
  46     return false;
  47   }
  48 };
  49
  50 struct sortTriggers {
  51   bool operator() (Node i, Node j) {
  52     int32_t wi = TriggerTermInfo::getTriggerWeight(i);
  53     int32_t wj = TriggerTermInfo::getTriggerWeight(j);
  54     if( wi==wj ){
  55       return i<j;
  56     }
  57     return wi < wj;
  58   }
  59 };
  60
  61 InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers(QuantifiersEngine* qe,
  62                                                          QuantifiersState& qs,
  63                                                          QuantRelevance* qr)
  64     : InstStrategy(qe, qs), d_quant_rel(qr)
  65 {
  66   //how to select trigger terms
  67   d_tr_strategy = options::triggerSelMode();
  68   //whether to select new triggers during the search
  69   if( options::incrementTriggers() ){
  70     d_regenerate_frequency = 3;
  71     d_regenerate = true;
  72   }else{
  73     d_regenerate_frequency = 1;
  74     d_regenerate = false;
  75   }
  76 }
  77
  78 void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort effort ){
  79   Trace("inst-alg-debug") << "reset auto-gen triggers" << std::endl;
  80   //reset triggers
  81   for( unsigned r=0; r<2; r++ ){
  82     std::map<Node, std::map<inst::Trigger*, bool> >& agts =
  83         d_auto_gen_trigger[r];
  84     for (std::pair<const Node, std::map<inst::Trigger*, bool> >& agt : agts)
  85     {
  86       for (std::map<inst::Trigger*, bool>::iterator it = agt.second.begin();
  87            it != agt.second.end();
  88            ++it)
  89       {
  90         it->first->resetInstantiationRound();
  91         it->first->reset(Node::null());
  92       }
  93     }
  94   }
  95   d_processed_trigger.clear();
  96   Trace("inst-alg-debug") << "done reset auto-gen triggers" << std::endl;
  97 }
  98
  99 InstStrategyStatus InstStrategyAutoGenTriggers::process(Node f,
 100                                                         Theory::Effort effort,
 101                                                         int e)
 102 {
 103   options::UserPatMode upMode = d_quantEngine->getInstUserPatMode();
 104   if (hasUserPatterns(f) && upMode == options::UserPatMode::TRUST)
 105   {
 106     return InstStrategyStatus::STATUS_UNKNOWN;
 107   }
 108   int peffort = (hasUserPatterns(f) && upMode != options::UserPatMode::IGNORE
 109                  && upMode != options::UserPatMode::RESORT)
 110                     ? 2
 111                     : 1;
 112   if (e < peffort)
 113   {
 114     return InstStrategyStatus::STATUS_UNFINISHED;
 115   }
 116   Trace("inst-alg") << "-> Auto-gen instantiate " << f << "..." << std::endl;
 117   bool gen = false;
 118   if (e == peffort)
 119   {
 120     if (d_counter.find(f) == d_counter.end())
 121     {
 122       d_counter[f] = 0;
 123       gen = true;
 124     }else{
 125       d_counter[f]++;
 126       gen = d_regenerate && d_counter[f] % d_regenerate_frequency == 0;
 127     }
 128   }
 129   else
 130   {
 131     gen = true;
 132   }
 133   if (gen)
 134   {
 135     generateTriggers(f);
 136     if (d_counter[f] == 0 && d_auto_gen_trigger[0][f].empty()
 137         && d_auto_gen_trigger[1][f].empty() && f.getNumChildren() == 2)
 138     {
 139       Trace("trigger-warn") << "Could not find trigger for " << f << std::endl;
 140     }
 141   }
 142   if (options::triggerActiveSelMode() != options::TriggerActiveSelMode::ALL)
 143   {
 144     int max_score = -1;
 145     Trigger* max_trigger = nullptr;
 146     std::map<Trigger*, bool>& agt = d_auto_gen_trigger[0][f];
 147     for (std::map<Trigger*, bool>::iterator it = agt.begin(); it != agt.end();
 148          ++it)
 149     {
 150       Trigger* t = it->first;
 151       int score = t->getActiveScore();
 152       if (options::triggerActiveSelMode() == options::TriggerActiveSelMode::MIN)
 153       {
 154         if (score >= 0 && (score < max_score || max_score < 0))
 155         {
 156           max_score = score;
 157           max_trigger = t;
 158         }
 159       }
 160       else
 161       {
 162         if (score > max_score)
 163         {
 164           max_score = score;
 165           max_trigger = t;
 166         }
 167       }
 168       agt[t] = false;
 169     }
 170     if (max_trigger != nullptr)
 171     {
 172       agt[max_trigger] = true;
 173     }
 174   }
 175
 176   bool hasInst = false;
 177   for (unsigned r = 0; r < 2; r++)
 178   {
 179     std::map<Trigger*, bool>& agt = d_auto_gen_trigger[r][f];
 180     for (std::map<Trigger*, bool>::iterator it = agt.begin(); it != agt.end();
 181          ++it)
 182     {
 183       Trigger* tr = it->first;
 184       if (tr == nullptr || !it->second)
 185       {
 186         // trigger is null or currently disabled
 187         continue;
 188       }
 189       if (d_processed_trigger[f].find(tr) != d_processed_trigger[f].end())
 190       {
 191         // trigger is already processed this round
 192         continue;
 193       }
 194       d_processed_trigger[f][tr] = true;
 195       Trace("process-trigger") << "  Process ";
 196       tr->debugPrint("process-trigger");
 197       Trace("process-trigger") << "..." << std::endl;
 198       unsigned numInst = tr->addInstantiations();
 199       hasInst = numInst > 0 || hasInst;
 200       Trace("process-trigger")
 201           << "  Done, numInst = " << numInst << "." << std::endl;
 202       d_quantEngine->d_statistics.d_instantiations_auto_gen += numInst;
 203       if (r == 1)
 204       {
 205         d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
 206       }
 207       if (d_qstate.isInConflict())
 208       {
 209         break;
 210       }
 211     }
 212     if (d_qstate.isInConflict() || (hasInst && options::multiTriggerPriority()))
 213     {
 214       break;
 215     }
 216   }
 217   return InstStrategyStatus::STATUS_UNKNOWN;
 218 }
 219
 220 void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
 221   Trace("auto-gen-trigger-debug") << "Generate triggers for " << f << ", #var=" << f[0].getNumChildren() << "..." << std::endl;
 222
 223   // first, generate the set of pattern terms
 224   if (!generatePatternTerms(f))
 225   {
 226     Trace("auto-gen-trigger-debug")
 227         << "...failed to generate pattern terms" << std::endl;
 228     return;
 229   }
 230
 231   // then, group them to make triggers
 232   unsigned rmin = d_patTerms[0][f].empty() ? 1 : 0;
 233   unsigned rmax = options::multiTriggerWhenSingle() ? 1 : rmin;
 234   for (unsigned r = rmin; r <= rmax; r++)
 235   {
 236     std::vector<Node> patTerms;
 237     std::vector<Node>& ptc = d_patTerms[r][f];
 238     for (const Node& p : ptc)
 239     {
 240       if (r == 1 || d_single_trigger_gen.find(p) == d_single_trigger_gen.end())
 241       {
 242         patTerms.push_back(p);
 243       }
 244     }
 245     if (patTerms.empty())
 246     {
 247       continue;
 248     }
 249     Trace("auto-gen-trigger") << "Generate trigger for " << f << std::endl;
 250     // sort terms based on relevance
 251     if (options::relevantTriggers())
 252     {
 253       Assert(d_quant_rel);
 254       sortQuantifiersForSymbol sqfs;
 255       sqfs.d_quant_rel = d_quant_rel;
 256       for (const Node& p : patTerms)
 257       {
 258         Assert(d_pat_to_mpat.find(p) != d_pat_to_mpat.end());
 259         Assert(d_pat_to_mpat[p].hasOperator());
 260         sqfs.d_op_map[p] = d_pat_to_mpat[p].getOperator();
 261       }
 262       // sort based on # occurrences (this will cause Trigger to select rarer
 263       // symbols)
 264       std::sort(patTerms.begin(), patTerms.end(), sqfs);
 265       if (Debug.isOn("relevant-trigger"))
 266       {
 267         Debug("relevant-trigger") << "Terms based on relevance: " << std::endl;
 268         for (const Node& p : patTerms)
 269         {
 270           Debug("relevant-trigger")
 271               << "   " << p << " from " << d_pat_to_mpat[p] << " (";
 272           Debug("relevant-trigger") << d_quant_rel->getNumQuantifiersForSymbol(
 273                                            d_pat_to_mpat[p].getOperator())
 274                                     << ")" << std::endl;
 275         }
 276       }
 277     }
 278     // now, generate the trigger...
 279     Trigger* tr = NULL;
 280     if (d_is_single_trigger[patTerms[0]])
 281     {
 282       tr = Trigger::mkTrigger(d_quantEngine,
 283                               f,
 284                               patTerms[0],
 285                               false,
 286                               Trigger::TR_RETURN_NULL,
 287                               d_num_trigger_vars[f]);
 288       d_single_trigger_gen[patTerms[0]] = true;
 289     }
 290     else
 291     {
 292       // only generate multi trigger if option set, or if no single triggers
 293       // exist
 294       if (!d_patTerms[0][f].empty())
 295       {
 296         if (options::multiTriggerWhenSingle())
 297         {
 298           Trace("multi-trigger-debug")
 299               << "Resort to choosing multi-triggers..." << std::endl;
 300         }
 301         else
 302         {
 303           return;
 304         }
 305       }
 306       // if we are re-generating triggers, shuffle based on some method
 307       if (d_made_multi_trigger[f])
 308       {
 309         std::shuffle(patTerms.begin(),
 310                      patTerms.end(),
 311                      Random::getRandom());  // shuffle randomly
 312       }
 313       else
 314       {
 315         d_made_multi_trigger[f] = true;
 316       }
 317       // will possibly want to get an old trigger
 318       tr = Trigger::mkTrigger(d_quantEngine,
 319                               f,
 320                               patTerms,
 321                               false,
 322                               Trigger::TR_GET_OLD,
 323                               d_num_trigger_vars[f]);
 324     }
 325     if (tr == nullptr)
 326     {
 327       // did not generate a trigger
 328       continue;
 329     }
 330     addTrigger(tr, f);
 331     if (tr->isMultiTrigger())
 332     {
 333       // only add a single multi-trigger
 334       continue;
 335     }
 336     // if we are generating additional triggers...
 337     size_t index = 0;
 338     if (index < patTerms.size())
 339     {
 340       // check if similar patterns exist, and if so, add them additionally
 341       unsigned nqfs_curr = 0;
 342       if (options::relevantTriggers())
 343       {
 344         nqfs_curr =
 345             d_quant_rel->getNumQuantifiersForSymbol(patTerms[0].getOperator());
 346       }
 347       index++;
 348       bool success = true;
 349       while (success && index < patTerms.size()
 350              && d_is_single_trigger[patTerms[index]])
 351       {
 352         success = false;
 353         if (!options::relevantTriggers()
 354             || d_quant_rel->getNumQuantifiersForSymbol(
 355                    patTerms[index].getOperator())
 356                    <= nqfs_curr)
 357         {
 358           d_single_trigger_gen[patTerms[index]] = true;
 359           Trigger* tr2 = Trigger::mkTrigger(d_quantEngine,
 360                                             f,
 361                                             patTerms[index],
 362                                             false,
 363                                             Trigger::TR_RETURN_NULL,
 364                                             d_num_trigger_vars[f]);
 365           addTrigger(tr2, f);
 366           success = true;
 367         }
 368         index++;
 369       }
 370     }
 371   }
 372 }
 373
 374 bool InstStrategyAutoGenTriggers::generatePatternTerms(Node f)
 375 {
 376   if (d_patTerms[0].find(f) != d_patTerms[0].end())
 377   {
 378     // already generated
 379     return true;
 380   }
 381   // determine all possible pattern terms based on trigger term selection
 382   // strategy d_tr_strategy
 383   d_patTerms[0][f].clear();
 384   d_patTerms[1][f].clear();
 385   bool ntrivTriggers = options::relationalTriggers();
 386   std::vector<Node> patTermsF;
 387   std::map<Node, inst::TriggerTermInfo> tinfo;
 388   TermUtil* tu = d_quantEngine->getTermUtil();
 389   NodeManager* nm = NodeManager::currentNM();
 390   // well-defined function: can assume LHS is only pattern
 391   if (options::quantFunWellDefined())
 392   {
 393     Node hd = QuantAttributes::getFunDefHead(f);
 394     if (!hd.isNull())
 395     {
 396       hd = tu->substituteBoundVariablesToInstConstants(hd, f);
 397       patTermsF.push_back(hd);
 398       tinfo[hd].init(f, hd);
 399     }
 400   }
 401   // otherwise, use algorithm for collecting pattern terms
 402   if (patTermsF.empty())
 403   {
 404     Node bd = tu->getInstConstantBody(f);
 405     PatternTermSelector pts(f, d_tr_strategy, d_user_no_gen[f], true);
 406     pts.collect(bd, patTermsF, tinfo);
 407     if (ntrivTriggers)
 408     {
 409       sortTriggers st;
 410       std::sort(patTermsF.begin(), patTermsF.end(), st);
 411     }
 412     if (Trace.isOn("auto-gen-trigger-debug"))
 413     {
 414       Trace("auto-gen-trigger-debug")
 415           << "Collected pat terms for " << bd
 416           << ", no-patterns : " << d_user_no_gen[f].size() << std::endl;
 417       for (const Node& p : patTermsF)
 418       {
 419         Assert(tinfo.find(p) != tinfo.end());
 420         Trace("auto-gen-trigger-debug") << "   " << p << std::endl;
 421         Trace("auto-gen-trigger-debug2")
 422             << "     info = [" << tinfo[p].d_reqPol << ", "
 423             << tinfo[p].d_reqPolEq << ", " << tinfo[p].d_fv.size() << "]"
 424             << std::endl;
 425       }
 426       Trace("auto-gen-trigger-debug") << std::endl;
 427     }
 428   }
 429   // sort into single/multi triggers, calculate which terms should not be
 430   // considered
 431   std::map<Node, bool> vcMap;
 432   std::map<Node, bool> rmPatTermsF;
 433   int32_t last_weight = -1;
 434   for (const Node& p : patTermsF)
 435   {
 436     Assert(p.getKind() != NOT);
 437     bool newVar = false;
 438     inst::TriggerTermInfo& tip = tinfo[p];
 439     for (const Node& v : tip.d_fv)
 440     {
 441       if (vcMap.find(v) == vcMap.end())
 442       {
 443         vcMap[v] = true;
 444         newVar = true;
 445       }
 446     }
 447     int32_t curr_w = TriggerTermInfo::getTriggerWeight(p);
 448     // triggers whose value is maximum (2) are considered expendable.
 449     if (ntrivTriggers && !newVar && last_weight != -1 && curr_w > last_weight
 450         && curr_w >= 2)
 451     {
 452       Trace("auto-gen-trigger-debug")
 453           << "...exclude expendible non-trivial trigger : " << p << std::endl;
 454       rmPatTermsF[p] = true;
 455     }
 456     else
 457     {
 458       last_weight = curr_w;
 459     }
 460   }
 461   d_num_trigger_vars[f] = vcMap.size();
 462   if (d_num_trigger_vars[f] > 0
 463       && d_num_trigger_vars[f] < f[0].getNumChildren())
 464   {
 465     Trace("auto-gen-trigger-partial")
 466         << "Quantified formula : " << f << std::endl;
 467     Trace("auto-gen-trigger-partial")
 468         << "...does not contain all variables in triggers!!!" << std::endl;
 469     // Invoke partial trigger strategy: partition variables of quantified
 470     // formula into (X,Y) where X are contained in a trigger and Y are not.
 471     // We then force a split of the quantified formula so that it becomes:
 472     //   forall X. forall Y. P( X, Y )
 473     // and hence is treatable by E-matching. We only do this for "standard"
 474     // quantified formulas (those with only two children), since this
 475     // technique should not be used for e.g. quantifiers marked for
 476     // quantifier elimination.
 477     QAttributes qa;
 478     QuantAttributes::computeQuantAttributes(f, qa);
 479     if (options::partialTriggers() && qa.isStandard())
 480     {
 481       std::vector<Node> vcs[2];
 482       for (size_t i = 0, nchild = f[0].getNumChildren(); i < nchild; i++)
 483       {
 484         Node ic = tu->getInstantiationConstant(f, i);
 485         vcs[vcMap.find(ic) == vcMap.end() ? 0 : 1].push_back(f[0][i]);
 486       }
 487       for (size_t i = 0; i < 2; i++)
 488       {
 489         d_vc_partition[i][f] = nm->mkNode(BOUND_VAR_LIST, vcs[i]);
 490       }
 491     }
 492     else
 493     {
 494       return false;
 495     }
 496   }
 497   for (const Node& patf : patTermsF)
 498   {
 499     Node pat = patf;
 500     if (rmPatTermsF.find(pat) != rmPatTermsF.end())
 501     {
 502       continue;
 503     }
 504     Trace("auto-gen-trigger-debug")
 505         << "...processing pattern " << pat << std::endl;
 506     Node mpat = pat;
 507     // process the pattern: if it has a required polarity, consider it
 508     Assert(tinfo.find(pat) != tinfo.end());
 509     int rpol = tinfo[pat].d_reqPol;
 510     Node rpoleq = tinfo[pat].d_reqPolEq;
 511     size_t num_fv = tinfo[pat].d_fv.size();
 512     Trace("auto-gen-trigger-debug")
 513         << "...required polarity for " << pat << " is " << rpol
 514         << ", eq=" << rpoleq << std::endl;
 515     if (rpol != 0)
 516     {
 517       Assert(rpol == 1 || rpol == -1);
 518       if (TriggerTermInfo::isRelationalTrigger(pat))
 519       {
 520         pat = rpol == -1 ? pat.negate() : pat;
 521       }
 522       else
 523       {
 524         Assert(TriggerTermInfo::isAtomicTrigger(pat));
 525         if (pat.getType().isBoolean() && rpoleq.isNull())
 526         {
 527           if (options::literalMatchMode() == options::LiteralMatchMode::USE)
 528           {
 529             pat = pat.eqNode(nm->mkConst(rpol == -1)).negate();
 530           }
 531           else if (options::literalMatchMode()
 532                    != options::LiteralMatchMode::NONE)
 533           {
 534             pat = pat.eqNode(nm->mkConst(rpol == 1));
 535           }
 536         }
 537         else
 538         {
 539           Assert(!rpoleq.isNull());
 540           if (rpol == -1)
 541           {
 542             if (options::literalMatchMode() != options::LiteralMatchMode::NONE)
 543             {
 544               // all equivalence classes except rpoleq
 545               pat = pat.eqNode(rpoleq).negate();
 546             }
 547           }
 548           else if (rpol == 1)
 549           {
 550             if (options::literalMatchMode() == options::LiteralMatchMode::AGG)
 551             {
 552               // only equivalence class rpoleq
 553               pat = pat.eqNode(rpoleq);
 554             }
 555           }
 556         }
 557       }
 558       Trace("auto-gen-trigger-debug") << "...got : " << pat << std::endl;
 559     }
 560     else
 561     {
 562       if (TriggerTermInfo::isRelationalTrigger(pat))
 563       {
 564         // consider both polarities
 565         addPatternToPool(f, pat.negate(), num_fv, mpat);
 566       }
 567     }
 568     addPatternToPool(f, pat, num_fv, mpat);
 569   }
 570   // tinfo not used below this point
 571   d_made_multi_trigger[f] = false;
 572   if (Trace.isOn("auto-gen-trigger"))
 573   {
 574     Trace("auto-gen-trigger")
 575         << "Single trigger pool for " << f << " : " << std::endl;
 576     std::vector<Node>& spats = d_patTerms[0][f];
 577     for (size_t i = 0, psize = spats.size(); i < psize; i++)
 578     {
 579       Trace("auto-gen-trigger") << "   " << spats[i] << std::endl;
 580     }
 581     std::vector<Node>& mpats = d_patTerms[0][f];
 582     if (!mpats.empty())
 583     {
 584       Trace("auto-gen-trigger")
 585           << "Multi-trigger term pool for " << f << " : " << std::endl;
 586       for (size_t i = 0, psize = mpats.size(); i < psize; i++)
 587       {
 588         Trace("auto-gen-trigger") << "   " << mpats[i] << std::endl;
 589       }
 590     }
 591   }
 592   return true;
 593 }
 594
 595 void InstStrategyAutoGenTriggers::addPatternToPool( Node q, Node pat, unsigned num_fv, Node mpat ) {
 596   d_pat_to_mpat[pat] = mpat;
 597   unsigned num_vars = options::partialTriggers() ? d_num_trigger_vars[q] : q[0].getNumChildren();
 598   if (num_fv == num_vars)
 599   {
 600     d_patTerms[0][q].push_back( pat );
 601     d_is_single_trigger[ pat ] = true;
 602   }else{
 603     d_patTerms[1][q].push_back( pat );
 604     d_is_single_trigger[ pat ] = false;
 605   }
 606 }
 607
 608
 609 void InstStrategyAutoGenTriggers::addTrigger( inst::Trigger * tr, Node q ) {
 610   if (tr == nullptr)
 611   {
 612     return;
 613   }
 614   if (d_num_trigger_vars[q] < q[0].getNumChildren())
 615   {
 616     NodeManager* nm = NodeManager::currentNM();
 617     // partial trigger : generate implication to mark user pattern
 618     Node pat =
 619         d_quantEngine->getTermUtil()->substituteInstConstantsToBoundVariables(
 620             tr->getInstPattern(), q);
 621     Node ipl = nm->mkNode(INST_PATTERN_LIST, pat);
 622     Node qq = nm->mkNode(FORALL,
 623                          d_vc_partition[1][q],
 624                          nm->mkNode(FORALL, d_vc_partition[0][q], q[1]),
 625                          ipl);
 626     Trace("auto-gen-trigger-partial")
 627         << "Make partially specified user pattern: " << std::endl;
 628     Trace("auto-gen-trigger-partial") << "  " << qq << std::endl;
 629     Node lem = nm->mkNode(OR, q.negate(), qq);
 630     d_quantEngine->addLemma(lem);
 631     return;
 632   }
 633   unsigned tindex;
 634   if (tr->isMultiTrigger())
 635   {
 636     // disable all other multi triggers
 637     std::map<Trigger*, bool>& agt = d_auto_gen_trigger[1][q];
 638     for (std::map<Trigger*, bool>::iterator it = agt.begin(); it != agt.end();
 639          ++it)
 640     {
 641       agt[it->first] = false;
 642     }
 643     tindex = 1;
 644   }
 645   else
 646   {
 647     tindex = 0;
 648   }
 649   // making it during an instantiation round, so must reset
 650   std::map<Trigger*, bool>& agt = d_auto_gen_trigger[tindex][q];
 651   if (agt.find(tr) == agt.end())
 652   {
 653     tr->resetInstantiationRound();
 654     tr->reset(Node::null());
 655   }
 656   agt[tr] = true;
 657 }
 658
 659 bool InstStrategyAutoGenTriggers::hasUserPatterns( Node q ) {
 660   if (q.getNumChildren() != 3)
 661   {
 662     return false;
 663   }
 664   std::map<Node, bool>::iterator it = d_hasUserPatterns.find(q);
 665   if (it != d_hasUserPatterns.end())
 666   {
 667     return it->second;
 668   }
 669   bool hasPat = false;
 670   for (const Node& ip : q[2])
 671   {
 672     if (ip.getKind() == INST_PATTERN)
 673     {
 674       hasPat = true;
 675       break;
 676     }
 677   }
 678   d_hasUserPatterns[q] = hasPat;
 679   return hasPat;
 680 }
 681
 682 void InstStrategyAutoGenTriggers::addUserNoPattern( Node q, Node pat ) {
 683   Assert(pat.getKind() == INST_NO_PATTERN && pat.getNumChildren() == 1);
 684   std::vector<Node>& ung = d_user_no_gen[q];
 685   if (std::find(ung.begin(), ung.end(), pat[0]) == ung.end())
 686   {
 687     Trace("user-pat") << "Add user no-pattern: " << pat[0] << " for " << q << std::endl;
 688     ung.push_back(pat[0]);
 689   }
 690 }
 691
 692 } /* CVC4::theory::quantifiers namespace */
 693 } /* CVC4::theory namespace */
 694 } /* CVC4 namespace */