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