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