src/theory/quantifiers/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, Tim King
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2016 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/inst_strategy_e_matching.h"
  16 #include "theory/quantifiers/inst_match_generator.h"
  17 #include "theory/quantifiers/relevant_domain.h"
  18 #include "theory/quantifiers/term_database.h"
  19 #include "theory/theory_engine.h"
  20
  21 using namespace std;
  22 using namespace CVC4;
  23 using namespace CVC4::kind;
  24 using namespace CVC4::context;
  25 using namespace CVC4::theory;
  26 using namespace CVC4::theory::inst;
  27 using namespace CVC4::theory::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   QuantifiersEngine* d_qe;
  37   bool operator() (Node i, Node j) {
  38     int nqfsi = d_qe->getQuantifierRelevance()->getNumQuantifiersForSymbol( i.getOperator() );
  39     int nqfsj = d_qe->getQuantifierRelevance()->getNumQuantifiersForSymbol( j.getOperator() );
  40     if( nqfsi<nqfsj ){
  41       return true;
  42     }else if( nqfsi>nqfsj ){
  43       return false;
  44     }else{
  45       return false;
  46     }
  47   }
  48 };
  49
  50 struct sortTriggers {
  51   bool operator() (Node i, Node j) {
  52     int wi = Trigger::getTriggerWeight( i );
  53     int wj = Trigger::getTriggerWeight( j );
  54     if( wi==wj ){
  55       return i<j;
  56     }else{
  57       return wi<wj;
  58     }
  59   }
  60 };
  61
  62 void InstStrategyUserPatterns::processResetInstantiationRound( Theory::Effort effort ){
  63   Trace("inst-alg-debug") << "reset user triggers" << std::endl;
  64   //reset triggers
  65   for( std::map< Node, std::vector< Trigger* > >::iterator it = d_user_gen.begin(); it != d_user_gen.end(); ++it ){
  66     for( unsigned i=0; i<it->second.size(); i++ ){
  67       it->second[i]->resetInstantiationRound();
  68       it->second[i]->reset( Node::null() );
  69     }
  70   }
  71   Trace("inst-alg-debug") << "done reset user triggers" << std::endl;
  72 }
  73
  74 int InstStrategyUserPatterns::process( Node f, Theory::Effort effort, int e ){
  75   if( e==0 ){
  76     return STATUS_UNFINISHED;
  77   }else{
  78     int peffort = d_quantEngine->getInstUserPatMode()==USER_PAT_MODE_RESORT ? 2 : 1;
  79     if( e<peffort ){
  80       return STATUS_UNFINISHED;
  81     }else if( e==peffort ){
  82       d_counter[f]++;
  83
  84       Trace("inst-alg") << "-> User-provided instantiate " << f << "..." << std::endl;
  85       if( d_quantEngine->getInstUserPatMode()==USER_PAT_MODE_RESORT  ){
  86         int matchOption = 0;
  87         for( unsigned i=0; i<d_user_gen_wait[f].size(); i++ ){
  88           Trigger * t = Trigger::mkTrigger( d_quantEngine, f, d_user_gen_wait[f][i], matchOption, true, Trigger::TR_RETURN_NULL );
  89           if( t ){
  90             d_user_gen[f].push_back( t );
  91           }
  92         }
  93         d_user_gen_wait[f].clear();
  94       }
  95
  96       for( unsigned i=0; i<d_user_gen[f].size(); i++ ){
  97         bool processTrigger = true;
  98         if( processTrigger ){
  99           Trace("process-trigger") << "  Process (user) ";
 100           d_user_gen[f][i]->debugPrint("process-trigger");
 101           Trace("process-trigger") << "..." << std::endl;
 102           InstMatch baseMatch( f );
 103           int numInst = d_user_gen[f][i]->addInstantiations( baseMatch );
 104           Trace("process-trigger") << "  Done, numInst = " << numInst << "." << std::endl;
 105           d_quantEngine->d_statistics.d_instantiations_user_patterns += numInst;
 106           if( d_user_gen[f][i]->isMultiTrigger() ){
 107             d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
 108           }
 109           if( d_quantEngine->inConflict() ){
 110             break;
 111           }
 112         }
 113       }
 114     }
 115   }
 116   return STATUS_UNKNOWN;
 117 }
 118
 119 void InstStrategyUserPatterns::addUserPattern( Node q, Node pat ){
 120   Assert( pat.getKind()==INST_PATTERN );
 121   //add to generators
 122   bool usable = true;
 123   std::vector< Node > nodes;
 124   for( unsigned i=0; i<pat.getNumChildren(); i++ ){
 125     Node pat_use = Trigger::getIsUsableTrigger( pat[i], q );
 126     if( pat_use.isNull() ){
 127       Trace("trigger-warn") << "User-provided trigger is not usable : " << pat << " because of " << pat[i] << std::endl;
 128       usable = false;
 129       break;
 130     }else{
 131       nodes.push_back( pat_use );
 132     }
 133   }
 134   if( usable ){
 135     Trace("user-pat") << "Add user pattern: " << pat << " for " << q << std::endl;
 136     //check match option
 137     int matchOption = 0;
 138     if( d_quantEngine->getInstUserPatMode()==USER_PAT_MODE_RESORT ){
 139       d_user_gen_wait[q].push_back( nodes );
 140     }else{
 141       Trigger * t = Trigger::mkTrigger( d_quantEngine, q, nodes, matchOption, true, Trigger::TR_MAKE_NEW );
 142       if( t ){
 143         d_user_gen[q].push_back( t );
 144       }else{
 145         Trace("trigger-warn") << "Failed to construct trigger : " << pat << " due to variable mismatch" << std::endl;
 146       }
 147     }
 148   }
 149 }
 150
 151 InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers( QuantifiersEngine* qe ) : InstStrategy( qe ){
 152   //how to select trigger terms
 153   if( options::triggerSelMode()==quantifiers::TRIGGER_SEL_DEFAULT ){
 154     d_tr_strategy = quantifiers::TRIGGER_SEL_MIN;
 155   }else{
 156     d_tr_strategy = options::triggerSelMode();
 157   }
 158   //whether to select new triggers during the search
 159   if( options::incrementTriggers() ){
 160     d_regenerate_frequency = 3;
 161     d_regenerate = true;
 162   }else{
 163     d_regenerate = false;
 164   }
 165 }
 166
 167 void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort effort ){
 168   Trace("inst-alg-debug") << "reset auto-gen triggers" << std::endl;
 169   //reset triggers
 170   for( unsigned r=0; r<2; r++ ){
 171     for( std::map< Node, std::map< Trigger*, bool > >::iterator it = d_auto_gen_trigger[r].begin(); it != d_auto_gen_trigger[r].end(); ++it ){
 172       for( std::map< Trigger*, bool >::iterator itt = it->second.begin(); itt != it->second.end(); ++itt ){
 173         itt->first->resetInstantiationRound();
 174         itt->first->reset( Node::null() );
 175       }
 176     }
 177   }
 178   d_processed_trigger.clear();
 179   Trace("inst-alg-debug") << "done reset auto-gen triggers" << std::endl;
 180 }
 181
 182 int InstStrategyAutoGenTriggers::process( Node f, Theory::Effort effort, int e ){
 183   UserPatMode upMode = d_quantEngine->getInstUserPatMode();
 184   if( hasUserPatterns( f ) && upMode==USER_PAT_MODE_TRUST ){
 185     return STATUS_UNKNOWN;
 186   }else{
 187     int peffort = ( hasUserPatterns( f ) && upMode!=USER_PAT_MODE_IGNORE && upMode!=USER_PAT_MODE_RESORT ) ? 2 : 1;
 188     if( e<peffort ){
 189       return STATUS_UNFINISHED;
 190     }else{
 191       Trace("inst-alg") << "-> Auto-gen instantiate " << f << "..." << std::endl;
 192       bool gen = false;
 193       if( e==peffort ){
 194         if( d_counter.find( f )==d_counter.end() ){
 195           d_counter[f] = 0;
 196           gen = true;
 197         }else{
 198           d_counter[f]++;
 199           gen = d_regenerate && d_counter[f]%d_regenerate_frequency==0;
 200         }
 201       }else{
 202         gen = true;
 203       }
 204       if( gen ){
 205         generateTriggers( f );
 206         if( d_counter[f]==0 && d_auto_gen_trigger[0][f].empty() && d_auto_gen_trigger[1][f].empty() && f.getNumChildren()==2 ){
 207           Trace("trigger-warn") << "Could not find trigger for " << f << std::endl;
 208         }
 209       }
 210
 211       //if( e==4 ){
 212       //  d_processed_trigger.clear();
 213       //  d_quantEngine->getEqualityQuery()->setLiberal( true );
 214       //}
 215       bool hasInst = false;
 216       for( unsigned r=0; r<2; r++ ){
 217         for( std::map< Trigger*, bool >::iterator itt = d_auto_gen_trigger[r][f].begin(); itt != d_auto_gen_trigger[r][f].end(); ++itt ){
 218           Trigger* tr = itt->first;
 219           if( tr ){
 220             bool processTrigger = itt->second;
 221             if( processTrigger && d_processed_trigger[f].find( tr )==d_processed_trigger[f].end() ){
 222               d_processed_trigger[f][tr] = true;
 223               Trace("process-trigger") << "  Process ";
 224               tr->debugPrint("process-trigger");
 225               Trace("process-trigger") << "..." << std::endl;
 226               InstMatch baseMatch( f );
 227               int numInst = tr->addInstantiations( baseMatch );
 228               hasInst = numInst>0 || hasInst;
 229               Trace("process-trigger") << "  Done, numInst = " << numInst << "." << std::endl;
 230               d_quantEngine->d_statistics.d_instantiations_auto_gen += numInst;
 231               if( r==1 ){
 232                 d_quantEngine->d_statistics.d_multi_trigger_instantiations += numInst;
 233               }
 234               if( d_quantEngine->inConflict() ){
 235                 break;
 236               }
 237             }
 238           }
 239         }
 240         if( d_quantEngine->inConflict() || ( hasInst && options::multiTriggerPriority() ) ){
 241           break;
 242         }
 243       }
 244       //if( e==4 ){
 245       //  d_quantEngine->getEqualityQuery()->setLiberal( false );
 246       //}
 247       return STATUS_UNKNOWN;
 248     }
 249   }
 250 }
 251
 252 void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
 253   Trace("auto-gen-trigger-debug") << "Generate triggers for " << f << ", #var=" << f[0].getNumChildren() << "..." << std::endl;
 254   if( d_patTerms[0].find( f )==d_patTerms[0].end() ){
 255     //determine all possible pattern terms based on trigger term selection strategy d_tr_strategy
 256     d_patTerms[0][f].clear();
 257     d_patTerms[1][f].clear();
 258     bool ntrivTriggers = options::relationalTriggers();
 259     std::vector< Node > patTermsF;
 260     std::map< Node, inst::TriggerTermInfo > tinfo;
 261     //well-defined function: can assume LHS is only trigger
 262     if( options::quantFunWellDefined() ){
 263       Node hd = TermDb::getFunDefHead( f );
 264       if( !hd.isNull() ){
 265         hd = d_quantEngine->getTermDatabase()->getInstConstantNode( hd, f );
 266         patTermsF.push_back( hd );
 267         tinfo[hd].init( f, hd );
 268       }
 269     }
 270     //otherwise, use algorithm for collecting pattern terms
 271     if( patTermsF.empty() ){
 272       Node bd = d_quantEngine->getTermDatabase()->getInstConstantBody( f );
 273       Trigger::collectPatTerms( f, bd, patTermsF, d_tr_strategy, d_user_no_gen[f], tinfo, true );
 274       if( ntrivTriggers ){
 275         sortTriggers st;
 276         std::sort( patTermsF.begin(), patTermsF.end(), st );
 277       }
 278       if( Trace.isOn("auto-gen-trigger-debug") ){
 279         Trace("auto-gen-trigger-debug") << "Collected pat terms for " << bd << ", no-patterns : " << d_user_no_gen[f].size() << std::endl;
 280         for( unsigned i=0; i<patTermsF.size(); i++ ){
 281           Assert( tinfo.find( patTermsF[i] )!=tinfo.end() );
 282           Trace("auto-gen-trigger-debug") << "   " << patTermsF[i];
 283           Trace("auto-gen-trigger-debug") << " info[" << tinfo[patTermsF[i]].d_reqPol << ", " << tinfo[patTermsF[i]].d_reqPolEq << ", " << tinfo[patTermsF[i]].d_fv.size() << "]" << std::endl;
 284         }
 285         Trace("auto-gen-trigger-debug") << std::endl;
 286       }
 287     }
 288     //sort into single/multi triggers, calculate which terms should not be considered
 289     std::map< Node, bool > vcMap;
 290     std::map< Node, bool > rmPatTermsF;
 291     int last_weight = -1;
 292     for( unsigned i=0; i<patTermsF.size(); i++ ){
 293       Assert( patTermsF[i].getKind()!=NOT );
 294       bool newVar = false;
 295       for( unsigned j=0; j<tinfo[ patTermsF[i] ].d_fv.size(); j++ ){
 296         if( vcMap.find( tinfo[ patTermsF[i] ].d_fv[j] )==vcMap.end() ){
 297           vcMap[tinfo[ patTermsF[i] ].d_fv[j]] = true;
 298           newVar = true;
 299         }
 300       }
 301       int curr_w = Trigger::getTriggerWeight( patTermsF[i] );
 302       if( ntrivTriggers && !newVar && last_weight!=-1 && curr_w>last_weight ){
 303         Trace("auto-gen-trigger-debug") << "...exclude expendible non-trivial trigger : " << patTermsF[i] << std::endl;
 304         rmPatTermsF[patTermsF[i]] = true;
 305       }else{
 306         last_weight = curr_w;
 307       }
 308     }
 309     for( unsigned i=0; i<patTermsF.size(); i++ ){
 310       Node pat = patTermsF[i];
 311       if( rmPatTermsF.find( pat )==rmPatTermsF.end() ){
 312         Trace("auto-gen-trigger-debug") << "...processing pattern " << pat << std::endl;
 313         //process the pattern: if it has a required polarity, consider it
 314         Assert( tinfo.find( pat )!=tinfo.end() );
 315         int rpol = tinfo[pat].d_reqPol;
 316         Node rpoleq = tinfo[pat].d_reqPolEq;
 317         unsigned num_fv = tinfo[pat].d_fv.size();
 318         Trace("auto-gen-trigger-debug") << "...required polarity for " << pat << " is " << rpol << ", eq=" << rpoleq << std::endl;
 319         if( rpol!=0 ){
 320           if( Trigger::isRelationalTrigger( pat ) ){
 321             pat = rpol==-1 ? pat.negate() : pat;
 322           }else{
 323             Assert( Trigger::isAtomicTrigger( pat ) );
 324             if( pat.getType().isBoolean() && rpoleq.isNull() ){
 325               pat = NodeManager::currentNM()->mkNode( IFF, pat, NodeManager::currentNM()->mkConst( rpol==-1 ) ).negate();
 326             }else{
 327               Assert( !rpoleq.isNull() );
 328               if( rpol==-1 ){
 329                 //all equivalence classes except rpoleq
 330                 pat = NodeManager::currentNM()->mkNode( EQUAL, pat, rpoleq ).negate();
 331               }else if( rpol==1 ){
 332                 //all equivalence classes that are not disequal to rpoleq TODO
 333               }
 334             }
 335           }
 336           Trace("auto-gen-trigger-debug") << "...got : " << pat << std::endl;
 337         }else{
 338           if( Trigger::isRelationalTrigger( pat ) ){
 339             //consider both polarities
 340             addPatternToPool( f, pat.negate(), num_fv );
 341           }
 342         }
 343         addPatternToPool( f, pat, num_fv );
 344       }
 345     }
 346     //tinfo not used below this point
 347     d_made_multi_trigger[f] = false;
 348     Trace("auto-gen-trigger") << "Single trigger pool for " << f << " : " << std::endl;
 349     for( unsigned i=0; i<d_patTerms[0][f].size(); i++ ){
 350       Trace("auto-gen-trigger") << "   " << d_patTerms[0][f][i] << std::endl;
 351     }
 352     if( !d_patTerms[1][f].empty() ){
 353       Trace("auto-gen-trigger") << "Multi-trigger term pool for " << f << " : " << std::endl;
 354       for( unsigned i=0; i<d_patTerms[1][f].size(); i++ ){
 355         Trace("auto-gen-trigger") << "   " << d_patTerms[1][f][i] << std::endl;
 356       }
 357     }
 358   }
 359
 360   unsigned rmin = d_patTerms[0][f].empty() ? 1 : 0;
 361   unsigned rmax = options::multiTriggerWhenSingle() ? 1 : rmin;
 362   for( unsigned r=rmin; r<=rmax; r++ ){
 363     std::vector< Node > patTerms;
 364     for( int i=0; i<(int)d_patTerms[r][f].size(); i++ ){
 365       if( r==1 || d_single_trigger_gen.find( d_patTerms[r][f][i] )==d_single_trigger_gen.end() ){
 366         patTerms.push_back( d_patTerms[r][f][i] );
 367       }
 368     }
 369     if( !patTerms.empty() ){
 370       Trace("auto-gen-trigger") << "Generate trigger for " << f << std::endl;
 371       //sort terms based on relevance
 372       if( options::relevantTriggers() ){
 373         sortQuantifiersForSymbol sqfs;
 374         sqfs.d_qe = d_quantEngine;
 375         //sort based on # occurrences (this will cause Trigger to select rarer symbols)
 376         std::sort( patTerms.begin(), patTerms.end(), sqfs );
 377         Debug("relevant-trigger") << "Terms based on relevance: " << std::endl;
 378         for( unsigned i=0; i<patTerms.size(); i++ ){
 379           Debug("relevant-trigger") << "   " << patTerms[i] << " (";
 380           Debug("relevant-trigger") << d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[i].getOperator() ) << ")" << std::endl;
 381         }
 382       }
 383       //now, generate the trigger...
 384       int matchOption = 0;
 385       Trigger* tr = NULL;
 386       if( d_is_single_trigger[ patTerms[0] ] ){
 387         tr = Trigger::mkTrigger( d_quantEngine, f, patTerms[0], matchOption, false, Trigger::TR_RETURN_NULL );
 388         d_single_trigger_gen[ patTerms[0] ] = true;
 389       }else{
 390         //only generate multi trigger if option set, or if no single triggers exist
 391         if( !d_patTerms[0][f].empty() ){
 392           if( options::multiTriggerWhenSingle() ){
 393             Trace("multi-trigger-debug") << "Resort to choosing multi-triggers..." << std::endl;
 394           }else{
 395             return;
 396           }
 397         }
 398         //if we are re-generating triggers, shuffle based on some method
 399         if( d_made_multi_trigger[f] ){
 400           std::random_shuffle( patTerms.begin(), patTerms.end() ); //shuffle randomly
 401         }else{
 402           d_made_multi_trigger[f] = true;
 403         }
 404         //will possibly want to get an old trigger
 405         tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, matchOption, false, Trigger::TR_GET_OLD );
 406       }
 407       if( tr ){
 408         unsigned tindex;
 409         if( tr->isMultiTrigger() ){
 410           //disable all other multi triggers
 411           for( std::map< Trigger*, bool >::iterator it = d_auto_gen_trigger[1][f].begin(); it != d_auto_gen_trigger[1][f].end(); ++it ){
 412             d_auto_gen_trigger[1][f][ it->first ] = false;
 413           }
 414           tindex = 1;
 415         }else{
 416           tindex = 0;
 417         }
 418         //making it during an instantiation round, so must reset
 419         if( d_auto_gen_trigger[tindex][f].find( tr )==d_auto_gen_trigger[tindex][f].end() ){
 420           tr->resetInstantiationRound();
 421           tr->reset( Node::null() );
 422         }
 423         d_auto_gen_trigger[tindex][f][tr] = true;
 424         //if we are generating additional triggers...
 425         if( tindex==0 ){
 426           int index = 0;
 427           if( index<(int)patTerms.size() ){
 428             //Notice() << "check add additional" << std::endl;
 429             //check if similar patterns exist, and if so, add them additionally
 430             int nqfs_curr = 0;
 431             if( options::relevantTriggers() ){
 432               nqfs_curr = d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[0].getOperator() );
 433             }
 434             index++;
 435             bool success = true;
 436             while( success && index<(int)patTerms.size() && d_is_single_trigger[ patTerms[index] ] ){
 437               success = false;
 438               if( !options::relevantTriggers() ||
 439                   d_quantEngine->getQuantifierRelevance()->getNumQuantifiersForSymbol( patTerms[index].getOperator() )<=nqfs_curr ){
 440                 d_single_trigger_gen[ patTerms[index] ] = true;
 441                 Trigger* tr2 = Trigger::mkTrigger( d_quantEngine, f, patTerms[index], matchOption, false, Trigger::TR_RETURN_NULL );
 442                 if( tr2 ){
 443                   //Notice() << "Add additional trigger " << patTerms[index] << std::endl;
 444                   tr2->resetInstantiationRound();
 445                   tr2->reset( Node::null() );
 446                   d_auto_gen_trigger[0][f][tr2] = true;
 447                 }
 448                 success = true;
 449               }
 450               index++;
 451             }
 452             //Notice() << "done check add additional" << std::endl;
 453           }
 454         }
 455       }
 456     }
 457   }
 458 }
 459
 460 void InstStrategyAutoGenTriggers::addPatternToPool( Node q, Node pat, unsigned num_fv ) {
 461   if( num_fv==q[0].getNumChildren() && ( options::pureThTriggers() || !Trigger::isPureTheoryTrigger( pat ) ) ){
 462     d_patTerms[0][q].push_back( pat );
 463     d_is_single_trigger[ pat ] = true;
 464   }else{
 465     d_patTerms[1][q].push_back( pat );
 466     d_is_single_trigger[ pat ] = false;
 467   }
 468 }
 469
 470 bool InstStrategyAutoGenTriggers::hasUserPatterns( Node q ) {
 471   if( q.getNumChildren()==3 ){
 472     std::map< Node, bool >::iterator it = d_hasUserPatterns.find( q );
 473     if( it==d_hasUserPatterns.end() ){
 474       bool hasPat = false;
 475       for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
 476         if( q[2][i].getKind()==INST_PATTERN ){
 477           hasPat = true;
 478           break;
 479         }
 480       }
 481       d_hasUserPatterns[q] = hasPat;
 482       return hasPat;
 483     }else{
 484       return it->second;
 485     }
 486   }else{
 487     return false;
 488   }
 489 }
 490
 491 void InstStrategyAutoGenTriggers::addUserNoPattern( Node q, Node pat ) {
 492   Assert( pat.getKind()==INST_NO_PATTERN && pat.getNumChildren()==1 );
 493   if( std::find( d_user_no_gen[q].begin(), d_user_no_gen[q].end(), pat[0] )==d_user_no_gen[q].end() ){
 494     Trace("user-pat") << "Add user no-pattern: " << pat[0] << " for " << q << std::endl;
 495     d_user_no_gen[q].push_back( pat[0] );
 496   }
 497 }
 498
 499 /*  TODO?
 500 bool InstStrategyLocalTheoryExt::isLocalTheoryExt( Node f ) {
 501   std::map< Node, bool >::iterator itq = d_quant.find( f );
 502   if( itq==d_quant.end() ){
 503     //generate triggers
 504     Node bd = d_quantEngine->getTermDatabase()->getInstConstantBody( f );
 505     std::vector< Node > vars;
 506     std::vector< Node > patTerms;
 507     bool ret = Trigger::isLocalTheoryExt( bd, vars, patTerms );
 508     if( ret ){
 509       d_quant[f] = ret;
 510       //add all variables to trigger that don't already occur
 511       for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
 512         Node x = d_quantEngine->getTermDatabase()->getInstantiationConstant( f, i );
 513         if( std::find( vars.begin(), vars.end(), x )==vars.end() ){
 514           patTerms.push_back( x );
 515         }
 516       }
 517       Trace("local-t-ext") << "Local theory extensions trigger for " << f << " : " << std::endl;
 518       for( unsigned i=0; i<patTerms.size(); i++ ){
 519         Trace("local-t-ext") << "  " << patTerms[i] << std::endl;
 520       }
 521       Trace("local-t-ext") << std::endl;
 522       int matchOption = 0;
 523       Trigger * tr = Trigger::mkTrigger( d_quantEngine, f, patTerms, matchOption, true, Trigger::TR_GET_OLD );
 524       d_lte_trigger[f] = tr;
 525     }else{
 526       Trace("local-t-ext") << "No local theory extensions trigger for " << f << "." << std::endl;
 527       Trace("local-t-ext-warn") << "WARNING: not local theory extensions : " << f << std::endl;
 528     }
 529     d_quant[f] = ret;
 530     return ret;
 531   }else{
 532     return itq->second;
 533   }
 534 }
 535 */
 536 FullSaturation::FullSaturation( QuantifiersEngine* qe ) : QuantifiersModule( qe ){
 537
 538 }
 539
 540 bool FullSaturation::needsCheck( Theory::Effort e ){
 541   if( options::fullSaturateInst() ){
 542     if( d_quantEngine->getInstWhenNeedsCheck( e ) ){
 543       return true;
 544     }
 545   }
 546   if( options::fullSaturateQuant() ){
 547     if( e>=Theory::EFFORT_LAST_CALL ){
 548       return true;
 549     }
 550   }
 551   return false;
 552 }
 553
 554 void FullSaturation::reset_round( Theory::Effort e ) {
 555
 556 }
 557
 558 void FullSaturation::check( Theory::Effort e, unsigned quant_e ) {
 559   bool doCheck = false;
 560   bool fullEffort = false;
 561   if( options::fullSaturateInst() ){
 562     //we only add when interleaved with other strategies
 563     doCheck = quant_e==QuantifiersEngine::QEFFORT_STANDARD && d_quantEngine->hasAddedLemma();
 564   }
 565   if( options::fullSaturateQuant() && !doCheck ){
 566     doCheck = quant_e==QuantifiersEngine::QEFFORT_LAST_CALL;
 567     fullEffort = !d_quantEngine->hasAddedLemma();
 568   }
 569   if( doCheck ){
 570     double clSet = 0;
 571     if( Trace.isOn("fs-engine") ){
 572       clSet = double(clock())/double(CLOCKS_PER_SEC);
 573       Trace("fs-engine") << "---Full Saturation Round, effort = " << e << "---" << std::endl;
 574     }
 575     int addedLemmas = 0;
 576     for( unsigned i=0; i<d_quantEngine->getModel()->getNumAssertedQuantifiers(); i++ ){
 577       Node q = d_quantEngine->getModel()->getAssertedQuantifier( i, true );
 578       if( d_quantEngine->hasOwnership( q, this ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
 579         if( process( q, fullEffort ) ){
 580           //added lemma
 581           addedLemmas++;
 582           if( d_quantEngine->inConflict() ){
 583             break;
 584           }
 585         }
 586       }
 587     }
 588     if( Trace.isOn("fs-engine") ){
 589       Trace("fs-engine") << "Added lemmas = " << addedLemmas  << std::endl;
 590       double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
 591       Trace("fs-engine") << "Finished instantiation engine, time = " << (clSet2-clSet) << std::endl;
 592     }
 593   }
 594 }
 595
 596 bool FullSaturation::process( Node f, bool fullEffort ){
 597   //first, try from relevant domain
 598   RelevantDomain * rd = d_quantEngine->getRelevantDomain();
 599   unsigned rstart = options::fullSaturateQuantRd() ? 0 : 1;
 600   unsigned rend = fullEffort ? 1 : rstart;
 601   for( unsigned r=rstart; r<=rend; r++ ){
 602       /*
 603       //complete guess
 604       if( d_guessed.find( f )==d_guessed.end() ){
 605         Trace("inst-alg") << "-> Guess instantiate " << f << "..." << std::endl;
 606         d_guessed[f] = true;
 607         InstMatch m( f );
 608         if( d_quantEngine->addInstantiation( f, m ) ){
 609           ++(d_quantEngine->d_statistics.d_instantiations_guess);
 610           return true;
 611         }
 612       }
 613       */
 614     if( rd || r>0 ){
 615       if( r==0 ){
 616         Trace("inst-alg") << "-> Relevant domain instantiate " << f << "..." << std::endl;
 617       }else{
 618         Trace("inst-alg") << "-> Ground term instantiate " << f << "..." << std::endl;
 619       }
 620       rd->compute();
 621       unsigned final_max_i = 0;
 622       std::vector< unsigned > maxs;
 623       std::vector< bool > max_zero;
 624       bool has_zero = false;
 625       for(unsigned i=0; i<f[0].getNumChildren(); i++ ){
 626         unsigned ts;
 627         if( r==0 ){
 628           ts = rd->getRDomain( f, i )->d_terms.size();
 629         }else{
 630           ts = d_quantEngine->getTermDatabase()->getNumTypeGroundTerms( f[0][i].getType() );
 631         }
 632         max_zero.push_back( fullEffort && ts==0 );
 633         ts = ( fullEffort && ts==0 ) ? 1 : ts;
 634         Trace("inst-alg-rd") << "Variable " << i << " has " << ts << " in relevant domain." << std::endl;
 635         if( ts==0 ){
 636           has_zero = true;
 637           break;
 638         }else{
 639           maxs.push_back( ts );
 640           if( ts>final_max_i ){
 641             final_max_i = ts;
 642           }
 643         }
 644       }
 645       if( !has_zero ){
 646         std::vector< TypeNode > ftypes;
 647         for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
 648           ftypes.push_back( f[0][i].getType() );
 649         }
 650
 651         Trace("inst-alg-rd") << "Will do " << final_max_i << " stages of instantiation." << std::endl;
 652         unsigned max_i = 0;
 653         bool success;
 654         while( max_i<=final_max_i ){
 655           Trace("inst-alg-rd") << "Try stage " << max_i << "..." << std::endl;
 656           std::vector< unsigned > childIndex;
 657           int index = 0;
 658           do {
 659             while( index>=0 && index<(int)f[0].getNumChildren() ){
 660               if( index==(int)childIndex.size() ){
 661                 childIndex.push_back( -1 );
 662               }else{
 663                 Assert( index==(int)(childIndex.size())-1 );
 664                 unsigned nv = childIndex[index]+1;
 665                 if( options::cbqi() && r==1 && !max_zero[index] ){
 666                   //skip inst constant nodes
 667                   while( nv<maxs[index] && nv<=max_i &&
 668                           quantifiers::TermDb::hasInstConstAttr( d_quantEngine->getTermDatabase()->getTypeGroundTerm( ftypes[index], nv ) ) ){
 669                     nv++;
 670                   }
 671                 }
 672                 if( nv<maxs[index] && nv<=max_i ){
 673                   childIndex[index] = nv;
 674                   index++;
 675                 }else{
 676                   childIndex.pop_back();
 677                   index--;
 678                 }
 679               }
 680             }
 681             success = index>=0;
 682             if( success ){
 683               Trace("inst-alg-rd") << "Try instantiation { ";
 684               for( unsigned j=0; j<childIndex.size(); j++ ){
 685                 Trace("inst-alg-rd") << childIndex[j] << " ";
 686               }
 687               Trace("inst-alg-rd") << "}" << std::endl;
 688               //try instantiation
 689               std::vector< Node > terms;
 690               for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
 691                 if( max_zero[i] ){
 692                   //no terms available, will report incomplete instantiation
 693                   terms.push_back( Node::null() );
 694                   Trace("inst-alg-rd") << "  null" << std::endl;
 695                 }else if( r==0 ){
 696                   terms.push_back( rd->getRDomain( f, i )->d_terms[childIndex[i]] );
 697                   Trace("inst-alg-rd") << "  " << rd->getRDomain( f, i )->d_terms[childIndex[i]] << std::endl;
 698                 }else{
 699                   terms.push_back( d_quantEngine->getTermDatabase()->getTypeGroundTerm( ftypes[i], childIndex[i] ) );
 700                   Trace("inst-alg-rd") << "  " << d_quantEngine->getTermDatabase()->getTypeGroundTerm( ftypes[i], childIndex[i] ) << std::endl;
 701                 }
 702               }
 703               if( d_quantEngine->addInstantiation( f, terms, false ) ){
 704                 Trace("inst-alg-rd") << "Success!" << std::endl;
 705                 ++(d_quantEngine->d_statistics.d_instantiations_guess);
 706                 return true;
 707               }else{
 708                 index--;
 709               }
 710             }
 711           }while( success );
 712           max_i++;
 713         }
 714       }
 715     }
 716   }
 717   //term enumerator?
 718   return false;
 719 }
 720
 721 void FullSaturation::registerQuantifier( Node q ) {
 722
 723 }