GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/ematching/pattern_term_selector.cpp Lines: 329 360 91.4 %
Date: 2021-03-23 Branches: 753 1548 48.6 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file pattern_term_selector.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner, Morgan Deters
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 pattern term selector class
13
 **/
14
15
#include "theory/quantifiers/ematching/pattern_term_selector.h"
16
17
#include "expr/node_algorithm.h"
18
#include "theory/arith/arith_msum.h"
19
#include "theory/quantifiers/quant_util.h"
20
#include "theory/quantifiers/term_util.h"
21
#include "theory/rewriter.h"
22
23
using namespace CVC4::kind;
24
25
namespace CVC4 {
26
namespace theory {
27
namespace inst {
28
29
10566
PatternTermSelector::PatternTermSelector(Node q,
30
                                         options::TriggerSelMode tstrt,
31
                                         const std::vector<Node>& exc,
32
10566
                                         bool filterInst)
33
10566
    : d_quant(q), d_tstrt(tstrt), d_excluded(exc), d_filterInst(filterInst)
34
{
35
10566
}
36
37
10566
PatternTermSelector::~PatternTermSelector() {}
38
39
2095403
bool PatternTermSelector::isUsable(Node n, Node q)
40
{
41
2095403
  if (quantifiers::TermUtil::getInstConstAttr(n) != q)
42
  {
43
308024
    return true;
44
  }
45
1787379
  if (TriggerTermInfo::isAtomicTrigger(n))
46
  {
47
2444720
    for (const Node& nc : n)
48
    {
49
1643110
      if (!isUsable(nc, q))
50
      {
51
10662
        return false;
52
      }
53
    }
54
801610
    return true;
55
  }
56
975107
  else if (n.getKind() == INST_CONSTANT)
57
  {
58
944232
    return true;
59
  }
60
61750
  std::map<Node, Node> coeffs;
61
30875
  if (options::purifyTriggers())
62
  {
63
176
    Node x = getInversionVariable(n);
64
128
    if (!x.isNull())
65
    {
66
80
      return true;
67
    }
68
  }
69
30795
  return false;
70
}
71
72
37327
Node PatternTermSelector::getIsUsableEq(Node q, Node n)
73
{
74
37327
  Assert(TriggerTermInfo::isRelationalTrigger(n));
75
97577
  for (size_t i = 0; i < 2; i++)
76
  {
77
71433
    if (isUsableEqTerms(q, n[i], n[1 - i]))
78
    {
79
19145
      if (i == 1 && n.getKind() == EQUAL
80
19125
          && !quantifiers::TermUtil::hasInstConstAttr(n[0]))
81
      {
82
7698
        return NodeManager::currentNM()->mkNode(n.getKind(), n[1], n[0]);
83
      }
84
      else
85
      {
86
3485
        return n;
87
      }
88
    }
89
  }
90
26144
  return Node::null();
91
}
92
93
71433
bool PatternTermSelector::isUsableEqTerms(Node q, Node n1, Node n2)
94
{
95
71433
  if (n1.getKind() == INST_CONSTANT)
96
  {
97
13551
    if (options::relationalTriggers())
98
    {
99
3075
      Node q1 = quantifiers::TermUtil::getInstConstAttr(n1);
100
2465
      if (q1 != q)
101
      {
102
        // x is a variable from another quantified formula, fail
103
        return false;
104
      }
105
3075
      Node q2 = quantifiers::TermUtil::getInstConstAttr(n2);
106
2465
      if (q2.isNull())
107
      {
108
        // x = c
109
1460
        return true;
110
      }
111
1005
      if (n2.getKind() == INST_CONSTANT && q2 == q)
112
      {
113
        // x = y
114
395
        return true;
115
      }
116
      // we dont check x = f(y), which is handled symmetrically below
117
      // when n1 and n2 are swapped
118
    }
119
  }
120
57882
  else if (isUsableAtomicTrigger(n1, q))
121
  {
122
60670
    if (options::relationalTriggers() && n2.getKind() == INST_CONSTANT
123
29088
        && quantifiers::TermUtil::getInstConstAttr(n2) == q
124
57590
        && !expr::hasSubterm(n1, n2))
125
    {
126
      // f(x) = y
127
244
      return true;
128
    }
129
28258
    else if (!quantifiers::TermUtil::hasInstConstAttr(n2))
130
    {
131
      // f(x) = c
132
9084
      return true;
133
    }
134
  }
135
60250
  return false;
136
}
137
138
279377
Node PatternTermSelector::getIsUsableTrigger(Node n, Node q)
139
{
140
279377
  bool pol = true;
141
279377
  Trace("trigger-debug") << "Is " << n << " a usable trigger?" << std::endl;
142
279377
  if (n.getKind() == NOT)
143
  {
144
    pol = !pol;
145
    n = n[0];
146
  }
147
279377
  NodeManager* nm = NodeManager::currentNM();
148
279377
  if (n.getKind() == INST_CONSTANT)
149
  {
150
12
    return pol ? n : nm->mkNode(EQUAL, n, nm->mkConst(true)).notNode();
151
  }
152
279365
  else if (TriggerTermInfo::isRelationalTrigger(n))
153
  {
154
68394
    Node rtr = getIsUsableEq(q, n);
155
34197
    if (rtr.isNull() && n[0].getType().isReal())
156
    {
157
      // try to solve relation
158
17888
      std::map<Node, Node> m;
159
8944
      if (ArithMSum::getMonomialSumLit(n, m))
160
      {
161
21530
        for (std::map<Node, Node>::iterator it = m.begin(); it != m.end(); ++it)
162
        {
163
15728
          bool trySolve = false;
164
15728
          if (!it->first.isNull())
165
          {
166
13856
            if (it->first.getKind() == INST_CONSTANT)
167
            {
168
7940
              trySolve = options::relationalTriggers();
169
            }
170
5916
            else if (isUsableTrigger(it->first, q))
171
            {
172
3118
              trySolve = true;
173
            }
174
          }
175
15728
          if (trySolve)
176
          {
177
6284
            Trace("trigger-debug")
178
3142
                << "Try to solve for " << it->first << std::endl;
179
6284
            Node veq;
180
3142
            if (ArithMSum::isolate(it->first, m, veq, n.getKind()) != 0)
181
            {
182
3130
              rtr = getIsUsableEq(q, veq);
183
            }
184
            // either all solves will succeed or all solves will fail
185
3142
            break;
186
          }
187
        }
188
      }
189
    }
190
34197
    if (!rtr.isNull())
191
    {
192
11183
      Trace("relational-trigger") << "Relational trigger : " << std::endl;
193
22366
      Trace("relational-trigger")
194
11183
          << "    " << rtr << " (from " << n << ")" << std::endl;
195
11183
      Trace("relational-trigger") << "    in quantifier " << q << std::endl;
196
22366
      Node rtr2 = pol ? rtr : rtr.negate();
197
11183
      Trace("relational-trigger") << "    return : " << rtr2 << std::endl;
198
11183
      return rtr2;
199
    }
200
23014
    return Node::null();
201
  }
202
490336
  Trace("trigger-debug") << n << " usable : "
203
490336
                         << (quantifiers::TermUtil::getInstConstAttr(n) == q)
204
490336
                         << " " << TriggerTermInfo::isAtomicTrigger(n) << " "
205
245168
                         << isUsable(n, q) << std::endl;
206
245168
  if (isUsableAtomicTrigger(n, q))
207
  {
208
174735
    return pol ? n : nm->mkNode(EQUAL, n, nm->mkConst(true)).notNode();
209
  }
210
70433
  return Node::null();
211
}
212
213
303050
bool PatternTermSelector::isUsableAtomicTrigger(Node n, Node q)
214
{
215
909150
  return quantifiers::TermUtil::getInstConstAttr(n) == q
216
1212200
         && TriggerTermInfo::isAtomicTrigger(n) && isUsable(n, q);
217
}
218
219
95352
bool PatternTermSelector::isUsableTrigger(Node n, Node q)
220
{
221
190704
  Node nu = getIsUsableTrigger(n, q);
222
190704
  return !nu.isNull();
223
}
224
225
// store triggers in reqPol, indicating their polarity (if any) they must appear
226
// to falsify the quantified formula
227
450257
void PatternTermSelector::collectTermsInternal(
228
    Node n,
229
    std::map<Node, std::vector<Node> >& visited,
230
    std::map<Node, TriggerTermInfo>& tinfo,
231
    options::TriggerSelMode tstrt,
232
    std::vector<Node>& added,
233
    bool pol,
234
    bool hasPol,
235
    bool epol,
236
    bool hasEPol,
237
    bool knowIsUsable)
238
{
239
450257
  std::map<Node, std::vector<Node> >::iterator itv = visited.find(n);
240
450257
  if (itv != visited.end())
241
  {
242
    // already visited
243
195386
    for (const Node& t : itv->second)
244
    {
245
16242
      if (std::find(added.begin(), added.end(), t) == added.end())
246
      {
247
14705
        added.push_back(t);
248
      }
249
    }
250
539965
    return;
251
  }
252
271113
  visited[n].clear();
253
542226
  Trace("auto-gen-trigger-debug2")
254
271113
      << "Collect pat terms " << n << " " << pol << " " << hasPol << " " << epol
255
271113
      << " " << hasEPol << std::endl;
256
271113
  Kind nk = n.getKind();
257
271113
  if (nk == FORALL || nk == INST_CONSTANT)
258
  {
259
    // do not traverse beneath quantified formulas
260
59341
    return;
261
  }
262
301208
  Node nu;
263
211772
  bool nu_single = false;
264
211772
  if (knowIsUsable)
265
  {
266
7714
    nu = n;
267
  }
268
204058
  else if (nk != NOT
269
564178
           && std::find(d_excluded.begin(), d_excluded.end(), n)
270
564178
                  == d_excluded.end())
271
  {
272
180060
    nu = getIsUsableTrigger(n, d_quant);
273
180060
    if (!nu.isNull() && nu != n)
274
    {
275
7714
      collectTermsInternal(
276
          nu, visited, tinfo, tstrt, added, pol, hasPol, epol, hasEPol, true);
277
      // copy to n
278
7714
      visited[n].insert(visited[n].end(), added.begin(), added.end());
279
7714
      return;
280
    }
281
  }
282
204058
  if (!nu.isNull())
283
  {
284
89436
    Assert(nu == n);
285
89436
    Assert(nu.getKind() != NOT);
286
178872
    Trace("auto-gen-trigger-debug2")
287
89436
        << "...found usable trigger : " << nu << std::endl;
288
178872
    Node reqEq;
289
89436
    if (nu.getKind() == EQUAL)
290
    {
291
27462
      if (TriggerTermInfo::isAtomicTrigger(nu[0])
292
27462
          && !quantifiers::TermUtil::hasInstConstAttr(nu[1]))
293
      {
294
8124
        if (hasPol)
295
        {
296
5222
          reqEq = nu[1];
297
        }
298
8124
        nu = nu[0];
299
      }
300
    }
301
89436
    Assert(reqEq.isNull() || !quantifiers::TermUtil::hasInstConstAttr(reqEq));
302
89436
    Assert(isUsableTrigger(nu, d_quant));
303
178872
    Trace("auto-gen-trigger-debug2")
304
89436
        << "...add usable trigger : " << nu << std::endl;
305
89436
    tinfo[nu].init(d_quant, nu, hasEPol ? (epol ? 1 : -1) : 0, reqEq);
306
89436
    nu_single = tinfo[nu].d_fv.size() == d_quant[0].getNumChildren();
307
  }
308
293494
  Node nrec = nu.isNull() ? n : nu;
309
293494
  std::vector<Node> added2;
310
625475
  for (size_t i = 0, nrecc = nrec.getNumChildren(); i < nrecc; i++)
311
  {
312
    bool newHasPol, newPol;
313
    bool newHasEPol, newEPol;
314
421417
    QuantPhaseReq::getPolarity(nrec, i, hasPol, pol, newHasPol, newPol);
315
421417
    QuantPhaseReq::getEntailPolarity(
316
        nrec, i, hasEPol, epol, newHasEPol, newEPol);
317
421417
    collectTermsInternal(nrec[i],
318
                         visited,
319
                         tinfo,
320
                         tstrt,
321
                         added2,
322
                         newPol,
323
                         newHasPol,
324
                         newEPol,
325
                         newHasEPol);
326
  }
327
  // if this is not a usable trigger, don't worry about caching the results,
328
  // since triggers do not contain non-usable subterms
329
204058
  if (nu.isNull())
330
  {
331
114622
    return;
332
  }
333
89436
  bool rm_nu = false;
334
179673
  for (size_t i = 0, asize = added2.size(); i < asize; i++)
335
  {
336
180474
    Trace("auto-gen-trigger-debug2") << "..." << nu << " added child " << i
337
90237
                                     << " : " << added2[i] << std::endl;
338
90237
    Assert(added2[i] != nu);
339
    // if child was not already removed
340
90237
    if (tinfo.find(added2[i]) != tinfo.end())
341
    {
342
90237
      if (tstrt == options::TriggerSelMode::MAX
343
90237
          || (tstrt == options::TriggerSelMode::MIN_SINGLE_MAX && !nu_single))
344
      {
345
        // discard all subterms
346
        // do not remove if it has smaller weight
347
        if (tinfo[nu].d_weight <= tinfo[added2[i]].d_weight)
348
        {
349
          Trace("auto-gen-trigger-debug2") << "......remove it." << std::endl;
350
          visited[added2[i]].clear();
351
          tinfo.erase(added2[i]);
352
        }
353
      }
354
      else
355
      {
356
90237
        if (tinfo[nu].d_fv.size() == tinfo[added2[i]].d_fv.size())
357
        {
358
16329
          if (tinfo[nu].d_weight >= tinfo[added2[i]].d_weight)
359
          {
360
            // discard if we added a subterm as a trigger with all
361
            // variables that nu has
362
30398
            Trace("auto-gen-trigger-debug2")
363
15199
                << "......subsumes parent " << tinfo[nu].d_weight << " "
364
15199
                << tinfo[added2[i]].d_weight << "." << std::endl;
365
15199
            rm_nu = true;
366
          }
367
        }
368
90237
        if (std::find(added.begin(), added.end(), added2[i]) == added.end())
369
        {
370
84820
          added.push_back(added2[i]);
371
        }
372
      }
373
    }
374
  }
375
89436
  if (rm_nu
376
12847
      && (tstrt == options::TriggerSelMode::MIN
377
6720
          || (tstrt == options::TriggerSelMode::MIN_SINGLE_ALL && nu_single)))
378
  {
379
6127
    tinfo.erase(nu);
380
  }
381
  else
382
  {
383
83309
    if (std::find(added.begin(), added.end(), nu) == added.end())
384
    {
385
83285
      added.push_back(nu);
386
    }
387
  }
388
89436
  visited[n].insert(visited[n].end(), added.begin(), added.end());
389
}
390
391
10566
void PatternTermSelector::collect(Node n,
392
                                  std::vector<Node>& patTerms,
393
                                  std::map<Node, TriggerTermInfo>& tinfo)
394
{
395
10566
  collectInternal(n, patTerms, tinfo, d_tstrt, d_filterInst);
396
10566
}
397
398
21132
void PatternTermSelector::collectInternal(
399
    Node n,
400
    std::vector<Node>& patTerms,
401
    std::map<Node, TriggerTermInfo>& tinfo,
402
    options::TriggerSelMode tstrt,
403
    bool filterInst)
404
{
405
42258
  std::map<Node, std::vector<Node> > visited;
406
21132
  if (filterInst)
407
  {
408
    // immediately do not consider any term t for which another term is an
409
    // instance of t
410
21126
    std::vector<Node> patTerms2;
411
21126
    std::map<Node, TriggerTermInfo> tinfo2;
412
10566
    collectInternal(n, patTerms2, tinfo2, options::TriggerSelMode::ALL, false);
413
21126
    std::vector<Node> temp;
414
10566
    temp.insert(temp.begin(), patTerms2.begin(), patTerms2.end());
415
10566
    filterInstances(temp);
416
10566
    if (Trace.isOn("trigger-filter-instance"))
417
    {
418
      if (temp.size() != patTerms2.size())
419
      {
420
        Trace("trigger-filter-instance")
421
            << "Filtered an instance: " << std::endl;
422
        Trace("trigger-filter-instance") << "Old: ";
423
        for (unsigned i = 0; i < patTerms2.size(); i++)
424
        {
425
          Trace("trigger-filter-instance") << patTerms2[i] << " ";
426
        }
427
        Trace("trigger-filter-instance") << std::endl << "New: ";
428
        for (unsigned i = 0; i < temp.size(); i++)
429
        {
430
          Trace("trigger-filter-instance") << temp[i] << " ";
431
        }
432
        Trace("trigger-filter-instance") << std::endl;
433
      }
434
    }
435
10566
    if (tstrt == options::TriggerSelMode::ALL)
436
    {
437
6
      for (const Node& t : temp)
438
      {
439
        // copy information
440
        tinfo[t].d_fv.insert(
441
            tinfo[t].d_fv.end(), tinfo2[t].d_fv.begin(), tinfo2[t].d_fv.end());
442
        tinfo[t].d_reqPol = tinfo2[t].d_reqPol;
443
        tinfo[t].d_reqPolEq = tinfo2[t].d_reqPolEq;
444
        patTerms.push_back(t);
445
      }
446
6
      return;
447
    }
448
    // do not consider terms that have instances
449
56771
    for (const Node& t : patTerms2)
450
    {
451
46211
      if (std::find(temp.begin(), temp.end(), t) == temp.end())
452
      {
453
3525
        visited[t].clear();
454
      }
455
    }
456
  }
457
42252
  std::vector<Node> added;
458
21126
  collectTermsInternal(
459
      n, visited, tinfo, tstrt, added, true, true, false, true);
460
104033
  for (const std::pair<const Node, TriggerTermInfo>& t : tinfo)
461
  {
462
82907
    patTerms.push_back(t.first);
463
  }
464
}
465
466
154152
int PatternTermSelector::isInstanceOf(Node n1,
467
                                      Node n2,
468
                                      const std::vector<Node>& fv1,
469
                                      const std::vector<Node>& fv2)
470
{
471
154152
  Assert(n1 != n2);
472
154152
  int status = 0;
473
308304
  std::unordered_set<TNode, TNodeHashFunction> subs_vars;
474
  std::unordered_set<
475
      std::pair<TNode, TNode>,
476
      PairHashFunction<TNode, TNode, TNodeHashFunction, TNodeHashFunction> >
477
308304
      visited;
478
308304
  std::vector<std::pair<TNode, TNode> > visit;
479
308304
  std::pair<TNode, TNode> cur;
480
308304
  TNode cur1;
481
308304
  TNode cur2;
482
154152
  visit.push_back(std::pair<TNode, TNode>(n1, n2));
483
33298
  do
484
  {
485
187450
    cur = visit.back();
486
187450
    visit.pop_back();
487
187450
    if (visited.find(cur) != visited.end())
488
    {
489
4789
      continue;
490
    }
491
182661
    visited.insert(cur);
492
182661
    cur1 = cur.first;
493
182661
    cur2 = cur.second;
494
182661
    Assert(cur1 != cur2);
495
    // recurse if they have the same operator
496
529957
    if (cur1.hasOperator() && cur2.hasOperator()
497
161614
        && cur1.getNumChildren() == cur2.getNumChildren()
498
285612
        && cur1.getOperator() == cur2.getOperator()
499
391348
        && cur1.getOperator().getKind() != INST_CONSTANT)
500
    {
501
25978
      visit.push_back(std::pair<TNode, TNode>(cur1, cur2));
502
77705
      for (size_t i = 0, size = cur1.getNumChildren(); i < size; i++)
503
      {
504
51752
        if (cur1[i] != cur2[i])
505
        {
506
37131
          visit.push_back(std::pair<TNode, TNode>(cur1[i], cur2[i]));
507
        }
508
14621
        else if (cur1[i].getKind() == INST_CONSTANT)
509
        {
510
5331
          if (subs_vars.find(cur1[i]) != subs_vars.end())
511
          {
512
25
            return 0;
513
          }
514
          // the variable must map to itself in the substitution
515
5306
          subs_vars.insert(cur1[i]);
516
        }
517
      }
518
25953
      continue;
519
    }
520
156683
    bool success = false;
521
    // check if we are in a unifiable instance case
522
    // must be only this case
523
459800
    for (unsigned r = 0; r < 2; r++)
524
    {
525
309198
      if (status == 0 || ((status == 1) == (r == 0)))
526
      {
527
607875
        TNode curi = r == 0 ? cur1 : cur2;
528
613956
        if (curi.getKind() == INST_CONSTANT
529
306978
            && subs_vars.find(curi) == subs_vars.end())
530
        {
531
49937
          TNode curj = r == 0 ? cur2 : cur1;
532
          // RHS must be a simple trigger
533
28009
          if (TriggerTermInfo::getTriggerWeight(curj) == 0)
534
          {
535
            // must occur in the free variables in the other
536
7668
            const std::vector<Node>& free_vars = r == 0 ? fv2 : fv1;
537
23004
            if (std::find(free_vars.begin(), free_vars.end(), curi)
538
23004
                != free_vars.end())
539
            {
540
6081
              status = r == 0 ? 1 : -1;
541
6081
              subs_vars.insert(curi);
542
6081
              success = true;
543
6081
              break;
544
            }
545
          }
546
        }
547
      }
548
    }
549
156683
    if (!success)
550
    {
551
150602
      return 0;
552
    }
553
36823
  } while (!visit.empty());
554
3525
  return status;
555
}
556
557
10566
void PatternTermSelector::filterInstances(std::vector<Node>& nodes)
558
{
559
21132
  std::map<unsigned, std::vector<Node> > fvs;
560
56777
  for (size_t i = 0, size = nodes.size(); i < size; i++)
561
  {
562
46211
    quantifiers::TermUtil::computeInstConstContains(nodes[i], fvs[i]);
563
  }
564
21132
  std::vector<bool> active;
565
10566
  active.resize(nodes.size(), true);
566
56777
  for (size_t i = 0, size = nodes.size(); i < size; i++)
567
  {
568
46211
    std::vector<Node>& fvsi = fvs[i];
569
46211
    if (!active[i])
570
    {
571
1520
      continue;
572
    }
573
197935
    for (size_t j = i + 1, size2 = nodes.size(); j < size2; j++)
574
    {
575
155249
      if (!active[j])
576
      {
577
1097
        continue;
578
      }
579
154152
      int result = isInstanceOf(nodes[i], nodes[j], fvsi, fvs[j]);
580
154152
      if (result == 1)
581
      {
582
4010
        Trace("filter-instances")
583
2005
            << nodes[j] << " is an instance of " << nodes[i] << std::endl;
584
2005
        active[i] = false;
585
2005
        break;
586
      }
587
152147
      else if (result == -1)
588
      {
589
3040
        Trace("filter-instances")
590
1520
            << nodes[i] << " is an instance of " << nodes[j] << std::endl;
591
1520
        active[j] = false;
592
      }
593
    }
594
  }
595
21132
  std::vector<Node> temp;
596
56777
  for (size_t i = 0, nsize = nodes.size(); i < nsize; i++)
597
  {
598
46211
    if (active[i])
599
    {
600
42686
      temp.push_back(nodes[i]);
601
    }
602
  }
603
10566
  nodes.clear();
604
10566
  nodes.insert(nodes.begin(), temp.begin(), temp.end());
605
10566
}
606
607
302
Node PatternTermSelector::getInversionVariable(Node n)
608
{
609
302
  Kind nk = n.getKind();
610
302
  if (nk == INST_CONSTANT)
611
  {
612
88
    return n;
613
  }
614
214
  else if (nk == PLUS || nk == MULT)
615
  {
616
212
    Node ret;
617
294
    for (const Node& nc : n)
618
    {
619
206
      if (quantifiers::TermUtil::hasInstConstAttr(nc))
620
      {
621
106
        if (ret.isNull())
622
        {
623
106
          ret = getInversionVariable(nc);
624
106
          if (ret.isNull())
625
          {
626
36
            Trace("var-trigger-debug")
627
18
                << "No : multiple variables " << n << std::endl;
628
18
            return Node::null();
629
          }
630
        }
631
        else
632
        {
633
          return Node::null();
634
        }
635
      }
636
100
      else if (nk == MULT)
637
      {
638
50
        if (!nc.isConst())
639
        {
640
          Trace("var-trigger-debug")
641
              << "No : non-linear coefficient " << n << std::endl;
642
          return Node::null();
643
        }
644
      }
645
    }
646
88
    return ret;
647
  }
648
216
  Trace("var-trigger-debug")
649
108
      << "No : unsupported operator " << n << "." << std::endl;
650
108
  return Node::null();
651
}
652
653
16
Node PatternTermSelector::getInversion(Node n, Node x)
654
{
655
16
  Kind nk = n.getKind();
656
16
  if (nk == INST_CONSTANT)
657
  {
658
8
    return x;
659
  }
660
8
  else if (nk == PLUS || nk == MULT)
661
  {
662
8
    NodeManager* nm = NodeManager::currentNM();
663
8
    int cindex = -1;
664
8
    bool cindexSet = false;
665
24
    for (size_t i = 0, nchild = n.getNumChildren(); i < nchild; i++)
666
    {
667
32
      Node nc = n[i];
668
16
      if (!quantifiers::TermUtil::hasInstConstAttr(nc))
669
      {
670
8
        if (nk == PLUS)
671
        {
672
4
          x = nm->mkNode(MINUS, x, nc);
673
        }
674
4
        else if (nk == MULT)
675
        {
676
4
          Assert(nc.isConst());
677
4
          if (x.getType().isInteger())
678
          {
679
8
            Node coeff = nm->mkConst(nc.getConst<Rational>().abs());
680
4
            if (!nc.getConst<Rational>().abs().isOne())
681
            {
682
4
              x = nm->mkNode(INTS_DIVISION_TOTAL, x, coeff);
683
            }
684
4
            if (nc.getConst<Rational>().sgn() < 0)
685
            {
686
              x = nm->mkNode(UMINUS, x);
687
            }
688
          }
689
          else
690
          {
691
            Node coeff = nm->mkConst(Rational(1) / nc.getConst<Rational>());
692
            x = nm->mkNode(MULT, x, coeff);
693
          }
694
        }
695
8
        x = Rewriter::rewrite(x);
696
      }
697
      else
698
      {
699
8
        Assert(!cindexSet);
700
8
        cindex = i;
701
8
        cindexSet = true;
702
      }
703
    }
704
8
    if (cindexSet)
705
    {
706
8
      return getInversion(n[cindex], x);
707
    }
708
  }
709
  return Node::null();
710
}
711
712
6
void PatternTermSelector::getTriggerVariables(Node n,
713
                                              Node q,
714
                                              std::vector<Node>& tvars)
715
{
716
12
  PatternTermSelector pts(q, options::TriggerSelMode::ALL);
717
12
  std::vector<Node> patTerms;
718
12
  std::map<Node, TriggerTermInfo> tinfo;
719
  // collect all patterns from n
720
6
  pts.collect(n, patTerms, tinfo);
721
  // collect all variables from all patterns in patTerms, add to tvars
722
6
  for (const Node& pat : patTerms)
723
  {
724
    quantifiers::TermUtil::computeInstConstContainsForQuant(q, pat, tvars);
725
  }
726
6
}
727
728
}  // namespace inst
729
}  // namespace theory
730
26685
}  // namespace CVC4