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