src/theory/inst_match.cpp

   1 /*********************                                                        */
   2 /*! \file inst_match.cpp
   3  ** \verbatim
   4  ** Original author: ajreynol
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): none
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **
  14  ** \brief Implementation of inst match class
  15  **/
  16
  17 #include "theory/inst_match.h"
  18 #include "theory/theory_engine.h"
  19 #include "theory/quantifiers_engine.h"
  20 #include "theory/candidate_generator.h"
  21 #include "theory/uf/theory_uf_instantiator.h"
  22 #include "theory/uf/equality_engine.h"
  23 #include "theory/quantifiers/options.h"
  24 #include "theory/quantifiers/model_engine.h"
  25 #include "theory/quantifiers/term_database.h"
  26 #include "theory/quantifiers/first_order_model.h"
  27 #include "theory/quantifiers/term_database.h"
  28
  29 using namespace std;
  30 using namespace CVC4;
  31 using namespace CVC4::kind;
  32 using namespace CVC4::context;
  33 using namespace CVC4::theory;
  34 using namespace CVC4::theory::inst;
  35
  36
  37 InstMatch::InstMatch() {
  38 }
  39
  40 InstMatch::InstMatch( InstMatch* m ) {
  41   d_map = m->d_map;
  42 }
  43
  44 bool InstMatch::setMatch( EqualityQuery* q, TNode v, TNode m, bool & set ){
  45   std::map< Node, Node >::iterator vn = d_map.find( v );
  46   if( vn==d_map.end() ){
  47     set = true;
  48     this->set(v,m);
  49     Debug("matching-debug") << "Add partial " << v << "->" << m << std::endl;
  50     return true;
  51   }else{
  52     set = false;
  53     return q->areEqual( vn->second, m );
  54   }
  55 }
  56
  57 bool InstMatch::setMatch( EqualityQuery* q, TNode v, TNode m ){
  58   bool set;
  59   return setMatch(q,v,m,set);
  60 }
  61
  62 bool InstMatch::add( InstMatch& m ){
  63   for( std::map< Node, Node >::iterator it = m.d_map.begin(); it != m.d_map.end(); ++it ){
  64     if( d_map.find( it->first )==d_map.end() ){
  65       d_map[it->first] = it->second;
  66     }
  67   }
  68   return true;
  69 }
  70
  71 bool InstMatch::merge( EqualityQuery* q, InstMatch& m ){
  72   for( std::map< Node, Node >::iterator it = m.d_map.begin(); it != m.d_map.end(); ++it ){
  73     if( d_map.find( it->first )==d_map.end() ){
  74       d_map[ it->first ] = it->second;
  75     }else{
  76       if( it->second!=d_map[it->first] ){
  77         if( !q->areEqual( it->second, d_map[it->first] ) ){
  78           d_map.clear();
  79           return false;
  80         }
  81       }
  82     }
  83   }
  84   return true;
  85 }
  86
  87 void InstMatch::debugPrint( const char* c ){
  88   for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){
  89     Debug( c ) << "   " << it->first << " -> " << it->second << std::endl;
  90   }
  91   //if( !d_splits.empty() ){
  92   //  Debug( c ) << "   Conditions: ";
  93   //  for( std::map< Node, Node >::iterator it = d_splits.begin(); it !=d_splits.end(); ++it ){
  94   //    Debug( c ) << it->first << " = " << it->second << " ";
  95   //  }
  96   //  Debug( c ) << std::endl;
  97   //}
  98 }
  99
 100 void InstMatch::makeComplete( Node f, QuantifiersEngine* qe ){
 101   for( int i=0; i<(int)qe->getTermDatabase()->d_inst_constants[f].size(); i++ ){
 102     Node ic = qe->getTermDatabase()->d_inst_constants[f][i];
 103     if( d_map.find( ic )==d_map.end() ){
 104       d_map[ ic ] = qe->getTermDatabase()->getFreeVariableForInstConstant( ic );
 105     }
 106   }
 107 }
 108
 109 void InstMatch::makeInternal( QuantifiersEngine* qe ){
 110   if( options::cbqi() ){
 111     for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){
 112       if( it->second.hasAttribute(InstConstantAttribute()) ){
 113         d_map[ it->first ] = qe->getEqualityQuery()->getInternalRepresentative( it->second );
 114         if( it->second.hasAttribute(InstConstantAttribute()) ){
 115           d_map[ it->first ] = qe->getTermDatabase()->getFreeVariableForInstConstant( it->first );
 116         }
 117       }
 118     }
 119   }
 120 }
 121
 122 void InstMatch::makeRepresentative( QuantifiersEngine* qe ){
 123   for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){
 124     d_map[ it->first ] = qe->getEqualityQuery()->getInternalRepresentative( it->second );
 125     if( options::cbqi() && it->second.hasAttribute(InstConstantAttribute()) ){
 126       d_map[ it->first ] = qe->getTermDatabase()->getFreeVariableForInstConstant( it->first );
 127     }
 128   }
 129 }
 130
 131 void InstMatch::applyRewrite(){
 132   for( std::map< Node, Node >::iterator it = d_map.begin(); it != d_map.end(); ++it ){
 133     it->second = Rewriter::rewrite(it->second);
 134   }
 135 }
 136
 137 void InstMatch::computeTermVec( QuantifiersEngine* qe, const std::vector< Node >& vars, std::vector< Node >& match ){
 138   for( int i=0; i<(int)vars.size(); i++ ){
 139     std::map< Node, Node >::iterator it = d_map.find( vars[i] );
 140     if( it!=d_map.end() && !it->second.isNull() ){
 141       match.push_back( it->second );
 142     }else{
 143       match.push_back( qe->getTermDatabase()->getFreeVariableForInstConstant( vars[i] ) );
 144     }
 145   }
 146 }
 147 void InstMatch::computeTermVec( const std::vector< Node >& vars, std::vector< Node >& match ){
 148   for( int i=0; i<(int)vars.size(); i++ ){
 149     match.push_back( d_map[ vars[i] ] );
 150   }
 151 }
 152
 153
 154 /** add match m for quantifier f starting at index, take into account equalities q, return true if successful */
 155 void InstMatchTrie::addInstMatch2( QuantifiersEngine* qe, Node f, InstMatch& m, int index, ImtIndexOrder* imtio ){
 156   if( long(index)<long(f[0].getNumChildren()) && ( !imtio || long(index)<long(imtio->d_order.size()) ) ){
 157     int i_index = imtio ? imtio->d_order[index] : index;
 158     Node n = m.get( qe->getTermDatabase()->getInstantiationConstant( f, i_index ) );
 159     d_data[n].addInstMatch2( qe, f, m, index+1, imtio );
 160   }
 161 }
 162
 163 /** exists match */
 164 bool InstMatchTrie::existsInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, int index, ImtIndexOrder* imtio ){
 165   if( long(index)==long(f[0].getNumChildren()) || ( imtio && long(index)==long(imtio->d_order.size()) ) ){
 166     return true;
 167   }else{
 168     int i_index = imtio ? imtio->d_order[index] : index;
 169     Node n = m.get( qe->getTermDatabase()->getInstantiationConstant( f, i_index ) );
 170     std::map< Node, InstMatchTrie >::iterator it = d_data.find( n );
 171     if( it!=d_data.end() ){
 172       if( it->second.existsInstMatch( qe, f, m, modEq, index+1, imtio ) ){
 173         return true;
 174       }
 175     }
 176     if( modEq ){
 177       //check modulo equality if any other instantiation match exists
 178       if( qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){
 179         eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( n ),
 180                                  qe->getEqualityQuery()->getEngine() );
 181         while( !eqc.isFinished() ){
 182           Node en = (*eqc);
 183           if( en!=n ){
 184             std::map< Node, InstMatchTrie >::iterator itc = d_data.find( en );
 185             if( itc!=d_data.end() ){
 186               if( itc->second.existsInstMatch( qe, f, m, modEq, index+1, imtio ) ){
 187                 return true;
 188               }
 189             }
 190           }
 191           ++eqc;
 192         }
 193       }
 194       //for( std::map< Node, InstMatchTrie >::iterator itc = d_data.begin(); itc != d_data.end(); ++itc ){
 195       //  if( itc->first!=n && qe->getEqualityQuery()->areEqual( n, itc->first ) ){
 196       //    if( itc->second.existsInstMatch( qe, f, m, modEq, index+1 ) ){
 197       //      return true;
 198       //    }
 199       //  }
 200       //}
 201     }
 202     return false;
 203   }
 204 }
 205
 206 bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, InstMatch& m, bool modEq, ImtIndexOrder* imtio ){
 207   if( !existsInstMatch( qe, f, m, modEq, 0, imtio ) ){
 208     addInstMatch2( qe, f, m, 0, imtio );
 209     return true;
 210   }else{
 211     return false;
 212   }
 213 }
 214
 215 InstMatchGenerator::InstMatchGenerator( Node pat, QuantifiersEngine* qe, int matchPolicy ) : d_matchPolicy( matchPolicy ){
 216   initializePattern( pat, qe );
 217 }
 218
 219 InstMatchGenerator::InstMatchGenerator( std::vector< Node >& pats, QuantifiersEngine* qe, int matchPolicy ) : d_matchPolicy( matchPolicy ){
 220   if( pats.size()==1 ){
 221     initializePattern( pats[0], qe );
 222   }else{
 223     initializePatterns( pats, qe );
 224   }
 225 }
 226
 227 void InstMatchGenerator::initializePatterns( std::vector< Node >& pats, QuantifiersEngine* qe ){
 228   int childMatchPolicy = d_matchPolicy==MATCH_GEN_EFFICIENT_E_MATCH ? 0 : d_matchPolicy;
 229   for( int i=0; i<(int)pats.size(); i++ ){
 230     d_children.push_back( new InstMatchGenerator( pats[i], qe, childMatchPolicy ) );
 231   }
 232   d_pattern = Node::null();
 233   d_match_pattern = Node::null();
 234   d_cg = NULL;
 235 }
 236
 237 void InstMatchGenerator::initializePattern( Node pat, QuantifiersEngine* qe ){
 238   Debug("inst-match-gen") << "Pattern term is " << pat << std::endl;
 239   Assert( pat.hasAttribute(InstConstantAttribute()) );
 240   d_pattern = pat;
 241   d_match_pattern = pat;
 242   if( d_match_pattern.getKind()==NOT ){
 243     //we want to add the children of the NOT
 244     d_match_pattern = d_pattern[0];
 245   }
 246   if( d_match_pattern.getKind()==IFF || d_match_pattern.getKind()==EQUAL ){
 247     if( !d_match_pattern[0].hasAttribute(InstConstantAttribute()) ){
 248       Assert( d_match_pattern[1].hasAttribute(InstConstantAttribute()) );
 249       //swap sides
 250       d_pattern = NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), d_match_pattern[1], d_match_pattern[0] );
 251       d_pattern = pat.getKind()==NOT ? d_pattern.notNode() : d_pattern;
 252       if( pat.getKind()!=NOT ){   //TEMPORARY until we do better implementation of disequality matching
 253         d_match_pattern = d_match_pattern[1];
 254       }else{
 255         d_match_pattern = d_pattern[0][0];
 256       }
 257     }else if( !d_match_pattern[1].hasAttribute(InstConstantAttribute()) ){
 258       Assert( d_match_pattern[0].hasAttribute(InstConstantAttribute()) );
 259       if( pat.getKind()!=NOT ){   //TEMPORARY until we do better implementation of disequality matching
 260         d_match_pattern = d_match_pattern[0];
 261       }
 262     }
 263   }
 264   int childMatchPolicy = MATCH_GEN_DEFAULT;
 265   for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){
 266     if( d_match_pattern[i].hasAttribute(InstConstantAttribute()) ){
 267       if( d_match_pattern[i].getKind()!=INST_CONSTANT ){
 268         d_children.push_back( new InstMatchGenerator( d_match_pattern[i], qe, childMatchPolicy ) );
 269         d_children_index.push_back( i );
 270       }
 271     }
 272   }
 273
 274   Debug("inst-match-gen") << "Pattern is " << d_pattern << ", match pattern is " << d_match_pattern << std::endl;
 275
 276   //create candidate generator
 277   if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==IFF ){
 278     Assert( d_matchPolicy==MATCH_GEN_DEFAULT );
 279     //we will be producing candidates via literal matching heuristics
 280     if( d_pattern.getKind()!=NOT ){
 281       //candidates will be all equalities
 282       d_cg = new inst::CandidateGeneratorQELitEq( qe, d_match_pattern );
 283     }else{
 284       //candidates will be all disequalities
 285       d_cg = new inst::CandidateGeneratorQELitDeq( qe, d_match_pattern );
 286     }
 287   }else if( d_pattern.getKind()==EQUAL || d_pattern.getKind()==IFF || d_pattern.getKind()==NOT ){
 288     Assert( d_matchPolicy==MATCH_GEN_DEFAULT );
 289     if( d_pattern.getKind()==NOT ){
 290       Unimplemented("Disequal generator unimplemented");
 291     }else{
 292       Assert( Trigger::isAtomicTrigger( d_match_pattern ) );
 293       //we are matching only in a particular equivalence class
 294       d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern.getOperator() );
 295       //store the equivalence class that we will call d_cg->reset( ... ) on
 296       d_eq_class = d_pattern[1];
 297     }
 298   }else if( Trigger::isAtomicTrigger( d_match_pattern ) ){
 299     //if( d_matchPolicy==MATCH_GEN_EFFICIENT_E_MATCH ){
 300       //Warning() << "Currently efficient e matching is not taken into account for quantifiers: " << d_pattern << std::endl;
 301     //}
 302     //we will be scanning lists trying to find d_match_pattern.getOperator()
 303     d_cg = new inst::CandidateGeneratorQE( qe, d_match_pattern.getOperator() );
 304   }else{
 305     d_cg = new CandidateGeneratorQueue;
 306     if( !Trigger::getPatternArithmetic( d_match_pattern.getAttribute(InstConstantAttribute()), d_match_pattern, d_arith_coeffs ) ){
 307       Debug("inst-match-gen") << "(?) Unknown matching pattern is " << d_match_pattern << std::endl;
 308       Warning() << "(?) Unknown matching pattern is " << d_match_pattern << std::endl;
 309       d_matchPolicy = MATCH_GEN_INTERNAL_ERROR;
 310     }else{
 311       Debug("matching-arith") << "Generated arithmetic pattern for " << d_match_pattern << ": " << std::endl;
 312       for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){
 313         Debug("matching-arith") << "   " << it->first << " -> " << it->second << std::endl;
 314       }
 315       //we will treat this as match gen internal arithmetic
 316       d_matchPolicy = MATCH_GEN_INTERNAL_ARITHMETIC;
 317     }
 318   }
 319 }
 320
 321 /** get match (not modulo equality) */
 322 bool InstMatchGenerator::getMatch( Node t, InstMatch& m, QuantifiersEngine* qe ){
 323   Debug("matching") << "Matching " << t << " against pattern " << d_match_pattern << " ("
 324                     << m.size() << ")" << ", " << d_children.size() << std::endl;
 325   Assert( !d_match_pattern.isNull() );
 326   if( qe->d_optMatchIgnoreModelBasis && t.getAttribute(ModelBasisAttribute()) ){
 327     return true;
 328   }else if( d_matchPolicy==MATCH_GEN_INTERNAL_ARITHMETIC ){
 329     return getMatchArithmetic( t, m, qe );
 330   }else if( d_matchPolicy==MATCH_GEN_INTERNAL_ERROR ){
 331     return false;
 332   }else{
 333     EqualityQuery* q = qe->getEqualityQuery();
 334     //add m to partial match vector
 335     std::vector< InstMatch > partial;
 336     partial.push_back( InstMatch( &m ) );
 337     //if t is null
 338     Assert( !t.isNull() );
 339     Assert( !t.hasAttribute(InstConstantAttribute()) );
 340     Assert( t.getKind()==d_match_pattern.getKind() );
 341     Assert( !Trigger::isAtomicTrigger( d_match_pattern ) || t.getOperator()==d_match_pattern.getOperator() );
 342     //first, check if ground arguments are not equal, or a match is in conflict
 343     for( int i=0; i<(int)d_match_pattern.getNumChildren(); i++ ){
 344       if( d_match_pattern[i].hasAttribute(InstConstantAttribute()) ){
 345         if( d_match_pattern[i].getKind()==INST_CONSTANT ){
 346           if( !partial[0].setMatch( q, d_match_pattern[i], t[i] ) ){
 347             //match is in conflict
 348             Debug("matching-debug") << "Match in conflict " << t[i] << " and "
 349                                     << d_match_pattern[i] << " because "
 350                                     << partial[0].get(d_match_pattern[i])
 351                                     << std::endl;
 352             Debug("matching-fail") << "Match fail: " << partial[0].get(d_match_pattern[i]) << " and " << t[i] << std::endl;
 353             return false;
 354           }
 355         }
 356       }else{
 357         if( !q->areEqual( d_match_pattern[i], t[i] ) ){
 358           Debug("matching-fail") << "Match fail arg: " << d_match_pattern[i] << " and " << t[i] << std::endl;
 359           //ground arguments are not equal
 360           return false;
 361         }
 362       }
 363     }
 364     //now, fit children into match
 365     //we will be requesting candidates for matching terms for each child
 366     std::vector< Node > reps;
 367     for( int i=0; i<(int)d_children.size(); i++ ){
 368       Node rep = q->getRepresentative( t[ d_children_index[i] ] );
 369       reps.push_back( rep );
 370       d_children[i]->d_cg->reset( rep );
 371     }
 372
 373     //combine child matches
 374     int index = 0;
 375     while( index>=0 && index<(int)d_children.size() ){
 376       partial.push_back( InstMatch( &partial[index] ) );
 377       if( d_children[index]->getNextMatch2( partial[index+1], qe ) ){
 378         index++;
 379       }else{
 380         d_children[index]->d_cg->reset( reps[index] );
 381         partial.pop_back();
 382         if( !partial.empty() ){
 383           partial.pop_back();
 384         }
 385         index--;
 386       }
 387     }
 388     if( index>=0 ){
 389       m = partial.back();
 390       return true;
 391     }else{
 392       return false;
 393     }
 394   }
 395 }
 396
 397 bool InstMatchGenerator::getNextMatch2( InstMatch& m, QuantifiersEngine* qe, bool saveMatched ){
 398   bool success = false;
 399   Node t;
 400   do{
 401     //get the next candidate term t
 402     t = d_cg->getNextCandidate();
 403     //if t not null, try to fit it into match m
 404     if( !t.isNull() && t.getType()==d_match_pattern.getType() ){
 405       success = getMatch( t, m, qe );
 406     }
 407   }while( !success && !t.isNull() );
 408   if (saveMatched) m.d_matched = t;
 409   return success;
 410 }
 411
 412 bool InstMatchGenerator::getMatchArithmetic( Node t, InstMatch& m, QuantifiersEngine* qe ){
 413   Debug("matching-arith") << "Matching " << t << " " << d_match_pattern << std::endl;
 414   if( !d_arith_coeffs.empty() ){
 415     NodeBuilder<> tb(kind::PLUS);
 416     Node ic = Node::null();
 417     for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){
 418       Debug("matching-arith") << it->first << " -> " << it->second << std::endl;
 419       if( !it->first.isNull() ){
 420         if( m.find( it->first )==m.end() ){
 421           //see if we can choose this to set
 422           if( ic.isNull() && ( it->second.isNull() || !it->first.getType().isInteger() ) ){
 423             ic = it->first;
 424           }
 425         }else{
 426           Debug("matching-arith") << "already set " << m.get( it->first ) << std::endl;
 427           Node tm = m.get( it->first );
 428           if( !it->second.isNull() ){
 429             tm = NodeManager::currentNM()->mkNode( MULT, it->second, tm );
 430           }
 431           tb << tm;
 432         }
 433       }else{
 434         tb << it->second;
 435       }
 436     }
 437     if( !ic.isNull() ){
 438       Node tm;
 439       if( tb.getNumChildren()==0 ){
 440         tm = t;
 441       }else{
 442         tm = tb.getNumChildren()==1 ? tb.getChild( 0 ) : tb;
 443         tm = NodeManager::currentNM()->mkNode( MINUS, t, tm );
 444       }
 445       if( !d_arith_coeffs[ ic ].isNull() ){
 446         Assert( !ic.getType().isInteger() );
 447         Node coeff = NodeManager::currentNM()->mkConst( Rational(1) / d_arith_coeffs[ ic ].getConst<Rational>() );
 448         tm = NodeManager::currentNM()->mkNode( MULT, coeff, tm );
 449       }
 450       m.set( ic, Rewriter::rewrite( tm ));
 451       //set the rest to zeros
 452       for( std::map< Node, Node >::iterator it = d_arith_coeffs.begin(); it != d_arith_coeffs.end(); ++it ){
 453         if( !it->first.isNull() ){
 454           if( m.find( it->first )==m.end() ){
 455             m.set( it->first, NodeManager::currentNM()->mkConst( Rational(0) ) );
 456           }
 457         }
 458       }
 459       Debug("matching-arith") << "Setting " << ic << " to " << tm << std::endl;
 460       return true;
 461     }else{
 462       return false;
 463     }
 464   }else{
 465     return false;
 466   }
 467 }
 468
 469
 470 /** reset instantiation round */
 471 void InstMatchGenerator::resetInstantiationRound( QuantifiersEngine* qe ){
 472   if( d_match_pattern.isNull() ){
 473     for( int i=0; i<(int)d_children.size(); i++ ){
 474       d_children[i]->resetInstantiationRound( qe );
 475     }
 476   }else{
 477     if( d_cg ){
 478       d_cg->resetInstantiationRound();
 479     }
 480   }
 481 }
 482
 483 void InstMatchGenerator::reset( Node eqc, QuantifiersEngine* qe ){
 484   if( d_match_pattern.isNull() ){
 485     for( int i=0; i<(int)d_children.size(); i++ ){
 486       d_children[i]->reset( eqc, qe );
 487     }
 488     d_partial.clear();
 489   }else{
 490     if( !d_eq_class.isNull() ){
 491       //we have a specific equivalence class in mind
 492       //we are producing matches for f(E) ~ t, where E is a non-ground vector of terms, and t is a ground term
 493       //just look in equivalence class of the RHS
 494       d_cg->reset( d_eq_class );
 495     }else{
 496       d_cg->reset( eqc );
 497     }
 498   }
 499 }
 500
 501 bool InstMatchGenerator::getNextMatch( InstMatch& m, QuantifiersEngine* qe ){
 502   m.d_matched = Node::null();
 503   if( d_match_pattern.isNull() ){
 504     int index = (int)d_partial.size();
 505     while( index>=0 && index<(int)d_children.size() ){
 506       if( index>0 ){
 507         d_partial.push_back( InstMatch( &d_partial[index-1] ) );
 508       }else{
 509         d_partial.push_back( InstMatch() );
 510       }
 511       if( d_children[index]->getNextMatch( d_partial[index], qe ) ){
 512         index++;
 513       }else{
 514         d_children[index]->reset( Node::null(), qe );
 515         d_partial.pop_back();
 516         if( !d_partial.empty() ){
 517           d_partial.pop_back();
 518         }
 519         index--;
 520       }
 521     }
 522     if( index>=0 ){
 523       m = d_partial.back();
 524       d_partial.pop_back();
 525       return true;
 526     }else{
 527       return false;
 528     }
 529   }else{
 530     bool res = getNextMatch2( m, qe, true );
 531     Assert(!res || !m.d_matched.isNull());
 532     return res;
 533   }
 534 }
 535
 536
 537
 538 // Currently the implementation doesn't take into account that
 539 // variable should have the same value given.
 540 // TODO use the d_children way perhaps
 541 // TODO replace by a real dictionnary
 542 // We should create a real substitution? slower more precise
 543 // We don't do that often
 544 bool InstMatchGenerator::nonunifiable( TNode t0, const std::vector<Node> & vars){
 545   if(d_match_pattern.isNull()) return true;
 546
 547   typedef std::vector<std::pair<TNode,TNode> > tstack;
 548   tstack stack(1,std::make_pair(t0,d_match_pattern)); // t * pat
 549
 550   while(!stack.empty()){
 551     const std::pair<TNode,TNode> p = stack.back(); stack.pop_back();
 552     const TNode & t = p.first;
 553     const TNode & pat = p.second;
 554
 555     // t or pat is a variable currently we consider that can match anything
 556     if( find(vars.begin(),vars.end(),t) != vars.end() ) continue;
 557     if( pat.getKind() == INST_CONSTANT ) continue;
 558
 559     // t and pat are nonunifiable
 560     if( !Trigger::isAtomicTrigger( t ) || !Trigger::isAtomicTrigger( pat ) ) {
 561       if(t == pat) continue;
 562       else return true;
 563     };
 564     if( t.getOperator() != pat.getOperator() ) return true;
 565
 566     //put the children on the stack
 567     for( size_t i=0; i < pat.getNumChildren(); i++ ){
 568       stack.push_back(std::make_pair(t[i],pat[i]));
 569     };
 570   }
 571   // The heuristic can't find non-unifiability
 572   return false;
 573 }
 574
 575 int InstMatchGenerator::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){
 576   //now, try to add instantiation for each match produced
 577   int addedLemmas = 0;
 578   InstMatch m;
 579   while( getNextMatch( m, qe ) ){
 580     //m.makeInternal( d_quantEngine->getEqualityQuery() );
 581     m.add( baseMatch );
 582     if( qe->addInstantiation( f, m ) ){
 583       addedLemmas++;
 584       if( qe->d_optInstLimitActive && qe->d_optInstLimit<=0 ){
 585         return addedLemmas;
 586       }
 587     }
 588     m.clear();
 589   }
 590   //return number of lemmas added
 591   return addedLemmas;
 592 }
 593
 594 int InstMatchGenerator::addTerm( Node f, Node t, QuantifiersEngine* qe ){
 595   Assert( options::eagerInstQuant() );
 596   if( !d_match_pattern.isNull() ){
 597     InstMatch m;
 598     if( getMatch( t, m, qe ) ){
 599       if( qe->addInstantiation( f, m ) ){
 600         return 1;
 601       }
 602     }
 603   }else{
 604     for( int i=0; i<(int)d_children.size(); i++ ){
 605       d_children[i]->addTerm( f, t, qe );
 606     }
 607   }
 608   return 0;
 609 }
 610
 611 /** constructors */
 612 InstMatchGeneratorMulti::InstMatchGeneratorMulti( Node f, std::vector< Node >& pats, QuantifiersEngine* qe, int matchOption ) :
 613 d_f( f ){
 614   Debug("smart-multi-trigger") << "Making smart multi-trigger for " << f << std::endl;
 615   std::map< Node, std::vector< Node > > var_contains;
 616   Trigger::getVarContains( f, pats, var_contains );
 617   //convert to indicies
 618   for( std::map< Node, std::vector< Node > >::iterator it = var_contains.begin(); it != var_contains.end(); ++it ){
 619     Debug("smart-multi-trigger") << "Pattern " << it->first << " contains: ";
 620     for( int i=0; i<(int)it->second.size(); i++ ){
 621       Debug("smart-multi-trigger") << it->second[i] << " ";
 622       int index = it->second[i].getAttribute(InstVarNumAttribute());
 623       d_var_contains[ it->first ].push_back( index );
 624       d_var_to_node[ index ].push_back( it->first );
 625     }
 626     Debug("smart-multi-trigger") << std::endl;
 627   }
 628   for( int i=0; i<(int)pats.size(); i++ ){
 629     Node n = pats[i];
 630     //make the match generator
 631     d_children.push_back( new InstMatchGenerator( n, qe, matchOption ) );
 632     //compute unique/shared variables
 633     std::vector< int > unique_vars;
 634     std::map< int, bool > shared_vars;
 635     int numSharedVars = 0;
 636     for( int j=0; j<(int)d_var_contains[n].size(); j++ ){
 637       if( d_var_to_node[ d_var_contains[n][j] ].size()==1 ){
 638         Debug("smart-multi-trigger") << "Var " << d_var_contains[n][j] << " is unique to " << pats[i] << std::endl;
 639         unique_vars.push_back( d_var_contains[n][j] );
 640       }else{
 641         shared_vars[ d_var_contains[n][j] ] = true;
 642         numSharedVars++;
 643       }
 644     }
 645     //we use the latest shared variables, then unique variables
 646     std::vector< int > vars;
 647     int index = i==0 ? (int)(pats.size()-1) : (i-1);
 648     while( numSharedVars>0 && index!=i ){
 649       for( std::map< int, bool >::iterator it = shared_vars.begin(); it != shared_vars.end(); ++it ){
 650         if( it->second ){
 651           if( std::find( d_var_contains[ pats[index] ].begin(), d_var_contains[ pats[index] ].end(), it->first )!=
 652               d_var_contains[ pats[index] ].end() ){
 653             vars.push_back( it->first );
 654             shared_vars[ it->first ] = false;
 655             numSharedVars--;
 656           }
 657         }
 658       }
 659       index = index==0 ? (int)(pats.size()-1) : (index-1);
 660     }
 661     vars.insert( vars.end(), unique_vars.begin(), unique_vars.end() );
 662     Debug("smart-multi-trigger") << "   Index[" << i << "]: ";
 663     for( int i=0; i<(int)vars.size(); i++ ){
 664       Debug("smart-multi-trigger") << vars[i] << " ";
 665     }
 666     Debug("smart-multi-trigger") << std::endl;
 667     //make ordered inst match trie
 668     InstMatchTrie::ImtIndexOrder* imtio = new InstMatchTrie::ImtIndexOrder;
 669     imtio->d_order.insert( imtio->d_order.begin(), vars.begin(), vars.end() );
 670     d_children_trie.push_back( InstMatchTrieOrdered( imtio ) );
 671   }
 672
 673 }
 674
 675 /** reset instantiation round (call this whenever equivalence classes have changed) */
 676 void InstMatchGeneratorMulti::resetInstantiationRound( QuantifiersEngine* qe ){
 677   for( int i=0; i<(int)d_children.size(); i++ ){
 678     d_children[i]->resetInstantiationRound( qe );
 679   }
 680 }
 681
 682 /** reset, eqc is the equivalence class to search in (any if eqc=null) */
 683 void InstMatchGeneratorMulti::reset( Node eqc, QuantifiersEngine* qe ){
 684   for( int i=0; i<(int)d_children.size(); i++ ){
 685     d_children[i]->reset( eqc, qe );
 686   }
 687 }
 688
 689 int InstMatchGeneratorMulti::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){
 690   int addedLemmas = 0;
 691   Debug("smart-multi-trigger") << "Process smart multi trigger" << std::endl;
 692   for( int i=0; i<(int)d_children.size(); i++ ){
 693     Debug("smart-multi-trigger") << "Calculate matches " << i << std::endl;
 694     std::vector< InstMatch > newMatches;
 695     InstMatch m;
 696     while( d_children[i]->getNextMatch( m, qe ) ){
 697       m.makeRepresentative( qe );
 698       newMatches.push_back( InstMatch( &m ) );
 699       m.clear();
 700     }
 701     for( int j=0; j<(int)newMatches.size(); j++ ){
 702       processNewMatch( qe, newMatches[j], i, addedLemmas );
 703     }
 704   }
 705   return addedLemmas;
 706 }
 707
 708 void InstMatchGeneratorMulti::processNewMatch( QuantifiersEngine* qe, InstMatch& m, int fromChildIndex, int& addedLemmas ){
 709   //see if these produce new matches
 710   d_children_trie[fromChildIndex].addInstMatch( qe, d_f, m, true );
 711   //possibly only do the following if we know that new matches will be produced?
 712   //the issue is that instantiations are filtered in quantifiers engine, and so there is no guarentee that
 713   // we can safely skip the following lines, even when we have already produced this match.
 714   Debug("smart-multi-trigger") << "Child " << fromChildIndex << " produced match " << m << std::endl;
 715   //process new instantiations
 716   int childIndex = (fromChildIndex+1)%(int)d_children.size();
 717   std::vector< IndexedTrie > unique_var_tries;
 718   processNewInstantiations( qe, m, addedLemmas, d_children_trie[childIndex].getTrie(),
 719                             unique_var_tries, 0, childIndex, fromChildIndex, true );
 720 }
 721
 722 void InstMatchGeneratorMulti::processNewInstantiations( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas, InstMatchTrie* tr,
 723                                                         std::vector< IndexedTrie >& unique_var_tries,
 724                                                         int trieIndex, int childIndex, int endChildIndex, bool modEq ){
 725   if( childIndex==endChildIndex ){
 726     //now, process unique variables
 727     processNewInstantiations2( qe, m, addedLemmas, unique_var_tries, 0 );
 728   }else if( trieIndex<(int)d_children_trie[childIndex].getOrdering()->d_order.size() ){
 729     int curr_index = d_children_trie[childIndex].getOrdering()->d_order[trieIndex];
 730     Node curr_ic = qe->getTermDatabase()->getInstantiationConstant( d_f, curr_index );
 731     if( m.find( curr_ic )==m.end() ){
 732       //if( d_var_to_node[ curr_index ].size()==1 ){    //FIXME
 733       //  //unique variable(s), defer calculation
 734       //  unique_var_tries.push_back( IndexedTrie( std::pair< int, int >( childIndex, trieIndex ), tr ) );
 735       //  int newChildIndex = (childIndex+1)%(int)d_children.size();
 736       //  processNewInstantiations( qe, m, d_children_trie[newChildIndex].getTrie(), unique_var_tries,
 737       //                            0, newChildIndex, endChildIndex, modEq );
 738       //}else{
 739         //shared and non-set variable, add to InstMatch
 740         for( std::map< Node, InstMatchTrie >::iterator it = tr->d_data.begin(); it != tr->d_data.end(); ++it ){
 741           InstMatch mn( &m );
 742           mn.set( curr_ic, it->first);
 743           processNewInstantiations( qe, mn, addedLemmas, &(it->second), unique_var_tries,
 744                                     trieIndex+1, childIndex, endChildIndex, modEq );
 745         }
 746       //}
 747     }else{
 748       //shared and set variable, try to merge
 749       Node n = m.get( curr_ic );
 750       std::map< Node, InstMatchTrie >::iterator it = tr->d_data.find( n );
 751       if( it!=tr->d_data.end() ){
 752         processNewInstantiations( qe, m, addedLemmas, &(it->second), unique_var_tries,
 753                                   trieIndex+1, childIndex, endChildIndex, modEq );
 754       }
 755       if( modEq ){
 756         //check modulo equality for other possible instantiations
 757         if( qe->getEqualityQuery()->getEngine()->hasTerm( n ) ){
 758           eq::EqClassIterator eqc( qe->getEqualityQuery()->getEngine()->getRepresentative( n ),
 759                                    qe->getEqualityQuery()->getEngine() );
 760           while( !eqc.isFinished() ){
 761             Node en = (*eqc);
 762             if( en!=n ){
 763               std::map< Node, InstMatchTrie >::iterator itc = tr->d_data.find( en );
 764               if( itc!=tr->d_data.end() ){
 765                 processNewInstantiations( qe, m, addedLemmas, &(itc->second), unique_var_tries,
 766                                           trieIndex+1, childIndex, endChildIndex, modEq );
 767               }
 768             }
 769             ++eqc;
 770           }
 771         }
 772       }
 773     }
 774   }else{
 775     int newChildIndex = (childIndex+1)%(int)d_children.size();
 776     processNewInstantiations( qe, m, addedLemmas, d_children_trie[newChildIndex].getTrie(), unique_var_tries,
 777                               0, newChildIndex, endChildIndex, modEq );
 778   }
 779 }
 780
 781 void InstMatchGeneratorMulti::processNewInstantiations2( QuantifiersEngine* qe, InstMatch& m, int& addedLemmas,
 782                                                          std::vector< IndexedTrie >& unique_var_tries,
 783                                                          int uvtIndex, InstMatchTrie* tr, int trieIndex ){
 784   if( uvtIndex<(int)unique_var_tries.size() ){
 785     int childIndex = unique_var_tries[uvtIndex].first.first;
 786     if( !tr ){
 787       tr = unique_var_tries[uvtIndex].second;
 788       trieIndex = unique_var_tries[uvtIndex].first.second;
 789     }
 790     if( trieIndex<(int)d_children_trie[childIndex].getOrdering()->d_order.size() ){
 791       int curr_index = d_children_trie[childIndex].getOrdering()->d_order[trieIndex];
 792       Node curr_ic = qe->getTermDatabase()->getInstantiationConstant( d_f, curr_index );
 793       //unique non-set variable, add to InstMatch
 794       for( std::map< Node, InstMatchTrie >::iterator it = tr->d_data.begin(); it != tr->d_data.end(); ++it ){
 795         InstMatch mn( &m );
 796         mn.set( curr_ic, it->first);
 797         processNewInstantiations2( qe, mn, addedLemmas, unique_var_tries, uvtIndex, &(it->second), trieIndex+1 );
 798       }
 799     }else{
 800       processNewInstantiations2( qe, m, addedLemmas, unique_var_tries, uvtIndex+1 );
 801     }
 802   }else{
 803     //m is an instantiation
 804     if( qe->addInstantiation( d_f, m ) ){
 805       addedLemmas++;
 806       Debug("smart-multi-trigger") << "-> Produced instantiation " << m << std::endl;
 807     }
 808   }
 809 }
 810
 811 int InstMatchGeneratorMulti::addTerm( Node f, Node t, QuantifiersEngine* qe ){
 812   Assert( options::eagerInstQuant() );
 813   int addedLemmas = 0;
 814   for( int i=0; i<(int)d_children.size(); i++ ){
 815     if( ((InstMatchGenerator*)d_children[i])->d_match_pattern.getOperator()==t.getOperator() ){
 816       InstMatch m;
 817       //if it produces a match, then process it with the rest
 818       if( ((InstMatchGenerator*)d_children[i])->getMatch( t, m, qe ) ){
 819         processNewMatch( qe, m, i, addedLemmas );
 820       }
 821     }
 822   }
 823   return addedLemmas;
 824 }
 825
 826 int InstMatchGeneratorSimple::addInstantiations( Node f, InstMatch& baseMatch, QuantifiersEngine* qe ){
 827   InstMatch m;
 828   m.add( baseMatch );
 829   int addedLemmas = 0;
 830   if( d_match_pattern.getType()==NodeManager::currentNM()->booleanType() ){
 831     for( int i=0; i<2; i++ ){
 832       addInstantiations( m, qe, addedLemmas, 0, &(qe->getTermDatabase()->d_pred_map_trie[i][ d_match_pattern.getOperator() ]) );
 833     }
 834   }else{
 835     addInstantiations( m, qe, addedLemmas, 0, &(qe->getTermDatabase()->d_func_map_trie[ d_match_pattern.getOperator() ]) );
 836   }
 837   return addedLemmas;
 838 }
 839
 840 void InstMatchGeneratorSimple::addInstantiations( InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, int argIndex, quantifiers::TermArgTrie* tat ){
 841   if( argIndex==(int)d_match_pattern.getNumChildren() ){
 842     //m is an instantiation
 843     if( qe->addInstantiation( d_f, m ) ){
 844       addedLemmas++;
 845       Debug("simple-multi-trigger") << "-> Produced instantiation " << m << std::endl;
 846     }
 847   }else{
 848     if( d_match_pattern[argIndex].getKind()==INST_CONSTANT ){
 849       Node ic = d_match_pattern[argIndex];
 850       for( std::map< Node, quantifiers::TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){
 851         Node t = it->first;
 852         if( m.get( ic ).isNull() || m.get( ic )==t ){
 853           Node prev = m.get( ic );
 854           m.set( ic, t);
 855           addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) );
 856           m.set( ic, prev);
 857         }
 858       }
 859     }else{
 860       Node r = qe->getEqualityQuery()->getRepresentative( d_match_pattern[argIndex] );
 861       std::map< Node, quantifiers::TermArgTrie >::iterator it = tat->d_data.find( r );
 862       if( it!=tat->d_data.end() ){
 863         addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) );
 864       }
 865     }
 866   }
 867 }
 868
 869 int InstMatchGeneratorSimple::addTerm( Node f, Node t, QuantifiersEngine* qe ){
 870   Assert( options::eagerInstQuant() );
 871   InstMatch m;
 872   for( int i=0; i<(int)t.getNumChildren(); i++ ){
 873     if( d_match_pattern[i].getKind()==INST_CONSTANT ){
 874       m.set(d_match_pattern[i], t[i]);
 875     }else if( !qe->getEqualityQuery()->areEqual( d_match_pattern[i], t[i] ) ){
 876       return 0;
 877     }
 878   }
 879   return qe->addInstantiation( f, m ) ? 1 : 0;
 880 }