GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/term_database.cpp Lines: 549 674 81.5 %
Date: 2021-03-22 Branches: 1274 2982 42.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file term_database.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner, Gereon Kremer
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 term databse class
13
 **/
14
15
#include "theory/quantifiers/term_database.h"
16
17
#include "options/base_options.h"
18
#include "options/quantifiers_options.h"
19
#include "options/smt_options.h"
20
#include "options/theory_options.h"
21
#include "options/uf_options.h"
22
#include "theory/quantifiers/ematching/trigger_term_info.h"
23
#include "theory/quantifiers/quantifiers_attributes.h"
24
#include "theory/quantifiers/quantifiers_inference_manager.h"
25
#include "theory/quantifiers/quantifiers_registry.h"
26
#include "theory/quantifiers/quantifiers_state.h"
27
#include "theory/quantifiers/term_util.h"
28
#include "theory/quantifiers_engine.h"
29
#include "theory/theory_engine.h"
30
31
using namespace std;
32
using namespace CVC4::kind;
33
using namespace CVC4::context;
34
using namespace CVC4::theory::inst;
35
36
namespace CVC4 {
37
namespace theory {
38
namespace quantifiers {
39
40
8995
TermDb::TermDb(QuantifiersState& qs, QuantifiersRegistry& qr)
41
    : d_qstate(qs),
42
      d_qim(nullptr),
43
      d_qreg(qr),
44
      d_termsContext(),
45
150897
      d_termsContextUse(options::termDbCd() ? qs.getSatContext()
46
                                            : &d_termsContext),
47
      d_processed(d_termsContextUse),
48
      d_typeMap(d_termsContextUse),
49
      d_ops(d_termsContextUse),
50
      d_opMap(d_termsContextUse),
51
17990
      d_inactive_map(qs.getSatContext())
52
{
53
8995
  d_consistent_ee = true;
54
8995
  d_true = NodeManager::currentNM()->mkConst(true);
55
8995
  d_false = NodeManager::currentNM()->mkConst(false);
56
8995
  if (!options::termDbCd())
57
  {
58
    // when not maintaining terms in a context-dependent manner, we clear during
59
    // each presolve, which requires maintaining a single outermost level
60
    d_termsContext.push();
61
  }
62
8995
}
63
64
17984
TermDb::~TermDb(){
65
66
17984
}
67
68
8995
void TermDb::finishInit(QuantifiersInferenceManager* qim) { d_qim = qim; }
69
70
23481
void TermDb::registerQuantifier( Node q ) {
71
23481
  Assert(q[0].getNumChildren() == d_qreg.getNumInstantiationConstants(q));
72
77915
  for (size_t i = 0, nvars = q[0].getNumChildren(); i < nvars; i++)
73
  {
74
108868
    Node ic = d_qreg.getInstantiationConstant(q, i);
75
54434
    setTermInactive( ic );
76
  }
77
23481
}
78
79
971
size_t TermDb::getNumOperators() const { return d_ops.size(); }
80
81
1947
Node TermDb::getOperator(size_t i) const
82
{
83
1947
  Assert(i < d_ops.size());
84
1947
  return d_ops[i];
85
}
86
87
/** ground terms */
88
588464
size_t TermDb::getNumGroundTerms(Node f) const
89
{
90
588464
  NodeDbListMap::const_iterator it = d_opMap.find(f);
91
588464
  if (it != d_opMap.end())
92
  {
93
579001
    return it->second->d_list.size();
94
  }
95
9463
  return 0;
96
}
97
98
3145955
Node TermDb::getGroundTerm(Node f, size_t i) const
99
{
100
3145955
  NodeDbListMap::const_iterator it = d_opMap.find(f);
101
3145955
  if (it != d_opMap.end())
102
  {
103
3145955
    Assert(i < it->second->d_list.size());
104
3145955
    return it->second->d_list[i];
105
  }
106
  Assert(false);
107
  return Node::null();
108
}
109
110
510
size_t TermDb::getNumTypeGroundTerms(TypeNode tn) const
111
{
112
510
  TypeNodeDbListMap::const_iterator it = d_typeMap.find(tn);
113
510
  if (it != d_typeMap.end())
114
  {
115
500
    return it->second->d_list.size();
116
  }
117
10
  return 0;
118
}
119
120
43635
Node TermDb::getTypeGroundTerm(TypeNode tn, size_t i) const
121
{
122
43635
  TypeNodeDbListMap::const_iterator it = d_typeMap.find(tn);
123
43635
  if (it != d_typeMap.end())
124
  {
125
43635
    Assert(i < it->second->d_list.size());
126
43635
    return it->second->d_list[i];
127
  }
128
  Assert(false);
129
  return Node::null();
130
}
131
132
2673
Node TermDb::getOrMakeTypeGroundTerm(TypeNode tn, bool reqVar)
133
{
134
2673
  TypeNodeDbListMap::const_iterator it = d_typeMap.find(tn);
135
2673
  if (it != d_typeMap.end())
136
  {
137
708
    Assert(!it->second->d_list.empty());
138
708
    if (!reqVar)
139
    {
140
383
      return it->second->d_list[0];
141
    }
142
508
    for (const Node& v : it->second->d_list)
143
    {
144
454
      if (v.isVar())
145
      {
146
271
        return v;
147
      }
148
    }
149
  }
150
2019
  return getOrMakeTypeFreshVariable(tn);
151
}
152
153
2019
Node TermDb::getOrMakeTypeFreshVariable(TypeNode tn)
154
{
155
  std::unordered_map<TypeNode, Node, TypeNodeHashFunction>::iterator it =
156
2019
      d_type_fv.find(tn);
157
2019
  if (it == d_type_fv.end())
158
  {
159
462
    std::stringstream ss;
160
231
    ss << language::SetLanguage(options::outputLanguage());
161
231
    ss << "e_" << tn;
162
    Node k = NodeManager::currentNM()->mkSkolem(
163
462
        ss.str(), tn, "is a termDb fresh variable");
164
462
    Trace("mkVar") << "TermDb:: Make variable " << k << " : " << tn
165
231
                   << std::endl;
166
231
    if (options::instMaxLevel() != -1)
167
    {
168
      QuantAttributes::setInstantiationLevelAttr(k, 0);
169
    }
170
231
    d_type_fv[tn] = k;
171
231
    return k;
172
  }
173
  else
174
  {
175
1788
    return it->second;
176
  }
177
}
178
179
6032110
Node TermDb::getMatchOperator( Node n ) {
180
6032110
  Kind k = n.getKind();
181
  //datatype operators may be parametric, always assume they are
182
6032110
  if (k == SELECT || k == STORE || k == UNION || k == INTERSECTION
183
5794101
      || k == SUBSET || k == SETMINUS || k == MEMBER || k == SINGLETON
184
5778138
      || k == APPLY_SELECTOR_TOTAL || k == APPLY_SELECTOR || k == APPLY_TESTER
185
5657468
      || k == SEP_PTO || k == HO_APPLY || k == SEQ_NTH)
186
  {
187
    //since it is parametric, use a particular one as op
188
760480
    TypeNode tn = n[0].getType();
189
760480
    Node op = n.getOperator();
190
380240
    std::map< Node, std::map< TypeNode, Node > >::iterator ito = d_par_op_map.find( op );
191
380240
    if( ito!=d_par_op_map.end() ){
192
371255
      std::map< TypeNode, Node >::iterator it = ito->second.find( tn );
193
371255
      if( it!=ito->second.end() ){
194
370638
        return it->second;
195
      }
196
    }
197
9602
    Trace("par-op") << "Parametric operator : " << k << ", " << n.getOperator() << ", " << tn << " : " << n << std::endl;
198
9602
    d_par_op_map[op][tn] = n;
199
9602
    return n;
200
  }
201
5651870
  else if (inst::TriggerTermInfo::isAtomicTriggerKind(k))
202
  {
203
5386057
    return n.getOperator();
204
  }else{
205
265813
    return Node::null();
206
  }
207
}
208
209
2222847
void TermDb::addTerm(Node n)
210
{
211
2222847
  if (d_processed.find(n) != d_processed.end())
212
  {
213
1323822
    return;
214
  }
215
899025
  d_processed.insert(n);
216
899025
  if (!TermUtil::hasInstConstAttr(n))
217
  {
218
873838
    Trace("term-db-debug") << "register term : " << n << std::endl;
219
873838
    DbList* dlt = getOrMkDbListForType(n.getType());
220
873838
    dlt->d_list.push_back(n);
221
    // if this is an atomic trigger, consider adding it
222
873838
    if (inst::TriggerTermInfo::isAtomicTrigger(n))
223
    {
224
349836
      Trace("term-db") << "register term in db " << n << std::endl;
225
226
699672
      Node op = getMatchOperator(n);
227
349836
      Trace("term-db-debug") << "  match operator is : " << op << std::endl;
228
349836
      DbList* dlo = getOrMkDbListForOp(op);
229
349836
      dlo->d_list.push_back(n);
230
      // If we are higher-order, we may need to register more terms.
231
349836
      if (options::ufHo())
232
      {
233
26237
        addTermHo(n);
234
      }
235
    }
236
  }
237
  else
238
  {
239
25187
    setTermInactive(n);
240
  }
241
899025
  if (!n.isClosure())
242
  {
243
2377373
    for (const Node& nc : n)
244
    {
245
1478370
      addTerm(nc);
246
    }
247
  }
248
}
249
250
873838
DbList* TermDb::getOrMkDbListForType(TypeNode tn)
251
{
252
873838
  TypeNodeDbListMap::iterator it = d_typeMap.find(tn);
253
873838
  if (it != d_typeMap.end())
254
  {
255
851923
    return it->second.get();
256
  }
257
43830
  std::shared_ptr<DbList> dl = std::make_shared<DbList>(d_termsContextUse);
258
21915
  d_typeMap.insert(tn, dl);
259
21915
  return dl.get();
260
}
261
262
399378
DbList* TermDb::getOrMkDbListForOp(TNode op)
263
{
264
399378
  NodeDbListMap::iterator it = d_opMap.find(op);
265
399378
  if (it != d_opMap.end())
266
  {
267
272550
    return it->second.get();
268
  }
269
253656
  std::shared_ptr<DbList> dl = std::make_shared<DbList>(d_termsContextUse);
270
126828
  d_opMap.insert(op, dl);
271
126828
  Assert(op.getKind() != BOUND_VARIABLE);
272
126828
  d_ops.push_back(op);
273
126828
  return dl.get();
274
}
275
276
758366
void TermDb::computeArgReps( TNode n ) {
277
758366
  if (d_arg_reps.find(n) == d_arg_reps.end())
278
  {
279
444475
    eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
280
1336316
    for (const TNode& nc : n)
281
    {
282
1783682
      TNode r = ee->hasTerm(nc) ? ee->getRepresentative(nc) : nc;
283
891841
      d_arg_reps[n].push_back( r );
284
    }
285
  }
286
758366
}
287
288
2117385
void TermDb::computeUfEqcTerms( TNode f ) {
289
2117385
  Assert(f == getOperatorRepresentative(f));
290
2117385
  if (d_func_map_eqc_trie.find(f) != d_func_map_eqc_trie.end())
291
  {
292
2069327
    return;
293
  }
294
48058
  d_func_map_eqc_trie[f].clear();
295
  // get the matchable operators in the equivalence class of f
296
96116
  std::vector<TNode> ops;
297
48058
  ops.push_back(f);
298
48058
  if (options::ufHo())
299
  {
300
1550
    ops.insert(ops.end(), d_ho_op_slaves[f].begin(), d_ho_op_slaves[f].end());
301
  }
302
48058
  eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
303
96165
  for (TNode ff : ops)
304
  {
305
48107
    DbList* dbl = getOrMkDbListForOp(ff);
306
459011
    for (const Node& n : dbl->d_list)
307
    {
308
410904
      if (hasTermCurrent(n) && isTermActive(n))
309
      {
310
373577
        computeArgReps(n);
311
747154
        TNode r = ee->hasTerm(n) ? ee->getRepresentative(n) : TNode(n);
312
373577
        d_func_map_eqc_trie[f].d_data[r].addTerm(n, d_arg_reps[n]);
313
      }
314
    }
315
  }
316
}
317
318
3906841
void TermDb::computeUfTerms( TNode f ) {
319
3906841
  if (d_op_nonred_count.find(f) != d_op_nonred_count.end())
320
  {
321
    // already computed
322
7726488
    return;
323
  }
324
43600
  Assert(f == getOperatorRepresentative(f));
325
43600
  d_op_nonred_count[f] = 0;
326
  // get the matchable operators in the equivalence class of f
327
87194
  std::vector<TNode> ops;
328
43600
  ops.push_back(f);
329
43600
  if (options::ufHo())
330
  {
331
2044
    ops.insert(ops.end(), d_ho_op_slaves[f].begin(), d_ho_op_slaves[f].end());
332
  }
333
43600
  Trace("term-db-debug") << "computeUfTerms for " << f << std::endl;
334
43600
  unsigned congruentCount = 0;
335
43600
  unsigned nonCongruentCount = 0;
336
43600
  unsigned alreadyCongruentCount = 0;
337
43600
  unsigned relevantCount = 0;
338
43600
  NodeManager* nm = NodeManager::currentNM();
339
79406
  for (TNode ff : ops)
340
  {
341
43647
    NodeDbListMap::iterator it = d_opMap.find(ff);
342
43647
    if (it == d_opMap.end())
343
    {
344
      // no terms for this operator
345
7835
      continue;
346
    }
347
35812
    Trace("term-db-debug") << "Adding terms for operator " << ff << std::endl;
348
452603
    for (const Node& n : it->second->d_list)
349
    {
350
      // to be added to term index, term must be relevant, and exist in EE
351
416797
      if (!hasTermCurrent(n) || !d_qstate.hasTerm(n))
352
      {
353
        Trace("term-db-debug") << n << " is not relevant." << std::endl;
354
121994
        continue;
355
      }
356
357
416797
      relevantCount++;
358
448805
      if (!isTermActive(n))
359
      {
360
32008
        Trace("term-db-debug") << n << " is already redundant." << std::endl;
361
32008
        alreadyCongruentCount++;
362
32008
        continue;
363
      }
364
365
384789
      computeArgReps(n);
366
384789
      Trace("term-db-debug") << "Adding term " << n << " with arg reps : ";
367
1168862
      for (unsigned i = 0, size = d_arg_reps[n].size(); i < size; i++)
368
      {
369
784073
        Trace("term-db-debug") << d_arg_reps[n][i] << " ";
370
3136292
        if (std::find(d_func_map_rel_dom[f][i].begin(),
371
1568146
                      d_func_map_rel_dom[f][i].end(),
372
3136292
                      d_arg_reps[n][i])
373
2352219
            == d_func_map_rel_dom[f][i].end())
374
        {
375
260837
          d_func_map_rel_dom[f][i].push_back(d_arg_reps[n][i]);
376
        }
377
      }
378
384789
      Trace("term-db-debug") << std::endl;
379
384789
      Assert(d_qstate.hasTerm(n));
380
769578
      Trace("term-db-debug")
381
384789
          << "  and value : " << d_qstate.getRepresentative(n) << std::endl;
382
679586
      Node at = d_func_map_trie[f].addOrGetTerm(n, d_arg_reps[n]);
383
384789
      Assert(d_qstate.hasTerm(at));
384
384789
      Trace("term-db-debug2") << "...add term returned " << at << std::endl;
385
474775
      if (at != n && d_qstate.areEqual(at, n))
386
      {
387
89986
        setTermInactive(n);
388
89986
        Trace("term-db-debug") << n << " is redundant." << std::endl;
389
89986
        congruentCount++;
390
89986
        continue;
391
      }
392
294803
      if (d_qstate.areDisequal(at, n))
393
      {
394
6
        std::vector<Node> lits;
395
6
        lits.push_back(nm->mkNode(EQUAL, at, n));
396
6
        bool success = true;
397
6
        if (options::ufHo())
398
        {
399
          // operators might be disequal
400
          if (ops.size() > 1)
401
          {
402
            Node atf = getMatchOperator(at);
403
            Node nf = getMatchOperator(n);
404
            if (atf != nf)
405
            {
406
              if (at.getKind() == APPLY_UF && n.getKind() == APPLY_UF)
407
              {
408
                lits.push_back(atf.eqNode(nf).negate());
409
              }
410
              else
411
              {
412
                success = false;
413
                Assert(false);
414
              }
415
            }
416
          }
417
        }
418
6
        if (success)
419
        {
420
6
          Assert(at.getNumChildren() == n.getNumChildren());
421
24
          for (unsigned k = 0, size = at.getNumChildren(); k < size; k++)
422
          {
423
18
            if (at[k] != n[k])
424
            {
425
6
              lits.push_back(nm->mkNode(EQUAL, at[k], n[k]).negate());
426
            }
427
          }
428
12
          Node lem = lits.size() == 1 ? lits[0] : nm->mkNode(OR, lits);
429
6
          if (Trace.isOn("term-db-lemma"))
430
          {
431
            Trace("term-db-lemma") << "Disequal congruent terms : " << at << " "
432
                                   << n << "!!!!" << std::endl;
433
            if (!d_qstate.getValuation().needCheck())
434
            {
435
              Trace("term-db-lemma") << "  all theories passed with no lemmas."
436
                                     << std::endl;
437
              // we should be a full effort check, prior to theory combination
438
            }
439
            Trace("term-db-lemma") << "  add lemma : " << lem << std::endl;
440
          }
441
6
          d_qim->addPendingLemma(lem, InferenceId::UNKNOWN);
442
6
          d_qstate.notifyInConflict();
443
6
          d_consistent_ee = false;
444
6
          return;
445
        }
446
      }
447
294797
      nonCongruentCount++;
448
294797
      d_op_nonred_count[f]++;
449
    }
450
35806
    if (Trace.isOn("tdb"))
451
    {
452
      Trace("tdb") << "Term db size [" << f << "] : " << nonCongruentCount
453
                   << " / ";
454
      Trace("tdb") << (nonCongruentCount + congruentCount) << " / "
455
                   << (nonCongruentCount + congruentCount
456
                       + alreadyCongruentCount)
457
                   << " / ";
458
      Trace("tdb") << relevantCount << " / " << it->second->d_list.size()
459
                   << std::endl;
460
    }
461
  }
462
}
463
464
26237
void TermDb::addTermHo(Node n)
465
{
466
26237
  Assert(options::ufHo());
467
26237
  if (n.getType().isFunction())
468
  {
469
    // nothing special to do with functions
470
252
    return;
471
  }
472
25985
  NodeManager* nm = NodeManager::currentNM();
473
51970
  Node curr = n;
474
51970
  std::vector<Node> args;
475
29191
  while (curr.getKind() == HO_APPLY)
476
  {
477
1603
    args.insert(args.begin(), curr[1]);
478
1603
    curr = curr[0];
479
1603
    if (!curr.isVar())
480
    {
481
      // purify the term
482
694
      std::map<Node, Node>::iterator itp = d_ho_fun_op_purify.find(curr);
483
1388
      Node psk;
484
694
      if (itp == d_ho_fun_op_purify.end())
485
      {
486
441
        psk = nm->mkSkolem("pfun",
487
294
                           curr.getType(),
488
                           "purify for function operator term indexing");
489
147
        d_ho_fun_op_purify[curr] = psk;
490
        // we do not add it to d_ops since it is an internal operator
491
      }
492
      else
493
      {
494
547
        psk = itp->second;
495
      }
496
1388
      std::vector<Node> children;
497
694
      children.push_back(psk);
498
694
      children.insert(children.end(), args.begin(), args.end());
499
1388
      Node p_n = nm->mkNode(APPLY_UF, children);
500
1388
      Trace("term-db") << "register term in db (via purify) " << p_n
501
694
                       << std::endl;
502
      // also add this one internally
503
694
      DbList* dblp = getOrMkDbListForOp(psk);
504
694
      dblp->d_list.push_back(p_n);
505
      // maintain backwards mapping
506
694
      d_ho_purify_to_term[p_n] = n;
507
    }
508
  }
509
25985
  if (!args.empty() && curr.isVar())
510
  {
511
    // also add standard application version
512
909
    args.insert(args.begin(), curr);
513
1818
    Node uf_n = nm->mkNode(APPLY_UF, args);
514
909
    addTerm(uf_n);
515
  }
516
}
517
518
3423702
Node TermDb::getOperatorRepresentative( TNode op ) const {
519
3423702
  std::map< TNode, TNode >::const_iterator it = d_ho_op_rep.find( op );
520
3423702
  if( it!=d_ho_op_rep.end() ){
521
1594203
    return it->second;
522
  }else{
523
1829499
    return op;
524
  }
525
}
526
527
2138965
bool TermDb::inRelevantDomain( TNode f, unsigned i, TNode r ) {
528
2138965
  if( options::ufHo() ){
529
199539
    f = getOperatorRepresentative( f );
530
  }
531
2138965
  computeUfTerms( f );
532
2138965
  Assert(!d_qstate.getEqualityEngine()->hasTerm(r)
533
         || d_qstate.getEqualityEngine()->getRepresentative(r) == r);
534
2138965
  std::map< Node, std::map< unsigned, std::vector< Node > > >::iterator it = d_func_map_rel_dom.find( f );
535
2138965
  if( it != d_func_map_rel_dom.end() ){
536
2114812
    std::map< unsigned, std::vector< Node > >::iterator it2 = it->second.find( i );
537
2114812
    if( it2!=it->second.end() ){
538
2114812
      return std::find( it2->second.begin(), it2->second.end(), r )!=it2->second.end();
539
    }else{
540
      return false;
541
    }
542
  }else{
543
24153
    return false;
544
  }
545
}
546
547
1090073
Node TermDb::evaluateTerm2(TNode n,
548
                           std::map<TNode, Node>& visited,
549
                           std::vector<Node>& exp,
550
                           bool useEntailmentTests,
551
                           bool computeExp,
552
                           bool reqHasTerm)
553
{
554
1090073
  std::map< TNode, Node >::iterator itv = visited.find( n );
555
1090073
  if( itv != visited.end() ){
556
31821
    return itv->second;
557
  }
558
1058252
  size_t prevSize = exp.size();
559
1058252
  Trace("term-db-eval") << "evaluate term : " << n << std::endl;
560
2116504
  Node ret = n;
561
1058252
  if( n.getKind()==FORALL || n.getKind()==BOUND_VARIABLE ){
562
    //do nothing
563
  }
564
1055793
  else if (d_qstate.hasTerm(n))
565
  {
566
441748
    Trace("term-db-eval") << "...exists in ee, return rep" << std::endl;
567
441748
    ret = d_qstate.getRepresentative(n);
568
441748
    if (computeExp)
569
    {
570
      if (n != ret)
571
      {
572
        exp.push_back(n.eqNode(ret));
573
      }
574
    }
575
441748
    reqHasTerm = false;
576
  }
577
614045
  else if (n.hasOperator())
578
  {
579
1226970
    std::vector<TNode> args;
580
613485
    bool ret_set = false;
581
613485
    Kind k = n.getKind();
582
1226970
    std::vector<Node> tempExp;
583
1145313
    for (unsigned i = 0, nchild = n.getNumChildren(); i < nchild; i++)
584
    {
585
1786672
      TNode c = evaluateTerm2(n[i],
586
                              visited,
587
                              tempExp,
588
                              useEntailmentTests,
589
                              computeExp,
590
1425164
                              reqHasTerm);
591
893336
      if (c.isNull())
592
      {
593
315851
        ret = Node::null();
594
315851
        ret_set = true;
595
315851
        break;
596
      }
597
577485
      else if (c == d_true || c == d_false)
598
      {
599
        // short-circuiting
600
232422
        if ((k == AND && c == d_false) || (k == OR && c == d_true))
601
        {
602
37509
          ret = c;
603
37509
          ret_set = true;
604
37509
          reqHasTerm = false;
605
37509
          break;
606
        }
607
194913
        else if (k == ITE && i == 0)
608
        {
609
8148
          ret = evaluateTerm2(n[c == d_true ? 1 : 2],
610
                              visited,
611
                              tempExp,
612
                              useEntailmentTests,
613
                              computeExp,
614
                              reqHasTerm);
615
8148
          ret_set = true;
616
8148
          reqHasTerm = false;
617
8148
          break;
618
        }
619
      }
620
531828
      if (computeExp)
621
      {
622
        exp.insert(exp.end(), tempExp.begin(), tempExp.end());
623
      }
624
531828
      Trace("term-db-eval") << "  child " << i << " : " << c << std::endl;
625
531828
      args.push_back(c);
626
    }
627
613485
    if (ret_set)
628
    {
629
      // if we short circuited
630
361508
      if (computeExp)
631
      {
632
        exp.clear();
633
        exp.insert(exp.end(), tempExp.begin(), tempExp.end());
634
      }
635
    }
636
    else
637
    {
638
      // get the (indexed) operator of n, if it exists
639
503954
      TNode f = getMatchOperator(n);
640
      // if it is an indexed term, return the congruent term
641
251977
      if (!f.isNull())
642
      {
643
        // if f is congruent to a term indexed by this class
644
308286
        TNode nn = getCongruentTerm(f, args);
645
308286
        Trace("term-db-eval") << "  got congruent term " << nn
646
154143
                              << " from DB for " << n << std::endl;
647
154143
        if (!nn.isNull())
648
        {
649
29513
          if (computeExp)
650
          {
651
            Assert(nn.getNumChildren() == n.getNumChildren());
652
            for (unsigned i = 0, nchild = nn.getNumChildren(); i < nchild; i++)
653
            {
654
              if (nn[i] != n[i])
655
              {
656
                exp.push_back(nn[i].eqNode(n[i]));
657
              }
658
            }
659
          }
660
29513
          ret = d_qstate.getRepresentative(nn);
661
29513
          Trace("term-db-eval") << "return rep" << std::endl;
662
29513
          ret_set = true;
663
29513
          reqHasTerm = false;
664
29513
          Assert(!ret.isNull());
665
29513
          if (computeExp)
666
          {
667
            if (n != ret)
668
            {
669
              exp.push_back(nn.eqNode(ret));
670
            }
671
          }
672
        }
673
      }
674
251977
      if( !ret_set ){
675
222464
        Trace("term-db-eval") << "return rewrite" << std::endl;
676
        // a theory symbol or a new UF term
677
222464
        if (n.getMetaKind() == metakind::PARAMETERIZED)
678
        {
679
124491
          args.insert(args.begin(), n.getOperator());
680
        }
681
222464
        ret = NodeManager::currentNM()->mkNode(n.getKind(), args);
682
222464
        ret = Rewriter::rewrite(ret);
683
222464
        if (ret.getKind() == EQUAL)
684
        {
685
4196
          if (d_qstate.areDisequal(ret[0], ret[1]))
686
          {
687
1921
            ret = d_false;
688
          }
689
        }
690
222464
        if (useEntailmentTests)
691
        {
692
1365
          if (ret.getKind() == EQUAL || ret.getKind() == GEQ)
693
          {
694
15
            Valuation& val = d_qstate.getValuation();
695
41
            for (unsigned j = 0; j < 2; j++)
696
            {
697
              std::pair<bool, Node> et = val.entailmentCheck(
698
                  options::TheoryOfMode::THEORY_OF_TYPE_BASED,
699
56
                  j == 0 ? ret : ret.negate());
700
30
              if (et.first)
701
              {
702
4
                ret = j == 0 ? d_true : d_false;
703
4
                if (computeExp)
704
                {
705
                  exp.push_back(et.second);
706
                }
707
4
                break;
708
              }
709
            }
710
          }
711
        }
712
      }
713
    }
714
  }
715
  // must have the term
716
1058252
  if (reqHasTerm && !ret.isNull())
717
  {
718
220665
    Kind k = ret.getKind();
719
220665
    if (k != OR && k != AND && k != EQUAL && k != ITE && k != NOT
720
218021
        && k != FORALL)
721
    {
722
217838
      if (!d_qstate.hasTerm(ret))
723
      {
724
122128
        ret = Node::null();
725
      }
726
    }
727
  }
728
2116504
  Trace("term-db-eval") << "evaluated term : " << n << ", got : " << ret
729
1058252
                        << ", reqHasTerm = " << reqHasTerm << std::endl;
730
  // clear the explanation if failed
731
1058252
  if (computeExp && ret.isNull())
732
  {
733
    exp.resize(prevSize);
734
  }
735
1058252
  visited[n] = ret;
736
1058252
  return ret;
737
}
738
739
11480443
TNode TermDb::getEntailedTerm2(TNode n,
740
                               std::map<TNode, TNode>& subs,
741
                               bool subsRep,
742
                               bool hasSubs)
743
{
744
11480443
  Trace("term-db-entail") << "get entailed term : " << n << std::endl;
745
11480443
  if (d_qstate.hasTerm(n))
746
  {
747
3730096
    Trace("term-db-entail") << "...exists in ee, return rep " << std::endl;
748
3730096
    return n;
749
7750347
  }else if( n.getKind()==BOUND_VARIABLE ){
750
4142300
    if( hasSubs ){
751
4142300
      std::map< TNode, TNode >::iterator it = subs.find( n );
752
4142300
      if( it!=subs.end() ){
753
3190818
        Trace("term-db-entail") << "...substitution is : " << it->second << std::endl;
754
3190818
        if( subsRep ){
755
354878
          Assert(d_qstate.hasTerm(it->second));
756
354878
          Assert(d_qstate.getRepresentative(it->second) == it->second);
757
3545696
          return it->second;
758
        }
759
2835940
        return getEntailedTerm2(it->second, subs, subsRep, hasSubs);
760
      }
761
    }
762
3608047
  }else if( n.getKind()==ITE ){
763
63249
    for( unsigned i=0; i<2; i++ ){
764
59607
      if (isEntailed2(n[0], subs, subsRep, hasSubs, i == 0))
765
      {
766
28616
        return getEntailedTerm2(n[i == 0 ? 1 : 2], subs, subsRep, hasSubs);
767
      }
768
    }
769
  }else{
770
3575789
    if( n.hasOperator() ){
771
3578358
      TNode f = getMatchOperator( n );
772
3567663
      if( !f.isNull() ){
773
7113936
        std::vector< TNode > args;
774
7691124
        for( unsigned i=0; i<n.getNumChildren(); i++ ){
775
10233497
          TNode c = getEntailedTerm2(n[i], subs, subsRep, hasSubs);
776
6099341
          if( c.isNull() ){
777
1965185
            return TNode::null();
778
          }
779
4134156
          c = d_qstate.getRepresentative(c);
780
4134156
          Trace("term-db-entail") << "  child " << i << " : " << c << std::endl;
781
4134156
          args.push_back( c );
782
        }
783
3183566
        TNode nn = getCongruentTerm(f, args);
784
1591783
        Trace("term-db-entail") << "  got congruent term " << nn << " for " << n << std::endl;
785
1591783
        return nn;
786
      }
787
    }
788
  }
789
973945
  return TNode::null();
790
}
791
792
188589
Node TermDb::evaluateTerm(TNode n,
793
                          bool useEntailmentTests,
794
                          bool reqHasTerm)
795
{
796
377178
  std::map< TNode, Node > visited;
797
377178
  std::vector<Node> exp;
798
377178
  return evaluateTerm2(n, visited, exp, useEntailmentTests, false, reqHasTerm);
799
}
800
801
Node TermDb::evaluateTerm(TNode n,
802
                          std::vector<Node>& exp,
803
                          bool useEntailmentTests,
804
                          bool reqHasTerm)
805
{
806
  std::map<TNode, Node> visited;
807
  return evaluateTerm2(n, visited, exp, useEntailmentTests, true, reqHasTerm);
808
}
809
810
882686
TNode TermDb::getEntailedTerm(TNode n,
811
                              std::map<TNode, TNode>& subs,
812
                              bool subsRep)
813
{
814
882686
  return getEntailedTerm2(n, subs, subsRep, true);
815
}
816
817
104522
TNode TermDb::getEntailedTerm(TNode n)
818
{
819
209044
  std::map< TNode, TNode > subs;
820
209044
  return getEntailedTerm2(n, subs, false, false);
821
}
822
823
2294853
bool TermDb::isEntailed2(
824
    TNode n, std::map<TNode, TNode>& subs, bool subsRep, bool hasSubs, bool pol)
825
{
826
2294853
  Trace("term-db-entail") << "Check entailed : " << n << ", pol = " << pol << std::endl;
827
2294853
  Assert(n.getType().isBoolean());
828
2294853
  if( n.getKind()==EQUAL && !n[0].getType().isBoolean() ){
829
516116
    TNode n1 = getEntailedTerm2(n[0], subs, subsRep, hasSubs);
830
445043
    if( !n1.isNull() ){
831
445672
      TNode n2 = getEntailedTerm2(n[1], subs, subsRep, hasSubs);
832
409821
      if( !n2.isNull() ){
833
373970
        if( n1==n2 ){
834
27078
          return pol;
835
        }else{
836
346892
          Assert(d_qstate.hasTerm(n1));
837
346892
          Assert(d_qstate.hasTerm(n2));
838
346892
          if( pol ){
839
174377
            return d_qstate.areEqual(n1, n2);
840
          }else{
841
172515
            return d_qstate.areDisequal(n1, n2);
842
          }
843
        }
844
      }
845
    }
846
1849810
  }else if( n.getKind()==NOT ){
847
481764
    return isEntailed2(n[0], subs, subsRep, hasSubs, !pol);
848
1368046
  }else if( n.getKind()==OR || n.getKind()==AND ){
849
266673
    bool simPol = ( pol && n.getKind()==OR ) || ( !pol && n.getKind()==AND );
850
831948
    for( unsigned i=0; i<n.getNumChildren(); i++ ){
851
747511
      if (isEntailed2(n[i], subs, subsRep, hasSubs, pol))
852
      {
853
205877
        if( simPol ){
854
94845
          return true;
855
        }
856
      }else{
857
541634
        if( !simPol ){
858
87391
          return false;
859
        }
860
      }
861
    }
862
84437
    return !simPol;
863
  //Boolean equality here
864
1101373
  }else if( n.getKind()==EQUAL || n.getKind()==ITE ){
865
603817
    for( unsigned i=0; i<2; i++ ){
866
432102
      if (isEntailed2(n[0], subs, subsRep, hasSubs, i == 0))
867
      {
868
58872
        unsigned ch = ( n.getKind()==EQUAL || i==0 ) ? 1 : 2;
869
58872
        bool reqPol = ( n.getKind()==ITE || i==0 ) ? pol : !pol;
870
58872
        return isEntailed2(n[ch], subs, subsRep, hasSubs, reqPol);
871
      }
872
    }
873
870786
  }else if( n.getKind()==APPLY_UF ){
874
1100481
    TNode n1 = getEntailedTerm2(n, subs, subsRep, hasSubs);
875
674474
    if( !n1.isNull() ){
876
248467
      Assert(d_qstate.hasTerm(n1));
877
248467
      if( n1==d_true ){
878
        return pol;
879
248467
      }else if( n1==d_false ){
880
        return !pol;
881
      }else{
882
248467
        return d_qstate.getRepresentative(n1) == (pol ? d_true : d_false);
883
      }
884
    }
885
196312
  }else if( n.getKind()==FORALL && !pol ){
886
7955
    return isEntailed2(n[1], subs, subsRep, hasSubs, pol);
887
  }
888
857152
  return false;
889
}
890
891
5574
bool TermDb::isEntailed(TNode n, bool pol)
892
{
893
5574
  Assert(d_consistent_ee);
894
11148
  std::map< TNode, TNode > subs;
895
11148
  return isEntailed2(n, subs, false, false, pol);
896
}
897
898
501468
bool TermDb::isEntailed(TNode n,
899
                        std::map<TNode, TNode>& subs,
900
                        bool subsRep,
901
                        bool pol)
902
{
903
501468
  Assert(d_consistent_ee);
904
501468
  return isEntailed2(n, subs, subsRep, true, pol);
905
}
906
907
4723139
bool TermDb::isTermActive( Node n ) {
908
4723139
  return d_inactive_map.find( n )==d_inactive_map.end();
909
  //return !n.getAttribute(NoMatchAttribute());
910
}
911
912
169607
void TermDb::setTermInactive( Node n ) {
913
169607
  d_inactive_map[n] = true;
914
  //Trace("term-db-debug2") << "set no match attribute" << std::endl;
915
  //NoMatchAttribute nma;
916
  //n.setAttribute(nma,true);
917
169607
}
918
919
4723348
bool TermDb::hasTermCurrent( Node n, bool useMode ) {
920
4723348
  if( !useMode ){
921
    return d_has_map.find( n )!=d_has_map.end();
922
  }
923
  //some assertions are not sent to EE
924
9474947
  if (options::termDbMode() == options::TermDbMode::ALL)
925
  {
926
4723348
    return true;
927
  }
928
  else if (options::termDbMode() == options::TermDbMode::RELEVANT)
929
  {
930
    return d_has_map.find( n )!=d_has_map.end();
931
  }
932
  Assert(false) << "TermDb::hasTermCurrent: Unknown termDbMode : " << options::termDbMode();
933
  return false;
934
}
935
936
854
bool TermDb::isTermEligibleForInstantiation(TNode n, TNode f)
937
{
938
854
  if( options::instMaxLevel()!=-1 ){
939
678
    if( n.hasAttribute(InstLevelAttribute()) ){
940
      int64_t fml =
941
678
          f.isNull() ? -1 : d_qreg.getQuantAttributes().getQuantInstLevel(f);
942
678
      unsigned ml = fml>=0 ? fml : options::instMaxLevel();
943
944
678
      if( n.getAttribute(InstLevelAttribute())>ml ){
945
        Trace("inst-add-debug") << "Term " << n << " has instantiation level " << n.getAttribute(InstLevelAttribute());
946
        Trace("inst-add-debug") << ", which is more than maximum allowed level " << ml << " for this quantified formula." << std::endl;
947
        return false;
948
      }
949
    }else{
950
      if( options::instLevelInputOnly() ){
951
        Trace("inst-add-debug") << "Term " << n << " does not have an instantiation level." << std::endl;
952
        return false;
953
      }
954
    }
955
  }
956
  // it cannot have instantiation constants, which originate from
957
  // counterexample-guided instantiation strategies.
958
854
  return !TermUtil::hasInstConstAttr(n);
959
}
960
961
176
Node TermDb::getEligibleTermInEqc( TNode r ) {
962
176
  if( isTermEligibleForInstantiation( r, TNode::null() ) ){
963
176
    return r;
964
  }else{
965
    std::map< Node, Node >::iterator it = d_term_elig_eqc.find( r );
966
    if( it==d_term_elig_eqc.end() ){
967
      Node h;
968
      eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
969
      eq::EqClassIterator eqc_i = eq::EqClassIterator(r, ee);
970
      while (!eqc_i.isFinished())
971
      {
972
        TNode n = (*eqc_i);
973
        ++eqc_i;
974
        if (isTermEligibleForInstantiation(n, TNode::null()))
975
        {
976
          h = n;
977
          break;
978
        }
979
      }
980
      d_term_elig_eqc[r] = h;
981
      return h;
982
    }else{
983
      return it->second;
984
    }
985
  }
986
}
987
988
void TermDb::setHasTerm( Node n ) {
989
  Trace("term-db-debug2") << "hasTerm : " << n  << std::endl;
990
  if( d_has_map.find( n )==d_has_map.end() ){
991
    d_has_map[n] = true;
992
    for( unsigned i=0; i<n.getNumChildren(); i++ ){
993
      setHasTerm( n[i] );
994
    }
995
  }
996
}
997
998
6438
void TermDb::presolve() {
999
6438
  if (options::incrementalSolving() && !options::termDbCd())
1000
  {
1001
    d_termsContext.pop();
1002
    d_termsContext.push();
1003
  }
1004
6438
}
1005
1006
28251
bool TermDb::reset( Theory::Effort effort ){
1007
28251
  d_op_nonred_count.clear();
1008
28251
  d_arg_reps.clear();
1009
28251
  d_func_map_trie.clear();
1010
28251
  d_func_map_eqc_trie.clear();
1011
28251
  d_func_map_rel_dom.clear();
1012
28251
  d_consistent_ee = true;
1013
1014
28251
  eq::EqualityEngine* ee = d_qstate.getEqualityEngine();
1015
1016
28251
  Assert(ee->consistent());
1017
  // if higher-order, add equalities for the purification terms now
1018
28251
  if (options::ufHo())
1019
  {
1020
2082
    Trace("quant-ho")
1021
1041
        << "TermDb::reset : assert higher-order purify equalities..."
1022
1041
        << std::endl;
1023
2061
    for (std::pair<const Node, Node>& pp : d_ho_purify_to_term)
1024
    {
1025
3060
      if (ee->hasTerm(pp.second)
1026
3060
          && (!ee->hasTerm(pp.first) || !ee->areEqual(pp.second, pp.first)))
1027
      {
1028
798
        Node eq;
1029
399
        std::map<Node, Node>::iterator itpe = d_ho_purify_to_eq.find(pp.first);
1030
399
        if (itpe == d_ho_purify_to_eq.end())
1031
        {
1032
202
          eq = Rewriter::rewrite(pp.first.eqNode(pp.second));
1033
202
          d_ho_purify_to_eq[pp.first] = eq;
1034
        }
1035
        else
1036
        {
1037
197
          eq = itpe->second;
1038
        }
1039
399
        Trace("quant-ho") << "- assert purify equality : " << eq << std::endl;
1040
399
        ee->assertEquality(eq, true, eq);
1041
399
        if (!ee->consistent())
1042
        {
1043
          // In some rare cases, purification functions (in the domain of
1044
          // d_ho_purify_to_term) may escape the term database. For example,
1045
          // matching algorithms may construct instantiations involving these
1046
          // functions. As a result, asserting these equalities internally may
1047
          // cause a conflict. In this case, we insist that the purification
1048
          // equality is sent out as a lemma here.
1049
          Trace("term-db-lemma")
1050
              << "Purify equality lemma: " << eq << std::endl;
1051
          d_qim->addPendingLemma(eq, InferenceId::UNKNOWN);
1052
          d_qstate.notifyInConflict();
1053
          d_consistent_ee = false;
1054
          return false;
1055
        }
1056
      }
1057
    }
1058
  }
1059
1060
  //compute has map
1061
28251
  if (options::termDbMode() == options::TermDbMode::RELEVANT)
1062
  {
1063
    d_has_map.clear();
1064
    d_term_elig_eqc.clear();
1065
    eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
1066
    while( !eqcs_i.isFinished() ){
1067
      TNode r = (*eqcs_i);
1068
      bool addedFirst = false;
1069
      Node first;
1070
      //TODO: ignoring singleton eqc isn't enough, need to ensure eqc are relevant
1071
      eq::EqClassIterator eqc_i = eq::EqClassIterator(r, ee);
1072
      while( !eqc_i.isFinished() ){
1073
        TNode n = (*eqc_i);
1074
        if( first.isNull() ){
1075
          first = n;
1076
        }else{
1077
          if( !addedFirst ){
1078
            addedFirst = true;
1079
            setHasTerm( first );
1080
          }
1081
          setHasTerm( n );
1082
        }
1083
        ++eqc_i;
1084
      }
1085
      ++eqcs_i;
1086
    }
1087
    const LogicInfo& logicInfo = d_qstate.getLogicInfo();
1088
    for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId)
1089
    {
1090
      if (!logicInfo.isTheoryEnabled(theoryId))
1091
      {
1092
        continue;
1093
      }
1094
      for (context::CDList<Assertion>::const_iterator
1095
               it = d_qstate.factsBegin(theoryId),
1096
               it_end = d_qstate.factsEnd(theoryId);
1097
           it != it_end;
1098
           ++it)
1099
      {
1100
        setHasTerm((*it).d_assertion);
1101
      }
1102
    }
1103
  }
1104
1105
29292
  if( options::ufHo() && options::hoMergeTermDb() ){
1106
1041
    Trace("quant-ho") << "TermDb::reset : compute equal functions..." << std::endl;
1107
    // build operator representative map
1108
1041
    d_ho_op_rep.clear();
1109
1041
    d_ho_op_slaves.clear();
1110
1041
    eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
1111
107763
    while( !eqcs_i.isFinished() ){
1112
106722
      TNode r = (*eqcs_i);
1113
53361
      if( r.getType().isFunction() ){
1114
3416
        Trace("quant-ho") << "  process function eqc " << r << std::endl;
1115
6832
        Node first;
1116
3416
        eq::EqClassIterator eqc_i = eq::EqClassIterator(r, ee);
1117
11504
        while( !eqc_i.isFinished() ){
1118
8088
          TNode n = (*eqc_i);
1119
8088
          Node n_use;
1120
4044
          if (n.isVar())
1121
          {
1122
3513
            n_use = n;
1123
          }
1124
          else
1125
          {
1126
            // use its purified variable, if it exists
1127
531
            std::map<Node, Node>::iterator itp = d_ho_fun_op_purify.find(n);
1128
531
            if (itp != d_ho_fun_op_purify.end())
1129
            {
1130
468
              n_use = itp->second;
1131
            }
1132
          }
1133
8088
          Trace("quant-ho") << "  - process " << n_use << ", from " << n
1134
4044
                            << std::endl;
1135
4044
          if (!n_use.isNull() && d_opMap.find(n_use) != d_opMap.end())
1136
          {
1137
3300
            if (first.isNull())
1138
            {
1139
3003
              first = n_use;
1140
3003
              d_ho_op_rep[n_use] = n_use;
1141
            }
1142
            else
1143
            {
1144
594
              Trace("quant-ho") << "  have : " << n_use << " == " << first
1145
297
                                << ", type = " << n_use.getType() << std::endl;
1146
297
              d_ho_op_rep[n_use] = first;
1147
297
              d_ho_op_slaves[first].push_back(n_use);
1148
            }
1149
          }
1150
4044
          ++eqc_i;
1151
        }
1152
      }
1153
53361
      ++eqcs_i;
1154
    }
1155
1041
    Trace("quant-ho") << "...finished compute equal functions." << std::endl;
1156
  }
1157
1158
28251
  return true;
1159
}
1160
1161
21950
TNodeTrie* TermDb::getTermArgTrie(Node f)
1162
{
1163
21950
  if( options::ufHo() ){
1164
4121
    f = getOperatorRepresentative( f );
1165
  }
1166
21950
  computeUfTerms( f );
1167
21950
  std::map<Node, TNodeTrie>::iterator itut = d_func_map_trie.find(f);
1168
21950
  if( itut!=d_func_map_trie.end() ){
1169
13988
    return &itut->second;
1170
  }else{
1171
7962
    return NULL;
1172
  }
1173
}
1174
1175
2117385
TNodeTrie* TermDb::getTermArgTrie(Node eqc, Node f)
1176
{
1177
2117385
  if( options::ufHo() ){
1178
345296
    f = getOperatorRepresentative( f );
1179
  }
1180
2117385
  computeUfEqcTerms( f );
1181
2117385
  std::map<Node, TNodeTrie>::iterator itut = d_func_map_eqc_trie.find(f);
1182
2117385
  if( itut==d_func_map_eqc_trie.end() ){
1183
    return NULL;
1184
  }else{
1185
2117385
    if( eqc.isNull() ){
1186
1137203
      return &itut->second;
1187
    }else{
1188
      std::map<TNode, TNodeTrie>::iterator itute =
1189
980182
          itut->second.d_data.find(eqc);
1190
980182
      if( itute!=itut->second.d_data.end() ){
1191
582190
        return &itute->second;
1192
      }else{
1193
397992
        return NULL;
1194
      }
1195
    }
1196
  }
1197
}
1198
1199
TNode TermDb::getCongruentTerm( Node f, Node n ) {
1200
  if( options::ufHo() ){
1201
    f = getOperatorRepresentative( f );
1202
  }
1203
  computeUfTerms( f );
1204
  std::map<Node, TNodeTrie>::iterator itut = d_func_map_trie.find(f);
1205
  if( itut!=d_func_map_trie.end() ){
1206
    computeArgReps( n );
1207
    return itut->second.existsTerm( d_arg_reps[n] );
1208
  }else{
1209
    return TNode::null();
1210
  }
1211
}
1212
1213
1745926
TNode TermDb::getCongruentTerm( Node f, std::vector< TNode >& args ) {
1214
1745926
  if( options::ufHo() ){
1215
713761
    f = getOperatorRepresentative( f );
1216
  }
1217
1745926
  computeUfTerms( f );
1218
1745926
  return d_func_map_trie[f].existsTerm( args );
1219
}
1220
1221
156
Node TermDb::getHoTypeMatchPredicate(TypeNode tn)
1222
{
1223
156
  std::map<TypeNode, Node>::iterator ithp = d_ho_type_match_pred.find(tn);
1224
156
  if (ithp != d_ho_type_match_pred.end())
1225
  {
1226
124
    return ithp->second;
1227
  }
1228
32
  NodeManager* nm = NodeManager::currentNM();
1229
64
  TypeNode ptn = nm->mkFunctionType(tn, nm->booleanType());
1230
64
  Node k = nm->mkSkolem("U", ptn, "predicate to force higher-order types");
1231
32
  d_ho_type_match_pred[tn] = k;
1232
32
  return k;
1233
}
1234
1235
}/* CVC4::theory::quantifiers namespace */
1236
}/* CVC4::theory namespace */
1237
4921218
}/* CVC4 namespace */