GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/uf/theory_uf.cpp Lines: 291 334 87.1 %
Date: 2021-03-23 Branches: 649 1360 47.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_uf.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Morgan Deters, Dejan Jovanovic
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 This is the interface to TheoryUF implementations
13
 **
14
 ** This is the interface to TheoryUF implementations.  All
15
 ** implementations of TheoryUF should inherit from this class.
16
 **/
17
18
#include "theory/uf/theory_uf.h"
19
20
#include <memory>
21
#include <sstream>
22
23
#include "expr/node_algorithm.h"
24
#include "expr/proof_node_manager.h"
25
#include "options/quantifiers_options.h"
26
#include "options/smt_options.h"
27
#include "options/theory_options.h"
28
#include "options/uf_options.h"
29
#include "smt/logic_exception.h"
30
#include "theory/theory_model.h"
31
#include "theory/type_enumerator.h"
32
#include "theory/uf/cardinality_extension.h"
33
#include "theory/uf/ho_extension.h"
34
#include "theory/uf/theory_uf_rewriter.h"
35
36
using namespace std;
37
38
namespace CVC4 {
39
namespace theory {
40
namespace uf {
41
42
/** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
43
8997
TheoryUF::TheoryUF(context::Context* c,
44
                   context::UserContext* u,
45
                   OutputChannel& out,
46
                   Valuation valuation,
47
                   const LogicInfo& logicInfo,
48
                   ProofNodeManager* pnm,
49
8997
                   std::string instanceName)
50
    : Theory(THEORY_UF, c, u, out, valuation, logicInfo, pnm, instanceName),
51
      d_thss(nullptr),
52
      d_ho(nullptr),
53
      d_functionsTerms(c),
54
      d_symb(u, instanceName),
55
      d_state(c, u, valuation),
56
      d_im(*this, d_state, pnm, "theory::uf", false),
57
8997
      d_notify(d_im, *this)
58
{
59
8997
  d_true = NodeManager::currentNM()->mkConst( true );
60
61
8997
  ProofChecker* pc = pnm != nullptr ? pnm->getChecker() : nullptr;
62
8997
  if (pc != nullptr)
63
  {
64
962
    d_ufProofChecker.registerTo(pc);
65
  }
66
  // indicate we are using the default theory state and inference managers
67
8997
  d_theoryState = &d_state;
68
8997
  d_inferManager = &d_im;
69
8997
}
70
71
17988
TheoryUF::~TheoryUF() {
72
17988
}
73
74
8997
TheoryRewriter* TheoryUF::getTheoryRewriter() { return &d_rewriter; }
75
76
8997
bool TheoryUF::needsEqualityEngine(EeSetupInfo& esi)
77
{
78
8997
  esi.d_notify = &d_notify;
79
8997
  esi.d_name = d_instanceName + "theory::uf::ee";
80
8997
  return true;
81
}
82
83
8997
void TheoryUF::finishInit() {
84
8997
  Assert(d_equalityEngine != nullptr);
85
  // combined cardinality constraints are not evaluated in getModelValue
86
8997
  d_valuation.setUnevaluatedKind(kind::COMBINED_CARDINALITY_CONSTRAINT);
87
  // Initialize the cardinality constraints solver if the logic includes UF,
88
  // finite model finding is enabled, and it is not disabled by
89
  // options::ufssMode().
90
17994
  if (options::finiteModelFind()
91
8997
      && options::ufssMode() != options::UfssMode::NONE)
92
  {
93
250
    d_thss.reset(new CardinalityExtension(d_state, d_im, this));
94
  }
95
  // The kinds we are treating as function application in congruence
96
8997
  d_equalityEngine->addFunctionKind(kind::APPLY_UF, false, options::ufHo());
97
8997
  if (options::ufHo())
98
  {
99
216
    d_equalityEngine->addFunctionKind(kind::HO_APPLY);
100
216
    d_ho.reset(new HoExtension(d_state, d_im));
101
  }
102
8997
}
103
104
static Node mkAnd(const std::vector<TNode>& conjunctions) {
105
  Assert(conjunctions.size() > 0);
106
107
  std::set<TNode> all;
108
  all.insert(conjunctions.begin(), conjunctions.end());
109
110
  if (all.size() == 1) {
111
    // All the same, or just one
112
    return conjunctions[0];
113
  }
114
115
  NodeBuilder<> conjunction(kind::AND);
116
  std::set<TNode>::const_iterator it = all.begin();
117
  std::set<TNode>::const_iterator it_end = all.end();
118
  while (it != it_end) {
119
    conjunction << *it;
120
    ++ it;
121
  }
122
123
  return conjunction;
124
}/* mkAnd() */
125
126
//--------------------------------- standard check
127
128
17911
bool TheoryUF::needsCheckLastEffort()
129
{
130
  // last call effort needed if using finite model finding
131
17911
  return d_thss != nullptr;
132
}
133
134
1556705
void TheoryUF::postCheck(Effort level)
135
{
136
1556705
  if (d_state.isInConflict())
137
  {
138
65684
    return;
139
  }
140
  // check with the cardinality constraints extension
141
1491021
  if (d_thss != nullptr)
142
  {
143
127301
    d_thss->check(level);
144
  }
145
  // check with the higher-order extension at full effort
146
1491021
  if (!d_state.isInConflict() && fullEffort(level))
147
  {
148
67840
    if (options::ufHo())
149
    {
150
1074
      d_ho->check();
151
    }
152
  }
153
}
154
155
4205857
bool TheoryUF::preNotifyFact(
156
    TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal)
157
{
158
4205857
  if (d_thss != nullptr)
159
  {
160
    bool isDecision =
161
274692
        d_valuation.isSatLiteral(fact) && d_valuation.isDecision(fact);
162
274692
    d_thss->assertNode(fact, isDecision);
163
274692
    if (d_state.isInConflict())
164
    {
165
771
      return true;
166
    }
167
  }
168
8410172
  if (atom.getKind() == kind::CARDINALITY_CONSTRAINT
169
4205086
      || atom.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT)
170
  {
171
11254
    if (d_thss == nullptr)
172
    {
173
      if (!getLogicInfo().hasCardinalityConstraints())
174
      {
175
        std::stringstream ss;
176
        ss << "Cardinality constraint " << atom
177
           << " was asserted, but the logic does not allow it." << std::endl;
178
        ss << "Try using a logic containing \"UFC\"." << std::endl;
179
        throw Exception(ss.str());
180
      }
181
      else
182
      {
183
        // support for cardinality constraints is not enabled, set incomplete
184
        d_im.setIncomplete();
185
      }
186
    }
187
    // don't need to assert cardinality constraints if not producing models
188
11254
    return !options::produceModels();
189
  }
190
4193832
  return false;
191
}
192
193
4196876
void TheoryUF::notifyFact(TNode atom, bool pol, TNode fact, bool isInternal)
194
{
195
4196876
  if (!d_state.isInConflict() && atom.getKind() == kind::EQUAL)
196
  {
197
3932798
    if (options::ufHo() && options::ufHoExt())
198
    {
199
69234
      if (!pol && !d_state.isInConflict() && atom[0].getType().isFunction())
200
      {
201
        // apply extensionality eagerly using the ho extension
202
295
        d_ho->applyExtensionality(fact);
203
      }
204
    }
205
  }
206
4196876
}
207
//--------------------------------- end standard check
208
209
469512
TrustNode TheoryUF::ppRewrite(TNode node, std::vector<SkolemLemma>& lems)
210
{
211
939024
  Trace("uf-exp-def") << "TheoryUF::ppRewrite: expanding definition : " << node
212
469512
                      << std::endl;
213
469512
  Kind k = node.getKind();
214
469512
  if (k == kind::HO_APPLY)
215
  {
216
256
    if( !options::ufHo() ){
217
      std::stringstream ss;
218
      ss << "Partial function applications are not supported in default mode, try --uf-ho.";
219
      throw LogicException(ss.str());
220
    }
221
392
    Node ret = d_ho->ppRewrite(node);
222
256
    if (ret != node)
223
    {
224
240
      Trace("uf-exp-def") << "TheoryUF::ppRewrite: higher-order: " << node
225
120
                          << " to " << ret << std::endl;
226
120
      return TrustNode::mkTrustRewrite(node, ret, nullptr);
227
    }
228
  }
229
469256
  else if (k == kind::APPLY_UF)
230
  {
231
    // check for higher-order
232
    // logic exception if higher-order is not enabled
233
80796
    if (isHigherOrderType(node.getOperator().getType()) && !options::ufHo())
234
    {
235
      std::stringstream ss;
236
      ss << "UF received an application whose operator has higher-order type "
237
         << node << ", which is not supported by default, try --uf-ho";
238
      throw LogicException(ss.str());
239
    }
240
  }
241
469392
  return TrustNode::null();
242
}
243
244
345184
void TheoryUF::preRegisterTerm(TNode node)
245
{
246
345184
  Debug("uf") << "TheoryUF::preRegisterTerm(" << node << ")" << std::endl;
247
248
345184
  if (d_thss != NULL) {
249
38904
    d_thss->preRegisterTerm(node);
250
  }
251
252
  // we always use APPLY_UF if not higher-order, HO_APPLY if higher-order
253
  //Assert( node.getKind()!=kind::APPLY_UF || !options::ufHo() );
254
345184
  Assert(node.getKind() != kind::HO_APPLY || options::ufHo());
255
256
345184
  Kind k = node.getKind();
257
345184
  switch (k)
258
  {
259
160016
    case kind::EQUAL:
260
      // Add the trigger for equality
261
160016
      d_equalityEngine->addTriggerPredicate(node);
262
160016
      break;
263
114022
    case kind::APPLY_UF:
264
    case kind::HO_APPLY:
265
    {
266
      // Maybe it's a predicate
267
114022
      if (node.getType().isBoolean())
268
      {
269
        // Get triggered for both equal and dis-equal
270
26935
        d_equalityEngine->addTriggerPredicate(node);
271
      }
272
      else
273
      {
274
        // Function applications/predicates
275
87087
        d_equalityEngine->addTerm(node);
276
      }
277
      // Remember the function and predicate terms
278
114022
      d_functionsTerms.push_back(node);
279
    }
280
114022
    break;
281
3014
  case kind::CARDINALITY_CONSTRAINT:
282
  case kind::COMBINED_CARDINALITY_CONSTRAINT:
283
    //do nothing
284
3014
    break;
285
68132
  default:
286
    // Variables etc
287
68132
    d_equalityEngine->addTerm(node);
288
68132
    break;
289
  }
290
345184
}
291
292
void TheoryUF::explain(TNode literal, Node& exp)
293
{
294
  Debug("uf") << "TheoryUF::explain(" << literal << ")" << std::endl;
295
  std::vector<TNode> assumptions;
296
  // Do the work
297
  bool polarity = literal.getKind() != kind::NOT;
298
  TNode atom = polarity ? literal : literal[0];
299
  if (atom.getKind() == kind::EQUAL)
300
  {
301
    d_equalityEngine->explainEquality(
302
        atom[0], atom[1], polarity, assumptions, nullptr);
303
  }
304
  else
305
  {
306
    d_equalityEngine->explainPredicate(atom, polarity, assumptions, nullptr);
307
  }
308
  exp = mkAnd(assumptions);
309
}
310
311
128927
TrustNode TheoryUF::explain(TNode literal) { return d_im.explainLit(literal); }
312
313
16246
bool TheoryUF::collectModelValues(TheoryModel* m, const std::set<Node>& termSet)
314
{
315
16246
  if( options::ufHo() ){
316
    // must add extensionality disequalities for all pairs of (non-disequal)
317
    // function equivalence classes.
318
504
    if (!d_ho->collectModelInfoHo(m, termSet))
319
    {
320
      Trace("uf") << "Collect model info fail HO" << std::endl;
321
      return false;
322
    }
323
  }
324
325
16246
  Debug("uf") << "UF : finish collectModelInfo " << std::endl;
326
16246
  return true;
327
}
328
329
12422
void TheoryUF::presolve() {
330
  // TimerStat::CodeTimer codeTimer(d_presolveTimer);
331
332
12422
  Debug("uf") << "uf: begin presolve()" << endl;
333
12422
  if(options::ufSymmetryBreaker()) {
334
298
    vector<Node> newClauses;
335
149
    d_symb.apply(newClauses);
336
151
    for(vector<Node>::const_iterator i = newClauses.begin();
337
151
        i != newClauses.end();
338
        ++i) {
339
2
      Debug("uf") << "uf: generating a lemma: " << *i << std::endl;
340
      // no proof generator provided
341
2
      d_im.lemma(*i, InferenceId::UF_BREAK_SYMMETRY);
342
    }
343
  }
344
12422
  if( d_thss ){
345
300
    d_thss->presolve();
346
  }
347
12422
  Debug("uf") << "uf: end presolve()" << endl;
348
12422
}
349
350
92002
void TheoryUF::ppStaticLearn(TNode n, NodeBuilder<>& learned) {
351
  //TimerStat::CodeTimer codeTimer(d_staticLearningTimer);
352
353
184004
  vector<TNode> workList;
354
92002
  workList.push_back(n);
355
184004
  std::unordered_set<TNode, TNodeHashFunction> processed;
356
357
4557310
  while(!workList.empty()) {
358
2232654
    n = workList.back();
359
360
2255829
    if (n.isClosure())
361
    {
362
      // unsafe to go under quantifiers; we might pull bound vars out of scope!
363
23175
      processed.insert(n);
364
23175
      workList.pop_back();
365
23175
      continue;
366
    }
367
368
2209479
    bool unprocessedChildren = false;
369
7220760
    for(TNode::iterator i = n.begin(), iend = n.end(); i != iend; ++i) {
370
5011281
      if(processed.find(*i) == processed.end()) {
371
        // unprocessed child
372
1450325
        workList.push_back(*i);
373
1450325
        unprocessedChildren = true;
374
      }
375
    }
376
377
2209479
    if(unprocessedChildren) {
378
690327
      continue;
379
    }
380
381
1519152
    workList.pop_back();
382
    // has node n been processed in the meantime ?
383
1519152
    if(processed.find(n) != processed.end()) {
384
18649
      continue;
385
    }
386
1500503
    processed.insert(n);
387
388
    // == DIAMONDS ==
389
390
3001006
    Debug("diamonds") << "===================== looking at" << endl
391
1500503
                      << n << endl;
392
393
    // binary OR of binary ANDs of EQUALities
394
3769520
    if(n.getKind() == kind::OR && n.getNumChildren() == 2 &&
395
1917952
       n[0].getKind() == kind::AND && n[0].getNumChildren() == 2 &&
396
1515401
       n[1].getKind() == kind::AND && n[1].getNumChildren() == 2 &&
397
1505605
       (n[0][0].getKind() == kind::EQUAL) &&
398
1503143
       (n[0][1].getKind() == kind::EQUAL) &&
399
4504081
       (n[1][0].getKind() == kind::EQUAL) &&
400
1501789
       (n[1][1].getKind() == kind::EQUAL)) {
401
      // now we have (a = b && c = d) || (e = f && g = h)
402
403
631
      Debug("diamonds") << "has form of a diamond!" << endl;
404
405
      TNode
406
1244
        a = n[0][0][0], b = n[0][0][1],
407
1244
        c = n[0][1][0], d = n[0][1][1],
408
1244
        e = n[1][0][0], f = n[1][0][1],
409
1244
        g = n[1][1][0], h = n[1][1][1];
410
411
      // test that one of {a, b} = one of {c, d}, and make "b" the
412
      // shared node (i.e. put in the form (a = b && b = d))
413
      // note we don't actually care about the shared ones, so the
414
      // "swaps" below are one-sided, ignoring b and c
415
631
      if(a == c) {
416
16
        a = b;
417
615
      } else if(a == d) {
418
442
        a = b;
419
442
        d = c;
420
173
      } else if(b == c) {
421
        // nothing to do
422
49
      } else if(b == d) {
423
17
        d = c;
424
      } else {
425
        // condition not satisfied
426
16
        Debug("diamonds") << "+ A fails" << endl;
427
16
        continue;
428
      }
429
430
615
      Debug("diamonds") << "+ A holds" << endl;
431
432
      // same: one of {e, f} = one of {g, h}, and make "f" the
433
      // shared node (i.e. put in the form (e = f && f = h))
434
615
      if(e == g) {
435
16
        e = f;
436
599
      } else if(e == h) {
437
454
        e = f;
438
454
        h = g;
439
145
      } else if(f == g) {
440
        // nothing to do
441
7
      } else if(f == h) {
442
3
        h = g;
443
      } else {
444
        // condition not satisfied
445
2
        Debug("diamonds") << "+ B fails" << endl;
446
2
        continue;
447
      }
448
449
613
      Debug("diamonds") << "+ B holds" << endl;
450
451
      // now we have (a = b && b = d) || (e = f && f = h)
452
      // test that {a, d} == {e, h}
453
1226
      if( (a == e && d == h) ||
454
          (a == h && d == e) ) {
455
        // learn: n implies a == d
456
613
        Debug("diamonds") << "+ C holds" << endl;
457
1226
        Node newEquality = a.eqNode(d);
458
613
        Debug("diamonds") << "  ==> " << newEquality << endl;
459
613
        learned << n.impNode(newEquality);
460
      } else {
461
        Debug("diamonds") << "+ C fails" << endl;
462
      }
463
    }
464
  }
465
466
92002
  if(options::ufSymmetryBreaker()) {
467
24116
    d_symb.assertFormula(n);
468
  }
469
92002
}/* TheoryUF::ppStaticLearn() */
470
471
1763
EqualityStatus TheoryUF::getEqualityStatus(TNode a, TNode b) {
472
473
  // Check for equality (simplest)
474
1763
  if (d_equalityEngine->areEqual(a, b))
475
  {
476
    // The terms are implied to be equal
477
    return EQUALITY_TRUE;
478
  }
479
480
  // Check for disequality
481
1763
  if (d_equalityEngine->areDisequal(a, b, false))
482
  {
483
    // The terms are implied to be dis-equal
484
    return EQUALITY_FALSE;
485
  }
486
487
  // All other terms we interpret as dis-equal in the model
488
1763
  return EQUALITY_FALSE_IN_MODEL;
489
}
490
491
1669161
bool TheoryUF::areCareDisequal(TNode x, TNode y){
492
1669161
  Assert(d_equalityEngine->hasTerm(x));
493
1669161
  Assert(d_equalityEngine->hasTerm(y));
494
5007483
  if (d_equalityEngine->isTriggerTerm(x, THEORY_UF)
495
5007483
      && d_equalityEngine->isTriggerTerm(y, THEORY_UF))
496
  {
497
    TNode x_shared =
498
1673070
        d_equalityEngine->getTriggerTermRepresentative(x, THEORY_UF);
499
    TNode y_shared =
500
1673070
        d_equalityEngine->getTriggerTermRepresentative(y, THEORY_UF);
501
1385112
    EqualityStatus eqStatus = d_valuation.getEqualityStatus(x_shared, y_shared);
502
1385112
    if( eqStatus==EQUALITY_FALSE_AND_PROPAGATED || eqStatus==EQUALITY_FALSE || eqStatus==EQUALITY_FALSE_IN_MODEL ){
503
1097154
      return true;
504
    }
505
  }
506
572007
  return false;
507
}
508
509
461961
void TheoryUF::addCarePairs(const TNodeTrie* t1,
510
                            const TNodeTrie* t2,
511
                            unsigned arity,
512
                            unsigned depth)
513
{
514
461961
  if( depth==arity ){
515
148316
    if( t2!=NULL ){
516
296632
      Node f1 = t1->getData();
517
296632
      Node f2 = t2->getData();
518
148316
      if (!d_equalityEngine->areEqual(f1, f2))
519
      {
520
137657
        Debug("uf::sharing") << "TheoryUf::computeCareGraph(): checking function " << f1 << " and " << f2 << std::endl;
521
275314
        vector< pair<TNode, TNode> > currentPairs;
522
357248
        for (size_t k = 0, nchildren = f1.getNumChildren(); k < nchildren; ++k)
523
        {
524
439182
          TNode x = f1[k];
525
439182
          TNode y = f2[k];
526
219591
          Assert(d_equalityEngine->hasTerm(x));
527
219591
          Assert(d_equalityEngine->hasTerm(y));
528
219591
          Assert(!d_equalityEngine->areDisequal(x, y, false));
529
219591
          Assert(!areCareDisequal(x, y));
530
219591
          if (!d_equalityEngine->areEqual(x, y))
531
          {
532
426216
            if (d_equalityEngine->isTriggerTerm(x, THEORY_UF)
533
426216
                && d_equalityEngine->isTriggerTerm(y, THEORY_UF))
534
            {
535
              TNode x_shared =
536
124592
                  d_equalityEngine->getTriggerTermRepresentative(x, THEORY_UF);
537
              TNode y_shared =
538
124592
                  d_equalityEngine->getTriggerTermRepresentative(y, THEORY_UF);
539
62296
              currentPairs.push_back(make_pair(x_shared, y_shared));
540
            }
541
          }
542
        }
543
199953
        for (unsigned c = 0; c < currentPairs.size(); ++ c) {
544
62296
          Debug("uf::sharing") << "TheoryUf::computeCareGraph(): adding to care-graph" << std::endl;
545
62296
          addCarePair(currentPairs[c].first, currentPairs[c].second);
546
        }
547
      }
548
    }
549
  }else{
550
313645
    if( t2==NULL ){
551
109545
      if( depth<(arity-1) ){
552
        //add care pairs internal to each child
553
111554
        for (const std::pair<const TNode, TNodeTrie>& tt : t1->d_data)
554
        {
555
64963
          addCarePairs(&tt.second, NULL, arity, depth + 1);
556
        }
557
      }
558
      //add care pairs based on each pair of non-disequal arguments
559
644626
      for (std::map<TNode, TNodeTrie>::const_iterator it = t1->d_data.begin();
560
644626
           it != t1->d_data.end();
561
           ++it)
562
      {
563
535081
        std::map<TNode, TNodeTrie>::const_iterator it2 = it;
564
535081
        ++it2;
565
7176577
        for( ; it2 != t1->d_data.end(); ++it2 ){
566
3320748
          if (!d_equalityEngine->areDisequal(it->first, it2->first, false))
567
          {
568
1139827
            if( !areCareDisequal(it->first, it2->first) ){
569
265161
              addCarePairs( &it->second, &it2->second, arity, depth+1 );
570
            }
571
          }
572
        }
573
      }
574
    }else{
575
      //add care pairs based on product of indices, non-disequal arguments
576
500649
      for (const std::pair<const TNode, TNodeTrie>& tt1 : t1->d_data)
577
      {
578
624462
        for (const std::pair<const TNode, TNodeTrie>& tt2 : t2->d_data)
579
        {
580
327913
          if (!d_equalityEngine->areDisequal(tt1.first, tt2.first, false))
581
          {
582
309743
            if (!areCareDisequal(tt1.first, tt2.first))
583
            {
584
87255
              addCarePairs(&tt1.second, &tt2.second, arity, depth + 1);
585
            }
586
          }
587
        }
588
      }
589
    }
590
  }
591
461961
}
592
593
29475
void TheoryUF::computeCareGraph() {
594
29475
  if (d_sharedTerms.empty())
595
  {
596
7900
    return;
597
  }
598
  // Use term indexing. We build separate indices for APPLY_UF and HO_APPLY.
599
  // We maintain indices per operator for the former, and indices per
600
  // function type for the latter.
601
43150
  Debug("uf::sharing") << "TheoryUf::computeCareGraph(): Build term indices..."
602
21575
                       << std::endl;
603
43150
  std::map<Node, TNodeTrie> index;
604
43150
  std::map<TypeNode, TNodeTrie> hoIndex;
605
43150
  std::map<Node, size_t> arity;
606
589571
  for (TNode app : d_functionsTerms)
607
  {
608
1135992
    std::vector<TNode> reps;
609
567996
    bool has_trigger_arg = false;
610
1267817
    for (const Node& j : app)
611
    {
612
699821
      reps.push_back(d_equalityEngine->getRepresentative(j));
613
699821
      if (d_equalityEngine->isTriggerTerm(j, THEORY_UF))
614
      {
615
608313
        has_trigger_arg = true;
616
      }
617
    }
618
567996
    if (has_trigger_arg)
619
    {
620
514387
      if (app.getKind() == kind::APPLY_UF)
621
      {
622
1028710
        Node op = app.getOperator();
623
514355
        index[op].addTerm(app, reps);
624
514355
        arity[op] = reps.size();
625
      }
626
      else
627
      {
628
32
        Assert(app.getKind() == kind::HO_APPLY);
629
        // add it to the hoIndex for the function type
630
32
        hoIndex[app[0].getType()].addTerm(app, reps);
631
      }
632
    }
633
  }
634
  // for each index
635
66147
  for (std::pair<const Node, TNodeTrie>& tt : index)
636
  {
637
89144
    Debug("uf::sharing") << "TheoryUf::computeCareGraph(): Process index "
638
44572
                         << tt.first << "..." << std::endl;
639
44572
    Assert(arity.find(tt.first) != arity.end());
640
44572
    addCarePairs(&tt.second, nullptr, arity[tt.first], 0);
641
  }
642
21585
  for (std::pair<const TypeNode, TNodeTrie>& tt : hoIndex)
643
  {
644
20
    Debug("uf::sharing") << "TheoryUf::computeCareGraph(): Process ho index "
645
10
                         << tt.first << "..." << std::endl;
646
    // the arity of HO_APPLY is always two
647
10
    addCarePairs(&tt.second, nullptr, 2, 0);
648
  }
649
43150
  Debug("uf::sharing") << "TheoryUf::computeCareGraph(): finished."
650
21575
                       << std::endl;
651
}/* TheoryUF::computeCareGraph() */
652
653
229842
void TheoryUF::eqNotifyNewClass(TNode t) {
654
229842
  if (d_thss != NULL) {
655
30484
    d_thss->newEqClass(t);
656
  }
657
229842
}
658
659
5533741
void TheoryUF::eqNotifyMerge(TNode t1, TNode t2)
660
{
661
5533741
  if (d_thss != NULL) {
662
394220
    d_thss->merge(t1, t2);
663
  }
664
5533741
}
665
666
996238
void TheoryUF::eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
667
996238
  if (d_thss != NULL) {
668
24443
    d_thss->assertDisequal(t1, t2, reason);
669
  }
670
996238
}
671
672
80796
bool TheoryUF::isHigherOrderType(TypeNode tn)
673
{
674
80796
  Assert(tn.isFunction());
675
80796
  std::map<TypeNode, bool>::iterator it = d_isHoType.find(tn);
676
80796
  if (it != d_isHoType.end())
677
  {
678
76207
    return it->second;
679
  }
680
4589
  bool ret = false;
681
9178
  const std::vector<TypeNode>& argTypes = tn.getArgTypes();
682
13422
  for (const TypeNode& tnc : argTypes)
683
  {
684
8895
    if (tnc.isFunction())
685
    {
686
62
      ret = true;
687
62
      break;
688
    }
689
  }
690
4589
  d_isHoType[tn] = ret;
691
4589
  return ret;
692
}
693
694
} /* namespace CVC4::theory::uf */
695
} /* namespace CVC4::theory */
696
26685
} /* namespace CVC4 */