src/theory/quantifiers/ematching/inst_match_generator.cpp

   1 /*********************                                                        */
   2 /*! \file inst_match_generator.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-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  ** [[ Add lengthier description here ]]
  13  ** \todo document this file
  14  **/
  15 #include "theory/quantifiers/ematching/inst_match_generator.h"
  16
  17 #include "expr/datatype.h"
  18 #include "options/datatypes_options.h"
  19 #include "options/quantifiers_options.h"
  20 #include "theory/quantifiers/ematching/candidate_generator.h"
  21 #include "theory/quantifiers/ematching/trigger.h"
  22 #include "theory/quantifiers/instantiate.h"
  23 #include "theory/quantifiers/term_database.h"
  24 #include "theory/quantifiers/term_util.h"
  25 #include "theory/quantifiers_engine.h"
  26
  27 using namespace std;
  28 using namespace CVC4;
  29 using namespace CVC4::kind;
  30 using namespace CVC4::context;
  31 using namespace CVC4::theory;
  32
  33 namespace CVC4 {
  34 namespace theory {
  35 namespace inst {
  36
  37 bool IMGenerator::sendInstantiation(Trigger* tparent, InstMatch& m)
  38 {
  39   return tparent->sendInstantiation(m);
  40 }
  41
  42 InstMatchGenerator::InstMatchGenerator( Node pat ){
  43   d_cg = NULL;
  44   d_needsReset = true;
  45   d_active_add = true;
  46   Assert( quantifiers::TermUtil::hasInstConstAttr(pat) );
  47   d_pattern = pat;
  48   d_match_pattern = pat;
  49   d_match_pattern_type = pat.getType();
  50   d_next = NULL;
  51   d_independent_gen = false;
  52 }
  53
  54 InstMatchGenerator::InstMatchGenerator() {
  55   d_cg = NULL;
  56   d_needsReset = true;
  57   d_active_add = true;
  58   d_next = NULL;
  59   d_independent_gen = false;
  60 }
  61
  62 InstMatchGenerator::~InstMatchGenerator()
  63 {
  64   for( unsigned i=0; i<d_children.size(); i++ ){
  65     delete d_children[i];
  66   }
  67   delete d_cg;
  68 }
  69
  70 void InstMatchGenerator::setActiveAdd(bool val){
  71   d_active_add = val;
  72   if( d_next!=NULL ){
  73     d_next->setActiveAdd(val);
  74   }
  75 }
  76
  77 int InstMatchGenerator::getActiveScore( QuantifiersEngine * qe ) {
  78   if( d_match_pattern.isNull() ){
  79     return -1;
  80   }else if( Trigger::isAtomicTrigger( d_match_pattern ) ){
  81     Node f = qe->getTermDatabase()->getMatchOperator( d_match_pattern );
  82     unsigned ngt = qe->getTermDatabase()->getNumGroundTerms( f );
  83     Trace("trigger-active-sel-debug") << "Number of ground terms for " << f << " is " << ngt << std::endl;
  84     return ngt;
  85   }else if( d_match_pattern.getKind()==INST_CONSTANT ){
  86     TypeNode tn = d_match_pattern.getType();
  87     unsigned ngtt = qe->getTermDatabase()->getNumTypeGroundTerms( tn );
  88     Trace("trigger-active-sel-debug") << "Number of ground terms for " << tn << " is " << ngtt << std::endl;
  89     return ngtt;
  90 //  }else if( d_match_pattern_getKind()==EQUAL ){
  91
  92   }else{
  93     return -1;
  94   }
  95 }
  96
  97 void InstMatchGenerator::initialize( Node q, QuantifiersEngine* qe, std::vector< InstMatchGenerator * > & gens ){
  98   if( !d_pattern.isNull() ){
  99     Trace("inst-match-gen") << "Initialize, pattern term is " << d_pattern << std::endl;
 100     if( d_match_pattern.getKind()==NOT ){
 101       //we want to add the children of the NOT
 102       d_match_pattern = d_pattern[0];
 103     }
 104     if( d_match_pattern.getKind()==EQUAL || d_match_pattern.getKind()==GEQ ){
 105       //make sure the matching portion of the equality is on the LHS of d_pattern
 106       //  and record what d_match_pattern is
 107       for( unsigned i=0; i<2; i++ ){
 108         if( !quantifiers::TermUtil::hasInstConstAttr(d_match_pattern[i]) || d_match_pattern[i].getKind()==INST_CONSTANT ){
 109           Node mp = d_match_pattern[1-i];
 110           Node mpo = d_match_pattern[i];
 111           if( mp.getKind()!=INST_CONSTANT ){
 112             if( i==0 ){
 113               if( d_match_pattern.getKind()==GEQ ){
 114                 d_pattern = NodeManager::currentNM()->mkNode( kind::GT, mp, mpo );
 115                 d_pattern = d_pattern.negate();
 116               }else{
 117                 d_pattern = NodeManager::currentNM()->mkNode( d_match_pattern.getKind(), mp, mpo );
 118               }
 119             }
 120             d_eq_class_rel = mpo;
 121             d_match_pattern = mp;
 122           }
 123           break;
 124         }
 125       }
 126     }else if( d_match_pattern.getKind()==APPLY_SELECTOR_TOTAL && d_match_pattern[0].getKind()==INST_CONSTANT &&
 127               options::purifyDtTriggers() && !options::dtSharedSelectors() ){
 128       d_match_pattern = d_match_pattern[0];
 129     }
 130     d_match_pattern_type = d_match_pattern.getType();
 131     Trace("inst-match-gen") << "Pattern is " << d_pattern << ", match pattern is " << d_match_pattern << std::endl;
 132     d_match_pattern_op = qe->getTermDatabase()->getMatchOperator( d_match_pattern );
 133
 134     //now, collect children of d_match_pattern
 135     if (d_match_pattern.getKind() == INST_CONSTANT)
 136     {
 137       d_children_types.push_back(
 138           d_match_pattern.getAttribute(InstVarNumAttribute()));
 139     }
 140     else
 141     {
 142       for (unsigned i = 0, size = d_match_pattern.getNumChildren(); i < size;
 143            i++)
 144       {
 145         Node pat = d_match_pattern[i];
 146         Node qa = quantifiers::TermUtil::getInstConstAttr(pat);
 147         if (!qa.isNull())
 148         {
 149           if (pat.getKind() == INST_CONSTANT && qa == q)
 150           {
 151             d_children_types.push_back(pat.getAttribute(InstVarNumAttribute()));
 152           }
 153           else
 154           {
 155             InstMatchGenerator* cimg = getInstMatchGenerator(q, pat);
 156             if (cimg)
 157             {
 158               d_children.push_back(cimg);
 159               d_children_index.push_back(i);
 160               d_children_types.push_back(-2);
 161             }
 162             else
 163             {
 164               d_children_types.push_back(-1);
 165             }
 166           }
 167         }
 168         else
 169         {
 170           d_children_types.push_back(-1);
 171         }
 172       }
 173     }
 174
 175     //create candidate generator
 176     if( Trigger::isAtomicTrigger( d_match_pattern ) ){
 177       if (d_match_pattern.getKind() == APPLY_CONSTRUCTOR)
 178       {
 179         // 1-constructors have a trivial way of generating candidates in a
 180         // given equivalence class
 181         const Datatype& dt =
 182             static_cast<DatatypeType>(d_match_pattern.getType().toType())
 183                 .getDatatype();
 184         if (dt.getNumConstructors() == 1)
 185         {
 186           d_cg = new inst::CandidateGeneratorConsExpand(qe, d_match_pattern);
 187         }
 188       }
 189       if (d_cg == nullptr)
 190       {
 191         // we will be scanning lists trying to find
 192         // d_match_pattern.getOperator()
 193         d_cg = new inst::CandidateGeneratorQE(qe, d_match_pattern);
 194       }
 195       //if matching on disequality, inform the candidate generator not to match on eqc
 196       if( d_pattern.getKind()==NOT && d_pattern[0].getKind()==EQUAL ){
 197         ((inst::CandidateGeneratorQE*)d_cg)->excludeEqc( d_eq_class_rel );
 198         d_eq_class_rel = Node::null();
 199       }
 200     }else if( d_match_pattern.getKind()==INST_CONSTANT ){
 201       if( d_pattern.getKind()==APPLY_SELECTOR_TOTAL ){
 202         Expr selectorExpr = qe->getTermDatabase()->getMatchOperator( d_pattern ).toExpr();
 203         size_t selectorIndex = Datatype::cindexOf(selectorExpr);
 204         const Datatype& dt = Datatype::datatypeOf(selectorExpr);
 205         const DatatypeConstructor& c = dt[selectorIndex];
 206         Node cOp = Node::fromExpr(c.getConstructor());
 207         Trace("inst-match-gen") << "Purify dt trigger " << d_pattern << ", will match terms of op " << cOp << std::endl;
 208         d_cg = new inst::CandidateGeneratorQE( qe, cOp );
 209       }else{
 210         d_cg = new CandidateGeneratorQEAll( qe, d_match_pattern );
 211       }
 212     }else if( d_match_pattern.getKind()==EQUAL &&
 213               d_match_pattern[0].getKind()==INST_CONSTANT && d_match_pattern[1].getKind()==INST_CONSTANT ){
 214       //we will be producing candidates via literal matching heuristics
 215       Assert(d_pattern.getKind() == NOT);
 216       // candidates will be all disequalities
 217       d_cg = new inst::CandidateGeneratorQELitDeq(qe, d_match_pattern);
 218     }else{
 219       Trace("inst-match-gen-warn") << "(?) Unknown matching pattern is " << d_match_pattern << std::endl;
 220     }
 221   }
 222   gens.insert( gens.end(), d_children.begin(), d_children.end() );
 223 }
 224
 225 /** get match (not modulo equality) */
 226 int InstMatchGenerator::getMatch(
 227     Node f, Node t, InstMatch& m, QuantifiersEngine* qe, Trigger* tparent)
 228 {
 229   Trace("matching") << "Matching " << t << " against pattern " << d_match_pattern << " ("
 230                     << m << ")" << ", " << d_children.size() << ", pattern is " << d_pattern << std::endl;
 231   Assert( !d_match_pattern.isNull() );
 232   if (d_cg == nullptr)
 233   {
 234     Trace("matching-fail") << "Internal error for match generator." << std::endl;
 235     return -2;
 236   }else{
 237     EqualityQuery* q = qe->getEqualityQuery();
 238     bool success = true;
 239     //save previous match
 240     //InstMatch prev( &m );
 241     std::vector< int > prev;
 242     //if t is null
 243     Assert( !t.isNull() );
 244     Assert( !quantifiers::TermUtil::hasInstConstAttr(t) );
 245     Assert( d_match_pattern.getKind()==INST_CONSTANT || t.getKind()==d_match_pattern.getKind() );
 246     Assert( !Trigger::isAtomicTrigger( d_match_pattern ) || t.getOperator()==d_match_pattern.getOperator() );
 247     //first, check if ground arguments are not equal, or a match is in conflict
 248     Trace("matching-debug2") << "Setting immediate matches..." << std::endl;
 249     for (unsigned i = 0, size = d_match_pattern.getNumChildren(); i < size; i++)
 250     {
 251       int ct = d_children_types[i];
 252       if (ct >= 0)
 253       {
 254         Trace("matching-debug2") << "Setting " << ct << " to " << t[i] << "..."
 255                                  << std::endl;
 256         bool addToPrev = m.get(ct).isNull();
 257         if (!m.set(q, ct, t[i]))
 258         {
 259           //match is in conflict
 260           Trace("matching-fail") << "Match fail: " << m.get(ct) << " and "
 261                                  << t[i] << std::endl;
 262           success = false;
 263           break;
 264         }else if( addToPrev ){
 265           Trace("matching-debug2") << "Success." << std::endl;
 266           prev.push_back(ct);
 267         }
 268       }
 269       else if (ct == -1)
 270       {
 271         if( !q->areEqual( d_match_pattern[i], t[i] ) ){
 272           Trace("matching-fail") << "Match fail arg: " << d_match_pattern[i] << " and " << t[i] << std::endl;
 273           //ground arguments are not equal
 274           success = false;
 275           break;
 276         }
 277       }
 278     }
 279     Trace("matching-debug2") << "Done setting immediate matches, success = " << success << "." << std::endl;
 280     //for variable matching
 281     if( d_match_pattern.getKind()==INST_CONSTANT ){
 282       bool addToPrev = m.get(d_children_types[0]).isNull();
 283       if (!m.set(q, d_children_types[0], t))
 284       {
 285         success = false;
 286       }else{
 287         if( addToPrev ){
 288           prev.push_back(d_children_types[0]);
 289         }
 290       }
 291     //for relational matching
 292     }else if( !d_eq_class_rel.isNull() && d_eq_class_rel.getKind()==INST_CONSTANT ){
 293       int v = d_eq_class_rel.getAttribute(InstVarNumAttribute());
 294       //also must fit match to equivalence class
 295       bool pol = d_pattern.getKind()!=NOT;
 296       Node pat = d_pattern.getKind()==NOT ? d_pattern[0] : d_pattern;
 297       Node t_match;
 298       if( pol ){
 299         if( pat.getKind()==GT ){
 300           t_match = NodeManager::currentNM()->mkNode(MINUS, t, qe->getTermUtil()->d_one);
 301         }else{
 302           t_match = t;
 303         }
 304       }else{
 305         if( pat.getKind()==EQUAL ){
 306           if( t.getType().isBoolean() ){
 307             t_match = NodeManager::currentNM()->mkConst( !q->areEqual( qe->getTermUtil()->d_true, t ) );
 308           }else{
 309             Assert( t.getType().isReal() );
 310             t_match = NodeManager::currentNM()->mkNode(PLUS, t, qe->getTermUtil()->d_one);
 311           }
 312         }else if( pat.getKind()==GEQ ){
 313           t_match = NodeManager::currentNM()->mkNode(PLUS, t, qe->getTermUtil()->d_one);
 314         }else if( pat.getKind()==GT ){
 315           t_match = t;
 316         }
 317       }
 318       if( !t_match.isNull() ){
 319         bool addToPrev = m.get( v ).isNull();
 320         if (!m.set(q, v, t_match))
 321         {
 322           success = false;
 323         }else if( addToPrev ){
 324           prev.push_back( v );
 325         }
 326       }
 327     }
 328     int ret_val = -1;
 329     if( success ){
 330       Trace("matching-debug2") << "Reset children..." << std::endl;
 331       //now, fit children into match
 332       //we will be requesting candidates for matching terms for each child
 333       for (unsigned i = 0, size = d_children.size(); i < size; i++)
 334       {
 335         if( !d_children[i]->reset( t[ d_children_index[i] ], qe ) ){
 336           success = false;
 337           break;
 338         }
 339       }
 340       if( success ){
 341         Trace("matching-debug2") << "Continue next " << d_next << std::endl;
 342         ret_val = continueNextMatch(f, m, qe, tparent);
 343       }
 344     }
 345     if( ret_val<0 ){
 346       for (int& pv : prev)
 347       {
 348         m.d_vals[pv] = Node::null();
 349       }
 350     }
 351     return ret_val;
 352   }
 353 }
 354
 355 int InstMatchGenerator::continueNextMatch(Node f,
 356                                           InstMatch& m,
 357                                           QuantifiersEngine* qe,
 358                                           Trigger* tparent)
 359 {
 360   if( d_next!=NULL ){
 361     return d_next->getNextMatch(f, m, qe, tparent);
 362   }else{
 363     if( d_active_add ){
 364       return sendInstantiation(tparent, m) ? 1 : -1;
 365     }else{
 366       return 1;
 367     }
 368   }
 369 }
 370
 371 /** reset instantiation round */
 372 void InstMatchGenerator::resetInstantiationRound( QuantifiersEngine* qe ){
 373   if( !d_match_pattern.isNull() ){
 374     Trace("matching-debug2") << this << " reset instantiation round." << std::endl;
 375     d_needsReset = true;
 376     if( d_cg ){
 377       d_cg->resetInstantiationRound();
 378     }
 379   }
 380   if( d_next ){
 381     d_next->resetInstantiationRound( qe );
 382   }
 383   d_curr_exclude_match.clear();
 384 }
 385
 386 bool InstMatchGenerator::reset( Node eqc, QuantifiersEngine* qe ){
 387   if (d_cg == nullptr)
 388   {
 389     // we did not properly initialize the candidate generator, thus we fail
 390     return false;
 391   }
 392   eqc = qe->getEqualityQuery()->getRepresentative( eqc );
 393   Trace("matching-debug2") << this << " reset " << eqc << "." << std::endl;
 394   if( !d_eq_class_rel.isNull() && d_eq_class_rel.getKind()!=INST_CONSTANT ){
 395     d_eq_class = d_eq_class_rel;
 396   }else if( !eqc.isNull() ){
 397     d_eq_class = eqc;
 398   }
 399   //we have a specific equivalence class in mind
 400   //we are producing matches for f(E) ~ t, where E is a non-ground vector of terms, and t is a ground term
 401   //just look in equivalence class of the RHS
 402   d_cg->reset( d_eq_class );
 403   d_needsReset = false;
 404
 405   //generate the first candidate preemptively
 406   d_curr_first_candidate = Node::null();
 407   Node t;
 408   do {
 409     t = d_cg->getNextCandidate();
 410     if( d_curr_exclude_match.find( t )==d_curr_exclude_match.end() ){
 411       d_curr_first_candidate = t;
 412     }
 413   }while( !t.isNull() && d_curr_first_candidate.isNull() );
 414   Trace("matching-summary") << "Reset " << d_match_pattern << " in " << eqc << " returns " << !d_curr_first_candidate.isNull() << "." << std::endl;
 415
 416   return !d_curr_first_candidate.isNull();
 417 }
 418
 419 int InstMatchGenerator::getNextMatch(Node f,
 420                                      InstMatch& m,
 421                                      QuantifiersEngine* qe,
 422                                      Trigger* tparent)
 423 {
 424   if( d_needsReset ){
 425     Trace("matching") << "Reset not done yet, must do the reset..." << std::endl;
 426     reset( d_eq_class, qe );
 427   }
 428   d_curr_matched = Node::null();
 429   Trace("matching") << this << " " << d_match_pattern << " get next match " << m << " in eq class " << d_eq_class << std::endl;
 430   int success = -1;
 431   Node t = d_curr_first_candidate;
 432   do{
 433     Trace("matching-debug2") << "Matching candidate : " << t << std::endl;
 434     Assert(!qe->inConflict());
 435     //if t not null, try to fit it into match m
 436     if( !t.isNull() ){
 437       if( d_curr_exclude_match.find( t )==d_curr_exclude_match.end() ){
 438         Assert( t.getType().isComparableTo( d_match_pattern_type ) );
 439         Trace("matching-summary") << "Try " << d_match_pattern << " : " << t << std::endl;
 440         success = getMatch(f, t, m, qe, tparent);
 441         if( d_independent_gen && success<0 ){
 442           Assert(d_eq_class.isNull() || !d_eq_class_rel.isNull());
 443           d_curr_exclude_match[t] = true;
 444         }
 445       }
 446       //get the next candidate term t
 447       if( success<0 ){
 448         t = qe->inConflict() ? Node::null() : d_cg->getNextCandidate();
 449       }else{
 450         d_curr_first_candidate = d_cg->getNextCandidate();
 451       }
 452     }
 453   }while( success<0 && !t.isNull() );
 454   d_curr_matched = t;
 455   if( success<0 ){
 456     Trace("matching-summary") << "..." << d_match_pattern << " failed, reset." << std::endl;
 457     Trace("matching") << this << " failed, reset " << d_eq_class << std::endl;
 458     //we failed, must reset
 459     reset( d_eq_class, qe );
 460   }else{
 461     Trace("matching-summary") << "..." << d_match_pattern << " success." << std::endl;
 462   }
 463   return success;
 464 }
 465
 466 int InstMatchGenerator::addInstantiations(Node f,
 467                                           QuantifiersEngine* qe,
 468                                           Trigger* tparent)
 469 {
 470   //try to add instantiation for each match produced
 471   int addedLemmas = 0;
 472   InstMatch m( f );
 473   while (getNextMatch(f, m, qe, tparent) > 0)
 474   {
 475     if( !d_active_add ){
 476       if (sendInstantiation(tparent, m))
 477       {
 478         addedLemmas++;
 479         if( qe->inConflict() ){
 480           break;
 481         }
 482       }
 483     }else{
 484       addedLemmas++;
 485       if( qe->inConflict() ){
 486         break;
 487       }
 488     }
 489     m.clear();
 490   }
 491   //return number of lemmas added
 492   return addedLemmas;
 493 }
 494
 495
 496 InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator( Node q, Node pat, QuantifiersEngine* qe ) {
 497   std::vector< Node > pats;
 498   pats.push_back( pat );
 499   std::map< Node, InstMatchGenerator * > pat_map_init;
 500   return mkInstMatchGenerator( q, pats, qe, pat_map_init );
 501 }
 502
 503 InstMatchGenerator* InstMatchGenerator::mkInstMatchGeneratorMulti( Node q, std::vector< Node >& pats, QuantifiersEngine* qe ) {
 504   Assert( pats.size()>1 );
 505   InstMatchGeneratorMultiLinear * imgm = new InstMatchGeneratorMultiLinear( q, pats, qe );
 506   std::vector< InstMatchGenerator* > gens;
 507   imgm->initialize(q, qe, gens);
 508   Assert( gens.size()==pats.size() );
 509   std::vector< Node > patsn;
 510   std::map< Node, InstMatchGenerator * > pat_map_init;
 511   for( unsigned i=0; i<gens.size(); i++ ){
 512     Node pn = gens[i]->d_match_pattern;
 513     patsn.push_back( pn );
 514     pat_map_init[pn] = gens[i];
 515   }
 516   //return mkInstMatchGenerator( q, patsn, qe, pat_map_init );
 517   imgm->d_next = mkInstMatchGenerator( q, patsn, qe, pat_map_init );
 518   return imgm;
 519 }
 520
 521 InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator( Node q, std::vector< Node >& pats, QuantifiersEngine* qe,
 522                                                               std::map< Node, InstMatchGenerator * >& pat_map_init ) {
 523   size_t pCounter = 0;
 524   InstMatchGenerator* prev = NULL;
 525   InstMatchGenerator* oinit = NULL;
 526   while( pCounter<pats.size() ){
 527     size_t counter = 0;
 528     std::vector< InstMatchGenerator* > gens;
 529     InstMatchGenerator* init;
 530     std::map< Node, InstMatchGenerator * >::iterator iti = pat_map_init.find( pats[pCounter] );
 531     if( iti==pat_map_init.end() ){
 532       init = new InstMatchGenerator(pats[pCounter]);
 533     }else{
 534       init = iti->second;
 535     }
 536     if(pCounter==0){
 537       oinit = init;
 538     }
 539     gens.push_back(init);
 540     //chain the resulting match generators together
 541     while (counter<gens.size()) {
 542       InstMatchGenerator* curr = gens[counter];
 543       if( prev ){
 544         prev->d_next = curr;
 545       }
 546       curr->initialize(q, qe, gens);
 547       prev = curr;
 548       counter++;
 549     }
 550     pCounter++;
 551   }
 552   return oinit;
 553 }
 554
 555 InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Node q, Node n)
 556 {
 557   if (n.getKind() != INST_CONSTANT)
 558   {
 559     Trace("var-trigger-debug")
 560         << "Is " << n << " a variable trigger?" << std::endl;
 561     Node x;
 562     if (options::purifyTriggers())
 563     {
 564       x = Trigger::getInversionVariable(n);
 565     }
 566     if (!x.isNull())
 567     {
 568       Node s = Trigger::getInversion(n, x);
 569       VarMatchGeneratorTermSubs* vmg = new VarMatchGeneratorTermSubs(x, s);
 570       Trace("var-trigger") << "Term substitution trigger : " << n
 571                            << ", var = " << x << ", subs = " << s << std::endl;
 572       return vmg;
 573     }
 574   }
 575   return new InstMatchGenerator(n);
 576 }
 577
 578 VarMatchGeneratorTermSubs::VarMatchGeneratorTermSubs( Node var, Node subs ) :
 579   InstMatchGenerator(), d_var( var ), d_subs( subs ), d_rm_prev( false ){
 580   d_children_types.push_back(d_var.getAttribute(InstVarNumAttribute()));
 581   d_var_type = d_var.getType();
 582 }
 583
 584 int VarMatchGeneratorTermSubs::getNextMatch(Node q,
 585                                             InstMatch& m,
 586                                             QuantifiersEngine* qe,
 587                                             Trigger* tparent)
 588 {
 589   int ret_val = -1;
 590   if( !d_eq_class.isNull() ){
 591     Trace("var-trigger-matching") << "Matching " << d_eq_class << " against " << d_var << " in " << d_subs << std::endl;
 592     Node s = d_subs.substitute( d_var, d_eq_class );
 593     s = Rewriter::rewrite( s );
 594     Trace("var-trigger-matching") << "...got " << s << ", " << s.getKind() << std::endl;
 595     d_eq_class = Node::null();
 596     //if( s.getType().isSubtypeOf( d_var_type ) ){
 597     d_rm_prev = m.get(d_children_types[0]).isNull();
 598     if (!m.set(qe->getEqualityQuery(), d_children_types[0], s))
 599     {
 600       return -1;
 601     }else{
 602       ret_val = continueNextMatch(q, m, qe, tparent);
 603       if( ret_val>0 ){
 604         return ret_val;
 605       }
 606     }
 607   }
 608   if( d_rm_prev ){
 609     m.d_vals[d_children_types[0]] = Node::null();
 610     d_rm_prev = false;
 611   }
 612   return -1;
 613 }
 614
 615 InstMatchGeneratorMultiLinear::InstMatchGeneratorMultiLinear( Node q, std::vector< Node >& pats, QuantifiersEngine* qe ) {
 616   //order patterns to maximize eager matching failures
 617   std::map< Node, std::vector< Node > > var_contains;
 618   for (const Node& pat : pats)
 619   {
 620     quantifiers::TermUtil::computeInstConstContainsForQuant(
 621         q, pat, var_contains[pat]);
 622   }
 623   std::map< Node, std::vector< Node > > var_to_node;
 624   for( std::map< Node, std::vector< Node > >::iterator it = var_contains.begin(); it != var_contains.end(); ++it ){
 625     for( unsigned i=0; i<it->second.size(); i++ ){
 626       var_to_node[ it->second[i] ].push_back( it->first );
 627     }
 628   }
 629   std::vector< Node > pats_ordered;
 630   std::vector< bool > pats_ordered_independent;
 631   std::map< Node, bool > var_bound;
 632   while( pats_ordered.size()<pats.size() ){
 633     // score is lexographic ( bound vars, shared vars )
 634     int score_max_1 = -1;
 635     int score_max_2 = -1;
 636     unsigned score_index = 0;
 637     bool set_score_index = false;
 638     for( unsigned i=0; i<pats.size(); i++ ){
 639       Node p = pats[i];
 640       if( std::find( pats_ordered.begin(), pats_ordered.end(), p )==pats_ordered.end() ){
 641         int score_1 = 0;
 642         int score_2 = 0;
 643         for( unsigned j=0; j<var_contains[p].size(); j++ ){
 644           Node v = var_contains[p][j];
 645           if( var_bound.find( v )!=var_bound.end() ){
 646             score_1++;
 647           }else if( var_to_node[v].size()>1 ){
 648             score_2++;
 649           }
 650         }
 651         if (!set_score_index || score_1 > score_max_1
 652             || (score_1 == score_max_1 && score_2 > score_max_2))
 653         {
 654           score_index = i;
 655           set_score_index = true;
 656           score_max_1 = score_1;
 657           score_max_2 = score_2;
 658         }
 659       }
 660     }
 661     Assert(set_score_index);
 662     //update the variable bounds
 663     Node mp = pats[score_index];
 664     for( unsigned i=0; i<var_contains[mp].size(); i++ ){
 665       var_bound[var_contains[mp][i]] = true;
 666     }
 667     pats_ordered.push_back( mp );
 668     pats_ordered_independent.push_back( score_max_1==0 );
 669   }
 670
 671   Trace("multi-trigger-linear") << "Make children for linear multi trigger." << std::endl;
 672   for( unsigned i=0; i<pats_ordered.size(); i++ ){
 673     Trace("multi-trigger-linear") << "...make for " << pats_ordered[i] << std::endl;
 674     InstMatchGenerator* cimg = getInstMatchGenerator(q, pats_ordered[i]);
 675     Assert( cimg!=NULL );
 676     d_children.push_back( cimg );
 677     if( i==0 ){  //TODO : improve
 678       cimg->setIndependent();
 679     }
 680   }
 681 }
 682
 683 int InstMatchGeneratorMultiLinear::resetChildren( QuantifiersEngine* qe ){
 684   for( unsigned i=0; i<d_children.size(); i++ ){
 685     if( !d_children[i]->reset( Node::null(), qe ) ){
 686       return -2;
 687     }
 688   }
 689   return 1;
 690 }
 691
 692 bool InstMatchGeneratorMultiLinear::reset( Node eqc, QuantifiersEngine* qe ) {
 693   Assert( eqc.isNull() );
 694   if( options::multiTriggerLinear() ){
 695     return true;
 696   }else{
 697     return resetChildren( qe )>0;
 698   }
 699 }
 700
 701 int InstMatchGeneratorMultiLinear::getNextMatch(Node q,
 702                                                 InstMatch& m,
 703                                                 QuantifiersEngine* qe,
 704                                                 Trigger* tparent)
 705 {
 706   Trace("multi-trigger-linear-debug") << "InstMatchGeneratorMultiLinear::getNextMatch : reset " << std::endl;
 707   if( options::multiTriggerLinear() ){
 708     //reset everyone
 709     int rc_ret = resetChildren( qe );
 710     if( rc_ret<0 ){
 711       return rc_ret;
 712     }
 713   }
 714   Trace("multi-trigger-linear-debug") << "InstMatchGeneratorMultiLinear::getNextMatch : continue match " << std::endl;
 715   Assert( d_next!=NULL );
 716   int ret_val = continueNextMatch(q, m, qe, tparent);
 717   if( ret_val>0 ){
 718     Trace("multi-trigger-linear") << "Successful multi-trigger instantiation." << std::endl;
 719     if( options::multiTriggerLinear() ){
 720       // now, restrict everyone
 721       for( unsigned i=0; i<d_children.size(); i++ ){
 722         Node mi = d_children[i]->getCurrentMatch();
 723         Trace("multi-trigger-linear") << "   child " << i << " match : " << mi << std::endl;
 724         d_children[i]->excludeMatch( mi );
 725       }
 726     }
 727   }
 728   return ret_val;
 729 }
 730
 731
 732 /** constructors */
 733 InstMatchGeneratorMulti::InstMatchGeneratorMulti(Node q,
 734                                                  std::vector<Node>& pats,
 735                                                  QuantifiersEngine* qe)
 736     : d_quant(q)
 737 {
 738   Trace("multi-trigger-cache") << "Making smart multi-trigger for " << q << std::endl;
 739   std::map< Node, std::vector< Node > > var_contains;
 740   for (const Node& pat : pats)
 741   {
 742     quantifiers::TermUtil::computeInstConstContainsForQuant(
 743         q, pat, var_contains[pat]);
 744   }
 745   //convert to indicies
 746   for( std::map< Node, std::vector< Node > >::iterator it = var_contains.begin(); it != var_contains.end(); ++it ){
 747     Trace("multi-trigger-cache") << "Pattern " << it->first << " contains: ";
 748     for( int i=0; i<(int)it->second.size(); i++ ){
 749       Trace("multi-trigger-cache") << it->second[i] << " ";
 750       int index = it->second[i].getAttribute(InstVarNumAttribute());
 751       d_var_contains[ it->first ].push_back( index );
 752       d_var_to_node[ index ].push_back( it->first );
 753     }
 754     Trace("multi-trigger-cache") << std::endl;
 755   }
 756   for( unsigned i=0; i<pats.size(); i++ ){
 757     Node n = pats[i];
 758     //make the match generator
 759     InstMatchGenerator* img =
 760         InstMatchGenerator::mkInstMatchGenerator(q, n, qe);
 761     img->setActiveAdd(false);
 762     d_children.push_back(img);
 763     //compute unique/shared variables
 764     std::vector< int > unique_vars;
 765     std::map< int, bool > shared_vars;
 766     int numSharedVars = 0;
 767     for( unsigned j=0; j<d_var_contains[n].size(); j++ ){
 768       if( d_var_to_node[ d_var_contains[n][j] ].size()==1 ){
 769         Trace("multi-trigger-cache") << "Var " << d_var_contains[n][j] << " is unique to " << pats[i] << std::endl;
 770         unique_vars.push_back( d_var_contains[n][j] );
 771       }else{
 772         shared_vars[ d_var_contains[n][j] ] = true;
 773         numSharedVars++;
 774       }
 775     }
 776     //we use the latest shared variables, then unique variables
 777     std::vector< int > vars;
 778     unsigned index = i==0 ? pats.size()-1 : (i-1);
 779     while( numSharedVars>0 && index!=i ){
 780       for( std::map< int, bool >::iterator it = shared_vars.begin(); it != shared_vars.end(); ++it ){
 781         if( it->second ){
 782           if( std::find( d_var_contains[ pats[index] ].begin(), d_var_contains[ pats[index] ].end(), it->first )!=
 783               d_var_contains[ pats[index] ].end() ){
 784             vars.push_back( it->first );
 785             shared_vars[ it->first ] = false;
 786             numSharedVars--;
 787           }
 788         }
 789       }
 790       index = index==0 ? (int)(pats.size()-1) : (index-1);
 791     }
 792     vars.insert( vars.end(), unique_vars.begin(), unique_vars.end() );
 793     Trace("multi-trigger-cache") << "   Index[" << i << "]: ";
 794     for( unsigned j=0; j<vars.size(); j++ ){
 795       Trace("multi-trigger-cache") << vars[j] << " ";
 796     }
 797     Trace("multi-trigger-cache") << std::endl;
 798     //make ordered inst match trie
 799     d_imtio[i] = new InstMatchTrie::ImtIndexOrder;
 800     d_imtio[i]->d_order.insert( d_imtio[i]->d_order.begin(), vars.begin(), vars.end() );
 801     d_children_trie.push_back( InstMatchTrieOrdered( d_imtio[i] ) );
 802   }
 803 }
 804
 805 InstMatchGeneratorMulti::~InstMatchGeneratorMulti()
 806 {
 807   for( unsigned i=0; i<d_children.size(); i++ ){
 808     delete d_children[i];
 809   }
 810   for( std::map< unsigned, InstMatchTrie::ImtIndexOrder* >::iterator it = d_imtio.begin(); it != d_imtio.end(); ++it ){
 811     delete it->second;
 812   }
 813 }
 814
 815 /** reset instantiation round (call this whenever equivalence classes have changed) */
 816 void InstMatchGeneratorMulti::resetInstantiationRound( QuantifiersEngine* qe ){
 817   for( unsigned i=0; i<d_children.size(); i++ ){
 818     d_children[i]->resetInstantiationRound( qe );
 819   }
 820 }
 821
 822 /** reset, eqc is the equivalence class to search in (any if eqc=null) */
 823 bool InstMatchGeneratorMulti::reset( Node eqc, QuantifiersEngine* qe ){
 824   for( unsigned i=0; i<d_children.size(); i++ ){
 825     if( !d_children[i]->reset( eqc, qe ) ){
 826       //return false;
 827     }
 828   }
 829   return true;
 830 }
 831
 832 int InstMatchGeneratorMulti::addInstantiations(Node q,
 833                                                QuantifiersEngine* qe,
 834                                                Trigger* tparent)
 835 {
 836   int addedLemmas = 0;
 837   Trace("multi-trigger-cache") << "Process smart multi trigger" << std::endl;
 838   for( unsigned i=0; i<d_children.size(); i++ ){
 839     Trace("multi-trigger-cache") << "Calculate matches " << i << std::endl;
 840     std::vector< InstMatch > newMatches;
 841     InstMatch m( q );
 842     while (d_children[i]->getNextMatch(q, m, qe, tparent) > 0)
 843     {
 844       //m.makeRepresentative( qe );
 845       newMatches.push_back( InstMatch( &m ) );
 846       m.clear();
 847     }
 848     Trace("multi-trigger-cache") << "Made " << newMatches.size() << " new matches for index " << i << std::endl;
 849     for( unsigned j=0; j<newMatches.size(); j++ ){
 850       Trace("multi-trigger-cache2") << "...processing " << j << " / " << newMatches.size() << ", #lemmas = " << addedLemmas << std::endl;
 851       processNewMatch(qe, tparent, newMatches[j], i, addedLemmas);
 852       if( qe->inConflict() ){
 853         return addedLemmas;
 854       }
 855     }
 856   }
 857   return addedLemmas;
 858 }
 859
 860 void InstMatchGeneratorMulti::processNewMatch(QuantifiersEngine* qe,
 861                                               Trigger* tparent,
 862                                               InstMatch& m,
 863                                               int fromChildIndex,
 864                                               int& addedLemmas)
 865 {
 866   //see if these produce new matches
 867   d_children_trie[fromChildIndex].addInstMatch(qe, d_quant, m);
 868   //possibly only do the following if we know that new matches will be produced?
 869   //the issue is that instantiations are filtered in quantifiers engine, and so there is no guarentee that
 870   // we can safely skip the following lines, even when we have already produced this match.
 871   Trace("multi-trigger-cache-debug") << "Child " << fromChildIndex << " produced match " << m << std::endl;
 872   //process new instantiations
 873   int childIndex = (fromChildIndex+1)%(int)d_children.size();
 874   processNewInstantiations(qe,
 875                            tparent,
 876                            m,
 877                            addedLemmas,
 878                            d_children_trie[childIndex].getTrie(),
 879                            0,
 880                            childIndex,
 881                            fromChildIndex,
 882                            true);
 883 }
 884
 885 void InstMatchGeneratorMulti::processNewInstantiations(QuantifiersEngine* qe,
 886                                                        Trigger* tparent,
 887                                                        InstMatch& m,
 888                                                        int& addedLemmas,
 889                                                        InstMatchTrie* tr,
 890                                                        int trieIndex,
 891                                                        int childIndex,
 892                                                        int endChildIndex,
 893                                                        bool modEq)
 894 {
 895   Assert( !qe->inConflict() );
 896   if( childIndex==endChildIndex ){
 897     // m is an instantiation
 898     if (sendInstantiation(tparent, m))
 899     {
 900       addedLemmas++;
 901       Trace("multi-trigger-cache-debug") << "-> Produced instantiation " << m
 902                                          << std::endl;
 903     }
 904   }else if( trieIndex<(int)d_children_trie[childIndex].getOrdering()->d_order.size() ){
 905     int curr_index = d_children_trie[childIndex].getOrdering()->d_order[trieIndex];
 906     // Node curr_ic = qe->getTermUtil()->getInstantiationConstant( d_quant,
 907     // curr_index );
 908     Node n = m.get( curr_index );
 909     if( n.isNull() ){
 910       // add to InstMatch
 911       for (std::pair<const Node, InstMatchTrie>& d : tr->d_data)
 912       {
 913         InstMatch mn(&m);
 914         mn.setValue(curr_index, d.first);
 915         processNewInstantiations(qe,
 916                                  tparent,
 917                                  mn,
 918                                  addedLemmas,
 919                                  &(d.second),
 920                                  trieIndex + 1,
 921                                  childIndex,
 922                                  endChildIndex,
 923                                  modEq);
 924         if (qe->inConflict())
 925         {
 926           break;
 927         }
 928       }
 929     }
 930     // shared and set variable, try to merge
 931     std::map<Node, InstMatchTrie>::iterator it = tr->d_data.find(n);
 932     if (it != tr->d_data.end())
 933     {
 934       processNewInstantiations(qe,
 935                                tparent,
 936                                m,
 937                                addedLemmas,
 938                                &(it->second),
 939                                trieIndex + 1,
 940                                childIndex,
 941                                endChildIndex,
 942                                modEq);
 943     }
 944     if (modEq)
 945     {
 946       // check modulo equality for other possible instantiations
 947       if (qe->getEqualityQuery()->getEngine()->hasTerm(n))
 948       {
 949         eq::EqClassIterator eqc(
 950             qe->getEqualityQuery()->getEngine()->getRepresentative(n),
 951             qe->getEqualityQuery()->getEngine());
 952         while (!eqc.isFinished())
 953         {
 954           Node en = (*eqc);
 955           if (en != n)
 956           {
 957             std::map<Node, InstMatchTrie>::iterator itc = tr->d_data.find(en);
 958             if (itc != tr->d_data.end())
 959             {
 960               processNewInstantiations(qe,
 961                                        tparent,
 962                                        m,
 963                                        addedLemmas,
 964                                        &(itc->second),
 965                                        trieIndex + 1,
 966                                        childIndex,
 967                                        endChildIndex,
 968                                        modEq);
 969               if (qe->inConflict())
 970               {
 971                 break;
 972               }
 973             }
 974           }
 975           ++eqc;
 976         }
 977       }
 978     }
 979   }else{
 980     int newChildIndex = (childIndex+1)%(int)d_children.size();
 981     processNewInstantiations(qe,
 982                              tparent,
 983                              m,
 984                              addedLemmas,
 985                              d_children_trie[newChildIndex].getTrie(),
 986                              0,
 987                              newChildIndex,
 988                              endChildIndex,
 989                              modEq);
 990   }
 991 }
 992
 993 InstMatchGeneratorSimple::InstMatchGeneratorSimple(Node q,
 994                                                    Node pat,
 995                                                    QuantifiersEngine* qe)
 996     : d_quant(q), d_match_pattern(pat)
 997 {
 998   if( d_match_pattern.getKind()==NOT ){
 999     d_match_pattern = d_match_pattern[0];
1000     d_pol = false;
1001   }else{
1002     d_pol = true;
1003   }
1004   if( d_match_pattern.getKind()==EQUAL ){
1005     d_eqc = d_match_pattern[1];
1006     d_match_pattern = d_match_pattern[0];
1007     Assert( !quantifiers::TermUtil::hasInstConstAttr( d_eqc ) );
1008   }
1009   Assert( Trigger::isSimpleTrigger( d_match_pattern ) );
1010   for( unsigned i=0; i<d_match_pattern.getNumChildren(); i++ ){
1011     if( d_match_pattern[i].getKind()==INST_CONSTANT ){
1012       if( !options::cbqi() || quantifiers::TermUtil::getInstConstAttr(d_match_pattern[i])==q ){
1013         d_var_num[i] = d_match_pattern[i].getAttribute(InstVarNumAttribute());
1014       }else{
1015         d_var_num[i] = -1;
1016       }
1017     }
1018     d_match_pattern_arg_types.push_back( d_match_pattern[i].getType() );
1019   }
1020   d_op = qe->getTermDatabase()->getMatchOperator( d_match_pattern );
1021 }
1022
1023 void InstMatchGeneratorSimple::resetInstantiationRound( QuantifiersEngine* qe ) {
1024
1025 }
1026 int InstMatchGeneratorSimple::addInstantiations(Node q,
1027                                                 QuantifiersEngine* qe,
1028                                                 Trigger* tparent)
1029 {
1030   int addedLemmas = 0;
1031   TNodeTrie* tat;
1032   if( d_eqc.isNull() ){
1033     tat = qe->getTermDatabase()->getTermArgTrie( d_op );
1034   }else{
1035     if( d_pol ){
1036       tat = qe->getTermDatabase()->getTermArgTrie( d_eqc, d_op );
1037     }else{
1038       //iterate over all classes except r
1039       tat = qe->getTermDatabase()->getTermArgTrie( Node::null(), d_op );
1040       if (tat && !qe->inConflict())
1041       {
1042         Node r = qe->getEqualityQuery()->getRepresentative(d_eqc);
1043         for (std::pair<const TNode, TNodeTrie>& t : tat->d_data)
1044         {
1045           if (t.first != r)
1046           {
1047             InstMatch m( q );
1048             addInstantiations(m, qe, addedLemmas, 0, &(t.second));
1049             if( qe->inConflict() ){
1050               break;
1051             }
1052           }
1053         }
1054       }
1055       tat = nullptr;
1056     }
1057   }
1058   Debug("simple-trigger-debug") << "Adding instantiations based on " << tat << " from " << d_op << " " << d_eqc << std::endl;
1059   if (tat && !qe->inConflict())
1060   {
1061     InstMatch m( q );
1062     addInstantiations( m, qe, addedLemmas, 0, tat );
1063   }
1064   return addedLemmas;
1065 }
1066
1067 void InstMatchGeneratorSimple::addInstantiations(InstMatch& m,
1068                                                  QuantifiersEngine* qe,
1069                                                  int& addedLemmas,
1070                                                  unsigned argIndex,
1071                                                  TNodeTrie* tat)
1072 {
1073   Debug("simple-trigger-debug") << "Add inst " << argIndex << " " << d_match_pattern << std::endl;
1074   if (argIndex == d_match_pattern.getNumChildren())
1075   {
1076     Assert( !tat->d_data.empty() );
1077     TNode t = tat->getData();
1078     Debug("simple-trigger") << "Actual term is " << t << std::endl;
1079     //convert to actual used terms
1080     for (std::map<unsigned, int>::iterator it = d_var_num.begin();
1081          it != d_var_num.end();
1082          ++it)
1083     {
1084       if( it->second>=0 ){
1085         Assert(it->first < t.getNumChildren());
1086         Debug("simple-trigger") << "...set " << it->second << " " << t[it->first] << std::endl;
1087         m.setValue( it->second, t[it->first] );
1088       }
1089     }
1090     // we do not need the trigger parent for simple triggers (no post-processing
1091     // required)
1092     if (qe->getInstantiate()->addInstantiation(d_quant, m))
1093     {
1094       addedLemmas++;
1095       Debug("simple-trigger") << "-> Produced instantiation " << m << std::endl;
1096     }
1097   }else{
1098     if( d_match_pattern[argIndex].getKind()==INST_CONSTANT ){
1099       int v = d_var_num[argIndex];
1100       if( v!=-1 ){
1101         for (std::pair<const TNode, TNodeTrie>& tt : tat->d_data)
1102         {
1103           Node t = tt.first;
1104           Node prev = m.get( v );
1105           //using representatives, just check if equal
1106           Assert( t.getType().isComparableTo( d_match_pattern_arg_types[argIndex] ) );
1107           if( prev.isNull() || prev==t ){
1108             m.setValue( v, t);
1109             addInstantiations(m, qe, addedLemmas, argIndex + 1, &(tt.second));
1110             m.setValue( v, prev);
1111             if( qe->inConflict() ){
1112               break;
1113             }
1114           }
1115         }
1116         return;
1117       }
1118       //inst constant from another quantified formula, treat as ground term  TODO: remove this?
1119     }
1120     Node r = qe->getEqualityQuery()->getRepresentative( d_match_pattern[argIndex] );
1121     std::map<TNode, TNodeTrie>::iterator it = tat->d_data.find(r);
1122     if( it!=tat->d_data.end() ){
1123       addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) );
1124     }
1125   }
1126 }
1127
1128 int InstMatchGeneratorSimple::getActiveScore( QuantifiersEngine * qe ) {
1129   Node f = qe->getTermDatabase()->getMatchOperator( d_match_pattern );
1130   unsigned ngt = qe->getTermDatabase()->getNumGroundTerms( f );
1131   Trace("trigger-active-sel-debug") << "Number of ground terms for (simple) " << f << " is " << ngt << std::endl;
1132   return ngt;
1133 }
1134
1135
1136 }/* CVC4::theory::inst namespace */
1137 }/* CVC4::theory namespace */
1138 }/* CVC4 namespace */