GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/uf/equality_engine.cpp Lines: 1263 1378 91.7 %
Date: 2021-03-22 Branches: 2454 5608 43.8 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file equality_engine.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Dejan Jovanovic, Andrew Reynolds, Haniel Barbosa
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 [[ Add one-line brief description here ]]
13
 **
14
 ** [[ Add lengthier description here ]]
15
 ** \todo document this file
16
 **/
17
18
#include "theory/uf/equality_engine.h"
19
20
#include "base/output.h"
21
#include "options/smt_options.h"
22
#include "proof/proof_manager.h"
23
#include "smt/smt_statistics_registry.h"
24
#include "theory/rewriter.h"
25
#include "theory/uf/eq_proof.h"
26
27
namespace CVC4 {
28
namespace theory {
29
namespace eq {
30
31
131959
EqualityEngine::Statistics::Statistics(std::string name)
32
263918
    : d_mergesCount(name + "::mergesCount", 0),
33
263918
      d_termsCount(name + "::termsCount", 0),
34
263918
      d_functionTermsCount(name + "::functionTermsCount", 0),
35
923713
      d_constantTermsCount(name + "::constantTermsCount", 0)
36
{
37
131959
  smtStatisticsRegistry()->registerStat(&d_mergesCount);
38
131959
  smtStatisticsRegistry()->registerStat(&d_termsCount);
39
131959
  smtStatisticsRegistry()->registerStat(&d_functionTermsCount);
40
131959
  smtStatisticsRegistry()->registerStat(&d_constantTermsCount);
41
131959
}
42
43
263828
EqualityEngine::Statistics::~Statistics() {
44
131914
  smtStatisticsRegistry()->unregisterStat(&d_mergesCount);
45
131914
  smtStatisticsRegistry()->unregisterStat(&d_termsCount);
46
131914
  smtStatisticsRegistry()->unregisterStat(&d_functionTermsCount);
47
131914
  smtStatisticsRegistry()->unregisterStat(&d_constantTermsCount);
48
131914
}
49
50
/**
51
 * Data used in the BFS search through the equality graph.
52
 */
53
struct BfsData {
54
  // The current node
55
  EqualityNodeId d_nodeId;
56
  // The index of the edge we traversed
57
  EqualityEdgeId d_edgeId;
58
  // Index in the queue of the previous node. Shouldn't be too much of them, at most the size
59
  // of the biggest equivalence class
60
  size_t d_previousIndex;
61
62
23729728
  BfsData(EqualityNodeId nodeId = null_id,
63
          EqualityEdgeId edgeId = null_edge,
64
          size_t prev = 0)
65
23729728
      : d_nodeId(nodeId), d_edgeId(edgeId), d_previousIndex(prev)
66
  {
67
23729728
  }
68
};
69
70
class ScopedBool {
71
  bool& d_watch;
72
  bool d_oldValue;
73
74
 public:
75
23350226
  ScopedBool(bool& watch, bool newValue) : d_watch(watch), d_oldValue(watch)
76
  {
77
23350226
    d_watch = newValue;
78
23350226
  }
79
23350226
  ~ScopedBool() { d_watch = d_oldValue; }
80
};
81
82
8892
EqualityEngineNotifyNone EqualityEngine::s_notifyNone;
83
84
131959
void EqualityEngine::init() {
85
131959
  Debug("equality") << "EqualityEdge::EqualityEngine(): id_null = " << +null_id << std::endl;
86
131959
  Debug("equality") << "EqualityEdge::EqualityEngine(): edge_null = " << +null_edge << std::endl;
87
131959
  Debug("equality") << "EqualityEdge::EqualityEngine(): trigger_null = " << +null_trigger << std::endl;
88
89
  // If we are not at level zero when we initialize this equality engine, we
90
  // may remove true/false from the equality engine when we pop to level zero,
91
  // which leads to issues.
92
131959
  Assert(d_context->getLevel() == 0);
93
94
131959
  d_true = NodeManager::currentNM()->mkConst<bool>(true);
95
131959
  d_false = NodeManager::currentNM()->mkConst<bool>(false);
96
97
131959
  d_triggerDatabaseAllocatedSize = 100000;
98
131959
  d_triggerDatabase = (char*) malloc(d_triggerDatabaseAllocatedSize);
99
100
  //We can't notify during the initialization because it notifies
101
  // QuantifiersEngine.AddTermToDatabase that try to access to the uf
102
  // instantiator that currently doesn't exist.
103
263918
  ScopedBool sb(d_performNotify, false);
104
131959
  addTermInternal(d_true);
105
131959
  addTermInternal(d_false);
106
107
131959
  d_trueId = getNodeId(d_true);
108
131959
  d_falseId = getNodeId(d_false);
109
131959
}
110
111
377738
EqualityEngine::~EqualityEngine() {
112
131914
  free(d_triggerDatabase);
113
245824
}
114
115
26993
EqualityEngine::EqualityEngine(context::Context* context,
116
                               std::string name,
117
                               bool constantsAreTriggers,
118
26993
                               bool anyTermTriggers)
119
    : ContextNotifyObj(context),
120
      d_masterEqualityEngine(0),
121
      d_context(context),
122
      d_done(context, false),
123
      d_performNotify(true),
124
      d_notify(s_notifyNone),
125
      d_applicationLookupsCount(context, 0),
126
      d_nodesCount(context, 0),
127
      d_assertedEqualitiesCount(context, 0),
128
      d_equalityTriggersCount(context, 0),
129
      d_subtermEvaluatesSize(context, 0),
130
      d_stats(name),
131
      d_inPropagate(false),
132
      d_constantsAreTriggers(constantsAreTriggers),
133
      d_anyTermsAreTriggers(anyTermTriggers),
134
      d_triggerDatabaseSize(context, 0),
135
      d_triggerTermSetUpdatesSize(context, 0),
136
      d_deducedDisequalitiesSize(context, 0),
137
      d_deducedDisequalityReasonsSize(context, 0),
138
      d_propagatedDisequalities(context),
139
26993
      d_name(name)
140
{
141
26993
  init();
142
26993
}
143
144
104966
EqualityEngine::EqualityEngine(EqualityEngineNotify& notify,
145
                               context::Context* context,
146
                               std::string name,
147
                               bool constantsAreTriggers,
148
104966
                               bool anyTermTriggers)
149
    : ContextNotifyObj(context),
150
      d_masterEqualityEngine(0),
151
      d_context(context),
152
      d_done(context, false),
153
      d_performNotify(true),
154
      d_notify(notify),
155
      d_applicationLookupsCount(context, 0),
156
      d_nodesCount(context, 0),
157
      d_assertedEqualitiesCount(context, 0),
158
      d_equalityTriggersCount(context, 0),
159
      d_subtermEvaluatesSize(context, 0),
160
      d_stats(name),
161
      d_inPropagate(false),
162
      d_constantsAreTriggers(constantsAreTriggers),
163
      d_anyTermsAreTriggers(anyTermTriggers),
164
      d_triggerDatabaseSize(context, 0),
165
      d_triggerTermSetUpdatesSize(context, 0),
166
      d_deducedDisequalitiesSize(context, 0),
167
      d_deducedDisequalityReasonsSize(context, 0),
168
      d_propagatedDisequalities(context),
169
104966
      d_name(name)
170
{
171
104966
  init();
172
104966
}
173
174
60518
void EqualityEngine::setMasterEqualityEngine(EqualityEngine* master) {
175
60518
  Assert(d_masterEqualityEngine == 0);
176
60518
  d_masterEqualityEngine = master;
177
60518
}
178
179
35670723
void EqualityEngine::enqueue(const MergeCandidate& candidate, bool back) {
180
71341446
  Debug("equality") << d_name << "::eq::enqueue({" << candidate.d_t1Id << "} "
181
35670723
                    << d_nodes[candidate.d_t1Id] << ", {" << candidate.d_t2Id
182
35670723
                    << "} " << d_nodes[candidate.d_t2Id] << ", "
183
71341446
                    << static_cast<MergeReasonType>(candidate.d_type)
184
35670723
                    << "). reason: " << candidate.d_reason << std::endl;
185
35670723
  if (back) {
186
35670723
    d_propagationQueue.push_back(candidate);
187
  } else {
188
    d_propagationQueue.push_front(candidate);
189
  }
190
35670723
}
191
192
2901963
EqualityNodeId EqualityEngine::newApplicationNode(TNode original, EqualityNodeId t1, EqualityNodeId t2, FunctionApplicationType type) {
193
5803926
  Debug("equality") << d_name << "::eq::newApplicationNode(" << original
194
2901963
                    << ", {" << t1 << "} " << d_nodes[t1] << ", {" << t2 << "} "
195
2901963
                    << d_nodes[t2] << ")" << std::endl;
196
197
2901963
  ++d_stats.d_functionTermsCount;
198
199
  // Get another id for this
200
2901963
  EqualityNodeId funId = newNode(original);
201
2901963
  FunctionApplication funOriginal(type, t1, t2);
202
  // The function application we're creating
203
2901963
  EqualityNodeId t1ClassId = getEqualityNode(t1).getFind();
204
2901963
  EqualityNodeId t2ClassId = getEqualityNode(t2).getFind();
205
2901963
  FunctionApplication funNormalized(type, t1ClassId, t2ClassId);
206
207
5803926
  Debug("equality") << d_name << "::eq::newApplicationNode: funOriginal: ("
208
2901963
                    << type << " " << d_nodes[t1] << " " << d_nodes[t2]
209
2901963
                    << "), funNorm: (" << type << " " << d_nodes[t1ClassId]
210
2901963
                    << " " << d_nodes[t2ClassId] << ")\n";
211
212
  // We add the original version
213
2901963
  d_applications[funId] = FunctionApplicationPair(funOriginal, funNormalized);
214
215
  // Add the lookup data, if it's not already there
216
2901963
  ApplicationIdsMap::iterator find = d_applicationLookup.find(funNormalized);
217
2901963
  if (find == d_applicationLookup.end()) {
218
5272072
    Debug("equality") << d_name << "::eq::newApplicationNode(" << original
219
2636036
                      << ", " << t1 << ", " << t2
220
2636036
                      << "): no lookup, setting up funNorm: (" << type << " "
221
2636036
                      << d_nodes[t1ClassId] << " " << d_nodes[t2ClassId]
222
2636036
                      << ") => " << funId << std::endl;
223
    // Mark the normalization to the lookup
224
2636036
    storeApplicationLookup(funNormalized, funId);
225
  } else {
226
    // If it's there, we need to merge these two
227
265927
    Debug("equality") << d_name << "::eq::newApplicationNode(" << original << ", " << t1 << ", " << t2 << "): lookup exists, adding to queue" << std::endl;
228
265927
    Debug("equality") << d_name << "::eq::newApplicationNode(" << original << ", " << t1 << ", " << t2 << "): lookup = " << d_nodes[find->second] << std::endl;
229
265927
    enqueue(MergeCandidate(funId, find->second, MERGED_THROUGH_CONGRUENCE, TNode::null()));
230
  }
231
232
  // Add to the use lists
233
2901963
  Debug("equality") << d_name << "::eq::newApplicationNode(" << original << ", " << t1 << ", " << t2 << "): adding " << original << " to the uselist of " << d_nodes[t1] << std::endl;
234
2901963
  d_equalityNodes[t1].usedIn(funId, d_useListNodes);
235
2901963
  Debug("equality") << d_name << "::eq::newApplicationNode(" << original << ", " << t1 << ", " << t2 << "): adding " << original << " to the uselist of " << d_nodes[t2] << std::endl;
236
2901963
  d_equalityNodes[t2].usedIn(funId, d_useListNodes);
237
238
  // Return the new id
239
2901963
  Debug("equality") << d_name << "::eq::newApplicationNode(" << original << ", " << t1 << ", " << t2 << ") => " << funId << std::endl;
240
241
2901963
  return funId;
242
}
243
244
7641898
EqualityNodeId EqualityEngine::newNode(TNode node) {
245
246
7641898
  Debug("equality") << d_name << "::eq::newNode(" << node << ")" << std::endl;
247
248
7641898
  ++d_stats.d_termsCount;
249
250
  // Register the new id of the term
251
7641898
  EqualityNodeId newId = d_nodes.size();
252
7641898
  d_nodeIds[node] = newId;
253
  // Add the node to it's position
254
7641898
  d_nodes.push_back(node);
255
  // Note if this is an application or not
256
7641898
  d_applications.push_back(FunctionApplicationPair());
257
  // Add the trigger list for this node
258
7641898
  d_nodeTriggers.push_back(+null_trigger);
259
  // Add it to the equality graph
260
7641898
  d_equalityGraph.push_back(+null_edge);
261
  // Mark the no-individual trigger
262
7641898
  d_nodeIndividualTrigger.push_back(+null_set_id);
263
  // Mark non-constant by default
264
7641898
  d_isConstant.push_back(false);
265
  // No terms to evaluate by defaul
266
7641898
  d_subtermsToEvaluate.push_back(0);
267
  // Mark equality nodes
268
7641898
  d_isEquality.push_back(false);
269
  // Mark the node as internal by default
270
7641898
  d_isInternal.push_back(true);
271
  // Add the equality node to the nodes
272
7641898
  d_equalityNodes.push_back(EqualityNode(newId));
273
274
  // Increase the counters
275
7641898
  d_nodesCount = d_nodesCount + 1;
276
277
7641898
  Debug("equality") << d_name << "::eq::newNode(" << node << ") => " << newId << std::endl;
278
279
7641898
  return newId;
280
}
281
282
1000367
void EqualityEngine::addFunctionKind(Kind fun,
283
                                     bool interpreted,
284
                                     bool extOperator)
285
{
286
1000367
  d_congruenceKinds.set(fun);
287
1000367
  if (fun != kind::EQUAL)
288
  {
289
1000367
    if (interpreted)
290
    {
291
503032
      Debug("equality::evaluation")
292
251516
          << d_name << "::eq::addFunctionKind(): " << fun << " is interpreted "
293
251516
          << std::endl;
294
251516
      d_congruenceKindsInterpreted.set(fun);
295
    }
296
1000367
    if (extOperator)
297
    {
298
864
      Debug("equality::extoperator")
299
432
          << d_name << "::eq::addFunctionKind(): " << fun
300
432
          << " is an external operator kind " << std::endl;
301
432
      d_congruenceKindsExtOperators.set(fun);
302
    }
303
  }
304
1000367
}
305
306
668666
void EqualityEngine::subtermEvaluates(EqualityNodeId id)  {
307
668666
  Debug("equality::evaluation") << d_name << "::eq::subtermEvaluates(" << d_nodes[id] << "): " << d_subtermsToEvaluate[id] << std::endl;
308
668666
  Assert(!d_isInternal[id]);
309
668666
  Assert(d_subtermsToEvaluate[id] > 0);
310
668666
  if ((-- d_subtermsToEvaluate[id]) == 0) {
311
475555
    d_evaluationQueue.push(id);
312
  }
313
668666
  d_subtermEvaluates.push_back(id);
314
668666
  d_subtermEvaluatesSize = d_subtermEvaluates.size();
315
668666
  Debug("equality::evaluation") << d_name << "::eq::subtermEvaluates(" << d_nodes[id] << "): new " << d_subtermsToEvaluate[id] << std::endl;
316
668666
}
317
318
49124935
void EqualityEngine::addTermInternal(TNode t, bool isOperator) {
319
320
49124935
  Debug("equality") << d_name << "::eq::addTermInternal(" << t << ")" << std::endl;
321
322
  // If there already, we're done
323
49124935
  if (hasTerm(t)) {
324
42049660
    Debug("equality") << d_name << "::eq::addTermInternal(" << t << "): already there" << std::endl;
325
84099926
    return;
326
  }
327
328
7075275
  if (d_done) {
329
606
    return;
330
  }
331
332
  EqualityNodeId result;
333
334
7074669
  Kind tk = t.getKind();
335
7074669
  if (tk == kind::EQUAL)
336
  {
337
1615949
    addTermInternal(t[0]);
338
1615949
    addTermInternal(t[1]);
339
1615949
    EqualityNodeId t0id = getNodeId(t[0]);
340
1615949
    EqualityNodeId t1id = getNodeId(t[1]);
341
1615949
    result = newApplicationNode(t, t0id, t1id, APP_EQUALITY);
342
1615949
    d_isInternal[result] = false;
343
1615949
    d_isConstant[result] = false;
344
  }
345
5458720
  else if (t.getNumChildren() > 0 && d_congruenceKinds[tk])
346
  {
347
1437570
    TNode tOp = t.getOperator();
348
    // Add the operator
349
718785
    addTermInternal(tOp, !isExternalOperatorKind(tk));
350
718785
    result = getNodeId(tOp);
351
    // Add all the children and Curryfy
352
718785
    bool isInterpreted = isInterpretedFunctionKind(tk);
353
2004799
    for (unsigned i = 0; i < t.getNumChildren(); ++ i) {
354
      // Add the child
355
1286014
      addTermInternal(t[i]);
356
1286014
      EqualityNodeId tiId = getNodeId(t[i]);
357
      // Add the application
358
1286014
      result = newApplicationNode(t, result, tiId, isInterpreted ? APP_INTERPRETED : APP_UNINTERPRETED);
359
    }
360
718785
    d_isInternal[result] = false;
361
718785
    d_isConstant[result] = t.isConst();
362
    // If interpreted, set the number of non-interpreted children
363
718785
    if (isInterpreted) {
364
      // How many children are not constants yet
365
78647
      d_subtermsToEvaluate[result] = t.getNumChildren();
366
246406
      for (unsigned i = 0; i < t.getNumChildren(); ++ i) {
367
167759
        if (isConstant(getNodeId(t[i]))) {
368
37155
          Debug("equality::evaluation") << d_name << "::eq::addTermInternal(" << t << "): evaluates " << t[i] << std::endl;
369
37155
          subtermEvaluates(result);
370
        }
371
      }
372
    }
373
  }
374
  else
375
  {
376
    // Otherwise we just create the new id
377
4739935
    result = newNode(t);
378
    // Is this an operator
379
4739935
    d_isInternal[result] = isOperator;
380
4739935
    d_isConstant[result] = !isOperator && t.isConst();
381
  }
382
383
7074669
  if (tk == kind::EQUAL)
384
  {
385
    // We set this here as this only applies to actual terms, not the
386
    // intermediate application terms
387
1615949
    d_isEquality[result] = true;
388
  }
389
  else
390
  {
391
    // Notify e.g. the theory that owns this equality engine that there is a
392
    // new equivalence class.
393
5458720
    if (d_performNotify)
394
    {
395
5194802
      d_notify.eqNotifyNewClass(t);
396
    }
397
5458720
    if (d_constantsAreTriggers && d_isConstant[result])
398
    {
399
      // Non-Boolean constants are trigger terms for all tags
400
613732
      EqualityNodeId tId = getNodeId(t);
401
      // Setup the new set
402
613732
      TheoryIdSet newSetTags = 0;
403
      EqualityNodeId newSetTriggers[THEORY_LAST];
404
613732
      unsigned newSetTriggersSize = THEORY_LAST;
405
8592248
      for (TheoryId currentTheory = THEORY_FIRST; currentTheory != THEORY_LAST;
406
           ++currentTheory)
407
      {
408
7978516
        newSetTags = TheoryIdSetUtil::setInsert(currentTheory, newSetTags);
409
7978516
        newSetTriggers[currentTheory] = tId;
410
      }
411
      // Add it to the list for backtracking
412
613732
      d_triggerTermSetUpdates.push_back(TriggerSetUpdate(tId, null_set_id));
413
613732
      d_triggerTermSetUpdatesSize = d_triggerTermSetUpdatesSize + 1;
414
      // Mark the the new set as a trigger
415
613732
      d_nodeIndividualTrigger[tId] =
416
613732
          newTriggerTermSet(newSetTags, newSetTriggers, newSetTriggersSize);
417
    }
418
  }
419
420
  // If this is not an internal node, add it to the master
421
7074669
  if (d_masterEqualityEngine && !d_isInternal[result]) {
422
1635076
    d_masterEqualityEngine->addTermInternal(t);
423
  }
424
425
  // Empty the queue
426
7074669
  propagate();
427
428
7074669
  Assert(hasTerm(t));
429
430
7074669
  Debug("equality") << d_name << "::eq::addTermInternal(" << t << ") => " << result << std::endl;
431
}
432
433
515226917
bool EqualityEngine::hasTerm(TNode t) const {
434
515226917
  return d_nodeIds.find(t) != d_nodeIds.end();
435
}
436
437
255536698
EqualityNodeId EqualityEngine::getNodeId(TNode node) const {
438
255536698
  Assert(hasTerm(node)) << node;
439
255536698
  return (*d_nodeIds.find(node)).second;
440
}
441
442
67514046
EqualityNode& EqualityEngine::getEqualityNode(TNode t) {
443
67514046
  return getEqualityNode(getNodeId(t));
444
}
445
446
487533721
EqualityNode& EqualityEngine::getEqualityNode(EqualityNodeId nodeId) {
447
487533721
  Assert(nodeId < d_equalityNodes.size());
448
487533721
  return d_equalityNodes[nodeId];
449
}
450
451
75266227
const EqualityNode& EqualityEngine::getEqualityNode(TNode t) const {
452
75266227
  return getEqualityNode(getNodeId(t));
453
}
454
455
207006417
const EqualityNode& EqualityEngine::getEqualityNode(EqualityNodeId nodeId) const {
456
207006417
  Assert(nodeId < d_equalityNodes.size());
457
207006417
  return d_equalityNodes[nodeId];
458
}
459
460
16199423
void EqualityEngine::assertEqualityInternal(TNode t1, TNode t2, TNode reason, unsigned pid) {
461
32398846
  Debug("equality") << d_name << "::eq::addEqualityInternal(" << t1 << "," << t2
462
16199423
                    << "), reason = " << reason
463
32398846
                    << ", pid = " << static_cast<MergeReasonType>(pid)
464
16199423
                    << std::endl;
465
466
16199423
  if (d_done) {
467
309
    return;
468
  }
469
470
  // Add the terms if they are not already in the database
471
16199114
  addTermInternal(t1);
472
16199114
  addTermInternal(t2);
473
474
  // Add to the queue and propagate
475
16199114
  EqualityNodeId t1Id = getNodeId(t1);
476
16199114
  EqualityNodeId t2Id = getNodeId(t2);
477
16199114
  enqueue(MergeCandidate(t1Id, t2Id, pid, reason));
478
}
479
480
2016274
bool EqualityEngine::assertPredicate(TNode t,
481
                                     bool polarity,
482
                                     TNode reason,
483
                                     unsigned pid)
484
{
485
2016274
  Debug("equality") << d_name << "::eq::addPredicate(" << t << "," << (polarity ? "true" : "false") << ")" << std::endl;
486
2016274
  Assert(t.getKind() != kind::EQUAL) << "Use assertEquality instead";
487
4032548
  TNode b = polarity ? d_true : d_false;
488
2016274
  if (hasTerm(t) && areEqual(t, b))
489
  {
490
894013
    return false;
491
  }
492
1122261
  assertEqualityInternal(t, b, reason, pid);
493
1122261
  propagate();
494
1122261
  return true;
495
}
496
497
15825662
bool EqualityEngine::assertEquality(TNode eq,
498
                                    bool polarity,
499
                                    TNode reason,
500
                                    unsigned pid)
501
{
502
15825662
  Debug("equality") << d_name << "::eq::addEquality(" << eq << "," << (polarity ? "true" : "false") << ")" << std::endl;
503
15825662
  if (polarity) {
504
    // If two terms are already equal, don't assert anything
505
8368397
    if (hasTerm(eq[0]) && hasTerm(eq[1]) && areEqual(eq[0], eq[1])) {
506
2436724
      return false;
507
    }
508
    // Add equality between terms
509
5931673
    assertEqualityInternal(eq[0], eq[1], reason, pid);
510
5931673
    propagate();
511
  } else {
512
    // If two terms are already dis-equal, don't assert anything
513
7457265
    if (hasTerm(eq[0]) && hasTerm(eq[1]) && areDisequal(eq[0], eq[1], false)) {
514
8392963
      return false;
515
    }
516
517
    // notify the theory
518
3261239
    if (d_performNotify) {
519
3261239
      d_notify.eqNotifyDisequal(eq[0], eq[1], reason);
520
    }
521
522
3261239
    Debug("equality::trigger") << d_name << "::eq::addEquality(" << eq << "," << (polarity ? "true" : "false") << ")" << std::endl;
523
524
3261239
    assertEqualityInternal(eq, d_false, reason, pid);
525
3261239
    propagate();
526
527
3261239
    if (d_done) {
528
891
      return true;
529
    }
530
531
    // If both have constant representatives, we don't notify anyone
532
3260348
    EqualityNodeId a = getNodeId(eq[0]);
533
3260348
    EqualityNodeId b = getNodeId(eq[1]);
534
3260348
    EqualityNodeId aClassId = getEqualityNode(a).getFind();
535
3260348
    EqualityNodeId bClassId = getEqualityNode(b).getFind();
536
3260348
    if (d_isConstant[aClassId] && d_isConstant[bClassId]) {
537
20
      return true;
538
    }
539
540
    // If we are adding a disequality, notify of the shared term representatives
541
3260328
    EqualityNodeId eqId = getNodeId(eq);
542
3260328
    TriggerTermSetRef aTriggerRef = d_nodeIndividualTrigger[aClassId];
543
3260328
    TriggerTermSetRef bTriggerRef = d_nodeIndividualTrigger[bClassId];
544
3260328
    if (aTriggerRef != +null_set_id && bTriggerRef != +null_set_id) {
545
1441806
      Debug("equality::trigger") << d_name << "::eq::addEquality(" << eq << "," << (polarity ? "true" : "false") << ": have triggers" << std::endl;
546
      // The sets of trigger terms
547
1441806
      TriggerTermSet& aTriggerTerms = getTriggerTermSet(aTriggerRef);
548
1441806
      TriggerTermSet& bTriggerTerms = getTriggerTermSet(bTriggerRef);
549
      // Go through and notify the shared dis-equalities
550
1441806
      TheoryIdSet aTags = aTriggerTerms.d_tags;
551
1441806
      TheoryIdSet bTags = bTriggerTerms.d_tags;
552
1441806
      TheoryId aTag = TheoryIdSetUtil::setPop(aTags);
553
1441806
      TheoryId bTag = TheoryIdSetUtil::setPop(bTags);
554
1441806
      int a_i = 0, b_i = 0;
555
14555996
      while (aTag != THEORY_LAST && bTag != THEORY_LAST) {
556
6557107
        if (aTag < bTag) {
557
1633389
          aTag = TheoryIdSetUtil::setPop(aTags);
558
1633389
          ++ a_i;
559
4923718
        } else if (aTag > bTag) {
560
2836320
          bTag = TheoryIdSetUtil::setPop(bTags);
561
2836320
          ++ b_i;
562
        } else {
563
          // Same tags, notify
564
2087398
          EqualityNodeId aSharedId = aTriggerTerms.d_triggers[a_i++];
565
2087398
          EqualityNodeId bSharedId = bTriggerTerms.d_triggers[b_i++];
566
          // Propagate
567
2087398
          if (!hasPropagatedDisequality(aTag, aSharedId, bSharedId)) {
568
            // Store a proof if not there already
569
2087398
            if (!hasPropagatedDisequality(aSharedId, bSharedId)) {
570
972473
              d_deducedDisequalityReasons.push_back(EqualityPair(aSharedId, a));
571
972473
              d_deducedDisequalityReasons.push_back(EqualityPair(bSharedId, b));
572
972473
              d_deducedDisequalityReasons.push_back(EqualityPair(eqId, d_falseId));
573
            }
574
            // Store the propagation
575
2087398
            storePropagatedDisequality(aTag, aSharedId, bSharedId);
576
            // Notify
577
2087398
            Debug("equality::trigger") << d_name << "::eq::addEquality(" << eq << "," << (polarity ? "true" : "false") << ": notifying " << aTag << " for " << d_nodes[aSharedId] << " != " << d_nodes[bSharedId] << std::endl;
578
2087398
            if (!d_notify.eqNotifyTriggerTermEquality(aTag, d_nodes[aSharedId], d_nodes[bSharedId], false)) {
579
12
              break;
580
            }
581
          }
582
          // Pop the next tags
583
2087386
          aTag = TheoryIdSetUtil::setPop(aTags);
584
2087386
          bTag = TheoryIdSetUtil::setPop(bTags);
585
        }
586
      }
587
    }
588
  }
589
9191998
  return true;
590
}
591
592
24672668
TNode EqualityEngine::getRepresentative(TNode t) const {
593
24672668
  Debug("equality::internal") << d_name << "::eq::getRepresentative(" << t << ")" << std::endl;
594
24672668
  Assert(hasTerm(t));
595
24672668
  EqualityNodeId representativeId = getEqualityNode(t).getFind();
596
24672668
  Assert(!d_isInternal[representativeId]);
597
24672668
  Debug("equality::internal") << d_name << "::eq::getRepresentative(" << t << ") => " << d_nodes[representativeId] << std::endl;
598
24672668
  return d_nodes[representativeId];
599
}
600
601
25800132
bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vector<TriggerId>& triggersFired) {
602
603
25800132
  Debug("equality") << d_name << "::eq::merge(" << class1.getFind() << "," << class2.getFind() << ")" << std::endl;
604
605
25800132
  Assert(triggersFired.empty());
606
607
25800132
  ++d_stats.d_mergesCount;
608
609
25800132
  EqualityNodeId class1Id = class1.getFind();
610
25800132
  EqualityNodeId class2Id = class2.getFind();
611
612
51600264
  Node n1 = d_nodes[class1Id];
613
51600264
  Node n2 = d_nodes[class2Id];
614
25800132
  EqualityNode cc1 = getEqualityNode(n1);
615
25800132
  EqualityNode cc2 = getEqualityNode(n2);
616
25800132
  bool doNotify = false;
617
  // Determine if we should notify the owner of this class of this merge.
618
  // The second part of this check is needed due to the internal implementation
619
  // of this class. It ensures that we are merging terms and not operators.
620
25800132
  if (d_performNotify && class1Id == cc1.getFind() && class2Id == cc2.getFind())
621
  {
622
25145453
    doNotify = true;
623
  }
624
625
  // Check for constant merges
626
25800132
  bool class1isConstant = d_isConstant[class1Id];
627
25800132
  bool class2isConstant = d_isConstant[class2Id];
628
25800132
  Assert(class1isConstant || !class2isConstant)
629
      << "Should always merge into constants";
630
25800132
  Assert(!class1isConstant || !class2isConstant) << "Don't merge constants";
631
632
  // Trigger set of class 1
633
25800132
  TriggerTermSetRef class1triggerRef = d_nodeIndividualTrigger[class1Id];
634
  TheoryIdSet class1Tags = class1triggerRef == null_set_id
635
41291576
                               ? 0
636
41291576
                               : getTriggerTermSet(class1triggerRef).d_tags;
637
  // Trigger set of class 2
638
25800132
  TriggerTermSetRef class2triggerRef = d_nodeIndividualTrigger[class2Id];
639
  TheoryIdSet class2Tags = class2triggerRef == null_set_id
640
28550043
                               ? 0
641
28550043
                               : getTriggerTermSet(class2triggerRef).d_tags;
642
643
  // Disequalities coming from class2
644
51600264
  TaggedEqualitiesSet class2disequalitiesToNotify;
645
  // Disequalities coming from class1
646
51600264
  TaggedEqualitiesSet class1disequalitiesToNotify;
647
648
  // Individual tags
649
  TheoryIdSet class1OnlyTags =
650
25800132
      TheoryIdSetUtil::setDifference(class1Tags, class2Tags);
651
  TheoryIdSet class2OnlyTags =
652
25800132
      TheoryIdSetUtil::setDifference(class2Tags, class1Tags);
653
654
  // Only get disequalities if they are not both constant
655
25800132
  if (!class1isConstant || !class2isConstant) {
656
25800132
    getDisequalities(!class1isConstant, class2Id, class1OnlyTags, class2disequalitiesToNotify);
657
25800132
    getDisequalities(!class2isConstant, class1Id, class2OnlyTags, class1disequalitiesToNotify);
658
  }
659
660
  // Update class2 representative information
661
25800132
  Debug("equality") << d_name << "::eq::merge(" << class1.getFind() << "," << class2.getFind() << "): updating class " << class2Id << std::endl;
662
25800132
  EqualityNodeId currentId = class2Id;
663
7648585
  do {
664
    // Get the current node
665
33448717
    EqualityNode& currentNode = getEqualityNode(currentId);
666
667
    // Update it's find to class1 id
668
33448717
    Debug("equality") << d_name << "::eq::merge(" << class1.getFind() << "," << class2.getFind() << "): " << currentId << "->" << class1Id << std::endl;
669
33448717
    currentNode.setFind(class1Id);
670
671
    // Go through the triggers and inform if necessary
672
33448717
    TriggerId currentTrigger = d_nodeTriggers[currentId];
673
113582783
    while (currentTrigger != null_trigger) {
674
40067033
      Trigger& trigger = d_equalityTriggers[currentTrigger];
675
40067033
      Trigger& otherTrigger = d_equalityTriggers[currentTrigger ^ 1];
676
677
      // If the two are not already in the same class
678
40067033
      if (otherTrigger.d_classId != trigger.d_classId)
679
      {
680
35196007
        trigger.d_classId = class1Id;
681
        // If they became the same, call the trigger
682
35196007
        if (otherTrigger.d_classId == class1Id)
683
        {
684
          // Id of the real trigger is half the internal one
685
12787520
          triggersFired.push_back(currentTrigger);
686
        }
687
      }
688
689
      // Go to the next trigger
690
40067033
      currentTrigger = trigger.d_nextTrigger;
691
    }
692
693
    // Move to the next node
694
33448717
    currentId = currentNode.getNext();
695
696
33448717
  } while (currentId != class2Id);
697
698
  // Update class2 table lookup and information if not a boolean
699
  // since booleans can't be in an application
700
25800132
  if (!d_isEquality[class2Id]) {
701
13934864
    Debug("equality") << d_name << "::eq::merge(" << class1.getFind() << "," << class2.getFind() << "): updating lookups of " << class2Id << std::endl;
702
6123817
    do {
703
      // Get the current node
704
20058681
      EqualityNode& currentNode = getEqualityNode(currentId);
705
20058681
      Debug("equality") << d_name << "::eq::merge(" << class1.getFind() << "," << class2.getFind() << "): updating lookups of node " << currentId << std::endl;
706
707
      // Go through the uselist and check for congruences
708
20058681
      UseListNodeId currentUseId = currentNode.getUseList();
709
97704687
      while (currentUseId != null_uselist_id) {
710
        // Get the node of the use list
711
38823003
        UseListNode& useNode = d_useListNodes[currentUseId];
712
        // Get the function application
713
38823003
        EqualityNodeId funId = useNode.getApplicationId();
714
38823003
        Debug("equality") << d_name << "::eq::merge(" << class1.getFind() << "," << class2.getFind() << "): " << d_nodes[currentId] << " in " << d_nodes[funId] << std::endl;
715
        const FunctionApplication& fun =
716
38823003
            d_applications[useNode.getApplicationId()].d_normalized;
717
        // If it's interpreted and we can interpret
718
38823003
        if (fun.isInterpreted() && class1isConstant && !d_isInternal[currentId])
719
        {
720
          // Get the actual term id
721
1263022
          TNode term = d_nodes[funId];
722
631511
          subtermEvaluates(getNodeId(term));
723
        }
724
        // Check if there is an application with find arguments
725
38823003
        EqualityNodeId aNormalized = getEqualityNode(fun.d_a).getFind();
726
38823003
        EqualityNodeId bNormalized = getEqualityNode(fun.d_b).getFind();
727
38823003
        FunctionApplication funNormalized(fun.d_type, aNormalized, bNormalized);
728
38823003
        ApplicationIdsMap::iterator find = d_applicationLookup.find(funNormalized);
729
38823003
        if (find != d_applicationLookup.end()) {
730
          // Applications fun and the funNormalized can be merged due to congruence
731
27123390
          if (getEqualityNode(funId).getFind() != getEqualityNode(find->second).getFind()) {
732
16599854
            enqueue(MergeCandidate(funId, find->second, MERGED_THROUGH_CONGRUENCE, TNode::null()));
733
          }
734
        } else {
735
          // There is no representative, so we can add one, we remove this when backtracking
736
11699613
          storeApplicationLookup(funNormalized, funId);
737
        }
738
739
        // Go to the next one in the use list
740
38823003
        currentUseId = useNode.getNext();
741
      }
742
743
      // Move to the next node
744
20058681
      currentId = currentNode.getNext();
745
20058681
    } while (currentId != class2Id);
746
  }
747
748
  // Now merge the lists
749
25800132
  class1.merge<true>(class2);
750
751
  // notify the theory
752
25800132
  if (doNotify) {
753
25145456
    d_notify.eqNotifyMerge(n1, n2);
754
  }
755
756
  // Go through the trigger term disequalities and propagate
757
25800129
  if (!propagateTriggerTermDisequalities(class1OnlyTags, class1triggerRef, class2disequalitiesToNotify)) {
758
    return false;
759
  }
760
25800129
  if (!propagateTriggerTermDisequalities(class2OnlyTags, class2triggerRef, class1disequalitiesToNotify)) {
761
8
    return false;
762
  }
763
764
  // Notify the trigger term merges
765
25800121
  if (class2triggerRef != +null_set_id) {
766
2749903
    if (class1triggerRef == +null_set_id) {
767
      // If class1 doesn't have individual triggers, but class2 does, mark it
768
88284
      d_nodeIndividualTrigger[class1Id] = class2triggerRef;
769
      // Add it to the list for backtracking
770
88284
      d_triggerTermSetUpdates.push_back(TriggerSetUpdate(class1Id, +null_set_id));
771
88284
      d_triggerTermSetUpdatesSize = d_triggerTermSetUpdatesSize + 1;
772
    } else {
773
      // Get the triggers
774
2661619
      TriggerTermSet& class1triggers = getTriggerTermSet(class1triggerRef);
775
2661619
      TriggerTermSet& class2triggers = getTriggerTermSet(class2triggerRef);
776
777
      // Initialize the merged set
778
2661619
      TheoryIdSet newSetTags = TheoryIdSetUtil::setUnion(class1triggers.d_tags,
779
2661619
                                                         class2triggers.d_tags);
780
      EqualityNodeId newSetTriggers[THEORY_LAST];
781
2661619
      unsigned newSetTriggersSize = 0;
782
783
2661619
      int i1 = 0;
784
2661619
      int i2 = 0;
785
2661619
      TheoryIdSet tags1 = class1triggers.d_tags;
786
2661619
      TheoryIdSet tags2 = class2triggers.d_tags;
787
2661619
      TheoryId tag1 = TheoryIdSetUtil::setPop(tags1);
788
2661619
      TheoryId tag2 = TheoryIdSetUtil::setPop(tags2);
789
790
      // Comparing the THEORY_LAST is OK because all other theories are
791
      // smaller, and will therefore be preferred
792
54220715
      while (tag1 != THEORY_LAST || tag2 != THEORY_LAST)
793
      {
794
25790671
        if (tag1 < tag2) {
795
          // copy tag1
796
22257587
          newSetTriggers[newSetTriggersSize++] =
797
22257587
              class1triggers.d_triggers[i1++];
798
22257587
          tag1 = TheoryIdSetUtil::setPop(tags1);
799
3533084
        } else if (tag1 > tag2) {
800
          // copy tag2
801
1741
          newSetTriggers[newSetTriggersSize++] =
802
1741
              class2triggers.d_triggers[i2++];
803
1741
          tag2 = TheoryIdSetUtil::setPop(tags2);
804
        } else {
805
          // copy tag1
806
3531343
          EqualityNodeId tag1id = newSetTriggers[newSetTriggersSize++] =
807
7062686
              class1triggers.d_triggers[i1++];
808
          // since they are both tagged notify of merge
809
3531343
          if (d_performNotify) {
810
3531343
            EqualityNodeId tag2id = class2triggers.d_triggers[i2++];
811
3531343
            if (!d_notify.eqNotifyTriggerTermEquality(tag1, d_nodes[tag1id], d_nodes[tag2id], true)) {
812
11123
              return false;
813
            }
814
          }
815
          // Next tags
816
3520220
          tag1 = TheoryIdSetUtil::setPop(tags1);
817
3520220
          tag2 = TheoryIdSetUtil::setPop(tags2);
818
        }
819
      }
820
821
      // Add the new trigger set, if different from previous one
822
2650496
      if (class1triggers.d_tags != class2triggers.d_tags)
823
      {
824
        // Add it to the list for backtracking
825
1908931
        d_triggerTermSetUpdates.push_back(TriggerSetUpdate(class1Id, class1triggerRef));
826
1908931
        d_triggerTermSetUpdatesSize = d_triggerTermSetUpdatesSize + 1;
827
        // Mark the the new set as a trigger
828
1908931
        d_nodeIndividualTrigger[class1Id] = newTriggerTermSet(newSetTags, newSetTriggers, newSetTriggersSize);
829
      }
830
    }
831
  }
832
833
  // Everything fine
834
25788998
  return true;
835
}
836
837
25798277
void EqualityEngine::undoMerge(EqualityNode& class1, EqualityNode& class2, EqualityNodeId class2Id) {
838
839
25798277
  Debug("equality") << d_name << "::eq::undoMerge(" << class1.getFind() << "," << class2Id << ")" << std::endl;
840
841
  // Now unmerge the lists (same as merge)
842
25798277
  class1.merge<false>(class2);
843
844
  // Update class2 representative information
845
25798277
  EqualityNodeId currentId = class2Id;
846
25798277
  Debug("equality") << d_name << "::eq::undoMerge(" << class1.getFind() << "," << class2Id << "): undoing representative info" << std::endl;
847
7648264
  do {
848
    // Get the current node
849
33446541
    EqualityNode& currentNode = getEqualityNode(currentId);
850
851
    // Update it's find to class1 id
852
33446541
    currentNode.setFind(class2Id);
853
854
    // Go through the trigger list (if any) and undo the class
855
33446541
    TriggerId currentTrigger = d_nodeTriggers[currentId];
856
113580607
    while (currentTrigger != null_trigger) {
857
40067033
      Trigger& trigger = d_equalityTriggers[currentTrigger];
858
40067033
      trigger.d_classId = class2Id;
859
40067033
      currentTrigger = trigger.d_nextTrigger;
860
    }
861
862
    // Move to the next node
863
33446541
    currentId = currentNode.getNext();
864
865
33446541
  } while (currentId != class2Id);
866
867
25798277
}
868
869
31150837
void EqualityEngine::backtrack() {
870
871
31150837
  Debug("equality::backtrack") << "backtracking" << std::endl;
872
873
  // If we need to backtrack then do it
874
31150837
  if (d_assertedEqualitiesCount < d_assertedEqualities.size()) {
875
876
    // Clear the propagation queue
877
4398018
    while (!d_propagationQueue.empty()) {
878
6
      d_propagationQueue.pop_front();
879
    }
880
881
4398006
    Debug("equality") << d_name << "::eq::backtrack(): nodes" << std::endl;
882
883
30229527
    for (int i = (int)d_assertedEqualities.size() - 1, i_end = (int)d_assertedEqualitiesCount; i >= i_end; --i) {
884
      // Get the ids of the merged classes
885
25831521
      Equality& eq = d_assertedEqualities[i];
886
      // Undo the merge
887
25831521
      if (eq.d_lhs != null_id)
888
      {
889
51596554
        undoMerge(
890
25798277
            d_equalityNodes[eq.d_lhs], d_equalityNodes[eq.d_rhs], eq.d_rhs);
891
      }
892
    }
893
894
4398006
    d_assertedEqualities.resize(d_assertedEqualitiesCount);
895
896
4398006
    Debug("equality") << d_name << "::eq::backtrack(): edges" << std::endl;
897
898
30229527
    for (int i = (int)d_equalityEdges.size() - 2, i_end = (int)(2*d_assertedEqualitiesCount); i >= i_end; i -= 2) {
899
25831521
      EqualityEdge& edge1 = d_equalityEdges[i];
900
25831521
      EqualityEdge& edge2 = d_equalityEdges[i | 1];
901
25831521
      d_equalityGraph[edge2.getNodeId()] = edge1.getNext();
902
25831521
      d_equalityGraph[edge1.getNodeId()] = edge2.getNext();
903
    }
904
905
4398006
    d_equalityEdges.resize(2 * d_assertedEqualitiesCount);
906
  }
907
908
31150837
  if (d_triggerTermSetUpdates.size() > d_triggerTermSetUpdatesSize) {
909
    // Unset the individual triggers
910
7350584
    for (int i = d_triggerTermSetUpdates.size() - 1, i_end = d_triggerTermSetUpdatesSize; i >= i_end; -- i) {
911
5471509
      const TriggerSetUpdate& update = d_triggerTermSetUpdates[i];
912
5471509
      d_nodeIndividualTrigger[update.d_classId] = update.d_oldValue;
913
    }
914
1879075
    d_triggerTermSetUpdates.resize(d_triggerTermSetUpdatesSize);
915
  }
916
917
31150837
  if (d_equalityTriggers.size() > d_equalityTriggersCount) {
918
    // Unlink the triggers from the lists
919
3298846
    for (int i = d_equalityTriggers.size() - 1, i_end = d_equalityTriggersCount; i >= i_end; -- i) {
920
3229984
      const Trigger& trigger = d_equalityTriggers[i];
921
3229984
      d_nodeTriggers[trigger.d_classId] = trigger.d_nextTrigger;
922
    }
923
    // Get rid of the triggers
924
68862
    d_equalityTriggers.resize(d_equalityTriggersCount);
925
68862
    d_equalityTriggersOriginal.resize(d_equalityTriggersCount);
926
  }
927
928
31150837
  if (d_applicationLookups.size() > d_applicationLookupsCount) {
929
15940022
    for (int i = d_applicationLookups.size() - 1, i_end = (int) d_applicationLookupsCount; i >= i_end; -- i) {
930
14332444
      d_applicationLookup.erase(d_applicationLookups[i]);
931
    }
932
1607578
    d_applicationLookups.resize(d_applicationLookupsCount);
933
  }
934
935
31150837
  if (d_subtermEvaluates.size() > d_subtermEvaluatesSize) {
936
771125
    for(int i = d_subtermEvaluates.size() - 1, i_end = (int)d_subtermEvaluatesSize; i >= i_end; --i) {
937
668666
      d_subtermsToEvaluate[d_subtermEvaluates[i]] ++;
938
    }
939
102459
    d_subtermEvaluates.resize(d_subtermEvaluatesSize);
940
  }
941
942
31150837
  if (d_nodes.size() > d_nodesCount) {
943
    // Go down the nodes, check the application nodes and remove them from use-lists
944
8582225
    for(int i = d_nodes.size() - 1, i_end = (int)d_nodesCount; i >= i_end; -- i) {
945
      // Remove from the node -> id map
946
7375107
      Debug("equality") << d_name << "::eq::backtrack(): removing node " << d_nodes[i] << std::endl;
947
7375107
      d_nodeIds.erase(d_nodes[i]);
948
949
7375107
      const FunctionApplication& app = d_applications[i].d_original;
950
7375107
      if (!app.isNull()) {
951
        // Remove b from use-list
952
2899145
        getEqualityNode(app.d_b).removeTopFromUseList(d_useListNodes);
953
        // Remove a from use-list
954
2899145
        getEqualityNode(app.d_a).removeTopFromUseList(d_useListNodes);
955
      }
956
    }
957
958
    // Now get rid of the nodes and the rest
959
1207118
    d_nodes.resize(d_nodesCount);
960
1207118
    d_applications.resize(d_nodesCount);
961
1207118
    d_nodeTriggers.resize(d_nodesCount);
962
1207118
    d_nodeIndividualTrigger.resize(d_nodesCount);
963
1207118
    d_isConstant.resize(d_nodesCount);
964
1207118
    d_subtermsToEvaluate.resize(d_nodesCount);
965
1207118
    d_isEquality.resize(d_nodesCount);
966
1207118
    d_isInternal.resize(d_nodesCount);
967
1207118
    d_equalityGraph.resize(d_nodesCount);
968
1207118
    d_equalityNodes.resize(d_nodesCount);
969
  }
970
971
31150837
  if (d_deducedDisequalities.size() > d_deducedDisequalitiesSize) {
972
9641685
    for(int i = d_deducedDisequalities.size() - 1, i_end = (int)d_deducedDisequalitiesSize; i >= i_end; -- i) {
973
7371129
      EqualityPair pair = d_deducedDisequalities[i];
974
7371129
      Assert(d_disequalityReasonsMap.find(pair)
975
             != d_disequalityReasonsMap.end());
976
      // Remove from the map
977
7371129
      d_disequalityReasonsMap.erase(pair);
978
7371129
      std::swap(pair.first, pair.second);
979
7371129
      d_disequalityReasonsMap.erase(pair);
980
    }
981
2270556
    d_deducedDisequalityReasons.resize(d_deducedDisequalityReasonsSize);
982
2270556
    d_deducedDisequalities.resize(d_deducedDisequalitiesSize);
983
  }
984
985
31150837
}
986
987
25833376
void EqualityEngine::addGraphEdge(EqualityNodeId t1, EqualityNodeId t2, unsigned type, TNode reason) {
988
51666752
  Debug("equality") << d_name << "::eq::addGraphEdge({" << t1 << "} "
989
25833376
                    << d_nodes[t1] << ", {" << t2 << "} " << d_nodes[t2] << ","
990
25833376
                    << reason << ")" << std::endl;
991
25833376
  EqualityEdgeId edge = d_equalityEdges.size();
992
25833376
  d_equalityEdges.push_back(EqualityEdge(t2, d_equalityGraph[t1], type, reason));
993
25833376
  d_equalityEdges.push_back(EqualityEdge(t1, d_equalityGraph[t2], type, reason));
994
25833376
  d_equalityGraph[t1] = edge;
995
25833376
  d_equalityGraph[t2] = edge | 1;
996
997
25833376
  if (Debug.isOn("equality::internal")) {
998
    debugPrintGraph();
999
  }
1000
25833376
}
1001
1002
std::string EqualityEngine::edgesToString(EqualityEdgeId edgeId) const {
1003
  std::stringstream out;
1004
  bool first = true;
1005
  if (edgeId == null_edge) {
1006
    out << "null";
1007
  } else {
1008
    while (edgeId != null_edge) {
1009
      const EqualityEdge& edge = d_equalityEdges[edgeId];
1010
      if (!first) out << ",";
1011
      out << "{" << edge.getNodeId() << "} " << d_nodes[edge.getNodeId()];
1012
      edgeId = edge.getNext();
1013
      first = false;
1014
    }
1015
  }
1016
  return out.str();
1017
}
1018
1019
955764
void EqualityEngine::buildEqConclusion(EqualityNodeId id1,
1020
                                       EqualityNodeId id2,
1021
                                       EqProof* eqp) const
1022
{
1023
955764
  Kind k1 = d_nodes[id1].getKind();
1024
955764
  Kind k2 = d_nodes[id2].getKind();
1025
  // only try to build if ids do not correspond to internal nodes. If they do,
1026
  // only try to build build if full applications corresponding to the given ids
1027
  // have the same congruence n-ary non-APPLY_* kind, since the internal nodes
1028
  // may be full nodes.
1029
2311143
  if ((d_isInternal[id1] || d_isInternal[id2])
1030
2068018
      && (k1 != k2 || k1 == kind::APPLY_UF || k1 == kind::APPLY_CONSTRUCTOR
1031
7416
          || k1 == kind::APPLY_SELECTOR || k1 == kind::APPLY_TESTER
1032
7416
          || !NodeManager::isNAryKind(k1)))
1033
  {
1034
556105
    return;
1035
  }
1036
799318
  Debug("equality") << "buildEqConclusion: {" << id1 << "} " << d_nodes[id1]
1037
399659
                    << "\n";
1038
799318
  Debug("equality") << "buildEqConclusion: {" << id2 << "} " << d_nodes[id2]
1039
399659
                    << "\n";
1040
799318
  Node eq[2];
1041
399659
  NodeManager* nm = NodeManager::currentNM();
1042
1198977
  for (unsigned i = 0; i < 2; ++i)
1043
  {
1044
799318
    EqualityNodeId equalityNodeId = i == 0 ? id1 : id2;
1045
799406
    Node equalityNode = d_nodes[equalityNodeId];
1046
    // if not an internal node, just retrieve it
1047
1598548
    if (!d_isInternal[equalityNodeId])
1048
    {
1049
799230
      eq[i] = equalityNode;
1050
799230
      continue;
1051
    }
1052
    // build node relative to partial application of this
1053
    // n-ary kind. We get the full application, then we get
1054
    // the arguments relative to how partial the internal
1055
    // node is, and build the application
1056
1057
    // get number of children of partial app:
1058
    // #children of full app - (id of full app - id of
1059
    // partial app)
1060
88
    EqualityNodeId fullAppId = getNodeId(equalityNode);
1061
88
    EqualityNodeId curr = fullAppId;
1062
88
    unsigned separation = 0;
1063
88
    Assert(fullAppId >= equalityNodeId);
1064
284
    while (curr != equalityNodeId)
1065
    {
1066
98
      separation = separation + (d_nodes[curr--] == equalityNode ? 1 : 0);
1067
    }
1068
    // compute separation, which is how many ids with the
1069
    // same fullappnode exist between equalityNodeId and
1070
    // fullAppId
1071
88
    unsigned numChildren = equalityNode.getNumChildren() - separation;
1072
176
    Assert(numChildren < equalityNode.getNumChildren())
1073
        << "broke for numChildren " << numChildren << ", fullAppId "
1074
        << fullAppId << ", equalityNodeId " << equalityNodeId << ", node "
1075
88
        << equalityNode << ", cong: {" << id1 << "} " << d_nodes[id1] << " = {"
1076
88
        << id2 << "} " << d_nodes[id2] << "\n";
1077
    // if has at least as many children as the minimal
1078
    // number of children of the n-ary kind, build the node
1079
88
    if (numChildren >= kind::metakind::getMinArityForKind(k1))
1080
    {
1081
4
      std::vector<Node> children;
1082
6
      for (unsigned j = 0; j < numChildren; ++j)
1083
      {
1084
4
        children.push_back(equalityNode[j]);
1085
      }
1086
2
      eq[i] = nm->mkNode(k1, children);
1087
    }
1088
  }
1089
  // if built equality, add it as eqp's conclusion
1090
399659
  if (!eq[0].isNull() && !eq[1].isNull())
1091
  {
1092
399616
    eqp->d_node = eq[0].eqNode(eq[1]);
1093
  }
1094
}
1095
1096
478859
void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity,
1097
                                     std::vector<TNode>& equalities,
1098
                                     EqProof* eqp) const {
1099
957718
  Debug("pf::ee") << d_name << "::eq::explainEquality(" << t1 << ", " << t2
1100
957718
                  << ", " << (polarity ? "true" : "false") << ")"
1101
478859
                  << ", proof = " << (eqp ? "ON" : "OFF") << std::endl;
1102
1103
  // The terms must be there already
1104
478859
  Assert(hasTerm(t1) && hasTerm(t2));
1105
1106
478859
  if (Debug.isOn("equality::internal"))
1107
  {
1108
    debugPrintGraph();
1109
  }
1110
  // Get the ids
1111
478859
  EqualityNodeId t1Id = getNodeId(t1);
1112
478859
  EqualityNodeId t2Id = getNodeId(t2);
1113
1114
957718
  std::map<std::pair<EqualityNodeId, EqualityNodeId>, EqProof*> cache;
1115
478859
  if (polarity) {
1116
    // Get the explanation
1117
446130
    getExplanation(t1Id, t2Id, equalities, cache, eqp);
1118
  } else {
1119
32729
    if (eqp) {
1120
4889
      eqp->d_id = MERGED_THROUGH_TRANS;
1121
4889
      eqp->d_node = d_nodes[t1Id].eqNode(d_nodes[t2Id]).notNode();
1122
    }
1123
1124
    // Get the reason for this disequality
1125
32729
    EqualityPair pair(t1Id, t2Id);
1126
32729
    Assert(d_disequalityReasonsMap.find(pair) != d_disequalityReasonsMap.end())
1127
        << "Don't ask for stuff I didn't notify you about";
1128
32729
    DisequalityReasonRef reasonRef = d_disequalityReasonsMap.find(pair)->second;
1129
32729
    if (eqp)
1130
    {
1131
9778
      Debug("pf::ee") << "Deq reason for " << eqp->d_node << " "
1132
4889
                      << reasonRef.d_mergesStart << "..."
1133
4889
                      << reasonRef.d_mergesEnd << std::endl;
1134
    }
1135
95078
    for (unsigned i = reasonRef.d_mergesStart; i < reasonRef.d_mergesEnd; ++i)
1136
    {
1137
62349
      EqualityPair toExplain = d_deducedDisequalityReasons[i];
1138
124698
      std::shared_ptr<EqProof> eqpc;
1139
1140
      // If we're constructing a (transitivity) proof, we don't need to include an explanation for x=x.
1141
62349
      if (eqp && toExplain.first != toExplain.second) {
1142
5994
        eqpc = std::make_shared<EqProof>();
1143
11988
        Debug("pf::ee") << "Deq getExplanation #" << i << " for " << eqp->d_node
1144
5994
                        << " : " << toExplain.first << " " << toExplain.second
1145
5994
                        << std::endl;
1146
      }
1147
1148
62349
      getExplanation(
1149
          toExplain.first, toExplain.second, equalities, cache, eqpc.get());
1150
1151
62349
      if (eqpc) {
1152
5994
        if (Debug.isOn("pf::ee"))
1153
        {
1154
          Debug("pf::ee") << "Child proof is:" << std::endl;
1155
          eqpc->debug_print("pf::ee", 1);
1156
        }
1157
5994
        if (eqpc->d_id == MERGED_THROUGH_TRANS)
1158
        {
1159
5226
          std::vector<std::shared_ptr<EqProof>> orderedChildren;
1160
2613
          bool nullCongruenceFound = false;
1161
8866
          for (const auto& child : eqpc->d_children)
1162
          {
1163
12506
            if (child->d_id == MERGED_THROUGH_CONGRUENCE
1164
6253
                && child->d_node.isNull())
1165
            {
1166
2428
              nullCongruenceFound = true;
1167
4856
              Debug("pf::ee")
1168
2428
                  << "Have congruence with empty d_node. Splitting..."
1169
2428
                  << std::endl;
1170
7284
              orderedChildren.insert(orderedChildren.begin(),
1171
7284
                                     child->d_children[0]);
1172
2428
              orderedChildren.push_back(child->d_children[1]);
1173
            }
1174
            else
1175
            {
1176
3825
              orderedChildren.push_back(child);
1177
            }
1178
          }
1179
1180
2613
          if (nullCongruenceFound) {
1181
1893
            eqpc->d_children = orderedChildren;
1182
1893
            if (Debug.isOn("pf::ee"))
1183
            {
1184
              Debug("pf::ee")
1185
                  << "Child proof's children have been reordered. It is now:"
1186
                  << std::endl;
1187
              eqpc->debug_print("pf::ee", 1);
1188
            }
1189
          }
1190
        }
1191
1192
5994
        eqp->d_children.push_back(eqpc);
1193
      }
1194
    }
1195
1196
32729
    if (eqp) {
1197
4889
      if (eqp->d_children.size() == 0) {
1198
        // Corner case where this is actually a disequality between two constants
1199
        Debug("pf::ee") << "Encountered a constant disequality (not a transitivity proof): "
1200
                        << eqp->d_node << std::endl;
1201
        Assert(eqp->d_node[0][0].isConst());
1202
        Assert(eqp->d_node[0][1].isConst());
1203
        eqp->d_id = MERGED_THROUGH_CONSTANTS;
1204
4889
      } else if (eqp->d_children.size() == 1) {
1205
7694
        Node cnode = eqp->d_children[0]->d_node;
1206
7694
        Debug("pf::ee") << "Simplifying " << cnode << " from " << eqp->d_node
1207
3847
                        << std::endl;
1208
3847
        bool simpTrans = true;
1209
3847
        if (cnode.getKind() == kind::EQUAL)
1210
        {
1211
          // It may be the case that we have a proof of x = c2 and we want to
1212
          // conclude x != c1. If this is the case, below we construct:
1213
          //
1214
          //          -------- MERGED_THROUGH_EQUALITY
1215
          // x = c2   c1 != c2
1216
          // ----------------- TRANS
1217
          //     x != c1
1218
7694
          TNode c1 = t1.isConst() ? t1 : (t2.isConst() ? t2 : TNode::null());
1219
7694
          TNode nc = t1.isConst() ? t2 : (t2.isConst() ? t1 : TNode::null());
1220
7694
          Node c2;
1221
          // merge constants transitivity
1222
11509
          for (unsigned i = 0; i < 2; i++)
1223
          {
1224
7679
            if (cnode[i].isConst() && cnode[1 - i] == nc)
1225
            {
1226
17
              c2 = cnode[i];
1227
17
              break;
1228
            }
1229
          }
1230
3847
          if (!c1.isNull() && !c2.isNull())
1231
          {
1232
17
            simpTrans = false;
1233
17
            Assert(c1.getType().isComparableTo(c2.getType()));
1234
34
            std::shared_ptr<EqProof> eqpmc = std::make_shared<EqProof>();
1235
17
            eqpmc->d_id = MERGED_THROUGH_CONSTANTS;
1236
17
            eqpmc->d_node = c1.eqNode(c2).eqNode(d_false);
1237
17
            eqp->d_children.push_back(eqpmc);
1238
          }
1239
        }
1240
3847
        if (simpTrans)
1241
        {
1242
          // The transitivity proof has just one child. Simplify.
1243
7660
          std::shared_ptr<EqProof> temp = eqp->d_children[0];
1244
3830
          eqp->d_children.clear();
1245
3830
          *eqp = *temp;
1246
        }
1247
      }
1248
1249
4889
      if (Debug.isOn("pf::ee"))
1250
      {
1251
        Debug("pf::ee") << "Disequality explanation final proof: " << std::endl;
1252
        eqp->debug_print("pf::ee", 1);
1253
      }
1254
    }
1255
  }
1256
478859
}
1257
1258
31149
void EqualityEngine::explainPredicate(TNode p, bool polarity,
1259
                                      std::vector<TNode>& assertions,
1260
                                      EqProof* eqp) const {
1261
62298
  Debug("equality") << d_name << "::eq::explainPredicate(" << p << ")"
1262
31149
                    << std::endl;
1263
  // Must have the term
1264
31149
  Assert(hasTerm(p));
1265
62298
  std::map<std::pair<EqualityNodeId, EqualityNodeId>, EqProof*> cache;
1266
31149
  if (Debug.isOn("equality::internal"))
1267
  {
1268
    debugPrintGraph();
1269
  }
1270
  // Get the explanation
1271
31149
  getExplanation(
1272
      getNodeId(p), polarity ? d_trueId : d_falseId, assertions, cache, eqp);
1273
31149
}
1274
1275
417818
void EqualityEngine::explainLit(TNode lit, std::vector<TNode>& assumptions)
1276
{
1277
417818
  Assert(lit.getKind() != kind::AND);
1278
417818
  bool polarity = lit.getKind() != kind::NOT;
1279
835636
  TNode atom = polarity ? lit : lit[0];
1280
835636
  std::vector<TNode> tassumptions;
1281
417818
  if (atom.getKind() == kind::EQUAL)
1282
  {
1283
390542
    Assert(hasTerm(atom[0]));
1284
390542
    Assert(hasTerm(atom[1]));
1285
390542
    if (!polarity)
1286
    {
1287
      // ensure that we are ready to explain the disequality
1288
27246
      AlwaysAssert(areDisequal(atom[0], atom[1], true));
1289
    }
1290
363296
    else if (atom[0] == atom[1])
1291
    {
1292
      // no need to explain reflexivity
1293
      return;
1294
    }
1295
390542
    explainEquality(atom[0], atom[1], polarity, tassumptions);
1296
  }
1297
  else
1298
  {
1299
27276
    explainPredicate(atom, polarity, tassumptions);
1300
  }
1301
  // ensure that duplicates are removed
1302
2077713
  for (TNode a : tassumptions)
1303
  {
1304
4979685
    if (std::find(assumptions.begin(), assumptions.end(), a)
1305
4979685
        == assumptions.end())
1306
    {
1307
1495995
      Assert(!a.isNull());
1308
1495995
      assumptions.push_back(a);
1309
    }
1310
  }
1311
}
1312
1313
379395
Node EqualityEngine::mkExplainLit(TNode lit)
1314
{
1315
379395
  Assert(lit.getKind() != kind::AND);
1316
758790
  std::vector<TNode> assumptions;
1317
379395
  explainLit(lit, assumptions);
1318
379395
  Node ret;
1319
379395
  if (assumptions.empty())
1320
  {
1321
    ret = NodeManager::currentNM()->mkConst(true);
1322
  }
1323
379395
  else if (assumptions.size() == 1)
1324
  {
1325
90447
    ret = assumptions[0];
1326
  }
1327
  else
1328
  {
1329
288948
    ret = NodeManager::currentNM()->mkNode(kind::AND, assumptions);
1330
  }
1331
758790
  return ret;
1332
}
1333
1334
5702551
void EqualityEngine::getExplanation(
1335
    EqualityNodeId t1Id,
1336
    EqualityNodeId t2Id,
1337
    std::vector<TNode>& equalities,
1338
    std::map<std::pair<EqualityNodeId, EqualityNodeId>, EqProof*>& cache,
1339
    EqProof* eqp) const
1340
{
1341
11405102
  Trace("eq-exp") << d_name << "::eq::getExplanation({" << t1Id << "} "
1342
5702551
                  << d_nodes[t1Id] << ", {" << t2Id << "} " << d_nodes[t2Id]
1343
5702551
                  << ") size = " << cache.size() << std::endl;
1344
1345
  // determine if we have already computed the explanation.
1346
5702551
  std::pair<EqualityNodeId, EqualityNodeId> cacheKey;
1347
5702551
  std::map<std::pair<EqualityNodeId, EqualityNodeId>, EqProof*>::iterator it;
1348
5702551
  if (!eqp)
1349
  {
1350
    // If proofs are disabled, we order the ids, since explaining t1 = t2 is the
1351
    // same as explaining t2 = t1.
1352
4297437
    cacheKey = std::minmax(t1Id, t2Id);
1353
4297437
    it = cache.find(cacheKey);
1354
4297437
    if (it != cache.end())
1355
    {
1356
2163475
      return;
1357
    }
1358
  }
1359
  else
1360
  {
1361
    // If proofs are enabled, note that proofs are sensitive to the order of t1
1362
    // and t2, so we don't sort the ids in this case. TODO: Depending on how
1363
    // issue #2965 is resolved, we may be able to revisit this, if it is the
1364
    // case that proof/uf_proof.h,cpp is robust to equality ordering.
1365
1405114
    cacheKey = std::pair<EqualityNodeId, EqualityNodeId>(t1Id, t2Id);
1366
1405114
    it = cache.find(cacheKey);
1367
1405114
    if (it != cache.end())
1368
    {
1369
835813
      if (it->second)
1370
      {
1371
835811
        eqp->d_id = it->second->d_id;
1372
2507433
        eqp->d_children.insert(eqp->d_children.end(),
1373
835811
                               it->second->d_children.begin(),
1374
3343244
                               it->second->d_children.end());
1375
835811
        eqp->d_node = it->second->d_node;
1376
      }
1377
      else
1378
      {
1379
        // We may have cached null in its place, create the trivial proof now.
1380
2
        Assert(d_nodes[t1Id] == d_nodes[t2Id]);
1381
2
        Assert(eqp->d_id == MERGED_THROUGH_REFLEXIVITY);
1382
2
        eqp->d_node = d_nodes[t1Id].eqNode(d_nodes[t1Id]);
1383
      }
1384
835813
      return;
1385
    }
1386
  }
1387
2703263
  cache[cacheKey] = eqp;
1388
1389
  // We can only explain the nodes that got merged
1390
#ifdef CVC4_ASSERTIONS
1391
2703263
  bool canExplain = getEqualityNode(t1Id).getFind() == getEqualityNode(t2Id).getFind()
1392
2703263
                  || (d_done && isConstant(t1Id) && isConstant(t2Id));
1393
1394
2703263
  if (!canExplain) {
1395
    Warning() << "Can't explain equality:" << std::endl;
1396
    Warning() << d_nodes[t1Id] << " with find " << d_nodes[getEqualityNode(t1Id).getFind()] << std::endl;
1397
    Warning() << d_nodes[t2Id] << " with find " << d_nodes[getEqualityNode(t2Id).getFind()] << std::endl;
1398
  }
1399
2703263
  Assert(canExplain);
1400
#endif
1401
1402
  // If the nodes are the same, we're done
1403
2703263
  if (t1Id == t2Id)
1404
  {
1405
690447
    if (eqp)
1406
    {
1407
      // ignore equalities between function symbols, i.e. internal nullary
1408
      // non-constant nodes.
1409
      //
1410
      // Note that this is robust for HOL because in that case function
1411
      // symbols are not internal nodes
1412
308852
      if (d_isInternal[t1Id] && d_nodes[t1Id].getNumChildren() == 0
1413
177883
          && !d_isConstant[t1Id])
1414
      {
1415
47063
        eqp->d_node = Node::null();
1416
      }
1417
      else
1418
      {
1419
83757
        Assert(d_nodes[t1Id].getKind() != kind::BUILTIN);
1420
83757
        eqp->d_node = d_nodes[t1Id].eqNode(d_nodes[t1Id]);
1421
      }
1422
    }
1423
690447
    return;
1424
  }
1425
1426
  // Queue for the BFS containing nodes
1427
4025632
  std::vector<BfsData> bfsQueue;
1428
1429
  // Find a path from t1 to t2 in the graph (BFS)
1430
2012816
  bfsQueue.push_back(BfsData(t1Id, null_id, 0));
1431
2012816
  size_t currentIndex = 0;
1432
  while (true) {
1433
    // There should always be a path, and every node can be visited only once (tree)
1434
13425779
    Assert(currentIndex < bfsQueue.size());
1435
1436
    // The next node to visit
1437
13425779
    BfsData current = bfsQueue[currentIndex];
1438
13425779
    EqualityNodeId currentNode = current.d_nodeId;
1439
1440
26851558
    Debug("equality") << d_name << "::eq::getExplanation(): currentNode = {"
1441
13425779
                      << currentNode << "} " << d_nodes[currentNode]
1442
13425779
                      << std::endl;
1443
1444
    // Go through the equality edges of this node
1445
13425779
    EqualityEdgeId currentEdge = d_equalityGraph[currentNode];
1446
13425779
    if (Debug.isOn("equality")) {
1447
      Debug("equality") << d_name << "::eq::getExplanation(): edgesId =  " << currentEdge << std::endl;
1448
      Debug("equality") << d_name << "::eq::getExplanation(): edges =  " << edgesToString(currentEdge) << std::endl;
1449
    }
1450
1451
78526647
    while (currentEdge != null_edge) {
1452
      // Get the edge
1453
34563250
      const EqualityEdge& edge = d_equalityEdges[currentEdge];
1454
1455
      // If not just the backwards edge
1456
34563250
      if ((currentEdge | 1u) != (current.d_edgeId | 1u))
1457
      {
1458
47459456
        Debug("equality") << d_name
1459
23729728
                          << "::eq::getExplanation(): currentEdge = ({"
1460
23729728
                          << currentNode << "} " << d_nodes[currentNode]
1461
47459456
                          << ", {" << edge.getNodeId() << "} "
1462
23729728
                          << d_nodes[edge.getNodeId()] << ")" << std::endl;
1463
1464
        // Did we find the path
1465
23729728
        if (edge.getNodeId() == t2Id) {
1466
1467
2012816
          Debug("equality") << d_name << "::eq::getExplanation(): path found: " << std::endl;
1468
1469
4025632
          std::vector<std::shared_ptr<EqProof>> eqp_trans;
1470
1471
          // Reconstruct the path
1472
2753111
          do {
1473
            // The current node
1474
4765927
            currentNode = bfsQueue[currentIndex].d_nodeId;
1475
4765927
            EqualityNodeId edgeNode = d_equalityEdges[currentEdge].getNodeId();
1476
            MergeReasonType reasonType = static_cast<MergeReasonType>(
1477
4765927
                d_equalityEdges[currentEdge].getReasonType());
1478
9531854
            Node reason = d_equalityEdges[currentEdge].getReason();
1479
1480
9531854
            Debug("equality")
1481
4765927
                << d_name
1482
4765927
                << "::eq::getExplanation(): currentEdge = " << currentEdge
1483
4765927
                << ", currentNode = " << currentNode << std::endl;
1484
9531854
            Debug("equality")
1485
4765927
                << d_name << "                       targetNode = {" << edgeNode
1486
4765927
                << "} " << d_nodes[edgeNode] << std::endl;
1487
9531854
            Debug("equality")
1488
4765927
                << d_name << "                       in currentEdge = ({"
1489
4765927
                << currentNode << "} " << d_nodes[currentNode] << ", {"
1490
9531854
                << edge.getNodeId() << "} " << d_nodes[edge.getNodeId()] << ")"
1491
4765927
                << std::endl;
1492
9531854
            Debug("equality")
1493
4765927
                << d_name
1494
4765927
                << "                       reason type = " << reasonType
1495
4765927
                << "\n";
1496
1497
9531854
            std::shared_ptr<EqProof> eqpc;;
1498
            // Make child proof if a proof is being constructed
1499
4765927
            if (eqp) {
1500
1098473
              eqpc = std::make_shared<EqProof>();
1501
1098473
              eqpc->d_id = reasonType;
1502
            }
1503
1504
            // Add the actual equality to the vector
1505
4765927
            switch (reasonType) {
1506
2554129
            case MERGED_THROUGH_CONGRUENCE: {
1507
              // f(x1, x2) == f(y1, y2) because x1 = y1 and x2 = y2
1508
5108258
              Debug("equality")
1509
2554129
                  << d_name
1510
2554129
                  << "::eq::getExplanation(): due to congruence, going deeper"
1511
2554129
                  << std::endl;
1512
              const FunctionApplication& f1 =
1513
2554129
                  d_applications[currentNode].d_original;
1514
              const FunctionApplication& f2 =
1515
2554129
                  d_applications[edgeNode].d_original;
1516
1517
2554129
              Debug("equality") << push;
1518
2554129
              Debug("equality") << "Explaining left hand side equalities" << std::endl;
1519
              std::shared_ptr<EqProof> eqpc1 =
1520
5108258
                  eqpc ? std::make_shared<EqProof>() : nullptr;
1521
2554129
              getExplanation(f1.d_a, f2.d_a, equalities, cache, eqpc1.get());
1522
2554129
              Debug("equality") << "Explaining right hand side equalities" << std::endl;
1523
              std::shared_ptr<EqProof> eqpc2 =
1524
5108258
                  eqpc ? std::make_shared<EqProof>() : nullptr;
1525
2554129
              getExplanation(f1.d_b, f2.d_b, equalities, cache, eqpc2.get());
1526
2554129
              if (eqpc)
1527
              {
1528
661969
                eqpc->d_children.push_back(eqpc1);
1529
661969
                eqpc->d_children.push_back(eqpc2);
1530
                // build conclusion if ids correspond to non-internal nodes or
1531
                // if non-internal nodes can be retrieved from them (in the
1532
                // case of n-ary applications), otherwise leave conclusion as
1533
                // null. This is only done for congruence kinds, since
1534
                // congruence is not used otherwise.
1535
661969
                Kind k = d_nodes[currentNode].getKind();
1536
661969
                if (d_congruenceKinds[k])
1537
                {
1538
657778
                  buildEqConclusion(currentNode, edgeNode, eqpc.get());
1539
                }
1540
                else
1541
                {
1542
8382
                  Assert(k == kind::EQUAL)
1543
4191
                      << "not an internal node " << d_nodes[currentNode]
1544
                      << " with non-congruence with " << k << "\n";
1545
                }
1546
              }
1547
2554129
              Debug("equality") << pop;
1548
2554129
              break;
1549
            }
1550
1551
13666
            case MERGED_THROUGH_REFLEXIVITY: {
1552
              // x1 == x1
1553
13666
              Debug("equality") << d_name << "::eq::getExplanation(): due to reflexivity, going deeper" << std::endl;
1554
13666
              EqualityNodeId eqId = currentNode == d_trueId ? edgeNode : currentNode;
1555
13666
              const FunctionApplication& eq = d_applications[eqId].d_original;
1556
13666
              Assert(eq.isEquality()) << "Must be an equality";
1557
1558
              // Explain why a = b constant
1559
13666
              Debug("equality") << push;
1560
              std::shared_ptr<EqProof> eqpc1 =
1561
27332
                  eqpc ? std::make_shared<EqProof>() : nullptr;
1562
13666
              getExplanation(eq.d_a, eq.d_b, equalities, cache, eqpc1.get());
1563
13666
              if( eqpc ){
1564
1732
                eqpc->d_children.push_back( eqpc1 );
1565
              }
1566
13666
              Debug("equality") << pop;
1567
1568
13666
              break;
1569
            }
1570
1571
21866
            case MERGED_THROUGH_CONSTANTS: {
1572
              // f(c1, ..., cn) = c semantically, we can just ignore it
1573
21866
              Debug("equality") << d_name << "::eq::getExplanation(): due to constants, explain the constants" << std::endl;
1574
21866
              Debug("equality") << push;
1575
1576
              // Get the node we interpreted
1577
43732
              TNode interpreted;
1578
21866
              if (eqpc)
1579
              {
1580
                // build the conclusion f(c1, ..., cn) = c
1581
1225
                if (d_nodes[currentNode].isConst())
1582
                {
1583
403
                  interpreted = d_nodes[edgeNode];
1584
403
                  eqpc->d_node = d_nodes[edgeNode].eqNode(d_nodes[currentNode]);
1585
                }
1586
                else
1587
                {
1588
822
                  interpreted = d_nodes[currentNode];
1589
822
                  eqpc->d_node = d_nodes[currentNode].eqNode(d_nodes[edgeNode]);
1590
                }
1591
              }
1592
              else
1593
              {
1594
41282
                interpreted = d_nodes[currentNode].isConst()
1595
7415
                                  ? d_nodes[edgeNode]
1596
28056
                                  : d_nodes[currentNode];
1597
              }
1598
1599
              // Explain why a is a constant by explaining each argument
1600
62865
              for (unsigned i = 0; i < interpreted.getNumChildren(); ++ i) {
1601
40999
                EqualityNodeId childId = getNodeId(interpreted[i]);
1602
40999
                Assert(isConstant(childId));
1603
                std::shared_ptr<EqProof> eqpcc =
1604
81998
                    eqpc ? std::make_shared<EqProof>() : nullptr;
1605
81998
                getExplanation(childId,
1606
40999
                               getEqualityNode(childId).getFind(),
1607
                               equalities,
1608
                               cache,
1609
                               eqpcc.get());
1610
40999
                if( eqpc ) {
1611
2725
                  eqpc->d_children.push_back( eqpcc );
1612
2725
                  if (Debug.isOn("pf::ee"))
1613
                  {
1614
                    Debug("pf::ee")
1615
                        << "MERGED_THROUGH_CONSTANTS. Dumping the child proof"
1616
                        << std::endl;
1617
                    eqpc->debug_print("pf::ee", 1);
1618
                  }
1619
                }
1620
              }
1621
1622
21866
              Debug("equality") << pop;
1623
21866
              break;
1624
            }
1625
1626
2176266
            default: {
1627
              // Construct the equality
1628
4352532
              Debug("equality") << d_name << "::eq::getExplanation(): adding: "
1629
2176266
                                << reason << std::endl;
1630
4352532
              Debug("equality")
1631
2176266
                  << d_name
1632
2176266
                  << "::eq::getExplanation(): reason type = " << reasonType
1633
2176266
                  << "\n";
1634
4352532
              Node a = d_nodes[currentNode];
1635
4352532
              Node b = d_nodes[d_equalityEdges[currentEdge].getNodeId()];
1636
1637
2176266
              if (eqpc) {
1638
433547
                if (reasonType == MERGED_THROUGH_EQUALITY) {
1639
                  // in the new proof infrastructure we can assume that "theory
1640
                  // assumptions", which are a consequence of theory reasoning
1641
                  // on other assumptions, are externally justified. In this
1642
                  // case we can use (= a b) directly as the conclusion here.
1643
433547
                  eqpc->d_node = b.eqNode(a);
1644
                } else {
1645
                  // The LFSC translator prefers (not (= a b)) over (= (= a b) false)
1646
1647
                  if (a == NodeManager::currentNM()->mkConst(false)) {
1648
                    eqpc->d_node = b.notNode();
1649
                  } else if (b == NodeManager::currentNM()->mkConst(false)) {
1650
                    eqpc->d_node = a.notNode();
1651
                  } else {
1652
                    eqpc->d_node = b.eqNode(a);
1653
                  }
1654
                }
1655
433547
                eqpc->d_id = reasonType;
1656
              }
1657
2176266
              equalities.push_back(reason);
1658
2176266
              break;
1659
            }
1660
            }
1661
1662
            // Go to the previous
1663
4765927
            currentEdge = bfsQueue[currentIndex].d_edgeId;
1664
4765927
            currentIndex = bfsQueue[currentIndex].d_previousIndex;
1665
1666
            //---from Morgan---
1667
4765927
            if (eqpc != NULL && eqpc->d_id == MERGED_THROUGH_REFLEXIVITY) {
1668
1732
              if(eqpc->d_node.isNull()) {
1669
1732
                Assert(eqpc->d_children.size() == 1);
1670
3464
                std::shared_ptr<EqProof> p = eqpc;
1671
1732
                eqpc = p->d_children[0];
1672
              } else {
1673
                Assert(eqpc->d_children.empty());
1674
              }
1675
            }
1676
            //---end from Morgan---
1677
1678
4765927
            eqp_trans.push_back(eqpc);
1679
4765927
          } while (currentEdge != null_id);
1680
1681
2012816
          if (eqp) {
1682
438481
            if(eqp_trans.size() == 1) {
1683
140495
              *eqp = *eqp_trans[0];
1684
            } else {
1685
297986
              eqp->d_id = MERGED_THROUGH_TRANS;
1686
297986
              eqp->d_children.insert( eqp->d_children.end(), eqp_trans.begin(), eqp_trans.end() );
1687
              // build conclusion in case of equality between non-internal
1688
              // nodes or of n-ary congruence kinds, otherwise leave as
1689
              // null. The latter is necessary for the overall handling of
1690
              // congruence proofs involving n-ary kinds, see
1691
              // EqProof::reduceNestedCongruence for more details.
1692
297986
              buildEqConclusion(t1Id, t2Id, eqp);
1693
            }
1694
438481
            if (Debug.isOn("pf::ee"))
1695
            {
1696
              eqp->debug_print("pf::ee", 1);
1697
            }
1698
          }
1699
1700
          // Done
1701
2012816
          return;
1702
        }
1703
1704
        // Push to the visitation queue if it's not the backward edge
1705
21716912
        bfsQueue.push_back(BfsData(edge.getNodeId(), currentEdge, currentIndex));
1706
      }
1707
1708
      // Go to the next edge
1709
32550434
      currentEdge = edge.getNext();
1710
    }
1711
1712
    // Go to the next node to visit
1713
11412963
    ++ currentIndex;
1714
11412963
  }
1715
}
1716
1717
751612
void EqualityEngine::addTriggerEquality(TNode eq) {
1718
751612
  Assert(eq.getKind() == kind::EQUAL);
1719
1720
751612
  if (d_done) {
1721
30
    return;
1722
  }
1723
1724
  // Add the terms
1725
751582
  addTermInternal(eq[0]);
1726
751582
  addTermInternal(eq[1]);
1727
1728
751582
  bool skipTrigger = false;
1729
1730
  // If they are equal or disequal already, no need for the trigger
1731
751582
  if (areEqual(eq[0], eq[1])) {
1732
19561
    d_notify.eqNotifyTriggerPredicate(eq, true);
1733
19561
    skipTrigger = true;
1734
  }
1735
751582
  if (areDisequal(eq[0], eq[1], true)) {
1736
11441
    d_notify.eqNotifyTriggerPredicate(eq, false);
1737
11441
    skipTrigger = true;
1738
  }
1739
1740
751582
  if (skipTrigger) {
1741
31002
    return;
1742
  }
1743
1744
  // Add the equality
1745
720580
  addTermInternal(eq);
1746
1747
  // Positive trigger
1748
720580
  addTriggerEqualityInternal(eq[0], eq[1], eq, true);
1749
  // Negative trigger
1750
720580
  addTriggerEqualityInternal(eq, d_false, eq, false);
1751
}
1752
1753
843278
void EqualityEngine::addTriggerPredicate(TNode predicate) {
1754
843278
  Assert(predicate.getKind() != kind::NOT);
1755
843278
  if (predicate.getKind() == kind::EQUAL)
1756
  {
1757
    // equality is handled separately
1758
751612
    return addTriggerEquality(predicate);
1759
  }
1760
91666
  Assert(d_congruenceKinds.test(predicate.getKind()))
1761
      << "No point in adding non-congruence predicates, kind is "
1762
      << predicate.getKind();
1763
1764
91666
  if (d_done) {
1765
285
    return;
1766
  }
1767
1768
  // Add the term
1769
91381
  addTermInternal(predicate);
1770
1771
91381
  bool skipTrigger = false;
1772
1773
  // If it's know already, no need for the trigger
1774
91381
  if (areEqual(predicate, d_true)) {
1775
2632
    d_notify.eqNotifyTriggerPredicate(predicate, true);
1776
2632
    skipTrigger = true;
1777
  }
1778
91381
  if (areEqual(predicate, d_false)) {
1779
1833
    d_notify.eqNotifyTriggerPredicate(predicate, false);
1780
1833
    skipTrigger = true;
1781
  }
1782
1783
91381
  if (skipTrigger) {
1784
4465
    return;
1785
  }
1786
1787
  // Positive trigger
1788
86916
  addTriggerEqualityInternal(predicate, d_true, predicate, true);
1789
  // Negative trigger
1790
86916
  addTriggerEqualityInternal(predicate, d_false, predicate, false);
1791
}
1792
1793
1614992
void EqualityEngine::addTriggerEqualityInternal(TNode t1, TNode t2, TNode trigger, bool polarity) {
1794
1795
1614992
  Debug("equality") << d_name << "::eq::addTrigger(" << t1 << ", " << t2 << ", " << trigger << ")" << std::endl;
1796
1797
1614992
  Assert(hasTerm(t1));
1798
1614992
  Assert(hasTerm(t2));
1799
1800
1614992
  if (d_done) {
1801
    return;
1802
  }
1803
1804
  // Get the information about t1
1805
1614992
  EqualityNodeId t1Id = getNodeId(t1);
1806
1614992
  EqualityNodeId t1classId = getEqualityNode(t1Id).getFind();
1807
  // We will attach it to the class representative, since then we know how to backtrack it
1808
1614992
  TriggerId t1TriggerId = d_nodeTriggers[t1classId];
1809
1810
  // Get the information about t2
1811
1614992
  EqualityNodeId t2Id = getNodeId(t2);
1812
1614992
  EqualityNodeId t2classId = getEqualityNode(t2Id).getFind();
1813
  // We will attach it to the class representative, since then we know how to backtrack it
1814
1614992
  TriggerId t2TriggerId = d_nodeTriggers[t2classId];
1815
1816
1614992
  Debug("equality") << d_name << "::eq::addTrigger(" << trigger << "): " << t1Id << " (" << t1classId << ") = " << t2Id << " (" << t2classId << ")" << std::endl;
1817
1818
  // Create the triggers
1819
1614992
  TriggerId t1NewTriggerId = d_equalityTriggers.size();
1820
1614992
  d_equalityTriggers.push_back(Trigger(t1classId, t1TriggerId));
1821
1614992
  d_equalityTriggersOriginal.push_back(TriggerInfo(trigger, polarity));
1822
1614992
  TriggerId t2NewTriggerId = d_equalityTriggers.size();
1823
1614992
  d_equalityTriggers.push_back(Trigger(t2classId, t2TriggerId));
1824
1614992
  d_equalityTriggersOriginal.push_back(TriggerInfo(trigger, polarity));
1825
1826
  // Update the counters
1827
1614992
  d_equalityTriggersCount = d_equalityTriggers.size();
1828
1614992
  Assert(d_equalityTriggers.size() == d_equalityTriggersOriginal.size());
1829
1614992
  Assert(d_equalityTriggers.size() % 2 == 0);
1830
1831
  // Add the trigger to the trigger graph
1832
1614992
  d_nodeTriggers[t1classId] = t1NewTriggerId;
1833
1614992
  d_nodeTriggers[t2classId] = t2NewTriggerId;
1834
1835
1614992
  if (Debug.isOn("equality::internal")) {
1836
    debugPrintGraph();
1837
  }
1838
1839
1614992
  Debug("equality") << d_name << "::eq::addTrigger(" << t1 << "," << t2 << ") => (" << t1NewTriggerId << ", " << t2NewTriggerId << ")" << std::endl;
1840
}
1841
1842
473976
Node EqualityEngine::evaluateTerm(TNode node) {
1843
473976
  Debug("equality::evaluation") << d_name << "::eq::evaluateTerm(" << node << ")" << std::endl;
1844
947952
  NodeBuilder<> builder;
1845
473976
  builder << node.getKind();
1846
473976
  if (node.getMetaKind() == kind::metakind::PARAMETERIZED) {
1847
4588
    builder << node.getOperator();
1848
  }
1849
1290158
  for (unsigned i = 0; i < node.getNumChildren(); ++ i) {
1850
1632364
    TNode child = node[i];
1851
1632364
    TNode childRep = getRepresentative(child);
1852
816182
    Debug("equality::evaluation") << d_name << "::eq::evaluateTerm: " << child << " -> " << childRep << std::endl;
1853
816182
    Assert(childRep.isConst());
1854
816182
    builder << childRep;
1855
  }
1856
947952
  Node newNode = builder;
1857
947952
  return Rewriter::rewrite(newNode);
1858
}
1859
1860
277054
void EqualityEngine::processEvaluationQueue() {
1861
1862
277054
  Debug("equality::evaluation") << d_name << "::eq::processEvaluationQueue(): start" << std::endl;
1863
1864
1225006
  while (!d_evaluationQueue.empty()) {
1865
    // Get the node
1866
473976
    EqualityNodeId id = d_evaluationQueue.front();
1867
473976
    d_evaluationQueue.pop();
1868
1869
    // Replace the children with their representatives (must be constants)
1870
947952
    Node nodeEvaluated = evaluateTerm(d_nodes[id]);
1871
473976
    Debug("equality::evaluation") << d_name << "::eq::processEvaluationQueue(): " << d_nodes[id] << " evaluates to " << nodeEvaluated << std::endl;
1872
473976
    Assert(nodeEvaluated.isConst());
1873
473976
    addTermInternal(nodeEvaluated);
1874
473976
    EqualityNodeId nodeEvaluatedId = getNodeId(nodeEvaluated);
1875
1876
    // Enqueue the semantic equality
1877
473976
    enqueue(MergeCandidate(id, nodeEvaluatedId, MERGED_THROUGH_CONSTANTS, TNode::null()));
1878
  }
1879
1880
277054
  Debug("equality::evaluation") << d_name << "::eq::processEvaluationQueue(): done" << std::endl;
1881
277054
}
1882
1883
23274092
void EqualityEngine::propagate() {
1884
1885
23274092
  if (d_inPropagate) {
1886
    // We're already in propagate, go back
1887
55825
    return;
1888
  }
1889
1890
  // Make sure we don't get in again
1891
46436534
  ScopedBool inPropagate(d_inPropagate, true);
1892
1893
23218267
  Debug("equality") << d_name << "::eq::propagate()" << std::endl;
1894
1895
87069123
  while (!d_propagationQueue.empty() || !d_evaluationQueue.empty()) {
1896
1897
32013176
    if (d_done) {
1898
      // If we're done, just empty the queue
1899
4197830
      while (!d_propagationQueue.empty()) d_propagationQueue.pop_front();
1900
89324
      while (!d_evaluationQueue.empty()) d_evaluationQueue.pop();
1901
6213044
      continue;
1902
    }
1903
1904
    // Process any evaluation requests
1905
32114740
    if (!d_evaluationQueue.empty()) {
1906
277054
      processEvaluationQueue();
1907
277054
      continue;
1908
    }
1909
1910
    // The current merge candidate
1911
57360764
    const MergeCandidate current = d_propagationQueue.front();
1912
31560632
    d_propagationQueue.pop_front();
1913
1914
    // Get the representatives
1915
31560632
    EqualityNodeId t1classId = getEqualityNode(current.d_t1Id).getFind();
1916
31560632
    EqualityNodeId t2classId = getEqualityNode(current.d_t2Id).getFind();
1917
1918
    // If already the same, we're done
1919
31560632
    if (t1classId == t2classId) {
1920
5727256
      continue;
1921
    }
1922
1923
25833376
    Debug("equality::internal") << d_name << "::eq::propagate(): t1: " << (d_isInternal[t1classId] ? "internal" : "proper") << std::endl;
1924
25833376
    Debug("equality::internal") << d_name << "::eq::propagate(): t2: " << (d_isInternal[t2classId] ? "internal" : "proper") << std::endl;
1925
1926
    // Get the nodes of the representatives
1927
25833376
    EqualityNode& node1 = getEqualityNode(t1classId);
1928
25833376
    EqualityNode& node2 = getEqualityNode(t2classId);
1929
1930
25833376
    Assert(node1.getFind() == t1classId);
1931
25833376
    Assert(node2.getFind() == t2classId);
1932
1933
    // Add the actual equality to the equality graph
1934
51666752
    addGraphEdge(
1935
25833376
        current.d_t1Id, current.d_t2Id, current.d_type, current.d_reason);
1936
1937
    // If constants are being merged we're done
1938
25866620
    if (d_isConstant[t1classId] && d_isConstant[t2classId]) {
1939
      // When merging constants we are inconsistent, hence done
1940
33244
      d_done = true;
1941
      // But in order to keep invariants (edges = 2*equalities) we put an equalities in
1942
      // Note that we can explain this merge as we have a graph edge
1943
33244
      d_assertedEqualities.push_back(Equality(null_id, null_id));
1944
33244
      d_assertedEqualitiesCount = d_assertedEqualitiesCount + 1;
1945
      // Notify
1946
33244
      if (d_performNotify) {
1947
33244
        d_notify.eqNotifyConstantTermMerge(d_nodes[t1classId], d_nodes[t2classId]);
1948
      }
1949
      // Empty the queue and exit
1950
33244
      continue;
1951
    }
1952
1953
    // Vector to collect the triggered events
1954
51600264
    std::vector<TriggerId> triggers;
1955
1956
    // Figure out the merge preference
1957
25800132
    EqualityNodeId mergeInto = t1classId;
1958
25800132
    if (d_isInternal[t2classId] != d_isInternal[t1classId]) {
1959
      // We always keep non-internal nodes as representatives: if any node in
1960
      // the class is non-internal, then the representative will be non-internal
1961
11861
      if (d_isInternal[t1classId]) {
1962
6635
        mergeInto = t2classId;
1963
      } else {
1964
5226
        mergeInto = t1classId;
1965
      }
1966
25788271
    } else if (d_isConstant[t2classId] != d_isConstant[t1classId]) {
1967
      // We always keep constants as representatives: if any (at most one) node
1968
      // in the class in a constant, then the representative will be a constant
1969
19149944
      if (d_isConstant[t2classId]) {
1970
17240992
        mergeInto = t2classId;
1971
      } else {
1972
1908952
        mergeInto = t1classId;
1973
      }
1974
6638327
    } else if (node2.getSize() > node1.getSize()) {
1975
      // We always merge into the bigger class to reduce the amount of traversing
1976
      // we need to do
1977
2644891
      mergeInto = t2classId;
1978
    }
1979
1980
25800132
    if (mergeInto == t2classId) {
1981
39785036
      Debug("equality") << d_name << "::eq::propagate(): merging "
1982
19892518
                        << d_nodes[current.d_t1Id] << " into "
1983
19892518
                        << d_nodes[current.d_t2Id] << std::endl;
1984
19892518
      d_assertedEqualities.push_back(Equality(t2classId, t1classId));
1985
19892518
      d_assertedEqualitiesCount = d_assertedEqualitiesCount + 1;
1986
19892518
      if (!merge(node2, node1, triggers)) {
1987
5938
        d_done = true;
1988
      }
1989
    } else {
1990
11815228
      Debug("equality") << d_name << "::eq::propagate(): merging "
1991
5907614
                        << d_nodes[current.d_t2Id] << " into "
1992
5907614
                        << d_nodes[current.d_t1Id] << std::endl;
1993
5907614
      d_assertedEqualities.push_back(Equality(t1classId, t2classId));
1994
5907614
      d_assertedEqualitiesCount = d_assertedEqualitiesCount + 1;
1995
5907614
    if (!merge(node1, node2, triggers)) {
1996
5193
        d_done = true;
1997
      }
1998
    }
1999
2000
    // If not merging internal nodes, notify the master
2001
25800129
    if (d_masterEqualityEngine && !d_isInternal[t1classId] && !d_isInternal[t2classId]) {
2002
5884250
      d_masterEqualityEngine->assertEqualityInternal(d_nodes[t1classId], d_nodes[t2classId], TNode::null());
2003
5884250
      d_masterEqualityEngine->propagate();
2004
    }
2005
2006
    // Notify the triggers
2007
25800129
    if (d_performNotify && !d_done) {
2008
38361850
      for (size_t trigger_i = 0, trigger_end = triggers.size(); trigger_i < trigger_end && !d_done; ++ trigger_i) {
2009
12572852
        const TriggerInfo& triggerInfo = d_equalityTriggersOriginal[triggers[trigger_i]];
2010
12572852
        if (triggerInfo.d_trigger.getKind() == kind::EQUAL)
2011
        {
2012
          // Special treatment for disequalities
2013
10733705
          if (!triggerInfo.d_polarity)
2014
          {
2015
            // Store that we are propagating a diseauality
2016
13419282
            TNode equality = triggerInfo.d_trigger;
2017
6709641
            EqualityNodeId original = getNodeId(equality);
2018
13419282
            TNode lhs = equality[0];
2019
13419282
            TNode rhs = equality[1];
2020
6709641
            EqualityNodeId lhsId = getNodeId(lhs);
2021
6709641
            EqualityNodeId rhsId = getNodeId(rhs);
2022
            // We use the THEORY_LAST as a marker for "marked as propagated, reasons stored".
2023
            // This tag is added to an internal theories set that is only inserted in, so this is
2024
            // safe. Had we iterated over, or done other set operations this might be dangerous.
2025
6709641
            if (!hasPropagatedDisequality(THEORY_LAST, lhsId, rhsId)) {
2026
6372282
              if (!hasPropagatedDisequality(lhsId, rhsId)) {
2027
6358669
                d_deducedDisequalityReasons.push_back(EqualityPair(original, d_falseId));
2028
              }
2029
6372282
              storePropagatedDisequality(THEORY_LAST, lhsId, rhsId);
2030
12744564
              if (!d_notify.eqNotifyTriggerPredicate(triggerInfo.d_trigger,
2031
6372282
                                                     triggerInfo.d_polarity))
2032
              {
2033
401
                d_done = true;
2034
              }
2035
            }
2036
          }
2037
          else
2038
          {
2039
            // Equalities are simple
2040
8048128
            if (!d_notify.eqNotifyTriggerPredicate(triggerInfo.d_trigger,
2041
4024064
                                                   triggerInfo.d_polarity))
2042
            {
2043
58489
              d_done = true;
2044
            }
2045
          }
2046
        }
2047
        else
2048
        {
2049
3678294
          if (!d_notify.eqNotifyTriggerPredicate(triggerInfo.d_trigger,
2050
1839147
                                                 triggerInfo.d_polarity))
2051
          {
2052
3539
            d_done = true;
2053
          }
2054
        }
2055
      }
2056
    }
2057
  }
2058
}
2059
2060
void EqualityEngine::debugPrintGraph() const {
2061
  Debug("equality::graph") << std::endl << "Dumping graph" << std::endl;
2062
  for (EqualityNodeId nodeId = 0; nodeId < d_nodes.size(); ++ nodeId) {
2063
2064
    Debug("equality::graph") << d_nodes[nodeId] << " " << nodeId << "(" << getEqualityNode(nodeId).getFind() << "):";
2065
2066
    EqualityEdgeId edgeId = d_equalityGraph[nodeId];
2067
    while (edgeId != null_edge) {
2068
      const EqualityEdge& edge = d_equalityEdges[edgeId];
2069
      Debug("equality::graph") << " [" << edge.getNodeId() << "] " << d_nodes[edge.getNodeId()] << ":" << edge.getReason();
2070
      edgeId = edge.getNext();
2071
    }
2072
2073
    Debug("equality::graph") << std::endl;
2074
  }
2075
  Debug("equality::graph") << std::endl;
2076
}
2077
2078
std::string EqualityEngine::debugPrintEqc() const
2079
{
2080
  std::stringstream ss;
2081
  eq::EqClassesIterator eqcs2_i = eq::EqClassesIterator(this);
2082
  while (!eqcs2_i.isFinished())
2083
  {
2084
    Node eqc = (*eqcs2_i);
2085
    eq::EqClassIterator eqc2_i = eq::EqClassIterator(eqc, this);
2086
    ss << "Eqc( " << eqc << " ) : { ";
2087
    while (!eqc2_i.isFinished())
2088
    {
2089
      if ((*eqc2_i) != eqc && (*eqc2_i).getKind() != kind::EQUAL)
2090
      {
2091
        ss << (*eqc2_i) << " ";
2092
      }
2093
      ++eqc2_i;
2094
    }
2095
    ss << " } " << std::endl;
2096
    ++eqcs2_i;
2097
  }
2098
  return ss.str();
2099
}
2100
2101
19362065
bool EqualityEngine::areEqual(TNode t1, TNode t2) const {
2102
19362065
  Debug("equality") << d_name << "::eq::areEqual(" << t1 << "," << t2 << ")";
2103
2104
19362065
  Assert(hasTerm(t1));
2105
19362065
  Assert(hasTerm(t2));
2106
2107
19362065
  bool result = getEqualityNode(t1).getFind() == getEqualityNode(t2).getFind();
2108
19362065
  Debug("equality") << (result ? "\t(YES)" : "\t(NO)") << std::endl;
2109
19362065
  return result;
2110
}
2111
2112
14375008
bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const
2113
{
2114
14375008
  Debug("equality") << d_name << "::eq::areDisequal(" << t1 << "," << t2 << ")";
2115
2116
  // Add the terms
2117
14375008
  Assert(hasTerm(t1));
2118
14375008
  Assert(hasTerm(t2));
2119
2120
  // Get ids
2121
14375008
  EqualityNodeId t1Id = getNodeId(t1);
2122
14375008
  EqualityNodeId t2Id = getNodeId(t2);
2123
2124
  // If we propagated this disequality we're true
2125
14375008
  if (hasPropagatedDisequality(t1Id, t2Id)) {
2126
3803460
    Debug("equality") << "\t(YES)" << std::endl;
2127
3803460
    return true;
2128
  }
2129
2130
  // Get equivalence classes
2131
10571548
  EqualityNodeId t1ClassId = getEqualityNode(t1Id).getFind();
2132
10571548
  EqualityNodeId t2ClassId = getEqualityNode(t2Id).getFind();
2133
2134
  // We are semantically const, for remembering stuff
2135
10571548
  EqualityEngine* nonConst = const_cast<EqualityEngine*>(this);
2136
2137
  // Check for constants
2138
10571548
  if (d_isConstant[t1ClassId] && d_isConstant[t2ClassId] && t1ClassId != t2ClassId) {
2139
2513155
    if (ensureProof) {
2140
8375
      nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(t1Id, t1ClassId));
2141
8375
      nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(t2Id, t2ClassId));
2142
8375
      nonConst->storePropagatedDisequality(THEORY_LAST, t1Id, t2Id);
2143
    }
2144
2513155
    Debug("equality") << "\t(YES)" << std::endl;
2145
2513155
    return true;
2146
  }
2147
2148
  // Create the equality
2149
8058393
  FunctionApplication eqNormalized(APP_EQUALITY, t1ClassId, t2ClassId);
2150
8058393
  ApplicationIdsMap::const_iterator find = d_applicationLookup.find(eqNormalized);
2151
8058393
  if (find != d_applicationLookup.end()) {
2152
3409525
    if (getEqualityNode(find->second).getFind() == getEqualityNode(d_falseId).getFind()) {
2153
270289
      if (ensureProof) {
2154
        const FunctionApplication original =
2155
2075
            d_applications[find->second].d_original;
2156
4150
        nonConst->d_deducedDisequalityReasons.push_back(
2157
4150
            EqualityPair(t1Id, original.d_a));
2158
2075
        nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(find->second, d_falseId));
2159
4150
        nonConst->d_deducedDisequalityReasons.push_back(
2160
4150
            EqualityPair(t2Id, original.d_b));
2161
2075
        nonConst->storePropagatedDisequality(THEORY_LAST, t1Id, t2Id);
2162
      }
2163
270289
      Debug("equality") << "\t(YES)" << std::endl;
2164
270289
      return true;
2165
    }
2166
  }
2167
2168
  // Check the symmetric disequality
2169
7788104
  std::swap(eqNormalized.d_a, eqNormalized.d_b);
2170
7788104
  find = d_applicationLookup.find(eqNormalized);
2171
7788104
  if (find != d_applicationLookup.end()) {
2172
548731
    if (getEqualityNode(find->second).getFind() == getEqualityNode(d_falseId).getFind()) {
2173
353755
      if (ensureProof) {
2174
        const FunctionApplication original =
2175
1202
            d_applications[find->second].d_original;
2176
2404
        nonConst->d_deducedDisequalityReasons.push_back(
2177
2404
            EqualityPair(t2Id, original.d_a));
2178
1202
        nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(find->second, d_falseId));
2179
2404
        nonConst->d_deducedDisequalityReasons.push_back(
2180
2404
            EqualityPair(t1Id, original.d_b));
2181
1202
        nonConst->storePropagatedDisequality(THEORY_LAST, t1Id, t2Id);
2182
      }
2183
353755
      Debug("equality") << "\t(YES)" << std::endl;
2184
353755
      return true;
2185
    }
2186
  }
2187
2188
  // Couldn't deduce dis-equalityReturn whether the terms are disequal
2189
7434349
  Debug("equality") << "\t(NO)" << std::endl;
2190
7434349
  return false;
2191
}
2192
2193
size_t EqualityEngine::getSize(TNode t) {
2194
  // Add the term
2195
  addTermInternal(t);
2196
  return getEqualityNode(getEqualityNode(t).getFind()).getSize();
2197
}
2198
2199
14330
std::string EqualityEngine::identify() const { return d_name; }
2200
2201
4318781
void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag)
2202
{
2203
4318781
  Debug("equality::trigger") << d_name << "::eq::addTriggerTerm(" << t << ", " << tag << ")" << std::endl;
2204
2205
4318781
  Assert(tag != THEORY_LAST);
2206
2207
4318781
  if (d_done) {
2208
    return;
2209
  }
2210
2211
  // Add the term if it's not already there
2212
4318781
  addTermInternal(t);
2213
2214
4318781
  if (!d_anyTermsAreTriggers)
2215
  {
2216
    // if we are not using triggers, we only add the term, but not as a trigger
2217
    return;
2218
  }
2219
2220
  // Get the node id
2221
4318781
  EqualityNodeId eqNodeId = getNodeId(t);
2222
4318781
  EqualityNode& eqNode = getEqualityNode(eqNodeId);
2223
4318781
  EqualityNodeId classId = eqNode.getFind();
2224
2225
  // Possibly existing set of triggers
2226
4318781
  TriggerTermSetRef triggerSetRef = d_nodeIndividualTrigger[classId];
2227
4318781
  if (triggerSetRef != +null_set_id && getTriggerTermSet(triggerSetRef).hasTrigger(tag)) {
2228
    // If the term already is in the equivalence class that a tagged representative, just notify
2229
1224410
    if (d_performNotify) {
2230
1224410
      EqualityNodeId triggerId = getTriggerTermSet(triggerSetRef).getTrigger(tag);
2231
1224410
      Debug("equality::trigger") << d_name << "::eq::addTriggerTerm(" << t << ", " << tag << "): already have this trigger in class with " << d_nodes[triggerId] << std::endl;
2232
1224410
      if (eqNodeId != triggerId && !d_notify.eqNotifyTriggerTermEquality(tag, t, d_nodes[triggerId], true)) {
2233
527
        d_done = true;
2234
      }
2235
    }
2236
  } else {
2237
2238
    // Check for disequalities by going through the equivalence class looking for equalities in the
2239
    // uselists that have been asserted to false. All the representatives appearing on the other
2240
    // side of such disequalities, that have the tag on, are put in a set.
2241
6188742
    TaggedEqualitiesSet disequalitiesToNotify;
2242
3094371
    TheoryIdSet tags = TheoryIdSetUtil::setInsert(tag);
2243
3094371
    getDisequalities(!d_isConstant[classId], classId, tags, disequalitiesToNotify);
2244
2245
    // Trigger data
2246
    TheoryIdSet newSetTags;
2247
    EqualityNodeId newSetTriggers[THEORY_LAST];
2248
    unsigned newSetTriggersSize;
2249
2250
    // Setup the data for the new set
2251
3094371
    if (triggerSetRef != null_set_id) {
2252
      // Get the existing set
2253
703311
      TriggerTermSet& triggerSet = getTriggerTermSet(triggerSetRef);
2254
      // Initialize the new set for copy/insert
2255
703311
      newSetTags = TheoryIdSetUtil::setInsert(tag, triggerSet.d_tags);
2256
703311
      newSetTriggersSize = 0;
2257
      // Copy into to new one, and insert the new tag/id
2258
703311
      unsigned i = 0;
2259
703311
      TheoryIdSet tags2 = newSetTags;
2260
      TheoryId current;
2261
3564029
      while ((current = TheoryIdSetUtil::setPop(tags2)) != THEORY_LAST)
2262
      {
2263
        // Remove from the tags
2264
1430359
        tags2 = TheoryIdSetUtil::setRemove(current, tags2);
2265
        // Insert the id into the triggers
2266
1430359
        newSetTriggers[newSetTriggersSize++] =
2267
1430359
            current == tag ? eqNodeId : triggerSet.d_triggers[i++];
2268
      }
2269
    } else {
2270
      // Setup a singleton
2271
2391060
      newSetTags = TheoryIdSetUtil::setInsert(tag);
2272
2391060
      newSetTriggers[0] = eqNodeId;
2273
2391060
      newSetTriggersSize = 1;
2274
    }
2275
2276
    // Add it to the list for backtracking
2277
3094371
    d_triggerTermSetUpdates.push_back(TriggerSetUpdate(classId, triggerSetRef));
2278
3094371
    d_triggerTermSetUpdatesSize = d_triggerTermSetUpdatesSize + 1;
2279
    // Mark the the new set as a trigger
2280
3094371
    d_nodeIndividualTrigger[classId] = triggerSetRef = newTriggerTermSet(newSetTags, newSetTriggers, newSetTriggersSize);
2281
2282
    // Propagate trigger term disequalities we remembered
2283
3094371
    Debug("equality::trigger") << d_name << "::eq::addTriggerTerm(" << t << ", " << tag << "): propagating " << disequalitiesToNotify.size() << " disequalities " << std::endl;
2284
3094371
    propagateTriggerTermDisequalities(tags, triggerSetRef, disequalitiesToNotify);
2285
  }
2286
}
2287
2288
8612965
bool EqualityEngine::isTriggerTerm(TNode t, TheoryId tag) const {
2289
8612965
  if (!hasTerm(t)) return false;
2290
8612965
  EqualityNodeId classId = getEqualityNode(t).getFind();
2291
8612965
  TriggerTermSetRef triggerSetRef = d_nodeIndividualTrigger[classId];
2292
8612965
  return triggerSetRef != +null_set_id && getTriggerTermSet(triggerSetRef).hasTrigger(tag);
2293
}
2294
2295
2296
3256464
TNode EqualityEngine::getTriggerTermRepresentative(TNode t, TheoryId tag) const {
2297
3256464
  Assert(isTriggerTerm(t, tag));
2298
3256464
  EqualityNodeId classId = getEqualityNode(t).getFind();
2299
3256464
  const TriggerTermSet& triggerSet = getTriggerTermSet(d_nodeIndividualTrigger[classId]);
2300
3256464
  unsigned i = 0;
2301
3256464
  TheoryIdSet tags = triggerSet.d_tags;
2302
8238206
  while (TheoryIdSetUtil::setPop(tags) != tag)
2303
  {
2304
2490871
    ++ i;
2305
  }
2306
3256464
  return d_nodes[triggerSet.d_triggers[i]];
2307
}
2308
2309
14335649
void EqualityEngine::storeApplicationLookup(FunctionApplication& funNormalized, EqualityNodeId funId) {
2310
14335649
  Assert(d_applicationLookup.find(funNormalized) == d_applicationLookup.end());
2311
14335649
  d_applicationLookup[funNormalized] = funId;
2312
14335649
  d_applicationLookups.push_back(funNormalized);
2313
14335649
  d_applicationLookupsCount = d_applicationLookupsCount + 1;
2314
14335649
  Debug("equality::backtrack") << "d_applicationLookupsCount = " << d_applicationLookupsCount << std::endl;
2315
14335649
  Debug("equality::backtrack") << "d_applicationLookups.size() = " << d_applicationLookups.size() << std::endl;
2316
14335649
  Assert(d_applicationLookupsCount == d_applicationLookups.size());
2317
2318
  // If an equality over constants we merge to false
2319
14335649
  if (funNormalized.isEquality()) {
2320
10100593
    if (funNormalized.d_a == funNormalized.d_b)
2321
    {
2322
910652
      enqueue(MergeCandidate(funId, d_trueId, MERGED_THROUGH_REFLEXIVITY, TNode::null()));
2323
    }
2324
9189941
    else if (d_isConstant[funNormalized.d_a] && d_isConstant[funNormalized.d_b])
2325
    {
2326
1221200
      enqueue(MergeCandidate(funId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null()));
2327
    }
2328
  }
2329
14335649
}
2330
2331
void EqualityEngine::getUseListTerms(TNode t, std::set<TNode>& output) {
2332
  if (hasTerm(t)) {
2333
    // Get the equivalence class
2334
    EqualityNodeId classId = getEqualityNode(t).getFind();
2335
    // Go through the equivalence class and get where t is used in
2336
    EqualityNodeId currentId = classId;
2337
    do {
2338
      // Get the current node
2339
      EqualityNode& currentNode = getEqualityNode(currentId);
2340
      // Go through the use-list
2341
      UseListNodeId currentUseId = currentNode.getUseList();
2342
      while (currentUseId != null_uselist_id) {
2343
        // Get the node of the use list
2344
        UseListNode& useNode = d_useListNodes[currentUseId];
2345
        // Get the function application
2346
        EqualityNodeId funId = useNode.getApplicationId();
2347
        output.insert(d_nodes[funId]);
2348
        // Go to the next one in the use list
2349
        currentUseId = useNode.getNext();
2350
      }
2351
      // Move to the next node
2352
      currentId = currentNode.getNext();
2353
    } while (currentId != classId);
2354
  }
2355
}
2356
2357
5617034
EqualityEngine::TriggerTermSetRef EqualityEngine::newTriggerTermSet(
2358
    TheoryIdSet newSetTags,
2359
    EqualityNodeId* newSetTriggers,
2360
    unsigned newSetTriggersSize)
2361
{
2362
  // Size of the required set
2363
5617034
  size_t size = sizeof(TriggerTermSet) + newSetTriggersSize*sizeof(EqualityNodeId);
2364
  // Align the size
2365
5617034
  size = (size + 7) & ~((size_t)7);
2366
  // Reallocate if necessary
2367
5617034
  if (d_triggerDatabaseSize + size > d_triggerDatabaseAllocatedSize) {
2368
    d_triggerDatabaseAllocatedSize *= 2;
2369
    d_triggerDatabase = (char*) realloc(d_triggerDatabase, d_triggerDatabaseAllocatedSize);
2370
  }
2371
  // New reference
2372
5617034
  TriggerTermSetRef newTriggerSetRef = d_triggerDatabaseSize;
2373
  // Update the size
2374
5617034
  d_triggerDatabaseSize = d_triggerDatabaseSize + size;
2375
  // Copy the information
2376
5617034
  TriggerTermSet& newSet = getTriggerTermSet(newTriggerSetRef);
2377
5617034
  newSet.d_tags = newSetTags;
2378
42175242
  for (unsigned i = 0; i < newSetTriggersSize; ++i) {
2379
36558208
    newSet.d_triggers[i] = newSetTriggers[i];
2380
  }
2381
  // Return the new reference
2382
5617034
  return newTriggerSetRef;
2383
}
2384
2385
22909210
bool EqualityEngine::hasPropagatedDisequality(EqualityNodeId lhsId, EqualityNodeId rhsId) const {
2386
22909210
  EqualityPair eq(lhsId, rhsId);
2387
22909210
  bool propagated = d_propagatedDisequalities.find(eq) != d_propagatedDisequalities.end();
2388
#ifdef CVC4_ASSERTIONS
2389
22909210
  bool stored = d_disequalityReasonsMap.find(eq) != d_disequalityReasonsMap.end();
2390
22909210
  Assert(propagated == stored) << "These two should be in sync";
2391
#endif
2392
22909210
  Debug("equality::disequality") << d_name << "::eq::hasPropagatedDisequality(" << d_nodes[lhsId] << ", " << d_nodes[rhsId] << ") => " << (propagated ? "true" : "false") << std::endl;
2393
22909210
  return propagated;
2394
}
2395
2396
18556429
bool EqualityEngine::hasPropagatedDisequality(TheoryId tag, EqualityNodeId lhsId, EqualityNodeId rhsId) const {
2397
2398
18556429
  EqualityPair eq(lhsId, rhsId);
2399
2400
18556429
  PropagatedDisequalitiesMap::const_iterator it = d_propagatedDisequalities.find(eq);
2401
18556429
  if (it == d_propagatedDisequalities.end()) {
2402
14730606
    Assert(d_disequalityReasonsMap.find(eq) == d_disequalityReasonsMap.end())
2403
        << "Why do we have a proof if not propagated";
2404
14730606
    Debug("equality::disequality") << d_name << "::eq::hasPropagatedDisequality(" << tag << ", " << d_nodes[lhsId] << ", " << d_nodes[rhsId] << ") => false" << std::endl;
2405
14730606
    return false;
2406
  }
2407
3825823
  Assert(d_disequalityReasonsMap.find(eq) != d_disequalityReasonsMap.end())
2408
      << "We propagated but there is no proof";
2409
3825823
  bool result = TheoryIdSetUtil::setContains(tag, (*it).second);
2410
3825823
  Debug("equality::disequality") << d_name << "::eq::hasPropagatedDisequality(" << tag << ", " << d_nodes[lhsId] << ", " << d_nodes[rhsId] << ") => " << (result ? "true" : "false") << std::endl;
2411
3825823
  return result;
2412
}
2413
2414
2415
8545854
void EqualityEngine::storePropagatedDisequality(TheoryId tag, EqualityNodeId lhsId, EqualityNodeId rhsId) {
2416
8545854
  Assert(!hasPropagatedDisequality(tag, lhsId, rhsId))
2417
      << "Check before you store it";
2418
8545854
  Assert(lhsId != rhsId) << "Wow, wtf!";
2419
2420
8545854
  Debug("equality::disequality") << d_name << "::eq::storePropagatedDisequality(" << tag << ", " << d_nodes[lhsId] << ", " << d_nodes[rhsId] << ")" << std::endl;
2421
2422
8545854
  EqualityPair pair1(lhsId, rhsId);
2423
8545854
  EqualityPair pair2(rhsId, lhsId);
2424
2425
  // Store the fact that we've propagated this already
2426
8545854
  TheoryIdSet notified = 0;
2427
8545854
  PropagatedDisequalitiesMap::const_iterator find = d_propagatedDisequalities.find(pair1);
2428
8545854
  if (find == d_propagatedDisequalities.end()) {
2429
7371129
    notified = TheoryIdSetUtil::setInsert(tag);
2430
  } else {
2431
1174725
    notified = TheoryIdSetUtil::setInsert(tag, (*find).second);
2432
  }
2433
8545854
  d_propagatedDisequalities[pair1] = notified;
2434
8545854
  d_propagatedDisequalities[pair2] = notified;
2435
2436
  // Store the proof if provided
2437
8545854
  if (d_deducedDisequalityReasons.size() > d_deducedDisequalityReasonsSize) {
2438
7371129
    Debug("equality::disequality") << d_name << "::eq::storePropagatedDisequality(" << tag << ", " << d_nodes[lhsId] << ", " << d_nodes[rhsId] << "): storing proof" << std::endl;
2439
7371129
    Assert(d_disequalityReasonsMap.find(pair1) == d_disequalityReasonsMap.end())
2440
        << "There can't be a proof if you're adding a new one";
2441
7371129
    DisequalityReasonRef ref(d_deducedDisequalityReasonsSize, d_deducedDisequalityReasons.size());
2442
#ifdef CVC4_ASSERTIONS
2443
    // Check that the reasons are valid
2444
16758803
    for (unsigned i = ref.d_mergesStart; i < ref.d_mergesEnd; ++i)
2445
    {
2446
9387674
      Assert(
2447
          getEqualityNode(d_deducedDisequalityReasons[i].first).getFind()
2448
          == getEqualityNode(d_deducedDisequalityReasons[i].second).getFind());
2449
    }
2450
#endif
2451
7371129
    if (Debug.isOn("equality::disequality")) {
2452
      for (unsigned i = ref.d_mergesStart; i < ref.d_mergesEnd; ++i)
2453
      {
2454
        TNode lhs = d_nodes[d_deducedDisequalityReasons[i].first];
2455
        TNode rhs = d_nodes[d_deducedDisequalityReasons[i].second];
2456
        Debug("equality::disequality") << d_name << "::eq::storePropagatedDisequality(): because " << lhs << " == " << rhs << std::endl;
2457
      }
2458
    }
2459
2460
    // Store for backtracking
2461
7371129
    d_deducedDisequalities.push_back(pair1);
2462
7371129
    d_deducedDisequalitiesSize = d_deducedDisequalities.size();
2463
7371129
    d_deducedDisequalityReasonsSize = d_deducedDisequalityReasons.size();
2464
    // Store the proof reference
2465
7371129
    d_disequalityReasonsMap[pair1] = ref;
2466
7371129
    d_disequalityReasonsMap[pair2] = ref;
2467
  } else {
2468
1174725
    Assert(d_disequalityReasonsMap.find(pair1) != d_disequalityReasonsMap.end())
2469
        << "You must provide a proof initially";
2470
  }
2471
8545854
}
2472
2473
54694635
void EqualityEngine::getDisequalities(bool allowConstants,
2474
                                      EqualityNodeId classId,
2475
                                      TheoryIdSet inputTags,
2476
                                      TaggedEqualitiesSet& out)
2477
{
2478
  // Must be empty on input
2479
54694635
  Assert(out.size() == 0);
2480
  // The class we are looking for, shouldn't have any of the tags we are looking for already set
2481
54694635
  Assert(d_nodeIndividualTrigger[classId] == null_set_id
2482
         || TheoryIdSetUtil::setIntersection(
2483
                getTriggerTermSet(d_nodeIndividualTrigger[classId]).d_tags,
2484
                inputTags)
2485
                == 0);
2486
2487
54694635
  if (inputTags == 0) {
2488
73540796
    return;
2489
  }
2490
2491
  // Set of already (through disequalities) visited equivalence classes
2492
35848474
  std::set<EqualityNodeId> alreadyVisited;
2493
2494
  // Go through the equivalence class
2495
17924237
  EqualityNodeId currentId = classId;
2496
3116759
  do {
2497
2498
21040996
    Debug("equality::trigger") << d_name << "::getDisequalities() : going through uselist of " << d_nodes[currentId] << std::endl;
2499
2500
    // Current node in the equivalence class
2501
21040996
    EqualityNode& currentNode = getEqualityNode(currentId);
2502
2503
    // Go through the uselist and look for disequalities
2504
21040996
    UseListNodeId currentUseId = currentNode.getUseList();
2505
60016424
    while (currentUseId != null_uselist_id) {
2506
19487714
      UseListNode& useListNode = d_useListNodes[currentUseId];
2507
19487714
      EqualityNodeId funId = useListNode.getApplicationId();
2508
2509
19487714
      Debug("equality::trigger") << d_name << "::getDisequalities() : checking " << d_nodes[funId] << std::endl;
2510
2511
      const FunctionApplication& fun =
2512
19487714
          d_applications[useListNode.getApplicationId()].d_original;
2513
      // If it's an equality asserted to false, we do the work
2514
19487714
      if (fun.isEquality() && getEqualityNode(funId).getFind() == getEqualityNode(d_false).getFind()) {
2515
        // Get the other equality member
2516
3318881
        bool lhs = false;
2517
3318881
        EqualityNodeId toCompare = fun.d_b;
2518
3318881
        if (toCompare == currentId) {
2519
1823642
          toCompare = fun.d_a;
2520
1823642
          lhs = true;
2521
        }
2522
        // Representative of the other member
2523
3318881
        EqualityNodeId toCompareRep = getEqualityNode(toCompare).getFind();
2524
3318881
        if (toCompareRep == classId) {
2525
          // We're in conflict, so we will send it out from merge
2526
          out.clear();
2527
          return;
2528
        }
2529
        // Check if we already have this one
2530
3318881
        if (alreadyVisited.count(toCompareRep) == 0) {
2531
          // Mark as visited
2532
2740580
          alreadyVisited.insert(toCompareRep);
2533
          // Get the trigger set
2534
2740580
          TriggerTermSetRef toCompareTriggerSetRef = d_nodeIndividualTrigger[toCompareRep];
2535
          // We only care if we're not both constants and there are trigger terms in the other class
2536
2740580
          if ((allowConstants || !d_isConstant[toCompareRep]) && toCompareTriggerSetRef != null_set_id) {
2537
            // Tags of the other gey
2538
1296250
            TriggerTermSet& toCompareTriggerSet = getTriggerTermSet(toCompareTriggerSetRef);
2539
            // We only care if there are things in inputTags that is also in toCompareTags
2540
1296250
            TheoryIdSet commonTags = TheoryIdSetUtil::setIntersection(
2541
1296250
                inputTags, toCompareTriggerSet.d_tags);
2542
1296250
            if (commonTags) {
2543
857876
              out.push_back(TaggedEquality(funId, toCompareTriggerSetRef, lhs));
2544
            }
2545
          }
2546
        }
2547
      }
2548
      // Go to the next one in the use list
2549
19487714
      currentUseId = useListNode.getNext();
2550
    }
2551
    // Next in equivalence class
2552
21040996
    currentId = currentNode.getNext();
2553
21040996
  } while (!d_done && currentId != classId);
2554
2555
}
2556
2557
54694629
bool EqualityEngine::propagateTriggerTermDisequalities(
2558
    TheoryIdSet tags,
2559
    TriggerTermSetRef triggerSetRef,
2560
    const TaggedEqualitiesSet& disequalitiesToNotify)
2561
{
2562
  // No tags, no food
2563
54694629
  if (!tags) {
2564
36770393
    return !d_done;
2565
  }
2566
2567
17924236
  Assert(triggerSetRef != null_set_id);
2568
2569
  // This is the class trigger set
2570
17924236
  const TriggerTermSet& triggerSet = getTriggerTermSet(triggerSetRef);
2571
  // Go through the disequalities and notify
2572
17924236
  TaggedEqualitiesSet::const_iterator it = disequalitiesToNotify.begin();
2573
17924236
  TaggedEqualitiesSet::const_iterator it_end = disequalitiesToNotify.end();
2574
19569380
  for (; !d_done && it != it_end; ++ it) {
2575
    // The information about the equality that is asserted to false
2576
832125
    const TaggedEquality& disequalityInfo = *it;
2577
    const TriggerTermSet& disequalityTriggerSet =
2578
832125
        getTriggerTermSet(disequalityInfo.d_triggerSetRef);
2579
    TheoryIdSet commonTags =
2580
832125
        TheoryIdSetUtil::setIntersection(disequalityTriggerSet.d_tags, tags);
2581
832125
    Assert(commonTags);
2582
    // This is the actual function
2583
    const FunctionApplication& fun =
2584
832125
        d_applications[disequalityInfo.d_equalityId].d_original;
2585
    // Figure out who we are comparing to in the original equality
2586
832125
    EqualityNodeId toCompare = disequalityInfo.d_lhs ? fun.d_a : fun.d_b;
2587
832125
    EqualityNodeId myCompare = disequalityInfo.d_lhs ? fun.d_b : fun.d_a;
2588
832125
    if (getEqualityNode(toCompare).getFind() == getEqualityNode(myCompare).getFind()) {
2589
      // We're propagating a != a, which means we're inconsistent, just bail and let it go into
2590
      // a regular conflict
2591
9553
      return !d_done;
2592
    }
2593
    // Go through the tags, and add the disequalities
2594
    TheoryId currentTag;
2595
1213536
    while (
2596
2036108
        !d_done
2597
2036108
        && ((currentTag = TheoryIdSetUtil::setPop(commonTags)) != THEORY_LAST))
2598
    {
2599
      // Get the tag representative
2600
1213536
      EqualityNodeId tagRep = disequalityTriggerSet.getTrigger(currentTag);
2601
1213536
      EqualityNodeId myRep = triggerSet.getTrigger(currentTag);
2602
      // Propagate
2603
1213536
      if (!hasPropagatedDisequality(currentTag, myRep, tagRep)) {
2604
        // Construct the proof if not there already
2605
74522
        if (!hasPropagatedDisequality(myRep, tagRep)) {
2606
28335
          d_deducedDisequalityReasons.push_back(EqualityPair(myCompare, myRep));
2607
28335
          d_deducedDisequalityReasons.push_back(EqualityPair(toCompare, tagRep));
2608
56670
          d_deducedDisequalityReasons.push_back(
2609
56670
              EqualityPair(disequalityInfo.d_equalityId, d_falseId));
2610
        }
2611
        // Store the propagation
2612
74522
        storePropagatedDisequality(currentTag, myRep, tagRep);
2613
        // Notify
2614
74522
        if (d_performNotify) {
2615
74522
          if (!d_notify.eqNotifyTriggerTermEquality(currentTag, d_nodes[myRep], d_nodes[tagRep], false)) {
2616
10
            d_done = true;
2617
          }
2618
        }
2619
      }
2620
    }
2621
  }
2622
2623
17914683
  return !d_done;
2624
}
2625
2626
9939566
TheoryIdSet EqualityEngine::TriggerTermSet::hasTrigger(TheoryId tag) const
2627
{
2628
9939566
  return TheoryIdSetUtil::setContains(tag, d_tags);
2629
}
2630
2631
3651482
EqualityNodeId EqualityEngine::TriggerTermSet::getTrigger(TheoryId tag) const
2632
{
2633
3651482
  return d_triggers[TheoryIdSetUtil::setIndex(tag, d_tags)];
2634
}
2635
2636
} // Namespace uf
2637
} // Namespace theory
2638
26676
} // Namespace CVC4