GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/ematching/inst_match_generator.cpp Lines: 291 342 85.1 %
Date: 2021-03-22 Branches: 590 1382 42.7 %

Line Exec Source
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-2021 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 inst match generator class
13
 **/
14
15
#include "theory/quantifiers/ematching/inst_match_generator.h"
16
17
#include "expr/dtype_cons.h"
18
#include "options/quantifiers_options.h"
19
#include "theory/datatypes/theory_datatypes_utils.h"
20
#include "theory/quantifiers/ematching/candidate_generator.h"
21
#include "theory/quantifiers/ematching/inst_match_generator_multi.h"
22
#include "theory/quantifiers/ematching/inst_match_generator_multi_linear.h"
23
#include "theory/quantifiers/ematching/inst_match_generator_simple.h"
24
#include "theory/quantifiers/ematching/pattern_term_selector.h"
25
#include "theory/quantifiers/ematching/var_match_generator.h"
26
#include "theory/quantifiers/instantiate.h"
27
#include "theory/quantifiers/quantifiers_state.h"
28
#include "theory/quantifiers/term_database.h"
29
#include "theory/quantifiers/term_util.h"
30
#include "theory/quantifiers_engine.h"
31
32
using namespace CVC4::kind;
33
34
namespace CVC4 {
35
namespace theory {
36
namespace inst {
37
38
33906
InstMatchGenerator::InstMatchGenerator(Trigger* tparent, Node pat)
39
33906
    : IMGenerator(tparent)
40
{
41
33906
  d_cg = nullptr;
42
33906
  d_needsReset = true;
43
33906
  d_active_add = true;
44
33906
  Assert(pat.isNull() || quantifiers::TermUtil::hasInstConstAttr(pat));
45
33906
  d_pattern = pat;
46
33906
  d_match_pattern = pat;
47
33906
  if (!pat.isNull())
48
  {
49
32673
    d_match_pattern_type = pat.getType();
50
  }
51
33906
  d_next = nullptr;
52
33906
  d_independent_gen = false;
53
33906
}
54
55
100485
InstMatchGenerator::~InstMatchGenerator()
56
{
57
58829
  for( unsigned i=0; i<d_children.size(); i++ ){
58
24923
    delete d_children[i];
59
  }
60
33906
  delete d_cg;
61
66579
}
62
63
144
void InstMatchGenerator::setActiveAdd(bool val){
64
144
  d_active_add = val;
65
144
  if (d_next != nullptr)
66
  {
67
108
    d_next->setActiveAdd(val);
68
  }
69
144
}
70
71
int InstMatchGenerator::getActiveScore()
72
{
73
  if( d_match_pattern.isNull() ){
74
    return -1;
75
  }
76
  quantifiers::TermDb* tdb = getQuantifiersEngine()->getTermDatabase();
77
  if (TriggerTermInfo::isAtomicTrigger(d_match_pattern))
78
  {
79
    Node f = tdb->getMatchOperator(d_match_pattern);
80
    unsigned ngt = tdb->getNumGroundTerms(f);
81
    Trace("trigger-active-sel-debug") << "Number of ground terms for " << f << " is " << ngt << std::endl;
82
    return ngt;
83
  }else if( d_match_pattern.getKind()==INST_CONSTANT ){
84
    TypeNode tn = d_match_pattern.getType();
85
    unsigned ngtt = tdb->getNumTypeGroundTerms(tn);
86
    Trace("trigger-active-sel-debug") << "Number of ground terms for " << tn << " is " << ngtt << std::endl;
87
    return ngtt;
88
  }
89
  return -1;
90
}
91
92
33906
void InstMatchGenerator::initialize(Node q,
93
                                    std::vector<InstMatchGenerator*>& gens)
94
{
95
33906
  if (d_pattern.isNull())
96
  {
97
1233
    gens.insert(gens.end(), d_children.begin(), d_children.end());
98
1233
    return;
99
  }
100
65346
  Trace("inst-match-gen") << "Initialize, pattern term is " << d_pattern
101
32673
                          << std::endl;
102
32673
  if (d_match_pattern.getKind() == NOT)
103
  {
104
2121
    Assert(d_pattern.getKind() == NOT);
105
    // we want to add the children of the NOT
106
2121
    d_match_pattern = d_match_pattern[0];
107
  }
108
109
67467
  if (d_pattern.getKind() == NOT && d_match_pattern.getKind() == EQUAL
110
34794
      && d_match_pattern[0].getKind() == INST_CONSTANT
111
65398
      && d_match_pattern[1].getKind() == INST_CONSTANT)
112
  {
113
    // special case: disequalities between variables x != y will match ground
114
    // disequalities.
115
  }
116
65332
  else if (d_match_pattern.getKind() == EQUAL
117
32666
           || d_match_pattern.getKind() == GEQ)
118
  {
119
    // We are one of the following cases:
120
    //   f(x)~a, f(x)~y, x~a, x~y
121
    // If we are the first or third case, we ensure that f(x)/x is on the left
122
    // hand side of the relation d_pattern, d_match_pattern is f(x)/x and
123
    // d_eq_class_rel (indicating the equivalence class that we are related
124
    // to) is set to a.
125
2144
    for (size_t i = 0; i < 2; i++)
126
    {
127
2152
      Node mp = d_match_pattern[i];
128
2152
      Node mpo = d_match_pattern[1 - i];
129
      // If this side has free variables, and the other side does not or
130
      // it is a free variable, then we will match on this side of the
131
      // relation.
132
6432
      if (quantifiers::TermUtil::hasInstConstAttr(mp)
133
8568
          && (!quantifiers::TermUtil::hasInstConstAttr(mpo)
134
19
              || mpo.getKind() == INST_CONSTANT))
135
      {
136
2136
        if (i == 1)
137
        {
138
8
          if (d_match_pattern.getKind() == GEQ)
139
          {
140
            d_pattern = NodeManager::currentNM()->mkNode(kind::GT, mp, mpo);
141
            d_pattern = d_pattern.negate();
142
          }
143
          else
144
          {
145
16
            d_pattern = NodeManager::currentNM()->mkNode(
146
8
                d_match_pattern.getKind(), mp, mpo);
147
          }
148
        }
149
2136
        d_eq_class_rel = mpo;
150
2136
        d_match_pattern = mp;
151
        // we won't find a term in the other direction
152
2136
        break;
153
      }
154
    }
155
  }
156
32673
  d_match_pattern_type = d_match_pattern.getType();
157
65346
  Trace("inst-match-gen") << "Pattern is " << d_pattern << ", match pattern is "
158
32673
                          << d_match_pattern << std::endl;
159
32673
  quantifiers::TermDb* tdb = getQuantifiersEngine()->getTermDatabase();
160
32673
  d_match_pattern_op = tdb->getMatchOperator(d_match_pattern);
161
162
  // now, collect children of d_match_pattern
163
32673
  Kind mpk = d_match_pattern.getKind();
164
32673
  if (mpk == INST_CONSTANT)
165
  {
166
142
    d_children_types.push_back(
167
142
        d_match_pattern.getAttribute(InstVarNumAttribute()));
168
  }
169
  else
170
  {
171
93773
    for (size_t i = 0, size = d_match_pattern.getNumChildren(); i < size; i++)
172
    {
173
122342
      Node pat = d_match_pattern[i];
174
122342
      Node qa = quantifiers::TermUtil::getInstConstAttr(pat);
175
61171
      if (!qa.isNull())
176
      {
177
53740
        if (pat.getKind() == INST_CONSTANT && qa == q)
178
        {
179
31573
          d_children_types.push_back(pat.getAttribute(InstVarNumAttribute()));
180
        }
181
        else
182
        {
183
22167
          InstMatchGenerator* cimg = getInstMatchGenerator(d_tparent, q, pat);
184
22167
          if (cimg)
185
          {
186
22167
            d_children.push_back(cimg);
187
22167
            d_children_index.push_back(i);
188
22167
            d_children_types.push_back(-2);
189
          }
190
          else
191
          {
192
            d_children_types.push_back(-1);
193
          }
194
        }
195
      }
196
      else
197
      {
198
7431
        d_children_types.push_back(-1);
199
      }
200
    }
201
  }
202
203
32673
  QuantifiersEngine* qe = getQuantifiersEngine();
204
  // create candidate generator
205
32673
  if (mpk == APPLY_SELECTOR)
206
  {
207
    // candidates for apply selector are a union of correctly and incorrectly
208
    // applied selectors
209
159
    d_cg = new inst::CandidateGeneratorSelector(qe, d_match_pattern);
210
  }
211
32514
  else if (TriggerTermInfo::isAtomicTriggerKind(mpk))
212
  {
213
32436
    if (mpk == APPLY_CONSTRUCTOR)
214
    {
215
      // 1-constructors have a trivial way of generating candidates in a
216
      // given equivalence class
217
2388
      const DType& dt = d_match_pattern.getType().getDType();
218
2388
      if (dt.getNumConstructors() == 1)
219
      {
220
2210
        d_cg = new inst::CandidateGeneratorConsExpand(qe, d_match_pattern);
221
      }
222
    }
223
32436
    if (d_cg == nullptr)
224
    {
225
30226
      CandidateGeneratorQE* cg = new CandidateGeneratorQE(qe, d_match_pattern);
226
      // we will be scanning lists trying to find ground terms whose operator
227
      // is the same as d_match_operator's.
228
30226
      d_cg = cg;
229
      // if matching on disequality, inform the candidate generator not to
230
      // match on eqc
231
30226
      if (d_pattern.getKind() == NOT && d_pattern[0].getKind() == EQUAL)
232
      {
233
2069
        cg->excludeEqc(d_eq_class_rel);
234
2069
        d_eq_class_rel = Node::null();
235
      }
236
    }
237
  }
238
78
  else if (mpk == INST_CONSTANT)
239
  {
240
71
    if (d_pattern.getKind() == APPLY_SELECTOR_TOTAL)
241
    {
242
      Node selectorExpr = tdb->getMatchOperator(d_pattern);
243
      size_t selectorIndex = datatypes::utils::cindexOf(selectorExpr);
244
      const DType& dt = datatypes::utils::datatypeOf(selectorExpr);
245
      const DTypeConstructor& c = dt[selectorIndex];
246
      Node cOp = c.getConstructor();
247
      Trace("inst-match-gen")
248
          << "Purify dt trigger " << d_pattern << ", will match terms of op "
249
          << cOp << std::endl;
250
      d_cg = new inst::CandidateGeneratorQE(qe, cOp);
251
    }else{
252
71
      d_cg = new CandidateGeneratorQEAll(qe, d_match_pattern);
253
    }
254
  }
255
7
  else if (mpk == EQUAL)
256
  {
257
    // we will be producing candidates via literal matching heuristics
258
7
    if (d_pattern.getKind() == NOT)
259
    {
260
      // candidates will be all disequalities
261
7
      d_cg = new inst::CandidateGeneratorQELitDeq(qe, d_match_pattern);
262
    }
263
  }
264
  else
265
  {
266
    Trace("inst-match-gen-warn")
267
        << "(?) Unknown matching pattern is " << d_match_pattern << std::endl;
268
  }
269
32673
  gens.insert( gens.end(), d_children.begin(), d_children.end() );
270
}
271
272
/** get match (not modulo equality) */
273
2618564
int InstMatchGenerator::getMatch(Node f, Node t, InstMatch& m)
274
{
275
5237128
  Trace("matching") << "Matching " << t << " against pattern " << d_match_pattern << " ("
276
2618564
                    << m << ")" << ", " << d_children.size() << ", pattern is " << d_pattern << std::endl;
277
2618564
  Assert(!d_match_pattern.isNull());
278
2618564
  if (d_cg == nullptr)
279
  {
280
    Trace("matching-fail") << "Internal error for match generator." << std::endl;
281
    return -2;
282
  }
283
2618564
  bool success = true;
284
5237128
  std::vector<int> prev;
285
  // if t is null
286
2618564
  Assert(!t.isNull());
287
2618564
  Assert(!quantifiers::TermUtil::hasInstConstAttr(t));
288
  // notice that t may have a different kind or operator from our match
289
  // pattern, e.g. for APPLY_SELECTOR triggers.
290
  // first, check if ground arguments are not equal, or a match is in conflict
291
2618564
  Trace("matching-debug2") << "Setting immediate matches..." << std::endl;
292
3823093
  for (size_t i = 0, size = d_match_pattern.getNumChildren(); i < size; i++)
293
  {
294
3350753
    int64_t ct = d_children_types[i];
295
3350753
    if (ct >= 0)
296
    {
297
4150936
      Trace("matching-debug2")
298
2075468
          << "Setting " << ct << " to " << t[i] << "..." << std::endl;
299
2075468
      bool addToPrev = m.get(ct).isNull();
300
2075468
      if (!m.set(d_qstate, ct, t[i]))
301
      {
302
        // match is in conflict
303
2643632
        Trace("matching-fail")
304
1321816
            << "Match fail: " << m.get(ct) << " and " << t[i] << std::endl;
305
1321816
        success = false;
306
3468040
        break;
307
      }
308
753652
      else if (addToPrev)
309
      {
310
705069
        Trace("matching-debug2") << "Success." << std::endl;
311
705069
        prev.push_back(ct);
312
      }
313
    }
314
1275285
    else if (ct == -1)
315
    {
316
855629
      if (!d_qstate.areEqual(d_match_pattern[i], t[i]))
317
      {
318
1648816
        Trace("matching-fail") << "Match fail arg: " << d_match_pattern[i]
319
824408
                               << " and " << t[i] << std::endl;
320
        // ground arguments are not equal
321
824408
        success = false;
322
824408
        break;
323
      }
324
    }
325
  }
326
5237128
  Trace("matching-debug2") << "Done setting immediate matches, success = "
327
2618564
                           << success << "." << std::endl;
328
  // for variable matching
329
2618564
  if (d_match_pattern.getKind() == INST_CONSTANT)
330
  {
331
102
    bool addToPrev = m.get(d_children_types[0]).isNull();
332
102
    if (!m.set(d_qstate, d_children_types[0], t))
333
    {
334
      success = false;
335
    }
336
    else
337
    {
338
102
      if (addToPrev)
339
      {
340
102
        prev.push_back(d_children_types[0]);
341
      }
342
    }
343
  }
344
  // for relational matching
345
2618564
  if (!d_eq_class_rel.isNull() && d_eq_class_rel.getKind() == INST_CONSTANT)
346
  {
347
28
    NodeManager* nm = NodeManager::currentNM();
348
28
    int v = d_eq_class_rel.getAttribute(InstVarNumAttribute());
349
    // also must fit match to equivalence class
350
28
    bool pol = d_pattern.getKind() != NOT;
351
56
    Node pat = d_pattern.getKind() == NOT ? d_pattern[0] : d_pattern;
352
56
    Node t_match;
353
28
    if (pol)
354
    {
355
28
      if (pat.getKind() == GT)
356
      {
357
        t_match = nm->mkNode(MINUS, t, nm->mkConst(Rational(1)));
358
      }else{
359
28
        t_match = t;
360
      }
361
    }
362
    else
363
    {
364
      if (pat.getKind() == EQUAL)
365
      {
366
        if (t.getType().isBoolean())
367
        {
368
          t_match = nm->mkConst(!d_qstate.areEqual(nm->mkConst(true), t));
369
        }
370
        else
371
        {
372
          Assert(t.getType().isReal());
373
          t_match = nm->mkNode(PLUS, t, nm->mkConst(Rational(1)));
374
        }
375
      }
376
      else if (pat.getKind() == GEQ)
377
      {
378
        t_match = nm->mkNode(PLUS, t, nm->mkConst(Rational(1)));
379
      }
380
      else if (pat.getKind() == GT)
381
      {
382
        t_match = t;
383
      }
384
    }
385
28
    if (!t_match.isNull())
386
    {
387
28
      bool addToPrev = m.get(v).isNull();
388
28
      if (!m.set(d_qstate, v, t_match))
389
      {
390
        success = false;
391
      }
392
28
      else if (addToPrev)
393
      {
394
28
        prev.push_back(v);
395
      }
396
    }
397
  }
398
2618564
  int ret_val = -1;
399
2618564
  if (success)
400
  {
401
472340
    Trace("matching-debug2") << "Reset children..." << std::endl;
402
    // now, fit children into match
403
    // we will be requesting candidates for matching terms for each child
404
591517
    for (size_t i = 0, size = d_children.size(); i < size; i++)
405
    {
406
371142
      if (!d_children[i]->reset(t[d_children_index[i]]))
407
      {
408
251965
        success = false;
409
251965
        break;
410
      }
411
    }
412
472340
    if (success)
413
    {
414
220375
      Trace("matching-debug2") << "Continue next " << d_next << std::endl;
415
220375
      ret_val =
416
440750
          continueNextMatch(f, m, InferenceId::QUANTIFIERS_INST_E_MATCHING);
417
    }
418
  }
419
2618564
  if (ret_val < 0)
420
  {
421
3254768
    for (int& pv : prev)
422
    {
423
667540
      m.d_vals[pv] = Node::null();
424
    }
425
  }
426
2618564
  return ret_val;
427
}
428
429
224908
int InstMatchGenerator::continueNextMatch(Node q,
430
                                          InstMatch& m,
431
                                          InferenceId id)
432
{
433
224908
  if( d_next!=NULL ){
434
151316
    return d_next->getNextMatch(q, m);
435
  }
436
73592
  if (d_active_add)
437
  {
438
70378
    return sendInstantiation(m, id) ? 1 : -1;
439
  }
440
3214
  return 1;
441
}
442
443
/** reset instantiation round */
444
222490
void InstMatchGenerator::resetInstantiationRound()
445
{
446
222490
  if( !d_match_pattern.isNull() ){
447
214077
    Trace("matching-debug2") << this << " reset instantiation round." << std::endl;
448
214077
    d_needsReset = true;
449
214077
    if( d_cg ){
450
214077
      d_cg->resetInstantiationRound();
451
    }
452
  }
453
222490
  if( d_next ){
454
154144
    d_next->resetInstantiationRound();
455
  }
456
222490
  d_curr_exclude_match.clear();
457
222490
}
458
459
589564
bool InstMatchGenerator::reset(Node eqc)
460
{
461
589564
  if (d_cg == nullptr)
462
  {
463
    // we did not properly initialize the candidate generator, thus we fail
464
    return false;
465
  }
466
589564
  eqc = d_qstate.getRepresentative(eqc);
467
589564
  Trace("matching-debug2") << this << " reset " << eqc << "." << std::endl;
468
589564
  if( !d_eq_class_rel.isNull() && d_eq_class_rel.getKind()!=INST_CONSTANT ){
469
112
    d_eq_class = d_eq_class_rel;
470
589452
  }else if( !eqc.isNull() ){
471
472443
    d_eq_class = eqc;
472
  }
473
  //we have a specific equivalence class in mind
474
  //we are producing matches for f(E) ~ t, where E is a non-ground vector of terms, and t is a ground term
475
  //just look in equivalence class of the RHS
476
589564
  d_cg->reset( d_eq_class );
477
589564
  d_needsReset = false;
478
479
  //generate the first candidate preemptively
480
589564
  d_curr_first_candidate = Node::null();
481
1179128
  Node t;
482
147509
  do {
483
737073
    t = d_cg->getNextCandidate();
484
737073
    if( d_curr_exclude_match.find( t )==d_curr_exclude_match.end() ){
485
589564
      d_curr_first_candidate = t;
486
    }
487
737073
  }while( !t.isNull() && d_curr_first_candidate.isNull() );
488
589564
  Trace("matching-summary") << "Reset " << d_match_pattern << " in " << eqc << " returns " << !d_curr_first_candidate.isNull() << "." << std::endl;
489
490
589564
  return !d_curr_first_candidate.isNull();
491
}
492
493
177739
int InstMatchGenerator::getNextMatch(Node f, InstMatch& m)
494
{
495
177739
  if( d_needsReset ){
496
    Trace("matching") << "Reset not done yet, must do the reset..." << std::endl;
497
    reset(d_eq_class);
498
  }
499
177739
  d_curr_matched = Node::null();
500
177739
  Trace("matching") << this << " " << d_match_pattern << " get next match " << m << " in eq class " << d_eq_class << std::endl;
501
177739
  int success = -1;
502
355478
  Node t = d_curr_first_candidate;
503
2543225
  do{
504
2720964
    Trace("matching-debug2") << "Matching candidate : " << t << std::endl;
505
2720964
    Assert(!d_qstate.isInConflict());
506
    //if t not null, try to fit it into match m
507
2720964
    if( !t.isNull() ){
508
2710695
      if( d_curr_exclude_match.find( t )==d_curr_exclude_match.end() ){
509
2618564
        Assert(t.getType().isComparableTo(d_match_pattern_type));
510
2618564
        Trace("matching-summary") << "Try " << d_match_pattern << " : " << t << std::endl;
511
2618564
        success = getMatch(f, t, m);
512
2618564
        if( d_independent_gen && success<0 ){
513
26848
          Assert(d_eq_class.isNull() || !d_eq_class_rel.isNull());
514
26848
          d_curr_exclude_match[t] = true;
515
        }
516
      }
517
      //get the next candidate term t
518
2710695
      if( success<0 ){
519
2679359
        t = d_qstate.isInConflict() ? Node::null() : d_cg->getNextCandidate();
520
      }else{
521
31336
        d_curr_first_candidate = d_cg->getNextCandidate();
522
      }
523
    }
524
2720964
  }while( success<0 && !t.isNull() );
525
177739
  d_curr_matched = t;
526
177739
  if( success<0 ){
527
146403
    Trace("matching-summary") << "..." << d_match_pattern << " failed, reset." << std::endl;
528
146403
    Trace("matching") << this << " failed, reset " << d_eq_class << std::endl;
529
    //we failed, must reset
530
146403
    reset(d_eq_class);
531
  }else{
532
31336
    Trace("matching-summary") << "..." << d_match_pattern << " success." << std::endl;
533
  }
534
355478
  return success;
535
}
536
537
20362
uint64_t InstMatchGenerator::addInstantiations(Node f)
538
{
539
  //try to add instantiation for each match produced
540
20362
  uint64_t addedLemmas = 0;
541
40724
  InstMatch m( f );
542
38806
  while (getNextMatch(f, m) > 0)
543
  {
544
9222
    if( !d_active_add ){
545
      if (sendInstantiation(m, InferenceId::UNKNOWN))
546
      {
547
        addedLemmas++;
548
        if (d_qstate.isInConflict())
549
        {
550
          break;
551
        }
552
      }
553
    }else{
554
9222
      addedLemmas++;
555
9222
      if (d_qstate.isInConflict())
556
      {
557
        break;
558
      }
559
    }
560
9222
    m.clear();
561
  }
562
  //return number of lemmas added
563
40724
  return addedLemmas;
564
}
565
566
7758
InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator(Trigger* tparent,
567
                                                             Node q,
568
                                                             Node pat)
569
{
570
15516
  std::vector< Node > pats;
571
7758
  pats.push_back( pat );
572
15516
  std::map< Node, InstMatchGenerator * > pat_map_init;
573
15516
  return mkInstMatchGenerator(tparent, q, pats, pat_map_init);
574
}
575
576
1225
InstMatchGenerator* InstMatchGenerator::mkInstMatchGeneratorMulti(
577
    Trigger* tparent, Node q, std::vector<Node>& pats)
578
{
579
1225
  Assert(pats.size() > 1);
580
  InstMatchGeneratorMultiLinear* imgm =
581
1225
      new InstMatchGeneratorMultiLinear(tparent, q, pats);
582
2450
  std::vector< InstMatchGenerator* > gens;
583
1225
  imgm->initialize(q, gens);
584
1225
  Assert(gens.size() == pats.size());
585
2450
  std::vector< Node > patsn;
586
2450
  std::map< Node, InstMatchGenerator * > pat_map_init;
587
3981
  for (InstMatchGenerator* g : gens)
588
  {
589
5512
    Node pn = g->d_match_pattern;
590
2756
    patsn.push_back( pn );
591
2756
    pat_map_init[pn] = g;
592
  }
593
1225
  imgm->d_next = mkInstMatchGenerator(tparent, q, patsn, pat_map_init);
594
2450
  return imgm;
595
}
596
597
8983
InstMatchGenerator* InstMatchGenerator::mkInstMatchGenerator(
598
    Trigger* tparent,
599
    Node q,
600
    std::vector<Node>& pats,
601
    std::map<Node, InstMatchGenerator*>& pat_map_init)
602
{
603
8983
  size_t pCounter = 0;
604
8983
  InstMatchGenerator* prev = NULL;
605
8983
  InstMatchGenerator* oinit = NULL;
606
30011
  while( pCounter<pats.size() ){
607
10514
    size_t counter = 0;
608
21028
    std::vector< InstMatchGenerator* > gens;
609
    InstMatchGenerator* init;
610
10514
    std::map< Node, InstMatchGenerator * >::iterator iti = pat_map_init.find( pats[pCounter] );
611
10514
    if( iti==pat_map_init.end() ){
612
7758
      init = new InstMatchGenerator(tparent, pats[pCounter]);
613
    }else{
614
2756
      init = iti->second;
615
    }
616
10514
    if(pCounter==0){
617
8983
      oinit = init;
618
    }
619
10514
    gens.push_back(init);
620
    //chain the resulting match generators together
621
75876
    while (counter<gens.size()) {
622
32681
      InstMatchGenerator* curr = gens[counter];
623
32681
      if( prev ){
624
23698
        prev->d_next = curr;
625
      }
626
32681
      curr->initialize(q, gens);
627
32681
      prev = curr;
628
32681
      counter++;
629
    }
630
10514
    pCounter++;
631
  }
632
8983
  return oinit;
633
}
634
635
24923
InstMatchGenerator* InstMatchGenerator::getInstMatchGenerator(Trigger* tparent,
636
                                                              Node q,
637
                                                              Node n)
638
{
639
24923
  if (n.getKind() != INST_CONSTANT)
640
  {
641
49838
    Trace("var-trigger-debug")
642
24919
        << "Is " << n << " a variable trigger?" << std::endl;
643
49830
    Node x;
644
24919
    if (options::purifyTriggers())
645
    {
646
136
      Node xi = PatternTermSelector::getInversionVariable(n);
647
68
      if (!xi.isNull())
648
      {
649
16
        Node qa = quantifiers::TermUtil::getInstConstAttr(xi);
650
8
        if (qa == q)
651
        {
652
8
          x = xi;
653
        }
654
      }
655
    }
656
24919
    if (!x.isNull())
657
    {
658
16
      Node s = PatternTermSelector::getInversion(n, x);
659
      VarMatchGeneratorTermSubs* vmg =
660
8
          new VarMatchGeneratorTermSubs(tparent, x, s);
661
16
      Trace("var-trigger") << "Term substitution trigger : " << n
662
8
                           << ", var = " << x << ", subs = " << s << std::endl;
663
8
      return vmg;
664
    }
665
  }
666
24915
  return new InstMatchGenerator(tparent, n);
667
}
668
669
}/* CVC4::theory::inst namespace */
670
}/* CVC4::theory namespace */
671
26676
}/* CVC4 namespace */