GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/ematching/inst_strategy_e_matching.cpp Lines: 265 352 75.3 %
Date: 2021-03-23 Branches: 494 1337 36.9 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file inst_strategy_e_matching.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Morgan Deters, Mathias Preiner
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 e matching instantiation strategies
13
 **/
14
15
#include "theory/quantifiers/ematching/inst_strategy_e_matching.h"
16
17
#include "theory/quantifiers/ematching/pattern_term_selector.h"
18
#include "theory/quantifiers/quant_relevance.h"
19
#include "theory/quantifiers/quantifiers_inference_manager.h"
20
#include "theory/quantifiers/quantifiers_registry.h"
21
#include "theory/quantifiers/quantifiers_state.h"
22
#include "theory/quantifiers_engine.h"
23
#include "util/random.h"
24
25
using namespace CVC4::kind;
26
using namespace CVC4::theory::inst;
27
28
namespace CVC4 {
29
namespace theory {
30
namespace quantifiers {
31
32
//priority levels :
33
//1 : user patterns (when user-pat!={resort,ignore}), auto-gen patterns (for non-user pattern quantifiers, or when user-pat={resort,ignore})
34
//2 : user patterns (when user-pat=resort), auto gen patterns (for user pattern quantifiers when user-pat=use)
35
36
// user-pat=interleave alternates between use and resort
37
38
6296
struct sortQuantifiersForSymbol {
39
  QuantRelevance* d_quant_rel;
40
  std::map< Node, Node > d_op_map;
41
596
  bool operator() (Node i, Node j) {
42
596
    size_t nqfsi = d_quant_rel->getNumQuantifiersForSymbol(d_op_map[i]);
43
596
    size_t nqfsj = d_quant_rel->getNumQuantifiersForSymbol(d_op_map[j]);
44
596
    if( nqfsi<nqfsj ){
45
      return true;
46
596
    }else if( nqfsi>nqfsj ){
47
      return false;
48
    }
49
596
    return false;
50
  }
51
};
52
53
struct sortTriggers {
54
5273
  bool operator() (Node i, Node j) {
55
5273
    int32_t wi = TriggerTermInfo::getTriggerWeight(i);
56
5273
    int32_t wj = TriggerTermInfo::getTriggerWeight(j);
57
5273
    if( wi==wj ){
58
4369
      return i<j;
59
    }
60
904
    return wi < wj;
61
  }
62
};
63
64
5825
InstStrategyAutoGenTriggers::InstStrategyAutoGenTriggers(
65
    QuantifiersEngine* qe,
66
    QuantifiersState& qs,
67
    QuantifiersInferenceManager& qim,
68
    QuantifiersRegistry& qr,
69
5825
    QuantRelevance* qrlv)
70
5825
    : InstStrategy(qe, qs, qim, qr), d_quant_rel(qrlv)
71
{
72
  //how to select trigger terms
73
11650
  d_tr_strategy = options::triggerSelMode();
74
  //whether to select new triggers during the search
75
11650
  if( options::incrementTriggers() ){
76
5825
    d_regenerate_frequency = 3;
77
5825
    d_regenerate = true;
78
  }else{
79
    d_regenerate_frequency = 1;
80
    d_regenerate = false;
81
  }
82
5825
}
83
84
24179
void InstStrategyAutoGenTriggers::processResetInstantiationRound( Theory::Effort effort ){
85
24179
  Trace("inst-alg-debug") << "reset auto-gen triggers" << std::endl;
86
  //reset triggers
87
72537
  for( unsigned r=0; r<2; r++ ){
88
48358
    std::map<Node, std::map<inst::Trigger*, bool> >& agts =
89
        d_auto_gen_trigger[r];
90
175602
    for (std::pair<const Node, std::map<inst::Trigger*, bool> >& agt : agts)
91
    {
92
202997
      for (std::map<inst::Trigger*, bool>::iterator it = agt.second.begin();
93
202997
           it != agt.second.end();
94
           ++it)
95
      {
96
75753
        it->first->resetInstantiationRound();
97
75753
        it->first->reset(Node::null());
98
      }
99
    }
100
  }
101
24179
  d_processed_trigger.clear();
102
24179
  Trace("inst-alg-debug") << "done reset auto-gen triggers" << std::endl;
103
24179
}
104
105
80632
InstStrategyStatus InstStrategyAutoGenTriggers::process(Node f,
106
                                                        Theory::Effort effort,
107
                                                        int e)
108
{
109
80632
  options::UserPatMode upMode = getInstUserPatMode();
110
80632
  if (hasUserPatterns(f) && upMode == options::UserPatMode::TRUST)
111
  {
112
25422
    return InstStrategyStatus::STATUS_UNKNOWN;
113
  }
114
165630
  int peffort = (hasUserPatterns(f) && upMode != options::UserPatMode::IGNORE
115
                 && upMode != options::UserPatMode::RESORT)
116
165630
                    ? 2
117
55210
                    : 1;
118
55210
  if (e < peffort)
119
  {
120
27605
    return InstStrategyStatus::STATUS_UNFINISHED;
121
  }
122
27605
  Trace("inst-alg") << "-> Auto-gen instantiate " << f << "..." << std::endl;
123
27605
  bool gen = false;
124
27605
  if (e == peffort)
125
  {
126
27605
    if (d_counter.find(f) == d_counter.end())
127
    {
128
10560
      d_counter[f] = 0;
129
10560
      gen = true;
130
    }else{
131
17045
      d_counter[f]++;
132
17045
      gen = d_regenerate && d_counter[f] % d_regenerate_frequency == 0;
133
    }
134
  }
135
  else
136
  {
137
    gen = true;
138
  }
139
27605
  if (gen)
140
  {
141
13604
    generateTriggers(f);
142
37768
    if (d_counter[f] == 0 && d_auto_gen_trigger[0][f].empty()
143
15690
        && d_auto_gen_trigger[1][f].empty() && f.getNumChildren() == 2)
144
    {
145
1075
      Trace("trigger-warn") << "Could not find trigger for " << f << std::endl;
146
    }
147
  }
148
55210
  if (options::triggerActiveSelMode() != options::TriggerActiveSelMode::ALL)
149
  {
150
    int max_score = -1;
151
    Trigger* max_trigger = nullptr;
152
    std::map<Trigger*, bool>& agt = d_auto_gen_trigger[0][f];
153
    for (std::map<Trigger*, bool>::iterator it = agt.begin(); it != agt.end();
154
         ++it)
155
    {
156
      Trigger* t = it->first;
157
      int score = t->getActiveScore();
158
      if (options::triggerActiveSelMode() == options::TriggerActiveSelMode::MIN)
159
      {
160
        if (score >= 0 && (score < max_score || max_score < 0))
161
        {
162
          max_score = score;
163
          max_trigger = t;
164
        }
165
      }
166
      else
167
      {
168
        if (score > max_score)
169
        {
170
          max_score = score;
171
          max_trigger = t;
172
        }
173
      }
174
      agt[t] = false;
175
    }
176
    if (max_trigger != nullptr)
177
    {
178
      agt[max_trigger] = true;
179
    }
180
  }
181
182
27605
  bool hasInst = false;
183
82815
  for (unsigned r = 0; r < 2; r++)
184
  {
185
55210
    std::map<Trigger*, bool>& agt = d_auto_gen_trigger[r][f];
186
88915
    for (std::map<Trigger*, bool>::iterator it = agt.begin(); it != agt.end();
187
         ++it)
188
    {
189
33705
      Trigger* tr = it->first;
190
33705
      if (tr == nullptr || !it->second)
191
      {
192
        // trigger is null or currently disabled
193
244
        continue;
194
      }
195
33583
      if (d_processed_trigger[f].find(tr) != d_processed_trigger[f].end())
196
      {
197
        // trigger is already processed this round
198
        continue;
199
      }
200
33583
      d_processed_trigger[f][tr] = true;
201
33583
      Trace("process-trigger") << "  Process ";
202
33583
      tr->debugPrint("process-trigger");
203
33583
      Trace("process-trigger") << "..." << std::endl;
204
33583
      unsigned numInst = tr->addInstantiations();
205
33583
      hasInst = numInst > 0 || hasInst;
206
67166
      Trace("process-trigger")
207
33583
          << "  Done, numInst = " << numInst << "." << std::endl;
208
33583
      if (d_qstate.isInConflict())
209
      {
210
        break;
211
      }
212
    }
213
63843
    if (d_qstate.isInConflict() || (hasInst && options::multiTriggerPriority()))
214
    {
215
      break;
216
    }
217
  }
218
27605
  return InstStrategyStatus::STATUS_UNKNOWN;
219
}
220
221
13604
void InstStrategyAutoGenTriggers::generateTriggers( Node f ){
222
13604
  Trace("auto-gen-trigger-debug") << "Generate triggers for " << f << ", #var=" << f[0].getNumChildren() << "..." << std::endl;
223
224
  // first, generate the set of pattern terms
225
13604
  if (!generatePatternTerms(f))
226
  {
227
146
    Trace("auto-gen-trigger-debug")
228
73
        << "...failed to generate pattern terms" << std::endl;
229
73
    return;
230
  }
231
232
  // then, group them to make triggers
233
13531
  unsigned rmin = d_patTerms[0][f].empty() ? 1 : 0;
234
27062
  unsigned rmax = options::multiTriggerWhenSingle() ? 1 : rmin;
235
27062
  for (unsigned r = rmin; r <= rmax; r++)
236
  {
237
22005
    std::vector<Node> patTerms;
238
13531
    std::vector<Node>& ptc = d_patTerms[r][f];
239
34070
    for (const Node& p : ptc)
240
    {
241
20539
      if (r == 1 || d_single_trigger_gen.find(p) == d_single_trigger_gen.end())
242
      {
243
17112
        patTerms.push_back(p);
244
      }
245
    }
246
13531
    if (patTerms.empty())
247
    {
248
3978
      continue;
249
    }
250
9553
    Trace("auto-gen-trigger") << "Generate trigger for " << f << std::endl;
251
    // sort terms based on relevance
252
36804
    if (options::relevantTriggers())
253
    {
254
319
      Assert(d_quant_rel);
255
638
      sortQuantifiersForSymbol sqfs;
256
319
      sqfs.d_quant_rel = d_quant_rel;
257
936
      for (const Node& p : patTerms)
258
      {
259
617
        Assert(d_pat_to_mpat.find(p) != d_pat_to_mpat.end());
260
617
        Assert(d_pat_to_mpat[p].hasOperator());
261
617
        sqfs.d_op_map[p] = d_pat_to_mpat[p].getOperator();
262
      }
263
      // sort based on # occurrences (this will cause Trigger to select rarer
264
      // symbols)
265
319
      std::sort(patTerms.begin(), patTerms.end(), sqfs);
266
319
      if (Debug.isOn("relevant-trigger"))
267
      {
268
        Debug("relevant-trigger") << "Terms based on relevance: " << std::endl;
269
        for (const Node& p : patTerms)
270
        {
271
          Debug("relevant-trigger")
272
              << "   " << p << " from " << d_pat_to_mpat[p] << " (";
273
          Debug("relevant-trigger") << d_quant_rel->getNumQuantifiersForSymbol(
274
                                           d_pat_to_mpat[p].getOperator())
275
                                    << ")" << std::endl;
276
        }
277
      }
278
    }
279
    // now, generate the trigger...
280
9553
    Trigger* tr = NULL;
281
9553
    if (d_is_single_trigger[patTerms[0]])
282
    {
283
16948
      tr = Trigger::mkTrigger(d_quantEngine,
284
                              d_qstate,
285
                              d_qim,
286
                              d_qreg,
287
                              f,
288
8474
                              patTerms[0],
289
                              false,
290
                              Trigger::TR_RETURN_NULL,
291
8474
                              d_num_trigger_vars[f]);
292
8474
      d_single_trigger_gen[patTerms[0]] = true;
293
    }
294
    else
295
    {
296
      // only generate multi trigger if option set, or if no single triggers
297
      // exist
298
1079
      if (!d_patTerms[0][f].empty())
299
      {
300
        if (options::multiTriggerWhenSingle())
301
        {
302
          Trace("multi-trigger-debug")
303
              << "Resort to choosing multi-triggers..." << std::endl;
304
        }
305
        else
306
        {
307
          return;
308
        }
309
      }
310
      // if we are re-generating triggers, shuffle based on some method
311
1079
      if (d_made_multi_trigger[f])
312
      {
313
68
        std::shuffle(patTerms.begin(),
314
                     patTerms.end(),
315
                     Random::getRandom());  // shuffle randomly
316
      }
317
      else
318
      {
319
1011
        d_made_multi_trigger[f] = true;
320
      }
321
      // will possibly want to get an old trigger
322
1079
      tr = Trigger::mkTrigger(d_quantEngine,
323
                              d_qstate,
324
                              d_qim,
325
                              d_qreg,
326
                              f,
327
                              patTerms,
328
                              false,
329
                              Trigger::TR_GET_OLD,
330
1079
                              d_num_trigger_vars[f]);
331
    }
332
9553
    if (tr == nullptr)
333
    {
334
      // did not generate a trigger
335
      continue;
336
    }
337
9553
    addTrigger(tr, f);
338
9553
    if (tr->isMultiTrigger())
339
    {
340
      // only add a single multi-trigger
341
1079
      continue;
342
    }
343
    // if we are generating additional triggers...
344
8474
    size_t index = 0;
345
8474
    if (index < patTerms.size())
346
    {
347
      // check if similar patterns exist, and if so, add them additionally
348
8474
      unsigned nqfs_curr = 0;
349
8474
      if (options::relevantTriggers())
350
      {
351
250
        nqfs_curr =
352
500
            d_quant_rel->getNumQuantifiersForSymbol(patTerms[0].getOperator());
353
      }
354
8474
      index++;
355
8474
      bool success = true;
356
15254
      while (success && index < patTerms.size()
357
15254
             && d_is_single_trigger[patTerms[index]])
358
      {
359
3390
        success = false;
360
6780
        if (!options::relevantTriggers()
361
6800
            || d_quant_rel->getNumQuantifiersForSymbol(
362
3400
                   patTerms[index].getOperator())
363
10
                   <= nqfs_curr)
364
        {
365
3390
          d_single_trigger_gen[patTerms[index]] = true;
366
10170
          Trigger* tr2 = Trigger::mkTrigger(d_quantEngine,
367
                                            d_qstate,
368
                                            d_qim,
369
                                            d_qreg,
370
                                            f,
371
3390
                                            patTerms[index],
372
                                            false,
373
                                            Trigger::TR_RETURN_NULL,
374
6780
                                            d_num_trigger_vars[f]);
375
3390
          addTrigger(tr2, f);
376
3390
          success = true;
377
        }
378
3390
        index++;
379
      }
380
    }
381
  }
382
}
383
384
13604
bool InstStrategyAutoGenTriggers::generatePatternTerms(Node f)
385
{
386
13604
  if (d_patTerms[0].find(f) != d_patTerms[0].end())
387
  {
388
    // already generated
389
3044
    return true;
390
  }
391
  // determine all possible pattern terms based on trigger term selection
392
  // strategy d_tr_strategy
393
10560
  d_patTerms[0][f].clear();
394
10560
  d_patTerms[1][f].clear();
395
71143
  bool ntrivTriggers = options::relationalTriggers();
396
21120
  std::vector<Node> patTermsF;
397
21120
  std::map<Node, inst::TriggerTermInfo> tinfo;
398
10560
  NodeManager* nm = NodeManager::currentNM();
399
  // well-defined function: can assume LHS is only pattern
400
21120
  if (options::quantFunWellDefined())
401
  {
402
    Node hd = QuantAttributes::getFunDefHead(f);
403
    if (!hd.isNull())
404
    {
405
      hd = d_qreg.substituteBoundVariablesToInstConstants(hd, f);
406
      patTermsF.push_back(hd);
407
      tinfo[hd].init(f, hd);
408
    }
409
  }
410
  // otherwise, use algorithm for collecting pattern terms
411
10560
  if (patTermsF.empty())
412
  {
413
21120
    Node bd = d_qreg.getInstConstantBody(f);
414
21120
    PatternTermSelector pts(f, d_tr_strategy, d_user_no_gen[f], true);
415
10560
    pts.collect(bd, patTermsF, tinfo);
416
10560
    if (ntrivTriggers)
417
    {
418
      sortTriggers st;
419
1174
      std::sort(patTermsF.begin(), patTermsF.end(), st);
420
    }
421
10560
    if (Trace.isOn("auto-gen-trigger-debug"))
422
    {
423
      Trace("auto-gen-trigger-debug")
424
          << "Collected pat terms for " << bd
425
          << ", no-patterns : " << d_user_no_gen[f].size() << std::endl;
426
      for (const Node& p : patTermsF)
427
      {
428
        Assert(tinfo.find(p) != tinfo.end());
429
        Trace("auto-gen-trigger-debug") << "   " << p << std::endl;
430
        Trace("auto-gen-trigger-debug2")
431
            << "     info = [" << tinfo[p].d_reqPol << ", "
432
            << tinfo[p].d_reqPolEq << ", " << tinfo[p].d_fv.size() << "]"
433
            << std::endl;
434
      }
435
      Trace("auto-gen-trigger-debug") << std::endl;
436
    }
437
  }
438
  // sort into single/multi triggers, calculate which terms should not be
439
  // considered
440
21120
  std::map<Node, bool> vcMap;
441
21120
  std::map<Node, bool> rmPatTermsF;
442
10560
  int32_t last_weight = -1;
443
47256
  for (const Node& p : patTermsF)
444
  {
445
36696
    Assert(p.getKind() != NOT);
446
36696
    bool newVar = false;
447
36696
    inst::TriggerTermInfo& tip = tinfo[p];
448
129055
    for (const Node& v : tip.d_fv)
449
    {
450
92359
      if (vcMap.find(v) == vcMap.end())
451
      {
452
26704
        vcMap[v] = true;
453
26704
        newVar = true;
454
      }
455
    }
456
36696
    int32_t curr_w = TriggerTermInfo::getTriggerWeight(p);
457
    // triggers whose value is maximum (2) are considered expendable.
458
36696
    if (ntrivTriggers && !newVar && last_weight != -1 && curr_w > last_weight
459
472
        && curr_w >= 2)
460
    {
461
944
      Trace("auto-gen-trigger-debug")
462
472
          << "...exclude expendible non-trivial trigger : " << p << std::endl;
463
472
      rmPatTermsF[p] = true;
464
    }
465
    else
466
    {
467
36224
      last_weight = curr_w;
468
    }
469
  }
470
10560
  d_num_trigger_vars[f] = vcMap.size();
471
21120
  if (d_num_trigger_vars[f] > 0
472
21120
      && d_num_trigger_vars[f] < f[0].getNumChildren())
473
  {
474
146
    Trace("auto-gen-trigger-partial")
475
73
        << "Quantified formula : " << f << std::endl;
476
146
    Trace("auto-gen-trigger-partial")
477
73
        << "...does not contain all variables in triggers!!!" << std::endl;
478
    // Invoke partial trigger strategy: partition variables of quantified
479
    // formula into (X,Y) where X are contained in a trigger and Y are not.
480
    // We then force a split of the quantified formula so that it becomes:
481
    //   forall X. forall Y. P( X, Y )
482
    // and hence is treatable by E-matching. We only do this for "standard"
483
    // quantified formulas (those with only two children), since this
484
    // technique should not be used for e.g. quantifiers marked for
485
    // quantifier elimination.
486
73
    QAttributes qa;
487
73
    QuantAttributes::computeQuantAttributes(f, qa);
488
36286
    if (options::partialTriggers() && qa.isStandard())
489
    {
490
      std::vector<Node> vcs[2];
491
      for (size_t i = 0, nchild = f[0].getNumChildren(); i < nchild; i++)
492
      {
493
        Node ic = d_qreg.getInstantiationConstant(f, i);
494
        vcs[vcMap.find(ic) == vcMap.end() ? 0 : 1].push_back(f[0][i]);
495
      }
496
      for (size_t i = 0; i < 2; i++)
497
      {
498
        d_vc_partition[i][f] = nm->mkNode(BOUND_VAR_LIST, vcs[i]);
499
      }
500
    }
501
    else
502
    {
503
73
      return false;
504
    }
505
  }
506
47074
  for (const Node& patf : patTermsF)
507
  {
508
72702
    Node pat = patf;
509
36587
    if (rmPatTermsF.find(pat) != rmPatTermsF.end())
510
    {
511
472
      continue;
512
    }
513
72230
    Trace("auto-gen-trigger-debug")
514
36115
        << "...processing pattern " << pat << std::endl;
515
72230
    Node mpat = pat;
516
    // process the pattern: if it has a required polarity, consider it
517
36115
    Assert(tinfo.find(pat) != tinfo.end());
518
36115
    int rpol = tinfo[pat].d_reqPol;
519
72230
    Node rpoleq = tinfo[pat].d_reqPolEq;
520
36115
    size_t num_fv = tinfo[pat].d_fv.size();
521
72230
    Trace("auto-gen-trigger-debug")
522
36115
        << "...required polarity for " << pat << " is " << rpol
523
36115
        << ", eq=" << rpoleq << std::endl;
524
36115
    if (rpol != 0)
525
    {
526
8735
      Assert(rpol == 1 || rpol == -1);
527
8735
      if (TriggerTermInfo::isRelationalTrigger(pat))
528
      {
529
36
        pat = rpol == -1 ? pat.negate() : pat;
530
      }
531
      else
532
      {
533
8699
        Assert(TriggerTermInfo::isAtomicTrigger(pat));
534
8699
        if (pat.getType().isBoolean() && rpoleq.isNull())
535
        {
536
15249
          if (options::literalMatchMode() == options::LiteralMatchMode::USE)
537
          {
538
6550
            pat = pat.eqNode(nm->mkConst(rpol == -1)).negate();
539
          }
540
          else if (options::literalMatchMode()
541
                   != options::LiteralMatchMode::NONE)
542
          {
543
            pat = pat.eqNode(nm->mkConst(rpol == 1));
544
          }
545
        }
546
        else
547
        {
548
2149
          Assert(!rpoleq.isNull());
549
2149
          if (rpol == -1)
550
          {
551
805
            if (options::literalMatchMode() != options::LiteralMatchMode::NONE)
552
            {
553
              // all equivalence classes except rpoleq
554
805
              pat = pat.eqNode(rpoleq).negate();
555
            }
556
          }
557
1344
          else if (rpol == 1)
558
          {
559
1344
            if (options::literalMatchMode() == options::LiteralMatchMode::AGG)
560
            {
561
              // only equivalence class rpoleq
562
              pat = pat.eqNode(rpoleq);
563
            }
564
          }
565
        }
566
      }
567
8735
      Trace("auto-gen-trigger-debug") << "...got : " << pat << std::endl;
568
    }
569
    else
570
    {
571
27380
      if (TriggerTermInfo::isRelationalTrigger(pat))
572
      {
573
        // consider both polarities
574
19
        addPatternToPool(f, pat.negate(), num_fv, mpat);
575
      }
576
    }
577
36115
    addPatternToPool(f, pat, num_fv, mpat);
578
  }
579
  // tinfo not used below this point
580
10487
  d_made_multi_trigger[f] = false;
581
10487
  if (Trace.isOn("auto-gen-trigger"))
582
  {
583
    Trace("auto-gen-trigger")
584
        << "Single trigger pool for " << f << " : " << std::endl;
585
    std::vector<Node>& spats = d_patTerms[0][f];
586
    for (size_t i = 0, psize = spats.size(); i < psize; i++)
587
    {
588
      Trace("auto-gen-trigger") << "   " << spats[i] << std::endl;
589
    }
590
    std::vector<Node>& mpats = d_patTerms[0][f];
591
    if (!mpats.empty())
592
    {
593
      Trace("auto-gen-trigger")
594
          << "Multi-trigger term pool for " << f << " : " << std::endl;
595
      for (size_t i = 0, psize = mpats.size(); i < psize; i++)
596
      {
597
        Trace("auto-gen-trigger") << "   " << mpats[i] << std::endl;
598
      }
599
    }
600
  }
601
10487
  return true;
602
}
603
604
36134
void InstStrategyAutoGenTriggers::addPatternToPool( Node q, Node pat, unsigned num_fv, Node mpat ) {
605
36134
  d_pat_to_mpat[pat] = mpat;
606
36134
  unsigned num_vars = options::partialTriggers() ? d_num_trigger_vars[q] : q[0].getNumChildren();
607
36134
  if (num_fv == num_vars)
608
  {
609
11864
    d_patTerms[0][q].push_back( pat );
610
11864
    d_is_single_trigger[ pat ] = true;
611
  }else{
612
24270
    d_patTerms[1][q].push_back( pat );
613
24270
    d_is_single_trigger[ pat ] = false;
614
  }
615
36134
}
616
617
618
12943
void InstStrategyAutoGenTriggers::addTrigger( inst::Trigger * tr, Node q ) {
619
12943
  if (tr == nullptr)
620
  {
621
    return;
622
  }
623
12943
  if (d_num_trigger_vars[q] < q[0].getNumChildren())
624
  {
625
    NodeManager* nm = NodeManager::currentNM();
626
    // partial trigger : generate implication to mark user pattern
627
    Node pat =
628
        d_qreg.substituteInstConstantsToBoundVariables(tr->getInstPattern(), q);
629
    Node ipl = nm->mkNode(INST_PATTERN_LIST, pat);
630
    Node qq = nm->mkNode(FORALL,
631
                         d_vc_partition[1][q],
632
                         nm->mkNode(FORALL, d_vc_partition[0][q], q[1]),
633
                         ipl);
634
    Trace("auto-gen-trigger-partial")
635
        << "Make partially specified user pattern: " << std::endl;
636
    Trace("auto-gen-trigger-partial") << "  " << qq << std::endl;
637
    Node lem = nm->mkNode(OR, q.negate(), qq);
638
    d_qim.addPendingLemma(lem, InferenceId::UNKNOWN);
639
    return;
640
  }
641
  unsigned tindex;
642
12943
  if (tr->isMultiTrigger())
643
  {
644
    // disable all other multi triggers
645
1079
    std::map<Trigger*, bool>& agt = d_auto_gen_trigger[1][q];
646
1175
    for (std::map<Trigger*, bool>::iterator it = agt.begin(); it != agt.end();
647
         ++it)
648
    {
649
96
      agt[it->first] = false;
650
    }
651
1079
    tindex = 1;
652
  }
653
  else
654
  {
655
11864
    tindex = 0;
656
  }
657
  // making it during an instantiation round, so must reset
658
12943
  std::map<Trigger*, bool>& agt = d_auto_gen_trigger[tindex][q];
659
12943
  if (agt.find(tr) == agt.end())
660
  {
661
12899
    tr->resetInstantiationRound();
662
12899
    tr->reset(Node::null());
663
  }
664
12943
  agt[tr] = true;
665
}
666
667
135842
bool InstStrategyAutoGenTriggers::hasUserPatterns( Node q ) {
668
135842
  if (q.getNumChildren() != 3)
669
  {
670
109244
    return false;
671
  }
672
26598
  std::map<Node, bool>::iterator it = d_hasUserPatterns.find(q);
673
26598
  if (it != d_hasUserPatterns.end())
674
  {
675
23375
    return it->second;
676
  }
677
3223
  bool hasPat = false;
678
3350
  for (const Node& ip : q[2])
679
  {
680
3275
    if (ip.getKind() == INST_PATTERN)
681
    {
682
3148
      hasPat = true;
683
3148
      break;
684
    }
685
  }
686
3223
  d_hasUserPatterns[q] = hasPat;
687
3223
  return hasPat;
688
}
689
690
8
void InstStrategyAutoGenTriggers::addUserNoPattern( Node q, Node pat ) {
691
8
  Assert(pat.getKind() == INST_NO_PATTERN && pat.getNumChildren() == 1);
692
8
  std::vector<Node>& ung = d_user_no_gen[q];
693
8
  if (std::find(ung.begin(), ung.end(), pat[0]) == ung.end())
694
  {
695
8
    Trace("user-pat") << "Add user no-pattern: " << pat[0] << " for " << q << std::endl;
696
8
    ung.push_back(pat[0]);
697
  }
698
8
}
699
700
} /* CVC4::theory::quantifiers namespace */
701
} /* CVC4::theory namespace */
702
231410
} /* CVC4 namespace */