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