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 : 452171 : EqualityEngine::Statistics::Statistics(StatisticsRegistry& sr,
29 : 452171 : const std::string& name)
30 : 452171 : : d_mergesCount(sr.registerInt(name + "mergesCount")),
31 : 452171 : d_termsCount(sr.registerInt(name + "termsCount")),
32 : 452171 : d_functionTermsCount(sr.registerInt(name + "functionTermsCount")),
33 : 452171 : d_constantTermsCount(sr.registerInt(name + "constantTermsCount"))
34 : : {
35 : 452171 : }
36 : :
37 : : /**
38 : : * Data used in the BFS search through the equality graph.
39 : : */
40 : : struct BfsData
41 : : {
42 : : // The current node
43 : : EqualityNodeId d_nodeId;
44 : : // The index of the edge we traversed
45 : : EqualityEdgeId d_edgeId;
46 : : // Index in the queue of the previous node. Shouldn't be too much of them, at
47 : : // most the size of the biggest equivalence class
48 : : size_t d_previousIndex;
49 : :
50 : 39419962 : BfsData(EqualityNodeId nodeId = null_id,
51 : : EqualityEdgeId edgeId = null_edge,
52 : : size_t prev = 0)
53 : 39419962 : : d_nodeId(nodeId), d_edgeId(edgeId), d_previousIndex(prev)
54 : : {
55 : 39419962 : }
56 : : };
57 : :
58 : : class ScopedBool
59 : : {
60 : : bool& d_watch;
61 : : bool d_oldValue;
62 : :
63 : : public:
64 : 56732800 : ScopedBool(bool& watch, bool newValue) : d_watch(watch), d_oldValue(watch)
65 : : {
66 : 56732800 : d_watch = newValue;
67 : 56732800 : }
68 : 56732800 : ~ScopedBool() { d_watch = d_oldValue; }
69 : : };
70 : :
71 : : EqualityEngineNotifyNone EqualityEngine::s_notifyNone;
72 : :
73 : 452171 : void EqualityEngine::init()
74 : : {
75 [ + - ]: 904342 : Trace("equality") << "EqualityEdge::EqualityEngine(): id_null = " << +null_id
76 : 452171 : << std::endl;
77 [ + - ]: 904342 : Trace("equality") << "EqualityEdge::EqualityEngine(): edge_null = "
78 : 452171 : << +null_edge << std::endl;
79 [ + - ]: 904342 : Trace("equality") << "EqualityEdge::EqualityEngine(): trigger_null = "
80 : 452171 : << +null_trigger << std::endl;
81 : :
82 : : // Note that we previously checked whether the context level was zero here,
83 : : // to ensure that true/false could never be removed. However, this assertion
84 : : // restricts our ability to construct equality engines in nested contexts.
85 : :
86 : 452171 : d_true = nodeManager()->mkConst<bool>(true);
87 : 452171 : d_false = nodeManager()->mkConst<bool>(false);
88 : :
89 : 452171 : d_triggerDatabaseAllocatedSize = 100000;
90 : 452171 : d_triggerDatabase = (char*)malloc(d_triggerDatabaseAllocatedSize);
91 : :
92 : 452171 : addTermInternal(d_true);
93 : 452171 : addTermInternal(d_false);
94 : :
95 : 452171 : d_trueId = getNodeId(d_true);
96 : 452171 : d_falseId = getNodeId(d_false);
97 : 452171 : }
98 : :
99 : 846394 : EqualityEngine::~EqualityEngine() { free(d_triggerDatabase); }
100 : :
101 : 86130 : EqualityEngine::EqualityEngine(Env& env,
102 : : context::Context* c,
103 : : std::string name,
104 : : bool constantsAreTriggers,
105 : 86130 : bool anyTermTriggers)
106 : : : ContextNotifyObj(c),
107 : : EnvObj(env),
108 : 86130 : d_masterEqualityEngine(nullptr),
109 : 86130 : d_context(c),
110 : 0 : d_done(c, false),
111 : 86130 : d_notify(&s_notifyNone),
112 : 86130 : d_applicationLookupsCount(c, 0),
113 : 86130 : d_nodesCount(c, 0),
114 : 86130 : d_assertedEqualitiesCount(c, 0),
115 : 86130 : d_equalityTriggersCount(c, 0),
116 : 86130 : d_subtermEvaluatesSize(c, 0),
117 : 86130 : d_stats(statisticsRegistry(), name + "::"),
118 : 86130 : d_inPropagate(false),
119 : 86130 : d_constantsAreTriggers(constantsAreTriggers),
120 : 86130 : d_anyTermsAreTriggers(anyTermTriggers),
121 : 86130 : d_triggerDatabaseSize(c, 0),
122 : 86130 : d_triggerTermSetUpdatesSize(c, 0),
123 : 86130 : d_deducedDisequalitiesSize(c, 0),
124 : 86130 : d_deducedDisequalityReasonsSize(c, 0),
125 : 86130 : d_propagatedDisequalities(c),
126 : 947430 : d_name(name)
127 : : {
128 : 86130 : init();
129 : 86130 : }
130 : :
131 : 366041 : EqualityEngine::EqualityEngine(Env& env,
132 : : context::Context* c,
133 : : EqualityEngineNotify& notify,
134 : : std::string name,
135 : : bool constantsAreTriggers,
136 : 366041 : bool anyTermTriggers)
137 : : : ContextNotifyObj(c),
138 : : EnvObj(env),
139 : 366041 : d_masterEqualityEngine(nullptr),
140 : 366041 : d_proofEqualityEngine(nullptr),
141 : 366041 : d_context(c),
142 : 0 : d_done(c, false),
143 : 366041 : d_notify(&s_notifyNone),
144 : 366041 : d_applicationLookupsCount(c, 0),
145 : 366041 : d_nodesCount(c, 0),
146 : 366041 : d_assertedEqualitiesCount(c, 0),
147 : 366041 : d_equalityTriggersCount(c, 0),
148 : 366041 : d_subtermEvaluatesSize(c, 0),
149 : 366041 : d_stats(statisticsRegistry(), name + "::"),
150 : 366041 : d_inPropagate(false),
151 : 366041 : d_constantsAreTriggers(constantsAreTriggers),
152 : 366041 : d_anyTermsAreTriggers(anyTermTriggers),
153 : 366041 : d_triggerDatabaseSize(c, 0),
154 : 366041 : d_triggerTermSetUpdatesSize(c, 0),
155 : 366041 : d_deducedDisequalitiesSize(c, 0),
156 : 366041 : d_deducedDisequalityReasonsSize(c, 0),
157 : 366041 : d_propagatedDisequalities(c),
158 : 4026451 : d_name(name)
159 : : {
160 : 366041 : init();
161 : : // since init makes notifications (e.g. new eq class for true/false), and
162 : : // since the notify class may not be fully constructed yet, we
163 : : // don't set up the provided notification class until after initialization.
164 : 366041 : d_notify = ¬ify;
165 : 366041 : }
166 : :
167 : 244682 : void EqualityEngine::setMasterEqualityEngine(EqualityEngine* master)
168 : : {
169 [ - + ][ - + ]: 244682 : Assert(d_masterEqualityEngine == nullptr);
[ - - ]
170 : 244682 : d_masterEqualityEngine = master;
171 : 244682 : }
172 : :
173 : 110016 : void EqualityEngine::setProofEqualityEngine(ProofEqEngine* pfee)
174 : : {
175 [ - + ][ - + ]: 110016 : Assert(d_proofEqualityEngine == nullptr);
[ - - ]
176 : 110016 : d_proofEqualityEngine = pfee;
177 : 110016 : }
178 : 138921 : ProofEqEngine* EqualityEngine::getProofEqualityEngine()
179 : : {
180 : 138921 : return d_proofEqualityEngine;
181 : : }
182 : :
183 : 82558323 : void EqualityEngine::enqueue(const MergeCandidate& candidate, bool back)
184 : : {
185 [ + - ]: 165116646 : Trace("equality") << d_name << "::eq::enqueue({" << candidate.d_t1Id << "} "
186 : 0 : << d_nodes[candidate.d_t1Id] << ", {" << candidate.d_t2Id
187 : 0 : << "} " << d_nodes[candidate.d_t2Id] << ", "
188 : 82558323 : << static_cast<MergeReasonType>(candidate.d_type)
189 : 82558323 : << "). reason: " << candidate.d_reason << std::endl;
190 [ + - ]: 82558323 : if (back)
191 : : {
192 : 82558323 : d_propagationQueue.push_back(candidate);
193 : : }
194 : : else
195 : : {
196 : 0 : d_propagationQueue.push_front(candidate);
197 : : }
198 : 82558323 : }
199 : :
200 : 6404595 : EqualityNodeId EqualityEngine::newApplicationNode(TNode original,
201 : : EqualityNodeId t1,
202 : : EqualityNodeId t2,
203 : : FunctionApplicationType type)
204 : : {
205 [ + - ]: 12809190 : Trace("equality") << d_name << "::eq::newApplicationNode(" << original
206 : 0 : << ", {" << t1 << "} " << d_nodes[t1] << ", {" << t2 << "} "
207 : 6404595 : << d_nodes[t2] << ")" << std::endl;
208 : :
209 : 6404595 : ++d_stats.d_functionTermsCount;
210 : :
211 : : // Get another id for this
212 : 6404595 : EqualityNodeId funId = newNode(original);
213 : 6404595 : FunctionApplication funOriginal(type, t1, t2);
214 : : // The function application we're creating
215 : 6404595 : EqualityNodeId t1ClassId = getEqualityNode(t1).getFind();
216 : 6404595 : EqualityNodeId t2ClassId = getEqualityNode(t2).getFind();
217 : 6404595 : FunctionApplication funNormalized(type, t1ClassId, t2ClassId);
218 : :
219 [ + - ]: 12809190 : Trace("equality") << d_name << "::eq::newApplicationNode: funOriginal: ("
220 : 0 : << type << " " << d_nodes[t1] << " " << d_nodes[t2]
221 : 0 : << "), funNorm: (" << type << " " << d_nodes[t1ClassId]
222 : 6404595 : << " " << d_nodes[t2ClassId] << ")\n";
223 : :
224 : : // We add the original version
225 : 6404595 : d_applications[funId] = FunctionApplicationPair(funOriginal, funNormalized);
226 : :
227 : : // Add the lookup data, if it's not already there
228 : 6404595 : ApplicationIdsMap::iterator find = d_applicationLookup.find(funNormalized);
229 [ + + ]: 6404595 : if (find == d_applicationLookup.end())
230 : : {
231 [ + - ]: 11332596 : Trace("equality") << d_name << "::eq::newApplicationNode(" << original
232 : 0 : << ", " << t1 << ", " << t2
233 : 0 : << "): no lookup, setting up funNorm: (" << type << " "
234 : 0 : << d_nodes[t1ClassId] << " " << d_nodes[t2ClassId]
235 : 5666298 : << ") => " << funId << std::endl;
236 : : // Mark the normalization to the lookup
237 : 5666298 : storeApplicationLookup(funNormalized, funId);
238 : : }
239 : : else
240 : : {
241 : : // If it's there, we need to merge these two
242 [ + - ]: 1476594 : Trace("equality") << d_name << "::eq::newApplicationNode(" << original
243 : 0 : << ", " << t1 << ", " << t2
244 : 738297 : << "): lookup exists, adding to queue" << std::endl;
245 [ + - ]: 1476594 : Trace("equality") << d_name << "::eq::newApplicationNode(" << original
246 : 0 : << ", " << t1 << ", " << t2
247 : 738297 : << "): lookup = " << d_nodes[find->second] << std::endl;
248 : 738297 : enqueue(MergeCandidate(
249 : 1476594 : funId, find->second, MERGED_THROUGH_CONGRUENCE, TNode::null()));
250 : : }
251 : :
252 : : // Add to the use lists
253 [ + - ]: 12809190 : Trace("equality") << d_name << "::eq::newApplicationNode(" << original << ", "
254 : 0 : << t1 << ", " << t2 << "): adding " << original
255 : 6404595 : << " to the uselist of " << d_nodes[t1] << std::endl;
256 : 6404595 : d_equalityNodes[t1].usedIn(funId, d_useListNodes);
257 [ + - ]: 12809190 : Trace("equality") << d_name << "::eq::newApplicationNode(" << original << ", "
258 : 0 : << t1 << ", " << t2 << "): adding " << original
259 : 6404595 : << " to the uselist of " << d_nodes[t2] << std::endl;
260 : 6404595 : d_equalityNodes[t2].usedIn(funId, d_useListNodes);
261 : :
262 : : // Return the new id
263 [ + - ]: 12809190 : Trace("equality") << d_name << "::eq::newApplicationNode(" << original << ", "
264 : 6404595 : << t1 << ", " << t2 << ") => " << funId << std::endl;
265 : :
266 : 6404595 : return funId;
267 : : }
268 : :
269 : 16565033 : EqualityNodeId EqualityEngine::newNode(TNode node)
270 : : {
271 [ + - ]: 16565033 : Trace("equality") << d_name << "::eq::newNode(" << node << ")" << std::endl;
272 : :
273 : 16565033 : ++d_stats.d_termsCount;
274 : :
275 : : // Register the new id of the term
276 : 16565033 : EqualityNodeId newId = d_nodes.size();
277 : 16565033 : d_nodeIds[node] = newId;
278 : : // Add the node to it's position
279 : 16565033 : d_nodes.push_back(node);
280 : : // Note if this is an application or not
281 : 16565033 : d_applications.push_back(FunctionApplicationPair());
282 : : // Add the trigger list for this node
283 : 16565033 : d_nodeTriggers.push_back(+null_trigger);
284 : : // Add it to the equality graph
285 : 16565033 : d_equalityGraph.push_back(+null_edge);
286 : : // Mark the no-individual trigger
287 : 16565033 : d_nodeIndividualTrigger.push_back(+null_set_id);
288 : : // Mark non-constant by default
289 : 16565033 : d_isConstant.push_back(false);
290 : : // No terms to evaluate by defaul
291 : 16565033 : d_subtermsToEvaluate.push_back(0);
292 : : // Mark equality nodes
293 : 16565033 : d_isEquality.push_back(false);
294 : : // Mark the node as internal by default
295 : 16565033 : d_isInternal.push_back(true);
296 : : // Add the equality node to the nodes
297 : 16565033 : d_equalityNodes.push_back(EqualityNode(newId));
298 : :
299 : : // Increase the counters
300 : 16565033 : d_nodesCount = d_nodesCount + 1;
301 : :
302 [ + - ]: 33130066 : Trace("equality") << d_name << "::eq::newNode(" << node << ") => " << newId
303 : 16565033 : << std::endl;
304 : :
305 : 16565033 : return newId;
306 : : }
307 : :
308 : 3220060 : void EqualityEngine::addFunctionKind(Kind fun,
309 : : bool interpreted,
310 : : bool extOperator)
311 : : {
312 : 3220060 : d_congruenceKinds.set(fun);
313 [ + - ]: 3220060 : if (fun != Kind::EQUAL)
314 : : {
315 [ + + ]: 3220060 : if (interpreted)
316 : : {
317 [ + - ]: 1319978 : Trace("equality::evaluation")
318 : 0 : << d_name << "::eq::addFunctionKind(): " << fun << " is interpreted "
319 : 659989 : << std::endl;
320 : 659989 : d_congruenceKindsInterpreted.set(fun);
321 : : }
322 [ + + ]: 3220060 : if (extOperator)
323 : : {
324 [ + - ]: 3888 : Trace("equality::extoperator")
325 : 0 : << d_name << "::eq::addFunctionKind(): " << fun
326 : 1944 : << " is an external operator kind " << std::endl;
327 : 1944 : d_congruenceKindsExtOperators.set(fun);
328 : : }
329 : : }
330 : 3220060 : }
331 : :
332 : 1289055 : void EqualityEngine::subtermEvaluates(EqualityNodeId id)
333 : : {
334 [ + - ]: 2578110 : Trace("equality::evaluation")
335 : 0 : << d_name << "::eq::subtermEvaluates(" << d_nodes[id]
336 : 1289055 : << "): " << d_subtermsToEvaluate[id] << std::endl;
337 [ - + ][ - + ]: 1289055 : Assert(!d_isInternal[id]);
[ - - ]
338 [ - + ][ - + ]: 1289055 : Assert(d_subtermsToEvaluate[id] > 0);
[ - - ]
339 [ + + ]: 1289055 : if ((--d_subtermsToEvaluate[id]) == 0)
340 : : {
341 : 899833 : d_evaluationQueue.push(id);
342 : : }
343 : 1289055 : d_subtermEvaluates.push_back(id);
344 : 1289055 : d_subtermEvaluatesSize = d_subtermEvaluates.size();
345 [ + - ]: 2578110 : Trace("equality::evaluation")
346 : 0 : << d_name << "::eq::subtermEvaluates(" << d_nodes[id] << "): new "
347 : 1289055 : << d_subtermsToEvaluate[id] << std::endl;
348 : 1289055 : }
349 : :
350 : 118141046 : void EqualityEngine::addTermInternal(TNode t, bool isOperator)
351 : : {
352 [ + - ]: 236282092 : Trace("equality") << d_name << "::eq::addTermInternal(" << t << ")"
353 : 118141046 : << std::endl;
354 : :
355 : : // If there already, we're done
356 [ + + ]: 118141046 : if (hasTerm(t))
357 : : {
358 [ + - ]: 205075066 : Trace("equality") << d_name << "::eq::addTermInternal(" << t
359 : 102537533 : << "): already there" << std::endl;
360 : 102537554 : return;
361 : : }
362 : :
363 [ + + ]: 15603513 : if (d_done)
364 : : {
365 : 21 : return;
366 : : }
367 : :
368 : : EqualityNodeId result;
369 : :
370 : 15603492 : Kind tk = t.getKind();
371 [ + + ]: 15603492 : if (tk == Kind::EQUAL)
372 : : {
373 : 4163645 : addTermInternal(t[0]);
374 : 4163645 : addTermInternal(t[1]);
375 : 4163645 : EqualityNodeId t0id = getNodeId(t[0]);
376 : 4163645 : EqualityNodeId t1id = getNodeId(t[1]);
377 : 4163645 : result = newApplicationNode(t, t0id, t1id, APP_EQUALITY);
378 : 4163645 : d_isInternal[result] = false;
379 : 4163645 : d_isConstant[result] = false;
380 : : }
381 [ + + ][ + + ]: 11439847 : else if (t.getNumChildren() > 0 && d_congruenceKinds[tk])
[ + + ]
382 : : {
383 : 1279409 : TNode tOp = t.getOperator();
384 : : // Add the operator
385 : 1279409 : addTermInternal(tOp, !isExternalOperatorKind(tk));
386 : 1279409 : result = getNodeId(tOp);
387 : : // Add all the children and Curryfy
388 : 1279409 : bool isInterpreted = isInterpretedFunctionKind(tk);
389 [ + + ]: 3520359 : for (unsigned i = 0; i < t.getNumChildren(); ++i)
390 : : {
391 : : // Add the child
392 : 2240950 : addTermInternal(t[i]);
393 : 2240950 : EqualityNodeId tiId = getNodeId(t[i]);
394 : : // Add the application
395 [ + + ]: 2240950 : result = newApplicationNode(
396 : : t, result, tiId, isInterpreted ? APP_INTERPRETED : APP_UNINTERPRETED);
397 : : }
398 : 1279409 : d_isInternal[result] = false;
399 : 1279409 : d_isConstant[result] = t.isConst();
400 : : // If interpreted, set the number of non-interpreted children
401 [ + + ]: 1279409 : if (isInterpreted)
402 : : {
403 : : // How many children are not constants yet
404 : 135719 : d_subtermsToEvaluate[result] = t.getNumChildren();
405 [ + + ]: 344906 : for (unsigned i = 0; i < t.getNumChildren(); ++i)
406 : : {
407 [ + + ]: 209187 : if (isConstant(getNodeId(t[i])))
408 : : {
409 [ + - ]: 69370 : Trace("equality::evaluation")
410 : 0 : << d_name << "::eq::addTermInternal(" << t << "): evaluates "
411 [ - + ][ - - ]: 34685 : << t[i] << std::endl;
412 : 34685 : subtermEvaluates(result);
413 : : }
414 : : }
415 : : }
416 : 1279409 : }
417 : : else
418 : : {
419 : : // Otherwise we just create the new id
420 : 10160438 : result = newNode(t);
421 : : // Is this an operator
422 : 10160438 : d_isInternal[result] = isOperator;
423 [ + + ][ + + ]: 10160438 : d_isConstant[result] = !isOperator && t.isConst();
424 : : }
425 : :
426 [ + + ]: 15603492 : if (tk == Kind::EQUAL)
427 : : {
428 : : // We set this here as this only applies to actual terms, not the
429 : : // intermediate application terms
430 : 4163645 : d_isEquality[result] = true;
431 : : }
432 : : else
433 : : {
434 : : // Notify e.g. the theory that owns this equality engine that there is a
435 : : // new equivalence class.
436 : 11439847 : d_notify->eqNotifyNewClass(t);
437 [ + + ][ + + ]: 11439847 : if (d_constantsAreTriggers && d_isConstant[result])
[ + + ]
438 : : {
439 : : // Non-Boolean constants are trigger terms for all tags
440 : 1366750 : EqualityNodeId tId = getNodeId(t);
441 : : // Setup the new set
442 : 1366750 : TheoryIdSet newSetTags = 0;
443 : : EqualityNodeId newSetTriggers[THEORY_LAST];
444 : 1366750 : unsigned newSetTriggersSize = THEORY_LAST;
445 [ + + ]: 20501250 : for (TheoryId currentTheory = THEORY_FIRST; currentTheory != THEORY_LAST;
446 : 19134500 : ++currentTheory)
447 : : {
448 : 19134500 : newSetTags = TheoryIdSetUtil::setInsert(currentTheory, newSetTags);
449 : 19134500 : newSetTriggers[currentTheory] = tId;
450 : : }
451 : : // Add it to the list for backtracking
452 : 1366750 : d_triggerTermSetUpdates.push_back(TriggerSetUpdate(tId, null_set_id));
453 : 1366750 : d_triggerTermSetUpdatesSize = d_triggerTermSetUpdatesSize + 1;
454 : : // Mark the the new set as a trigger
455 : 1366750 : d_nodeIndividualTrigger[tId] =
456 : 1366750 : newTriggerTermSet(newSetTags, newSetTriggers, newSetTriggersSize);
457 : : }
458 : : }
459 : :
460 : : // If this is not an internal node, add it to the master
461 [ + + ][ + + ]: 15603492 : if (d_masterEqualityEngine && !d_isInternal[result])
[ + + ]
462 : : {
463 : 4060894 : d_masterEqualityEngine->addTermInternal(t);
464 : : }
465 : :
466 : : // Empty the queue
467 : 15603492 : propagate();
468 : :
469 [ - + ][ - + ]: 15603492 : Assert(hasTerm(t));
[ - - ]
470 : :
471 [ + - ]: 31206984 : Trace("equality") << d_name << "::eq::addTermInternal(" << t << ") => "
472 : 15603492 : << result << std::endl;
473 : : }
474 : :
475 : 1442520523 : bool EqualityEngine::hasTerm(TNode t) const
476 : : {
477 : 1442520523 : return d_nodeIds.find(t) != d_nodeIds.end();
478 : : }
479 : :
480 : 665116184 : EqualityNodeId EqualityEngine::getNodeId(TNode node) const
481 : : {
482 : 665116184 : Assert(hasTerm(node)) << node;
483 : 665116184 : return (*d_nodeIds.find(node)).second;
484 : : }
485 : :
486 : 154631174 : EqualityNode& EqualityEngine::getEqualityNode(TNode t)
487 : : {
488 : 154631174 : return getEqualityNode(getNodeId(t));
489 : : }
490 : :
491 : 1113936101 : EqualityNode& EqualityEngine::getEqualityNode(EqualityNodeId nodeId)
492 : : {
493 [ - + ][ - + ]: 1113936101 : Assert(nodeId < d_equalityNodes.size());
[ - - ]
494 : 1113936101 : return d_equalityNodes[nodeId];
495 : : }
496 : :
497 : 285252961 : const EqualityNode& EqualityEngine::getEqualityNode(TNode t) const
498 : : {
499 : 285252961 : return getEqualityNode(getNodeId(t));
500 : : }
501 : :
502 : 712740478 : const EqualityNode& EqualityEngine::getEqualityNode(EqualityNodeId nodeId) const
503 : : {
504 [ - + ][ - + ]: 712740478 : Assert(nodeId < d_equalityNodes.size());
[ - - ]
505 : 712740478 : return d_equalityNodes[nodeId];
506 : : }
507 : :
508 : 41176977 : void EqualityEngine::assertEqualityInternal(TNode t1,
509 : : TNode t2,
510 : : TNode reason,
511 : : unsigned pid)
512 : : {
513 [ + - ]: 82353954 : Trace("equality") << d_name << "::eq::addEqualityInternal(" << t1 << "," << t2
514 : 0 : << "), reason = " << reason
515 : 41176977 : << ", pid = " << static_cast<MergeReasonType>(pid)
516 : 41176977 : << std::endl;
517 : :
518 [ + + ]: 41176977 : if (d_done)
519 : : {
520 : 487 : return;
521 : : }
522 : :
523 : : // Add the terms if they are not already in the database
524 : 41176490 : addTermInternal(t1);
525 : 41176490 : addTermInternal(t2);
526 : :
527 : : // Add to the queue and propagate
528 : 41176490 : EqualityNodeId t1Id = getNodeId(t1);
529 : 41176490 : EqualityNodeId t2Id = getNodeId(t2);
530 : 41176490 : enqueue(MergeCandidate(t1Id, t2Id, pid, reason));
531 : : }
532 : :
533 : 7939396 : bool EqualityEngine::assertPredicate(TNode t,
534 : : bool polarity,
535 : : TNode reason,
536 : : unsigned pid)
537 : : {
538 [ + - ]: 15878792 : Trace("equality") << d_name << "::eq::addPredicate(" << t << ","
539 [ - - ]: 7939396 : << (polarity ? "true" : "false") << ")" << std::endl;
540 [ - + ][ - + ]: 7939396 : Assert(t.getKind() != Kind::EQUAL) << "Use assertEquality instead";
[ - - ]
541 [ + + ]: 7939396 : TNode b = polarity ? d_true : d_false;
542 : 7939396 : if (hasTerm(t) && areEqual(t, b))
543 : : {
544 : 1787463 : return false;
545 : : }
546 : 6151933 : assertEqualityInternal(t, b, reason, pid);
547 : 6151933 : propagate();
548 : 6151933 : return true;
549 : 7939396 : }
550 : :
551 : 33306965 : bool EqualityEngine::assertEquality(TNode eq,
552 : : bool polarity,
553 : : TNode reason,
554 : : unsigned pid)
555 : : {
556 [ + - ]: 66613930 : Trace("equality") << d_name << "::eq::addEquality(" << eq << ","
557 [ - - ]: 33306965 : << (polarity ? "true" : "false") << ")" << std::endl;
558 [ + + ]: 33306965 : if (polarity)
559 : : {
560 : : // If two terms are already equal, don't assert anything
561 : 19842140 : if (hasTerm(eq[0]) && hasTerm(eq[1]) && areEqual(eq[0], eq[1]))
562 : : {
563 : 4929145 : return false;
564 : : }
565 : : // Add equality between terms
566 : 14912995 : assertEqualityInternal(eq[0], eq[1], reason, pid);
567 : 14912995 : propagate();
568 : : }
569 : : else
570 : : {
571 : : // If two terms are already dis-equal, don't assert anything
572 : 13464825 : if (hasTerm(eq[0]) && hasTerm(eq[1]) && areDisequal(eq[0], eq[1], false))
573 : : {
574 : 7329641 : return false;
575 : : }
576 : :
577 : : // notify the theory
578 : 6138250 : d_notify->eqNotifyDisequal(eq[0], eq[1], reason);
579 : :
580 [ + - ]: 12276500 : Trace("equality::trigger")
581 : 0 : << d_name << "::eq::addEquality(" << eq << ","
582 [ - - ]: 6138250 : << (polarity ? "true" : "false") << ")" << std::endl;
583 : :
584 : 6138250 : assertEqualityInternal(eq, d_false, reason, pid);
585 : 6138250 : propagate();
586 : :
587 [ + + ]: 6138250 : if (d_done)
588 : : {
589 : 2083 : return true;
590 : : }
591 : :
592 : : // If both have constant representatives, we don't notify anyone
593 : 6136167 : EqualityNodeId a = getNodeId(eq[0]);
594 : 6136167 : EqualityNodeId b = getNodeId(eq[1]);
595 : 6136167 : EqualityNodeId aClassId = getEqualityNode(a).getFind();
596 : 6136167 : EqualityNodeId bClassId = getEqualityNode(b).getFind();
597 [ + + ][ + + ]: 6136167 : if (d_isConstant[aClassId] && d_isConstant[bClassId])
[ + + ]
598 : : {
599 : 983 : return true;
600 : : }
601 : :
602 : : // If we are adding a disequality, notify of the shared term representatives
603 : 6135184 : EqualityNodeId eqId = getNodeId(eq);
604 : 6135184 : TriggerTermSetRef aTriggerRef = d_nodeIndividualTrigger[aClassId];
605 : 6135184 : TriggerTermSetRef bTriggerRef = d_nodeIndividualTrigger[bClassId];
606 [ + + ][ + + ]: 6135184 : if (aTriggerRef != +null_set_id && bTriggerRef != +null_set_id)
607 : : {
608 [ + - ]: 5203494 : Trace("equality::trigger")
609 : 0 : << d_name << "::eq::addEquality(" << eq << ","
610 [ - - ]: 2601747 : << (polarity ? "true" : "false") << ": have triggers" << std::endl;
611 : : // The sets of trigger terms
612 : 2601747 : TriggerTermSet& aTriggerTerms = getTriggerTermSet(aTriggerRef);
613 : 2601747 : TriggerTermSet& bTriggerTerms = getTriggerTermSet(bTriggerRef);
614 : : // Go through and notify the shared dis-equalities
615 : 2601747 : TheoryIdSet aTags = aTriggerTerms.d_tags;
616 : 2601747 : TheoryIdSet bTags = bTriggerTerms.d_tags;
617 : 2601747 : TheoryId aTag = TheoryIdSetUtil::setPop(aTags);
618 : 2601747 : TheoryId bTag = TheoryIdSetUtil::setPop(bTags);
619 : 2601747 : int a_i = 0, b_i = 0;
620 [ + + ][ + + ]: 15787062 : while (aTag != THEORY_LAST && bTag != THEORY_LAST)
621 : : {
622 [ + + ]: 13185409 : if (aTag < bTag)
623 : : {
624 : 5571246 : aTag = TheoryIdSetUtil::setPop(aTags);
625 : 5571246 : ++a_i;
626 : : }
627 [ + + ]: 7614163 : else if (aTag > bTag)
628 : : {
629 : 3915913 : bTag = TheoryIdSetUtil::setPop(bTags);
630 : 3915913 : ++b_i;
631 : : }
632 : : else
633 : : {
634 : : // Same tags, notify
635 : 3698250 : EqualityNodeId aSharedId = aTriggerTerms.d_triggers[a_i++];
636 : 3698250 : EqualityNodeId bSharedId = bTriggerTerms.d_triggers[b_i++];
637 : : // Propagate
638 [ + + ]: 3698250 : if (!hasPropagatedDisequality(aTag, aSharedId, bSharedId))
639 : : {
640 : : // Store a proof if not there already
641 [ + + ]: 3698246 : if (!hasPropagatedDisequality(aSharedId, bSharedId))
642 : : {
643 : 1755747 : d_deducedDisequalityReasons.push_back(EqualityPair(aSharedId, a));
644 : 1755747 : d_deducedDisequalityReasons.push_back(EqualityPair(bSharedId, b));
645 : 1755747 : d_deducedDisequalityReasons.push_back(
646 : 3511494 : EqualityPair(eqId, d_falseId));
647 : : }
648 : : // Store the propagation
649 : 3698246 : storePropagatedDisequality(aTag, aSharedId, bSharedId);
650 : : // Notify
651 [ + - ]: 7396492 : Trace("equality::trigger")
652 : 0 : << d_name << "::eq::addEquality(" << eq << ","
653 [ - - ]: 3698246 : << (polarity ? "true" : "false") << ": notifying " << aTag
654 : 0 : << " for " << d_nodes[aSharedId] << " != " << d_nodes[bSharedId]
655 : 3698246 : << std::endl;
656 [ + + ]: 7396492 : if (!notifyTriggerTermEquality(
657 : 7396492 : aTag, d_nodes[aSharedId], d_nodes[bSharedId], false))
658 : : {
659 : 94 : break;
660 : : }
661 : : }
662 : : // Pop the next tags
663 : 3698156 : aTag = TheoryIdSetUtil::setPop(aTags);
664 : 3698156 : bTag = TheoryIdSetUtil::setPop(bTags);
665 : : }
666 : : }
667 : : }
668 : : }
669 : 21048176 : return true;
670 : : }
671 : :
672 : 142629175 : TNode EqualityEngine::getRepresentative(TNode t) const
673 : : {
674 [ + - ]: 285258350 : Trace("equality::internal")
675 : 142629175 : << d_name << "::eq::getRepresentative(" << t << ")" << std::endl;
676 [ - + ][ - + ]: 142629175 : Assert(hasTerm(t));
[ - - ]
677 : 142629175 : EqualityNodeId representativeId = getEqualityNode(t).getFind();
678 [ - + ][ - + ]: 142629175 : Assert(!d_isInternal[representativeId]);
[ - - ]
679 [ + - ]: 285258350 : Trace("equality::internal")
680 : 0 : << d_name << "::eq::getRepresentative(" << t << ") => "
681 : 142629175 : << d_nodes[representativeId] << std::endl;
682 : 142629175 : return d_nodes[representativeId];
683 : : }
684 : :
685 : 63102415 : bool EqualityEngine::merge(EqualityNode& class1,
686 : : EqualityNode& class2,
687 : : std::vector<TriggerId>& triggersFired)
688 : : {
689 [ + - ]: 126204830 : Trace("equality") << d_name << "::eq::merge(" << class1.getFind() << ","
690 : 63102415 : << class2.getFind() << ")" << std::endl;
691 : :
692 [ - + ][ - + ]: 63102415 : Assert(triggersFired.empty());
[ - - ]
693 : :
694 : 63102415 : ++d_stats.d_mergesCount;
695 : :
696 : 63102415 : EqualityNodeId class1Id = class1.getFind();
697 : 63102415 : EqualityNodeId class2Id = class2.getFind();
698 : :
699 : 63102415 : Node n1 = d_nodes[class1Id];
700 : 63102415 : Node n2 = d_nodes[class2Id];
701 : 63102415 : EqualityNode cc1 = getEqualityNode(n1);
702 : 63102415 : EqualityNode cc2 = getEqualityNode(n2);
703 : 63102415 : bool doNotify = false;
704 : : // Determine if we should notify the owner of this class of this merge.
705 : : // The second part of this check is needed due to the internal implementation
706 : : // of this class. It ensures that we are merging terms and not operators.
707 [ + + ][ + + ]: 63102415 : if (class1Id == cc1.getFind() && class2Id == cc2.getFind())
[ + + ]
708 : : {
709 : 60377882 : doNotify = true;
710 : : }
711 : :
712 : : // Check for constant merges
713 : 63102415 : bool class1isConstant = d_isConstant[class1Id];
714 : 63102415 : bool class2isConstant = d_isConstant[class2Id];
715 [ + + ][ + - ]: 63102415 : Assert(class1isConstant || !class2isConstant)
[ - + ][ - + ]
[ - - ]
716 : 0 : << "Should always merge into constants";
717 [ + + ][ + - ]: 63102415 : Assert(!class1isConstant || !class2isConstant) << "Don't merge constants";
[ - + ][ - + ]
[ - - ]
718 : :
719 : : // Trigger set of class 1
720 : 63102415 : TriggerTermSetRef class1triggerRef = d_nodeIndividualTrigger[class1Id];
721 : : TheoryIdSet class1Tags = class1triggerRef == null_set_id
722 [ + + ]: 63102415 : ? 0
723 : 37890399 : : getTriggerTermSet(class1triggerRef).d_tags;
724 : : // Trigger set of class 2
725 : 63102415 : TriggerTermSetRef class2triggerRef = d_nodeIndividualTrigger[class2Id];
726 : : TheoryIdSet class2Tags = class2triggerRef == null_set_id
727 [ + + ]: 63102415 : ? 0
728 : 6615914 : : getTriggerTermSet(class2triggerRef).d_tags;
729 : :
730 : : // Disequalities coming from class2
731 : 63102415 : TaggedEqualitiesSet class2disequalitiesToNotify;
732 : : // Disequalities coming from class1
733 : 63102415 : TaggedEqualitiesSet class1disequalitiesToNotify;
734 : :
735 : : // Individual tags
736 : : TheoryIdSet class1OnlyTags =
737 : 63102415 : TheoryIdSetUtil::setDifference(class1Tags, class2Tags);
738 : : TheoryIdSet class2OnlyTags =
739 : 63102415 : TheoryIdSetUtil::setDifference(class2Tags, class1Tags);
740 : :
741 : : // Only get disequalities if they are not both constant
742 [ + + ][ + - ]: 63102415 : if (!class1isConstant || !class2isConstant)
743 : : {
744 : 63102415 : getDisequalities(!class1isConstant,
745 : : class2Id,
746 : : class1OnlyTags,
747 : : class2disequalitiesToNotify);
748 : 63102415 : getDisequalities(!class2isConstant,
749 : : class1Id,
750 : : class2OnlyTags,
751 : : class1disequalitiesToNotify);
752 : : }
753 : :
754 : : // Update class2 representative information
755 [ + - ]: 126204830 : Trace("equality") << d_name << "::eq::merge(" << class1.getFind() << ","
756 : 63102415 : << class2.getFind() << "): updating class " << class2Id
757 : 63102415 : << std::endl;
758 : 63102415 : EqualityNodeId currentId = class2Id;
759 : : do
760 : : {
761 : : // Get the current node
762 : 80997471 : EqualityNode& currentNode = getEqualityNode(currentId);
763 : :
764 : : // Update it's find to class1 id
765 [ + - ]: 161994942 : Trace("equality") << d_name << "::eq::merge(" << class1.getFind() << ","
766 : 80997471 : << class2.getFind() << "): " << currentId << "->"
767 : 80997471 : << class1Id << std::endl;
768 : 80997471 : currentNode.setFind(class1Id);
769 : :
770 : : // Go through the triggers and inform if necessary
771 : 80997471 : TriggerId currentTrigger = d_nodeTriggers[currentId];
772 [ + + ]: 165170709 : while (currentTrigger != null_trigger)
773 : : {
774 : 84173238 : Trigger& trigger = d_equalityTriggers[currentTrigger];
775 : 84173238 : Trigger& otherTrigger = d_equalityTriggers[currentTrigger ^ 1];
776 : :
777 : : // If the two are not already in the same class
778 [ + + ]: 84173238 : if (otherTrigger.d_classId != trigger.d_classId)
779 : : {
780 : 70295650 : trigger.d_classId = class1Id;
781 : : // If they became the same, call the trigger
782 [ + + ]: 70295650 : if (otherTrigger.d_classId == class1Id)
783 : : {
784 : : // Id of the real trigger is half the internal one
785 : 25237584 : triggersFired.push_back(currentTrigger);
786 : : }
787 : : }
788 : :
789 : : // Go to the next trigger
790 : 84173238 : currentTrigger = trigger.d_nextTrigger;
791 : : }
792 : :
793 : : // Move to the next node
794 : 80997471 : currentId = currentNode.getNext();
795 : :
796 [ + + ]: 80997471 : } while (currentId != class2Id);
797 : :
798 : : // Update class2 table lookup and information if not a boolean
799 : : // since booleans can't be in an application
800 [ + + ]: 63102415 : if (!d_isEquality[class2Id])
801 : : {
802 [ + - ]: 73874070 : Trace("equality") << d_name << "::eq::merge(" << class1.getFind() << ","
803 : 36937035 : << class2.getFind() << "): updating lookups of "
804 : 36937035 : << class2Id << std::endl;
805 : : do
806 : : {
807 : : // Get the current node
808 : 51726995 : EqualityNode& currentNode = getEqualityNode(currentId);
809 [ + - ]: 103453990 : Trace("equality") << d_name << "::eq::merge(" << class1.getFind() << ","
810 : 51726995 : << class2.getFind() << "): updating lookups of node "
811 : 51726995 : << currentId << std::endl;
812 : :
813 : : // Go through the uselist and check for congruences
814 : 51726995 : UseListNodeId currentUseId = currentNode.getUseList();
815 [ + + ]: 139322453 : while (currentUseId != null_uselist_id)
816 : : {
817 : : // Get the node of the use list
818 : 87595458 : UseListNode& useNode = d_useListNodes[currentUseId];
819 : : // Get the function application
820 : 87595458 : EqualityNodeId funId = useNode.getApplicationId();
821 [ + - ]: 175190916 : Trace("equality") << d_name << "::eq::merge(" << class1.getFind() << ","
822 : 87595458 : << class2.getFind() << "): " << d_nodes[currentId]
823 : 87595458 : << " in " << d_nodes[funId] << std::endl;
824 : : const FunctionApplication& fun =
825 : 87595458 : d_applications[useNode.getApplicationId()].d_normalized;
826 : : // If it's interpreted and we can interpret
827 [ + + ][ + + ]: 87595458 : if (fun.isInterpreted() && class1isConstant && !d_isInternal[currentId])
[ + + ][ + + ]
828 : : {
829 : : // Get the actual term id
830 : 1254370 : TNode term = d_nodes[funId];
831 : 1254370 : subtermEvaluates(getNodeId(term));
832 : 1254370 : }
833 : : // Check if there is an application with find arguments
834 : 87595458 : EqualityNodeId aNormalized = getEqualityNode(fun.d_a).getFind();
835 : 87595458 : EqualityNodeId bNormalized = getEqualityNode(fun.d_b).getFind();
836 : 87595458 : FunctionApplication funNormalized(fun.d_type, aNormalized, bNormalized);
837 : : ApplicationIdsMap::iterator find =
838 : 87595458 : d_applicationLookup.find(funNormalized);
839 [ + + ]: 87595458 : if (find != d_applicationLookup.end())
840 : : {
841 : : // Applications fun and the funNormalized can be merged due to
842 : : // congruence
843 : 61985975 : if (getEqualityNode(funId).getFind()
844 [ + + ]: 61985975 : != getEqualityNode(find->second).getFind())
845 : : {
846 : 35551929 : enqueue(MergeCandidate(
847 : 71103858 : funId, find->second, MERGED_THROUGH_CONGRUENCE, TNode::null()));
848 : : }
849 : : }
850 : : else
851 : : {
852 : : // There is no representative, so we can add one, we remove this when
853 : : // backtracking
854 : 25609483 : storeApplicationLookup(funNormalized, funId);
855 : : }
856 : :
857 : : // Go to the next one in the use list
858 : 87595458 : currentUseId = useNode.getNext();
859 : : }
860 : :
861 : : // Move to the next node
862 : 51726995 : currentId = currentNode.getNext();
863 [ + + ]: 51726995 : } while (currentId != class2Id);
864 : : }
865 : :
866 : : // Now merge the lists
867 : 63102415 : class1.merge<true>(class2);
868 : :
869 : : // notify the theory
870 [ + + ]: 63102415 : if (doNotify)
871 : : {
872 : 60377888 : d_notify->eqNotifyMerge(n1, n2);
873 : : }
874 : :
875 : : // Go through the trigger term disequalities and propagate
876 [ + + ]: 63102412 : if (!propagateTriggerTermDisequalities(
877 : : class1OnlyTags, class1triggerRef, class2disequalitiesToNotify))
878 : : {
879 : 22 : return false;
880 : : }
881 [ + + ]: 63102390 : if (!propagateTriggerTermDisequalities(
882 : : class2OnlyTags, class2triggerRef, class1disequalitiesToNotify))
883 : : {
884 : 19 : return false;
885 : : }
886 : :
887 : : // Notify the trigger term merges
888 [ + + ]: 63102371 : if (class2triggerRef != +null_set_id)
889 : : {
890 [ + + ]: 6615895 : if (class1triggerRef == +null_set_id)
891 : : {
892 : : // If class1 doesn't have individual triggers, but class2 does, mark it
893 : 343034 : d_nodeIndividualTrigger[class1Id] = class2triggerRef;
894 : : // Add it to the list for backtracking
895 : 343034 : d_triggerTermSetUpdates.push_back(
896 : 343034 : TriggerSetUpdate(class1Id, +null_set_id));
897 : 343034 : d_triggerTermSetUpdatesSize = d_triggerTermSetUpdatesSize + 1;
898 : : }
899 : : else
900 : : {
901 : : // Get the triggers
902 : 6272861 : TriggerTermSet& class1triggers = getTriggerTermSet(class1triggerRef);
903 : 6272861 : TriggerTermSet& class2triggers = getTriggerTermSet(class2triggerRef);
904 : :
905 : : // Initialize the merged set
906 : 6272861 : TheoryIdSet newSetTags = TheoryIdSetUtil::setUnion(class1triggers.d_tags,
907 : : class2triggers.d_tags);
908 : : EqualityNodeId newSetTriggers[THEORY_LAST];
909 : 6272861 : unsigned newSetTriggersSize = 0;
910 : :
911 : 6272861 : int i1 = 0;
912 : 6272861 : int i2 = 0;
913 : 6272861 : TheoryIdSet tags1 = class1triggers.d_tags;
914 : 6272861 : TheoryIdSet tags2 = class2triggers.d_tags;
915 : 6272861 : TheoryId tag1 = TheoryIdSetUtil::setPop(tags1);
916 : 6272861 : TheoryId tag2 = TheoryIdSetUtil::setPop(tags2);
917 : :
918 : : // Comparing the THEORY_LAST is OK because all other theories are
919 : : // smaller, and will therefore be preferred
920 [ + + ][ + + ]: 61280823 : while (tag1 != THEORY_LAST || tag2 != THEORY_LAST)
921 : : {
922 [ + + ]: 55036479 : if (tag1 < tag2)
923 : : {
924 : : // copy tag1
925 : 46682979 : newSetTriggers[newSetTriggersSize++] =
926 : 46682979 : class1triggers.d_triggers[i1++];
927 : 46682979 : tag1 = TheoryIdSetUtil::setPop(tags1);
928 : : }
929 [ + + ]: 8353500 : else if (tag1 > tag2)
930 : : {
931 : : // copy tag2
932 : 5116 : newSetTriggers[newSetTriggersSize++] =
933 : 5116 : class2triggers.d_triggers[i2++];
934 : 5116 : tag2 = TheoryIdSetUtil::setPop(tags2);
935 : : }
936 : : else
937 : : {
938 : : // copy tag1
939 : 8348384 : EqualityNodeId tag1id = newSetTriggers[newSetTriggersSize++] =
940 : 8348384 : class1triggers.d_triggers[i1++];
941 : : // since they are both tagged notify of merge
942 : 8348384 : EqualityNodeId tag2id = class2triggers.d_triggers[i2++];
943 [ + + ]: 16696768 : if (!notifyTriggerTermEquality(
944 : 16696768 : tag1, d_nodes[tag1id], d_nodes[tag2id], true))
945 : : {
946 : 28517 : return false;
947 : : }
948 : : // Next tags
949 : 8319867 : tag1 = TheoryIdSetUtil::setPop(tags1);
950 : 8319867 : tag2 = TheoryIdSetUtil::setPop(tags2);
951 : : }
952 : : }
953 : :
954 : : // Add the new trigger set, if different from previous one
955 [ + + ]: 6244344 : if (class1triggers.d_tags != class2triggers.d_tags)
956 : : {
957 : : // Add it to the list for backtracking
958 : 3694508 : d_triggerTermSetUpdates.push_back(
959 : 3694508 : TriggerSetUpdate(class1Id, class1triggerRef));
960 : 3694508 : d_triggerTermSetUpdatesSize = d_triggerTermSetUpdatesSize + 1;
961 : : // Mark the the new set as a trigger
962 : 3694508 : d_nodeIndividualTrigger[class1Id] =
963 : 3694508 : newTriggerTermSet(newSetTags, newSetTriggers, newSetTriggersSize);
964 : : }
965 : : }
966 : : }
967 : :
968 : : // Everything fine
969 : 63073854 : return true;
970 : 63102424 : }
971 : :
972 : 63102050 : void EqualityEngine::undoMerge(EqualityNode& class1,
973 : : EqualityNode& class2,
974 : : EqualityNodeId class2Id)
975 : : {
976 [ + - ]: 126204100 : Trace("equality") << d_name << "::eq::undoMerge(" << class1.getFind() << ","
977 : 63102050 : << class2Id << ")" << std::endl;
978 : :
979 : : // Now unmerge the lists (same as merge)
980 : 63102050 : class1.merge<false>(class2);
981 : :
982 : : // Update class2 representative information
983 : 63102050 : EqualityNodeId currentId = class2Id;
984 [ + - ]: 126204100 : Trace("equality") << d_name << "::eq::undoMerge(" << class1.getFind() << ","
985 : 0 : << class2Id << "): undoing representative info"
986 : 63102050 : << std::endl;
987 : : do
988 : : {
989 : : // Get the current node
990 : 80997065 : EqualityNode& currentNode = getEqualityNode(currentId);
991 : :
992 : : // Update it's find to class1 id
993 : 80997065 : currentNode.setFind(class2Id);
994 : :
995 : : // Go through the trigger list (if any) and undo the class
996 : 80997065 : TriggerId currentTrigger = d_nodeTriggers[currentId];
997 [ + + ]: 165170117 : while (currentTrigger != null_trigger)
998 : : {
999 : 84173052 : Trigger& trigger = d_equalityTriggers[currentTrigger];
1000 : 84173052 : trigger.d_classId = class2Id;
1001 : 84173052 : currentTrigger = trigger.d_nextTrigger;
1002 : : }
1003 : :
1004 : : // Move to the next node
1005 : 80997065 : currentId = currentNode.getNext();
1006 : :
1007 [ + + ]: 80997065 : } while (currentId != class2Id);
1008 : 63102050 : }
1009 : :
1010 : 119108767 : void EqualityEngine::backtrack()
1011 : : {
1012 [ + - ]: 119108767 : Trace("equality::backtrack") << "backtracking" << std::endl;
1013 : :
1014 : : // If we need to backtrack then do it
1015 [ + + ]: 119108767 : if (d_assertedEqualitiesCount < d_assertedEqualities.size())
1016 : : {
1017 : : // Clear the propagation queue
1018 [ + + ]: 10786830 : while (!d_propagationQueue.empty())
1019 : : {
1020 : 6 : d_propagationQueue.pop_front();
1021 : : }
1022 : :
1023 [ + - ]: 10786824 : Trace("equality") << d_name << "::eq::backtrack(): nodes" << std::endl;
1024 : :
1025 : 73947564 : for (int i = (int)d_assertedEqualities.size() - 1,
1026 : 10786824 : i_end = (int)d_assertedEqualitiesCount;
1027 [ + + ]: 73947564 : i >= i_end;
1028 : : --i)
1029 : : {
1030 : : // Get the ids of the merged classes
1031 : 63160740 : Equality& eq = d_assertedEqualities[i];
1032 : : // Undo the merge
1033 [ + + ]: 63160740 : if (eq.d_lhs != null_id)
1034 : : {
1035 : 63102050 : undoMerge(
1036 : 63102050 : d_equalityNodes[eq.d_lhs], d_equalityNodes[eq.d_rhs], eq.d_rhs);
1037 : : }
1038 : : }
1039 : :
1040 : 10786824 : d_assertedEqualities.resize(d_assertedEqualitiesCount);
1041 : :
1042 [ + - ]: 10786824 : Trace("equality") << d_name << "::eq::backtrack(): edges" << std::endl;
1043 : :
1044 : 10786824 : for (int i = (int)d_equalityEdges.size() - 2,
1045 : 10786824 : i_end = (int)(2 * d_assertedEqualitiesCount);
1046 [ + + ]: 73947564 : i >= i_end;
1047 : 63160740 : i -= 2)
1048 : : {
1049 : 63160740 : EqualityEdge& edge1 = d_equalityEdges[i];
1050 : 63160740 : EqualityEdge& edge2 = d_equalityEdges[i | 1];
1051 : 63160740 : d_equalityGraph[edge2.getNodeId()] = edge1.getNext();
1052 : 63160740 : d_equalityGraph[edge1.getNodeId()] = edge2.getNext();
1053 : : }
1054 : :
1055 : 10786824 : d_equalityEdges.resize(2 * d_assertedEqualitiesCount);
1056 : : }
1057 : :
1058 [ + + ]: 119108767 : if (d_triggerTermSetUpdates.size() > d_triggerTermSetUpdatesSize)
1059 : : {
1060 : : // Unset the individual triggers
1061 : 3200344 : for (int i = d_triggerTermSetUpdates.size() - 1,
1062 : 3200344 : i_end = d_triggerTermSetUpdatesSize;
1063 [ + + ]: 13488191 : i >= i_end;
1064 : : --i)
1065 : : {
1066 : 10287847 : const TriggerSetUpdate& update = d_triggerTermSetUpdates[i];
1067 : 10287847 : d_nodeIndividualTrigger[update.d_classId] = update.d_oldValue;
1068 : : }
1069 : 3200344 : d_triggerTermSetUpdates.resize(d_triggerTermSetUpdatesSize);
1070 : : }
1071 : :
1072 [ + + ]: 119108767 : if (d_equalityTriggers.size() > d_equalityTriggersCount)
1073 : : {
1074 : : // Unlink the triggers from the lists
1075 : 164464 : for (int i = d_equalityTriggers.size() - 1, i_end = d_equalityTriggersCount;
1076 [ + + ]: 7217816 : i >= i_end;
1077 : : --i)
1078 : : {
1079 : 7053352 : const Trigger& trigger = d_equalityTriggers[i];
1080 : 7053352 : d_nodeTriggers[trigger.d_classId] = trigger.d_nextTrigger;
1081 : : }
1082 : : // Get rid of the triggers
1083 : 164464 : d_equalityTriggers.resize(d_equalityTriggersCount);
1084 : 164464 : d_equalityTriggersOriginal.resize(d_equalityTriggersCount);
1085 : : }
1086 : :
1087 [ + + ]: 119108767 : if (d_applicationLookups.size() > d_applicationLookupsCount)
1088 : : {
1089 : 35224812 : for (int i = d_applicationLookups.size() - 1,
1090 : 3949336 : i_end = (int)d_applicationLookupsCount;
1091 [ + + ]: 35224812 : i >= i_end;
1092 : : --i)
1093 : : {
1094 : 31275476 : d_applicationLookup.erase(d_applicationLookups[i]);
1095 : : }
1096 : 3949336 : d_applicationLookups.resize(d_applicationLookupsCount);
1097 : : }
1098 : :
1099 [ + + ]: 119108767 : if (d_subtermEvaluates.size() > d_subtermEvaluatesSize)
1100 : : {
1101 : 272341 : for (int i = d_subtermEvaluates.size() - 1,
1102 : 272341 : i_end = (int)d_subtermEvaluatesSize;
1103 [ + + ]: 1561366 : i >= i_end;
1104 : : --i)
1105 : : {
1106 : 1289025 : d_subtermsToEvaluate[d_subtermEvaluates[i]]++;
1107 : : }
1108 : 272341 : d_subtermEvaluates.resize(d_subtermEvaluatesSize);
1109 : : }
1110 : :
1111 [ + + ]: 119108767 : if (d_nodes.size() > d_nodesCount)
1112 : : {
1113 : : // Go down the nodes, check the application nodes and remove them from
1114 : : // use-lists
1115 [ + + ]: 18059964 : for (int i = d_nodes.size() - 1, i_end = (int)d_nodesCount; i >= i_end; --i)
1116 : : {
1117 : : // Remove from the node -> id map
1118 [ + - ]: 31320710 : Trace("equality") << d_name << "::eq::backtrack(): removing node "
1119 : 15660355 : << d_nodes[i] << std::endl;
1120 : 15660355 : d_nodeIds.erase(d_nodes[i]);
1121 : :
1122 : 15660355 : const FunctionApplication& app = d_applications[i].d_original;
1123 [ + + ]: 15660355 : if (!app.isNull())
1124 : : {
1125 : : // Remove b from use-list
1126 : 6404388 : getEqualityNode(app.d_b).removeTopFromUseList(d_useListNodes);
1127 : : // Remove a from use-list
1128 : 6404388 : getEqualityNode(app.d_a).removeTopFromUseList(d_useListNodes);
1129 : : }
1130 : : }
1131 : :
1132 : : // Now get rid of the nodes and the rest
1133 : 2399609 : d_nodes.resize(d_nodesCount);
1134 : 2399609 : d_applications.resize(d_nodesCount);
1135 : 2399609 : d_nodeTriggers.resize(d_nodesCount);
1136 : 2399609 : d_nodeIndividualTrigger.resize(d_nodesCount);
1137 : 2399609 : d_isConstant.resize(d_nodesCount);
1138 : 2399609 : d_subtermsToEvaluate.resize(d_nodesCount);
1139 : 2399609 : d_isEquality.resize(d_nodesCount);
1140 : 2399609 : d_isInternal.resize(d_nodesCount);
1141 : 2399609 : d_equalityGraph.resize(d_nodesCount);
1142 : 2399609 : d_equalityNodes.resize(d_nodesCount);
1143 : : }
1144 : :
1145 [ + + ]: 119108767 : if (d_deducedDisequalities.size() > d_deducedDisequalitiesSize)
1146 : : {
1147 : 16929234 : for (int i = d_deducedDisequalities.size() - 1,
1148 : 4423094 : i_end = (int)d_deducedDisequalitiesSize;
1149 [ + + ]: 16929234 : i >= i_end;
1150 : : --i)
1151 : : {
1152 : 12506140 : EqualityPair pair = d_deducedDisequalities[i];
1153 [ - + ][ - + ]: 12506140 : Assert(d_disequalityReasonsMap.find(pair)
[ - - ]
1154 : : != d_disequalityReasonsMap.end());
1155 : : // Remove from the map
1156 : 12506140 : d_disequalityReasonsMap.erase(pair);
1157 : 12506140 : std::swap(pair.first, pair.second);
1158 : 12506140 : d_disequalityReasonsMap.erase(pair);
1159 : : }
1160 : 4423094 : d_deducedDisequalityReasons.resize(d_deducedDisequalityReasonsSize);
1161 : 4423094 : d_deducedDisequalities.resize(d_deducedDisequalitiesSize);
1162 : : }
1163 : 119108767 : }
1164 : :
1165 : 63161105 : void EqualityEngine::addGraphEdge(EqualityNodeId t1,
1166 : : EqualityNodeId t2,
1167 : : unsigned type,
1168 : : TNode reason)
1169 : : {
1170 [ + - ]: 126322210 : Trace("equality") << d_name << "::eq::addGraphEdge({" << t1 << "} "
1171 : 0 : << d_nodes[t1] << ", {" << t2 << "} " << d_nodes[t2] << ","
1172 : 63161105 : << reason << ")" << std::endl;
1173 : 63161105 : EqualityEdgeId edge = d_equalityEdges.size();
1174 : 63161105 : d_equalityEdges.push_back(
1175 : 126322210 : EqualityEdge(t2, d_equalityGraph[t1], type, reason));
1176 : 63161105 : d_equalityEdges.push_back(
1177 : 126322210 : EqualityEdge(t1, d_equalityGraph[t2], type, reason));
1178 : 63161105 : d_equalityGraph[t1] = edge;
1179 : 63161105 : d_equalityGraph[t2] = edge | 1;
1180 : :
1181 [ - + ]: 63161105 : if (TraceIsOn("equality::internal"))
1182 : : {
1183 : 0 : debugPrintGraph();
1184 : : }
1185 : 63161105 : }
1186 : :
1187 : 0 : std::string EqualityEngine::edgesToString(EqualityEdgeId edgeId) const
1188 : : {
1189 : 0 : std::stringstream out;
1190 : 0 : bool first = true;
1191 [ - - ]: 0 : if (edgeId == null_edge)
1192 : : {
1193 : 0 : out << "null";
1194 : : }
1195 : : else
1196 : : {
1197 [ - - ]: 0 : while (edgeId != null_edge)
1198 : : {
1199 : 0 : const EqualityEdge& edge = d_equalityEdges[edgeId];
1200 [ - - ]: 0 : if (!first) out << ",";
1201 : 0 : out << "{" << edge.getNodeId() << "} " << d_nodes[edge.getNodeId()];
1202 : 0 : edgeId = edge.getNext();
1203 : 0 : first = false;
1204 : : }
1205 : : }
1206 : 0 : return out.str();
1207 : 0 : }
1208 : :
1209 : 2926981 : void EqualityEngine::buildEqConclusion(EqualityNodeId id1,
1210 : : EqualityNodeId id2,
1211 : : EqProof* eqp) const
1212 : : {
1213 : 2926981 : Kind k1 = d_nodes[id1].getKind();
1214 : 2926981 : Kind k2 = d_nodes[id2].getKind();
1215 : : // only try to build if ids do not correspond to internal nodes. If they do,
1216 : : // only try to build build if full applications corresponding to the given ids
1217 : : // have the same congruence n-ary non-APPLY_* kind, since the internal nodes
1218 : : // may be full nodes.
1219 [ + + ]: 4345221 : if ((d_isInternal[id1] || d_isInternal[id2])
1220 [ + + ][ + - ]: 4729170 : && (k1 != k2 || k1 == Kind::APPLY_UF || k1 == Kind::APPLY_CONSTRUCTOR
[ + + ][ + + ]
[ + + ]
1221 [ + - ][ + - ]: 383949 : || k1 == Kind::APPLY_SELECTOR || k1 == Kind::APPLY_TESTER
1222 [ + + ]: 383949 : || !NodeManager::isNAryKind(k1)))
1223 : : {
1224 : 2912831 : return;
1225 : : }
1226 [ + - ]: 2875022 : Trace("equality") << "buildEqConclusion: {" << id1 << "} " << d_nodes[id1]
1227 : 1437511 : << "\n";
1228 [ + - ]: 2875022 : Trace("equality") << "buildEqConclusion: {" << id2 << "} " << d_nodes[id2]
1229 : 1437511 : << "\n";
1230 [ + + ]: 8625066 : Node eq[2];
1231 : 1437511 : NodeManager* nm = nodeManager();
1232 [ + + ]: 4312533 : for (unsigned i = 0; i < 2; ++i)
1233 : : {
1234 [ + + ]: 2875022 : EqualityNodeId equalityNodeId = i == 0 ? id1 : id2;
1235 : 2875022 : Node equalityNode = d_nodes[equalityNodeId];
1236 : : // if not an internal node, just retrieve it
1237 [ + + ]: 2875022 : if (!d_isInternal[equalityNodeId])
1238 : : {
1239 : 2836480 : eq[i] = equalityNode;
1240 : 2836480 : continue;
1241 : : }
1242 : : // build node relative to partial application of this
1243 : : // n-ary kind. We get the full application, then we get
1244 : : // the arguments relative to how partial the internal
1245 : : // node is, and build the application
1246 : :
1247 : : // get number of children of partial app:
1248 : : // #children of full app - (id of full app - id of
1249 : : // partial app)
1250 : 38542 : EqualityNodeId fullAppId = getNodeId(equalityNode);
1251 : 38542 : EqualityNodeId curr = fullAppId;
1252 : 38542 : unsigned separation = 0;
1253 [ - + ][ - + ]: 38542 : Assert(fullAppId >= equalityNodeId);
[ - - ]
1254 [ + + ]: 108684 : while (curr != equalityNodeId)
1255 : : {
1256 [ + + ]: 70142 : separation = separation + (d_nodes[curr--] == equalityNode ? 1 : 0);
1257 : : }
1258 : : // compute separation, which is how many ids with the
1259 : : // same fullappnode exist between equalityNodeId and
1260 : : // fullAppId
1261 : 38542 : unsigned numChildren = equalityNode.getNumChildren() - separation;
1262 [ - + ][ - - ]: 38542 : Assert(numChildren < equalityNode.getNumChildren())
1263 : 0 : << "broke for numChildren " << numChildren << ", fullAppId "
1264 : 0 : << fullAppId << ", equalityNodeId " << equalityNodeId << ", node "
1265 : 38542 : << equalityNode << ", cong: {" << id1 << "} " << d_nodes[id1] << " = {"
1266 [ - + ][ - + ]: 38542 : << id2 << "} " << d_nodes[id2] << "\n";
[ - - ]
1267 : : // if has at least as many children as the minimal
1268 : : // number of children of the n-ary kind, build the node
1269 [ + + ]: 38542 : if (numChildren >= kind::metakind::getMinArityForKind(k1))
1270 : : {
1271 : 10242 : std::vector<Node> children;
1272 [ + + ]: 33584 : for (unsigned j = 0; j < numChildren; ++j)
1273 : : {
1274 : 23342 : children.push_back(equalityNode[j]);
1275 : : }
1276 : 10242 : eq[i] = nm->mkNode(k1, children);
1277 : 10242 : }
1278 [ + + ]: 2875022 : }
1279 : : // if built equality, add it as eqp's conclusion
1280 [ + + ][ + - ]: 1437511 : if (!eq[0].isNull() && !eq[1].isNull())
[ + + ]
1281 : : {
1282 : 1423361 : eqp->d_node = eq[0].eqNode(eq[1]);
1283 [ + - ]: 2846722 : Trace("equality") << "buildEqConclusion: Built equality " << eqp->d_node
1284 : 1423361 : << "\n";
1285 : 1423361 : return;
1286 : : }
1287 [ + - ]: 14150 : Trace("equality") << "buildEqConclusion: Did not build equality\n";
1288 [ + + ][ - - ]: 4312533 : }
1289 : :
1290 : 850705 : void EqualityEngine::explainEquality(TNode t1,
1291 : : TNode t2,
1292 : : bool polarity,
1293 : : std::vector<TNode>& equalities,
1294 : : EqProof* eqp) const
1295 : : {
1296 [ + - ]: 1701410 : Trace("pf::ee") << d_name << "::eq::explainEquality(" << t1 << ", " << t2
1297 [ - - ]: 0 : << ", " << (polarity ? "true" : "false") << ")"
1298 [ - - ]: 850705 : << ", proof = " << (eqp ? "ON" : "OFF") << std::endl;
1299 : :
1300 : : // The terms must be there already
1301 : 850705 : Assert(hasTerm(t1) && hasTerm(t2));
1302 : :
1303 : : // Get the ids
1304 : 850705 : EqualityNodeId t1Id = getNodeId(t1);
1305 : 850705 : EqualityNodeId t2Id = getNodeId(t2);
1306 : :
1307 [ + - ]: 850705 : Trace("pf::ee") << "Ids: " << t1Id << ", " << t2Id << "\n";
1308 : :
1309 [ - + ]: 850705 : if (TraceIsOn("equality::internal"))
1310 : : {
1311 : 0 : debugPrintGraph();
1312 : : }
1313 : :
1314 : 850705 : std::map<std::pair<EqualityNodeId, EqualityNodeId>, EqProof*> cache;
1315 [ + + ]: 850705 : if (polarity)
1316 : : {
1317 : : // Get the explanation
1318 : 791433 : getExplanation(t1Id, t2Id, equalities, cache, eqp);
1319 : : }
1320 : : else
1321 : : {
1322 [ + + ]: 59272 : if (eqp)
1323 : : {
1324 : 23640 : eqp->d_id = MERGED_THROUGH_TRANS;
1325 : 23640 : eqp->d_node = d_nodes[t1Id].eqNode(d_nodes[t2Id]).notNode();
1326 : : }
1327 : :
1328 : : // Get the reason for this disequality
1329 : 59272 : EqualityPair pair(t1Id, t2Id);
1330 [ - + ][ - + ]: 59272 : Assert(d_disequalityReasonsMap.find(pair) != d_disequalityReasonsMap.end())
[ - - ]
1331 : 0 : << "Don't ask for stuff I didn't notify you about";
1332 : 59272 : DisequalityReasonRef reasonRef = d_disequalityReasonsMap.find(pair)->second;
1333 [ + + ]: 59272 : if (eqp)
1334 : : {
1335 [ + - ]: 47280 : Trace("pf::ee") << "Deq reason for " << eqp->d_node << " "
1336 : 0 : << reasonRef.d_mergesStart << "..."
1337 : 23640 : << reasonRef.d_mergesEnd << std::endl;
1338 : : }
1339 [ + + ]: 141314 : for (unsigned i = reasonRef.d_mergesStart; i < reasonRef.d_mergesEnd; ++i)
1340 : : {
1341 : 82042 : EqualityPair toExplain = d_deducedDisequalityReasons[i];
1342 : 82042 : std::shared_ptr<EqProof> eqpc;
1343 : :
1344 : : // If we're constructing a (transitivity) proof, we don't need to include
1345 : : // an explanation for x=x.
1346 [ + + ][ + + ]: 82042 : if (eqp && toExplain.first != toExplain.second)
1347 : : {
1348 : 27965 : eqpc = std::make_shared<EqProof>();
1349 [ + - ]: 55930 : Trace("pf::ee") << "Deq getExplanation #" << i << " for " << eqp->d_node
1350 : 0 : << " : " << toExplain.first << " " << toExplain.second
1351 : 27965 : << std::endl;
1352 : : }
1353 : :
1354 : 82042 : getExplanation(
1355 : : toExplain.first, toExplain.second, equalities, cache, eqpc.get());
1356 : :
1357 [ + + ]: 82042 : if (eqpc)
1358 : : {
1359 [ - + ]: 27965 : if (TraceIsOn("pf::ee"))
1360 : : {
1361 [ - - ]: 0 : Trace("pf::ee") << "Child proof is:" << std::endl;
1362 : 0 : eqpc->debug_print("pf::ee", 1);
1363 : : }
1364 [ + + ]: 27965 : if (eqpc->d_id == MERGED_THROUGH_TRANS)
1365 : : {
1366 : 16967 : std::vector<std::shared_ptr<EqProof>> orderedChildren;
1367 : 16967 : bool nullCongruenceFound = false;
1368 [ + + ]: 57763 : for (const auto& child : eqpc->d_children)
1369 : : {
1370 : 40796 : if (child->d_id == MERGED_THROUGH_CONGRUENCE
1371 [ + + ][ + + ]: 40796 : && child->d_node.isNull())
[ + + ]
1372 : : {
1373 : 21366 : nullCongruenceFound = true;
1374 [ + - ]: 42732 : Trace("pf::ee")
1375 : 0 : << "Have congruence with empty d_node. Splitting..."
1376 : 21366 : << std::endl;
1377 : 21366 : orderedChildren.insert(orderedChildren.begin(),
1378 : 21366 : child->d_children[0]);
1379 : 21366 : orderedChildren.push_back(child->d_children[1]);
1380 : : }
1381 : : else
1382 : : {
1383 : 19430 : orderedChildren.push_back(child);
1384 : : }
1385 : : }
1386 : :
1387 [ + + ]: 16967 : if (nullCongruenceFound)
1388 : : {
1389 : 15505 : eqpc->d_children = orderedChildren;
1390 [ - + ]: 15505 : if (TraceIsOn("pf::ee"))
1391 : : {
1392 [ - - ]: 0 : Trace("pf::ee")
1393 : 0 : << "Child proof's children have been reordered. It is now:"
1394 : 0 : << std::endl;
1395 : 0 : eqpc->debug_print("pf::ee", 1);
1396 : : }
1397 : : }
1398 : 16967 : }
1399 : :
1400 : 27965 : eqp->d_children.push_back(eqpc);
1401 : : }
1402 : 82042 : }
1403 : :
1404 [ + + ]: 59272 : if (eqp)
1405 : : {
1406 [ + + ]: 23640 : if (eqp->d_children.size() == 0)
1407 : : {
1408 : : // Corner case where this is actually a disequality between two
1409 : : // constants
1410 [ + - ]: 16 : Trace("pf::ee")
1411 : 0 : << "Encountered a constant disequality (not a transitivity proof): "
1412 : 8 : << eqp->d_node << std::endl;
1413 [ - + ][ - + ]: 8 : Assert(eqp->d_node[0][0].isConst());
[ - - ]
1414 [ - + ][ - + ]: 8 : Assert(eqp->d_node[0][1].isConst());
[ - - ]
1415 : 8 : eqp->d_id = MERGED_THROUGH_CONSTANTS;
1416 : : }
1417 [ + + ]: 23632 : else if (eqp->d_children.size() == 1)
1418 : : {
1419 : 19643 : Node cnode = eqp->d_children[0]->d_node;
1420 [ + - ]: 39286 : Trace("pf::ee") << "Simplifying " << cnode << " from " << eqp->d_node
1421 : 19643 : << std::endl;
1422 : 19643 : bool simpTrans = true;
1423 [ + - ]: 19643 : if (cnode.getKind() == Kind::EQUAL)
1424 : : {
1425 : : // It may be the case that we have a proof of x = c2 and we want to
1426 : : // conclude x != c1. If this is the case, below we construct:
1427 : : //
1428 : : // -------- MERGED_THROUGH_EQUALITY
1429 : : // x = c2 c1 != c2
1430 : : // ----------------- TRANS
1431 : : // x != c1
1432 [ + + ][ + + ]: 19643 : TNode c1 = t1.isConst() ? t1 : (t2.isConst() ? t2 : TNode::null());
1433 [ + + ][ + + ]: 19643 : TNode nc = t1.isConst() ? t2 : (t2.isConst() ? t1 : TNode::null());
1434 : 19643 : Node c2;
1435 : : // merge constants transitivity
1436 [ + + ]: 58380 : for (unsigned i = 0; i < 2; i++)
1437 : : {
1438 : 39025 : if (cnode[i].isConst() && cnode[1 - i] == nc)
1439 : : {
1440 : 288 : c2 = cnode[i];
1441 : 288 : break;
1442 : : }
1443 : : }
1444 [ + + ][ + + ]: 19643 : if (!c1.isNull() && !c2.isNull())
[ + + ]
1445 : : {
1446 : 288 : simpTrans = false;
1447 [ - + ][ - + ]: 864 : AssertEqual(c1.getType(), c2.getType());
[ - - ]
1448 : 288 : std::shared_ptr<EqProof> eqpmc = std::make_shared<EqProof>();
1449 : 288 : eqpmc->d_id = MERGED_THROUGH_CONSTANTS;
1450 : 288 : eqpmc->d_node = c1.eqNode(c2).eqNode(d_false);
1451 : 288 : eqp->d_children.push_back(eqpmc);
1452 : 288 : }
1453 : 19643 : }
1454 [ + + ]: 19643 : if (simpTrans)
1455 : : {
1456 : : // The transitivity proof has just one child. Simplify.
1457 : 19355 : std::shared_ptr<EqProof> temp = eqp->d_children[0];
1458 : 19355 : eqp->d_children.clear();
1459 : 19355 : *eqp = *temp;
1460 : 19355 : }
1461 : 19643 : }
1462 : :
1463 [ - + ]: 23640 : if (TraceIsOn("pf::ee"))
1464 : : {
1465 [ - - ]: 0 : Trace("pf::ee") << "Disequality explanation final proof: " << std::endl;
1466 : 0 : eqp->debug_print("pf::ee", 1);
1467 : : }
1468 : : }
1469 : : }
1470 : 850705 : }
1471 : :
1472 : 31487 : void EqualityEngine::explainPredicate(TNode p,
1473 : : bool polarity,
1474 : : std::vector<TNode>& assertions,
1475 : : EqProof* eqp) const
1476 : : {
1477 [ + - ]: 62974 : Trace("equality") << d_name << "::eq::explainPredicate(" << p << ")"
1478 : 31487 : << std::endl;
1479 : : // Must have the term
1480 [ - + ][ - + ]: 31487 : Assert(hasTerm(p));
[ - - ]
1481 : 31487 : std::map<std::pair<EqualityNodeId, EqualityNodeId>, EqProof*> cache;
1482 [ - + ]: 31487 : if (TraceIsOn("equality::internal"))
1483 : : {
1484 : 0 : debugPrintGraph();
1485 : : }
1486 : : // Get the explanation
1487 [ + + ]: 31487 : getExplanation(
1488 : : getNodeId(p), polarity ? d_trueId : d_falseId, assertions, cache, eqp);
1489 : 31487 : }
1490 : :
1491 : 513505 : void EqualityEngine::explainLit(TNode lit,
1492 : : std::vector<TNode>& assumptions) const
1493 : : {
1494 [ + - ]: 513505 : Trace("eq-exp") << "explainLit: " << lit << std::endl;
1495 [ - + ][ - + ]: 513505 : Assert(lit.getKind() != Kind::AND);
[ - - ]
1496 : 513505 : bool polarity = lit.getKind() != Kind::NOT;
1497 [ + + ]: 513505 : TNode atom = polarity ? lit : lit[0];
1498 : 513505 : std::vector<TNode> tassumptions;
1499 [ + + ]: 513505 : if (atom.getKind() == Kind::EQUAL)
1500 : : {
1501 [ - + ][ - + ]: 492863 : Assert(hasTerm(atom[0]));
[ - - ]
1502 [ - + ][ - + ]: 492863 : Assert(hasTerm(atom[1]));
[ - - ]
1503 [ + + ]: 492863 : if (!polarity)
1504 : : {
1505 : : // ensure that we are ready to explain the disequality
1506 [ - + ][ - + ]: 35630 : AlwaysAssert(areDisequal(atom[0], atom[1], true));
[ - - ]
1507 : : }
1508 [ - + ]: 457233 : else if (atom[0] == atom[1])
1509 : : {
1510 : : // no need to explain reflexivity
1511 : 0 : return;
1512 : : }
1513 : 492863 : explainEquality(atom[0], atom[1], polarity, tassumptions);
1514 : : }
1515 : : else
1516 : : {
1517 : 20642 : explainPredicate(atom, polarity, tassumptions);
1518 : : }
1519 : : // ensure that duplicates are removed
1520 [ + + ]: 2972108 : for (TNode a : tassumptions)
1521 : : {
1522 : 2458603 : if (std::find(assumptions.begin(), assumptions.end(), a)
1523 [ + + ]: 4917206 : == assumptions.end())
1524 : : {
1525 [ - + ][ - + ]: 2146241 : Assert(!a.isNull());
[ - - ]
1526 : 2146241 : assumptions.push_back(a);
1527 : : }
1528 : 2458603 : }
1529 [ + - ][ + - ]: 513505 : }
1530 : :
1531 : 433178 : Node EqualityEngine::mkExplainLit(TNode lit) const
1532 : : {
1533 [ - + ][ - + ]: 433178 : Assert(lit.getKind() != Kind::AND);
[ - - ]
1534 : 433178 : std::vector<TNode> assumptions;
1535 : 433178 : explainLit(lit, assumptions);
1536 : 433178 : Node ret;
1537 [ - + ]: 433178 : if (assumptions.empty())
1538 : : {
1539 : 0 : ret = nodeManager()->mkConst(true);
1540 : : }
1541 [ + + ]: 433178 : else if (assumptions.size() == 1)
1542 : : {
1543 : 73228 : ret = assumptions[0];
1544 : : }
1545 : : else
1546 : : {
1547 : 359950 : ret = nodeManager()->mkNode(Kind::AND, assumptions);
1548 : : }
1549 : 866356 : return ret;
1550 : 433178 : }
1551 : :
1552 : 10133075 : void EqualityEngine::getExplanation(
1553 : : EqualityNodeId t1Id,
1554 : : EqualityNodeId t2Id,
1555 : : std::vector<TNode>& equalities,
1556 : : std::map<std::pair<EqualityNodeId, EqualityNodeId>, EqProof*>& cache,
1557 : : EqProof* eqp) const
1558 : : {
1559 [ + - ]: 20266150 : Trace("eq-exp") << d_name << "::eq::getExplanation({" << t1Id << "} "
1560 : 0 : << d_nodes[t1Id] << ", {" << t2Id << "} " << d_nodes[t2Id]
1561 : 10133075 : << ") size = " << cache.size() << std::endl;
1562 : :
1563 : : // determine if we have already computed the explanation.
1564 : 10133075 : std::pair<EqualityNodeId, EqualityNodeId> cacheKey;
1565 : 10133075 : std::map<std::pair<EqualityNodeId, EqualityNodeId>, EqProof*>::iterator it;
1566 [ + + ]: 10133075 : if (!eqp)
1567 : : {
1568 : : // If proofs are disabled, we order the ids, since explaining t1 = t2 is the
1569 : : // same as explaining t2 = t1.
1570 : 5835042 : cacheKey = std::minmax(t1Id, t2Id);
1571 : 5835042 : it = cache.find(cacheKey);
1572 [ + + ]: 5835042 : if (it != cache.end())
1573 : : {
1574 : 2843994 : return;
1575 : : }
1576 : : }
1577 : : else
1578 : : {
1579 : : // If proofs are enabled, note that proofs are sensitive to the order of t1
1580 : : // and t2, so we don't sort the ids in this case. TODO: Depending on how
1581 : : // issue #2965 is resolved, we may be able to revisit this, if it is the
1582 : : // case that proof/uf_proof.h,cpp is robust to equality ordering.
1583 : 4298033 : cacheKey = std::pair<EqualityNodeId, EqualityNodeId>(t1Id, t2Id);
1584 : 4298033 : it = cache.find(cacheKey);
1585 [ + + ]: 4298033 : if (it != cache.end())
1586 : : {
1587 [ + + ]: 2029365 : if (it->second)
1588 : : {
1589 : 2029346 : eqp->d_id = it->second->d_id;
1590 : 2029346 : eqp->d_children.insert(eqp->d_children.end(),
1591 : 2029346 : it->second->d_children.begin(),
1592 : 2029346 : it->second->d_children.end());
1593 : 2029346 : eqp->d_node = it->second->d_node;
1594 : : }
1595 : : else
1596 : : {
1597 : : // We may have cached null in its place, create the trivial proof now.
1598 [ - + ][ - + ]: 19 : Assert(d_nodes[t1Id] == d_nodes[t2Id]);
[ - - ]
1599 [ - + ][ - + ]: 19 : Assert(eqp->d_id == MERGED_THROUGH_REFLEXIVITY);
[ - - ]
1600 : 19 : eqp->d_node = d_nodes[t1Id].eqNode(d_nodes[t1Id]);
1601 : : }
1602 : 2029365 : return;
1603 : : }
1604 : : }
1605 : 5259716 : cache[cacheKey] = eqp;
1606 : :
1607 : : // We can only explain the nodes that got merged
1608 : : #ifdef CVC5_ASSERTIONS
1609 : : bool canExplain =
1610 : 5259716 : getEqualityNode(t1Id).getFind() == getEqualityNode(t2Id).getFind()
1611 [ + + ][ + - ]: 5259716 : || (d_done && isConstant(t1Id) && isConstant(t2Id));
[ + - ][ + - ]
1612 : :
1613 [ - + ]: 5259716 : if (!canExplain)
1614 : : {
1615 : 0 : warning() << "Can't explain equality:" << std::endl;
1616 : 0 : warning() << d_nodes[t1Id] << " with find "
1617 : 0 : << d_nodes[getEqualityNode(t1Id).getFind()] << std::endl;
1618 : 0 : warning() << d_nodes[t2Id] << " with find "
1619 : 0 : << d_nodes[getEqualityNode(t2Id).getFind()] << std::endl;
1620 : : }
1621 [ - + ][ - + ]: 5259716 : Assert(canExplain);
[ - - ]
1622 : : #endif
1623 : :
1624 : : // If the nodes are the same, we're done
1625 [ + + ]: 5259716 : if (t1Id == t2Id)
1626 : : {
1627 [ + + ]: 1389202 : if (eqp)
1628 : : {
1629 : : // ignore equalities between function symbols, i.e. internal nullary
1630 : : // non-constant nodes.
1631 : : //
1632 : : // Note that this is robust for HOL because in that case function
1633 : : // symbols are not internal nodes
1634 [ + + ]: 773683 : if (d_isInternal[t1Id] && d_nodes[t1Id].getNumChildren() == 0
1635 [ + + ][ + - ]: 773683 : && !d_isConstant[t1Id])
[ + + ]
1636 : : {
1637 : 198366 : eqp->d_node = Node::null();
1638 : : }
1639 : : else
1640 : : {
1641 [ - + ][ - + ]: 376399 : Assert(d_nodes[t1Id].getKind() != Kind::BUILTIN);
[ - - ]
1642 : 376399 : eqp->d_node = d_nodes[t1Id].eqNode(d_nodes[t1Id]);
1643 : : }
1644 : : }
1645 : 1389202 : return;
1646 : : }
1647 : :
1648 : : // Queue for the BFS containing nodes
1649 : 3870514 : std::vector<BfsData> bfsQueue;
1650 : :
1651 : : // Find a path from t1 to t2 in the graph (BFS)
1652 : 3870514 : bfsQueue.push_back(BfsData(t1Id, null_id, 0));
1653 : 3870514 : size_t currentIndex = 0;
1654 : : while (true)
1655 : : {
1656 : : // There should always be a path, and every node can be visited only once
1657 : : // (tree)
1658 [ - + ][ - + ]: 23521722 : Assert(currentIndex < bfsQueue.size());
[ - - ]
1659 : :
1660 : : // The next node to visit
1661 : 23521722 : BfsData current = bfsQueue[currentIndex];
1662 : 23521722 : EqualityNodeId currentNode = current.d_nodeId;
1663 : :
1664 [ + - ]: 47043444 : Trace("equality") << d_name << "::eq::getExplanation(): currentNode = {"
1665 : 0 : << currentNode << "} " << d_nodes[currentNode]
1666 : 23521722 : << std::endl;
1667 : :
1668 : : // Go through the equality edges of this node
1669 : 23521722 : EqualityEdgeId currentEdge = d_equalityGraph[currentNode];
1670 [ - + ]: 23521722 : if (TraceIsOn("equality"))
1671 : : {
1672 [ - - ]: 0 : Trace("equality") << d_name
1673 : 0 : << "::eq::getExplanation(): edgesId = " << currentEdge
1674 : 0 : << std::endl;
1675 [ - - ]: 0 : Trace("equality") << d_name << "::eq::getExplanation(): edges = "
1676 : 0 : << edgesToString(currentEdge) << std::endl;
1677 : : }
1678 : :
1679 [ + + ]: 77632123 : while (currentEdge != null_edge)
1680 : : {
1681 : : // Get the edge
1682 : 57980915 : const EqualityEdge& edge = d_equalityEdges[currentEdge];
1683 : :
1684 : : // If not just the backwards edge
1685 [ + + ]: 57980915 : if ((currentEdge | 1u) != (current.d_edgeId | 1u))
1686 : : {
1687 [ + - ]: 78839924 : Trace("equality") << d_name
1688 : 0 : << "::eq::getExplanation(): currentEdge = ({"
1689 : 0 : << currentNode << "} " << d_nodes[currentNode]
1690 : 39419962 : << ", {" << edge.getNodeId() << "} "
1691 : 39419962 : << d_nodes[edge.getNodeId()] << ")" << std::endl;
1692 : :
1693 : : // Did we find the path
1694 [ + + ]: 39419962 : if (edge.getNodeId() == t2Id)
1695 : : {
1696 [ + - ]: 7741028 : Trace("equality")
1697 : 3870514 : << d_name << "::eq::getExplanation(): path found: " << std::endl;
1698 : :
1699 : 3870514 : std::vector<std::shared_ptr<EqProof>> eqp_trans;
1700 : :
1701 : : // Reconstruct the path
1702 : : do
1703 : : {
1704 : : // The current node
1705 : 9104696 : currentNode = bfsQueue[currentIndex].d_nodeId;
1706 : 9104696 : EqualityNodeId edgeNode = d_equalityEdges[currentEdge].getNodeId();
1707 : : MergeReasonType reasonType = static_cast<MergeReasonType>(
1708 : 9104696 : d_equalityEdges[currentEdge].getReasonType());
1709 : 9104696 : Node reason = d_equalityEdges[currentEdge].getReason();
1710 : :
1711 [ + - ]: 18209392 : Trace("equality")
1712 : 0 : << d_name
1713 : 0 : << "::eq::getExplanation(): currentEdge = " << currentEdge
1714 : 9104696 : << ", currentNode = " << currentNode << std::endl;
1715 [ + - ]: 18209392 : Trace("equality")
1716 : 0 : << d_name << " targetNode = {" << edgeNode
1717 : 9104696 : << "} " << d_nodes[edgeNode] << std::endl;
1718 [ + - ]: 18209392 : Trace("equality")
1719 : 0 : << d_name << " in currentEdge = ({"
1720 : 0 : << currentNode << "} " << d_nodes[currentNode] << ", {"
1721 : 9104696 : << edge.getNodeId() << "} " << d_nodes[edge.getNodeId()] << ")"
1722 : 9104696 : << std::endl;
1723 [ + - ]: 18209392 : Trace("equality")
1724 : 0 : << d_name
1725 : 0 : << " reason type = " << reasonType
1726 : 9104696 : << "\n";
1727 : :
1728 : 9104696 : std::shared_ptr<EqProof> eqpc;
1729 : : ;
1730 : : // Make child proof if a proof is being constructed
1731 [ + + ]: 9104696 : if (eqp)
1732 : : {
1733 : 3895630 : eqpc = std::make_shared<EqProof>();
1734 : 3895630 : eqpc->d_id = reasonType;
1735 : : }
1736 : :
1737 : : // Add the actual equality to the vector
1738 [ + + ][ + + ]: 9104696 : switch (reasonType)
1739 : : {
1740 : 4555028 : case MERGED_THROUGH_CONGRUENCE:
1741 : : {
1742 : : // f(x1, x2) == f(y1, y2) because x1 = y1 and x2 = y2
1743 [ + - ]: 9110056 : Trace("equality")
1744 : 0 : << d_name
1745 : 0 : << "::eq::getExplanation(): due to congruence, going deeper"
1746 : 4555028 : << std::endl;
1747 : : const FunctionApplication& f1 =
1748 : 4555028 : d_applications[currentNode].d_original;
1749 : : const FunctionApplication& f2 =
1750 : 4555028 : d_applications[edgeNode].d_original;
1751 : :
1752 [ + - ]: 4555028 : Trace("equality") << push;
1753 [ + - ]: 9110056 : Trace("equality")
1754 : 4555028 : << "Explaining left hand side equalities" << std::endl;
1755 : : std::shared_ptr<EqProof> eqpc1 =
1756 [ + + ]: 4555028 : eqpc ? std::make_shared<EqProof>() : nullptr;
1757 : 4555028 : getExplanation(f1.d_a, f2.d_a, equalities, cache, eqpc1.get());
1758 [ + - ]: 9110056 : Trace("equality")
1759 : 4555028 : << "Explaining right hand side equalities" << std::endl;
1760 : : std::shared_ptr<EqProof> eqpc2 =
1761 [ + + ]: 4555028 : eqpc ? std::make_shared<EqProof>() : nullptr;
1762 : 4555028 : getExplanation(f1.d_b, f2.d_b, equalities, cache, eqpc2.get());
1763 [ + + ]: 4555028 : if (eqpc)
1764 : : {
1765 : 1946984 : eqpc->d_children.push_back(eqpc1);
1766 : 1946984 : eqpc->d_children.push_back(eqpc2);
1767 : : // build conclusion if ids correspond to non-internal nodes or
1768 : : // if non-internal nodes can be retrieved from them (in the
1769 : : // case of n-ary applications), otherwise leave conclusion as
1770 : : // null. This is only done for congruence kinds, since
1771 : : // congruence is not used otherwise.
1772 : 1946984 : Kind k = d_nodes[currentNode].getKind();
1773 [ + + ]: 1946984 : if (d_congruenceKinds[k])
1774 : : {
1775 : 1915998 : buildEqConclusion(currentNode, edgeNode, eqpc.get());
1776 : : }
1777 : : else
1778 : : {
1779 [ - + ][ - - ]: 61972 : Assert(k == Kind::EQUAL)
1780 [ - + ][ - + ]: 30986 : << "not an internal node " << d_nodes[currentNode]
[ - - ]
1781 : 0 : << " with non-congruence with " << k << "\n";
1782 : : }
1783 : : }
1784 [ + - ]: 4555028 : Trace("equality") << pop;
1785 : 4555028 : break;
1786 : 4555028 : }
1787 : :
1788 : 25536 : case MERGED_THROUGH_REFLEXIVITY:
1789 : : {
1790 : : // x1 == x1
1791 [ + - ]: 51072 : Trace("equality") << d_name
1792 : : << "::eq::getExplanation(): due to "
1793 : 0 : "reflexivity, going deeper"
1794 : 25536 : << std::endl;
1795 : 25536 : EqualityNodeId eqId =
1796 [ + + ]: 25536 : currentNode == d_trueId ? edgeNode : currentNode;
1797 : 25536 : const FunctionApplication& eq = d_applications[eqId].d_original;
1798 [ - + ][ - + ]: 25536 : Assert(eq.isEquality()) << "Must be an equality";
[ - - ]
1799 : :
1800 : : // Explain why a = b constant
1801 [ + - ]: 25536 : Trace("equality") << push;
1802 : : std::shared_ptr<EqProof> eqpc1 =
1803 [ + + ]: 25536 : eqpc ? std::make_shared<EqProof>() : nullptr;
1804 : 25536 : getExplanation(eq.d_a, eq.d_b, equalities, cache, eqpc1.get());
1805 [ + + ]: 25536 : if (eqpc)
1806 : : {
1807 : 8304 : eqpc->d_children.push_back(eqpc1);
1808 : : }
1809 [ + - ]: 25536 : Trace("equality") << pop;
1810 : :
1811 : 25536 : break;
1812 : 25536 : }
1813 : :
1814 : 47910 : case MERGED_THROUGH_CONSTANTS:
1815 : : {
1816 : : // f(c1, ..., cn) = c semantically, we can just ignore it
1817 [ + - ]: 95820 : Trace("equality") << d_name
1818 : : << "::eq::getExplanation(): due to "
1819 : 0 : "constants, explain the constants"
1820 : 47910 : << std::endl;
1821 [ + - ]: 47910 : Trace("equality") << push;
1822 : :
1823 : : // Get the node we interpreted
1824 : 47910 : TNode interpreted;
1825 [ + + ]: 47910 : if (eqpc)
1826 : : {
1827 : : // build the conclusion f(c1, ..., cn) = c
1828 [ + + ]: 19896 : if (d_nodes[currentNode].isConst())
1829 : : {
1830 : 9453 : interpreted = d_nodes[edgeNode];
1831 : 9453 : eqpc->d_node =
1832 : 18906 : d_nodes[edgeNode].eqNode(d_nodes[currentNode]);
1833 : : }
1834 : : else
1835 : : {
1836 : 10443 : interpreted = d_nodes[currentNode];
1837 : 10443 : eqpc->d_node =
1838 : 20886 : d_nodes[currentNode].eqNode(d_nodes[edgeNode]);
1839 : : }
1840 : : }
1841 : : else
1842 : : {
1843 : 28014 : interpreted = d_nodes[currentNode].isConst()
1844 : 10948 : ? d_nodes[edgeNode]
1845 [ + + ]: 38962 : : d_nodes[currentNode];
1846 : : }
1847 : :
1848 : : // Explain why a is a constant by explaining each argument
1849 [ + + ]: 140431 : for (unsigned i = 0; i < interpreted.getNumChildren(); ++i)
1850 : : {
1851 : 92521 : EqualityNodeId childId = getNodeId(interpreted[i]);
1852 [ - + ][ - + ]: 92521 : Assert(isConstant(childId));
[ - - ]
1853 : : std::shared_ptr<EqProof> eqpcc =
1854 [ + + ]: 92521 : eqpc ? std::make_shared<EqProof>() : nullptr;
1855 : 185042 : getExplanation(childId,
1856 : 92521 : getEqualityNode(childId).getFind(),
1857 : : equalities,
1858 : : cache,
1859 : : eqpcc.get());
1860 [ + + ]: 92521 : if (eqpc)
1861 : : {
1862 : 38758 : eqpc->d_children.push_back(eqpcc);
1863 [ - + ]: 38758 : if (TraceIsOn("pf::ee"))
1864 : : {
1865 [ - - ]: 0 : Trace("pf::ee")
1866 : 0 : << "MERGED_THROUGH_CONSTANTS. Dumping the child proof"
1867 : 0 : << std::endl;
1868 : 0 : eqpc->debug_print("pf::ee", 1);
1869 : : }
1870 : : }
1871 : 92521 : }
1872 : :
1873 [ + - ]: 47910 : Trace("equality") << pop;
1874 : 47910 : break;
1875 : 47910 : }
1876 : :
1877 : 4476222 : default:
1878 : : {
1879 : : // Construct the equality
1880 [ + - ]: 8952444 : Trace("equality")
1881 : 0 : << d_name << "::eq::getExplanation(): adding: " << reason
1882 : 4476222 : << std::endl;
1883 [ + - ]: 8952444 : Trace("equality")
1884 : 0 : << d_name
1885 : 0 : << "::eq::getExplanation(): reason type = " << reasonType
1886 : 4476222 : << "\n";
1887 : 4476222 : Node a = d_nodes[currentNode];
1888 : 4476222 : Node b = d_nodes[d_equalityEdges[currentEdge].getNodeId()];
1889 : :
1890 [ + + ]: 4476222 : if (eqpc)
1891 : : {
1892 [ + - ]: 1920446 : if (reasonType == MERGED_THROUGH_EQUALITY)
1893 : : {
1894 : : // in the new proof infrastructure we can assume that
1895 : : // "theory assumptions", which are a consequence of theory
1896 : : // reasoning on other assumptions, are externally justified.
1897 : : // In this case we can use (= a b) directly as the
1898 : : // conclusion here.
1899 : 1920446 : eqpc->d_node = b.eqNode(a);
1900 : : }
1901 : : else
1902 : : {
1903 : : // The LFSC translator prefers (not (= a b)) over (= (= a b)
1904 : : // false)
1905 : :
1906 [ - - ]: 0 : if (a == nodeManager()->mkConst(false))
1907 : : {
1908 : 0 : eqpc->d_node = b.notNode();
1909 : : }
1910 [ - - ]: 0 : else if (b == nodeManager()->mkConst(false))
1911 : : {
1912 : 0 : eqpc->d_node = a.notNode();
1913 : : }
1914 : : else
1915 : : {
1916 : 0 : eqpc->d_node = b.eqNode(a);
1917 : : }
1918 : : }
1919 : 1920446 : eqpc->d_id = reasonType;
1920 : : }
1921 : 4476222 : equalities.push_back(reason);
1922 : 4476222 : break;
1923 : 4476222 : }
1924 : : }
1925 : :
1926 : : // Go to the previous
1927 : 9104696 : currentEdge = bfsQueue[currentIndex].d_edgeId;
1928 : 9104696 : currentIndex = bfsQueue[currentIndex].d_previousIndex;
1929 : :
1930 : : //---from Morgan---
1931 [ + + ][ + + ]: 9104696 : if (eqpc != nullptr && eqpc->d_id == MERGED_THROUGH_REFLEXIVITY)
[ + + ]
1932 : : {
1933 [ + - ]: 8304 : if (eqpc->d_node.isNull())
1934 : : {
1935 [ - + ][ - + ]: 8304 : Assert(eqpc->d_children.size() == 1);
[ - - ]
1936 : 8304 : std::shared_ptr<EqProof> p = eqpc;
1937 : 8304 : eqpc = p->d_children[0];
1938 : 8304 : }
1939 : : else
1940 : : {
1941 : 0 : Assert(eqpc->d_children.empty());
1942 : : }
1943 : : }
1944 : : //---end from Morgan---
1945 : :
1946 : 9104696 : eqp_trans.push_back(eqpc);
1947 [ + + ]: 9104696 : } while (currentEdge != null_id);
1948 : :
1949 [ + + ]: 3870514 : if (eqp)
1950 : : {
1951 [ + + ]: 1693903 : if (eqp_trans.size() == 1)
1952 : : {
1953 : 682920 : *eqp = *eqp_trans[0];
1954 : : }
1955 : : else
1956 : : {
1957 : 1010983 : eqp->d_id = MERGED_THROUGH_TRANS;
1958 : 2021966 : eqp->d_children.insert(
1959 : 1010983 : eqp->d_children.end(), eqp_trans.begin(), eqp_trans.end());
1960 : : // build conclusion in case of equality between non-internal
1961 : : // nodes or of n-ary congruence kinds, otherwise leave as
1962 : : // null. The latter is necessary for the overall handling of
1963 : : // congruence proofs involving n-ary kinds, see
1964 : : // EqProof::reduceNestedCongruence for more details.
1965 : 1010983 : buildEqConclusion(t1Id, t2Id, eqp);
1966 : : }
1967 [ - + ]: 1693903 : if (TraceIsOn("pf::ee"))
1968 : : {
1969 : 0 : eqp->debug_print("pf::ee", 1);
1970 : : }
1971 : : }
1972 : :
1973 : : // Done
1974 : 3870514 : return;
1975 : 3870514 : }
1976 : :
1977 : : // Push to the visitation queue if it's not the backward edge
1978 : 35549448 : bfsQueue.push_back(
1979 : 71098896 : BfsData(edge.getNodeId(), currentEdge, currentIndex));
1980 : : }
1981 : :
1982 : : // Go to the next edge
1983 : 54110401 : currentEdge = edge.getNext();
1984 : : }
1985 : :
1986 : : // Go to the next node to visit
1987 : 19651208 : ++currentIndex;
1988 : 19651208 : }
1989 : 3870514 : }
1990 : :
1991 : 1621824 : void EqualityEngine::addTriggerEquality(TNode eq)
1992 : : {
1993 [ - + ][ - + ]: 1621824 : Assert(eq.getKind() == Kind::EQUAL);
[ - - ]
1994 : :
1995 [ + + ]: 1621824 : if (d_done)
1996 : : {
1997 : 23 : return;
1998 : : }
1999 : :
2000 : : // Add the terms
2001 : 1621801 : addTermInternal(eq[0]);
2002 : 1621801 : addTermInternal(eq[1]);
2003 : :
2004 : 1621801 : bool skipTrigger = false;
2005 : :
2006 : : // If they are equal or disequal already, no need for the trigger
2007 [ + + ]: 1621801 : if (areEqual(eq[0], eq[1]))
2008 : : {
2009 : 49100 : d_notify->eqNotifyTriggerPredicate(eq, true);
2010 : 49100 : skipTrigger = true;
2011 : : }
2012 [ + + ]: 1621801 : if (areDisequal(eq[0], eq[1], true))
2013 : : {
2014 : 22271 : d_notify->eqNotifyTriggerPredicate(eq, false);
2015 : 22271 : skipTrigger = true;
2016 : : }
2017 : :
2018 [ + + ]: 1621801 : if (skipTrigger)
2019 : : {
2020 : 71371 : return;
2021 : : }
2022 : :
2023 : : // Add the equality
2024 : 1550430 : addTermInternal(eq);
2025 : :
2026 : : // Positive trigger
2027 : 1550430 : addTriggerEqualityInternal(eq[0], eq[1], eq, true);
2028 : : // Negative trigger
2029 : 1550430 : addTriggerEqualityInternal(eq, d_false, eq, false);
2030 : : }
2031 : :
2032 : 1854569 : void EqualityEngine::addTriggerPredicate(TNode predicate)
2033 : : {
2034 [ - + ][ - + ]: 1854569 : Assert(predicate.getKind() != Kind::NOT);
[ - - ]
2035 [ + + ]: 1854569 : if (predicate.getKind() == Kind::EQUAL)
2036 : : {
2037 : : // equality is handled separately
2038 : 1621824 : return addTriggerEquality(predicate);
2039 : : }
2040 [ - + ][ - + ]: 232745 : Assert(d_congruenceKinds.test(predicate.getKind()))
[ - - ]
2041 : 0 : << "No point in adding non-congruence predicates, kind is "
2042 : : << predicate.getKind();
2043 : :
2044 [ + + ]: 232745 : if (d_done)
2045 : : {
2046 : 90 : return;
2047 : : }
2048 : :
2049 : : // Add the term
2050 : 232655 : addTermInternal(predicate);
2051 : :
2052 : 232655 : bool skipTrigger = false;
2053 : :
2054 : : // If it's know already, no need for the trigger
2055 [ + + ]: 232655 : if (areEqual(predicate, d_true))
2056 : : {
2057 : 14928 : d_notify->eqNotifyTriggerPredicate(predicate, true);
2058 : 14928 : skipTrigger = true;
2059 : : }
2060 [ + + ]: 232655 : if (areEqual(predicate, d_false))
2061 : : {
2062 : 4731 : d_notify->eqNotifyTriggerPredicate(predicate, false);
2063 : 4731 : skipTrigger = true;
2064 : : }
2065 : :
2066 [ + + ]: 232655 : if (skipTrigger)
2067 : : {
2068 : 19659 : return;
2069 : : }
2070 : :
2071 : : // Positive trigger
2072 : 212996 : addTriggerEqualityInternal(predicate, d_true, predicate, true);
2073 : : // Negative trigger
2074 : 212996 : addTriggerEqualityInternal(predicate, d_false, predicate, false);
2075 : : }
2076 : :
2077 : 3526852 : void EqualityEngine::addTriggerEqualityInternal(TNode t1,
2078 : : TNode t2,
2079 : : TNode trigger,
2080 : : bool polarity)
2081 : : {
2082 [ + - ]: 7053704 : Trace("equality") << d_name << "::eq::addTrigger(" << t1 << ", " << t2 << ", "
2083 : 3526852 : << trigger << ")" << std::endl;
2084 : :
2085 [ - + ][ - + ]: 3526852 : Assert(hasTerm(t1));
[ - - ]
2086 [ - + ][ - + ]: 3526852 : Assert(hasTerm(t2));
[ - - ]
2087 : :
2088 [ - + ]: 3526852 : if (d_done)
2089 : : {
2090 : 0 : return;
2091 : : }
2092 : :
2093 : : // Get the information about t1
2094 : 3526852 : EqualityNodeId t1Id = getNodeId(t1);
2095 : 3526852 : EqualityNodeId t1classId = getEqualityNode(t1Id).getFind();
2096 : : // We will attach it to the class representative, since then we know how to
2097 : : // backtrack it
2098 : 3526852 : TriggerId t1TriggerId = d_nodeTriggers[t1classId];
2099 : :
2100 : : // Get the information about t2
2101 : 3526852 : EqualityNodeId t2Id = getNodeId(t2);
2102 : 3526852 : EqualityNodeId t2classId = getEqualityNode(t2Id).getFind();
2103 : : // We will attach it to the class representative, since then we know how to
2104 : : // backtrack it
2105 : 3526852 : TriggerId t2TriggerId = d_nodeTriggers[t2classId];
2106 : :
2107 [ + - ]: 7053704 : Trace("equality") << d_name << "::eq::addTrigger(" << trigger << "): " << t1Id
2108 : 0 : << " (" << t1classId << ") = " << t2Id << " (" << t2classId
2109 : 3526852 : << ")" << std::endl;
2110 : :
2111 : : // Create the triggers
2112 : 3526852 : TriggerId t1NewTriggerId = d_equalityTriggers.size();
2113 : 3526852 : d_equalityTriggers.push_back(Trigger(t1classId, t1TriggerId));
2114 : 3526852 : d_equalityTriggersOriginal.push_back(TriggerInfo(trigger, polarity));
2115 : 3526852 : TriggerId t2NewTriggerId = d_equalityTriggers.size();
2116 : 3526852 : d_equalityTriggers.push_back(Trigger(t2classId, t2TriggerId));
2117 : 3526852 : d_equalityTriggersOriginal.push_back(TriggerInfo(trigger, polarity));
2118 : :
2119 : : // Update the counters
2120 : 3526852 : d_equalityTriggersCount = d_equalityTriggers.size();
2121 [ - + ][ - + ]: 3526852 : Assert(d_equalityTriggers.size() == d_equalityTriggersOriginal.size());
[ - - ]
2122 [ - + ][ - + ]: 3526852 : Assert(d_equalityTriggers.size() % 2 == 0);
[ - - ]
2123 : :
2124 : : // Add the trigger to the trigger graph
2125 : 3526852 : d_nodeTriggers[t1classId] = t1NewTriggerId;
2126 : 3526852 : d_nodeTriggers[t2classId] = t2NewTriggerId;
2127 : :
2128 [ - + ]: 3526852 : if (TraceIsOn("equality::internal"))
2129 : : {
2130 : 0 : debugPrintGraph();
2131 : : }
2132 : :
2133 [ + - ]: 7053704 : Trace("equality") << d_name << "::eq::addTrigger(" << t1 << "," << t2
2134 : 0 : << ") => (" << t1NewTriggerId << ", " << t2NewTriggerId
2135 : 3526852 : << ")" << std::endl;
2136 : : }
2137 : :
2138 : 888057 : Node EqualityEngine::evaluateTerm(TNode node)
2139 : : {
2140 [ + - ]: 1776114 : Trace("equality::evaluation")
2141 : 888057 : << d_name << "::eq::evaluateTerm(" << node << ")" << std::endl;
2142 : 888057 : NodeBuilder builder(nodeManager());
2143 : 888057 : builder << node.getKind();
2144 [ + + ]: 888057 : if (node.getMetaKind() == kind::metakind::PARAMETERIZED)
2145 : : {
2146 : 31 : builder << node.getOperator();
2147 : : }
2148 [ + + ]: 2121085 : for (unsigned i = 0; i < node.getNumChildren(); ++i)
2149 : : {
2150 : 1233028 : TNode child = node[i];
2151 : 1233028 : TNode childRep = getRepresentative(child);
2152 [ + - ]: 2466056 : Trace("equality::evaluation") << d_name << "::eq::evaluateTerm: " << child
2153 : 1233028 : << " -> " << childRep << std::endl;
2154 [ - + ][ - + ]: 1233028 : Assert(childRep.isConst());
[ - - ]
2155 : 1233028 : builder << childRep;
2156 : 1233028 : }
2157 : 888057 : Node newNode = builder;
2158 : 1776114 : return d_env.getRewriter()->rewrite(newNode);
2159 : 888057 : }
2160 : :
2161 : 527935 : void EqualityEngine::processEvaluationQueue()
2162 : : {
2163 [ + - ]: 1055870 : Trace("equality::evaluation")
2164 : 527935 : << d_name << "::eq::processEvaluationQueue(): start" << std::endl;
2165 : :
2166 [ + + ]: 1415992 : while (!d_evaluationQueue.empty())
2167 : : {
2168 : : // Get the node
2169 : 888057 : EqualityNodeId id = d_evaluationQueue.front();
2170 : 888057 : d_evaluationQueue.pop();
2171 : :
2172 : : // Replace the children with their representatives (must be constants)
2173 : 888057 : Node nodeEvaluated = evaluateTerm(d_nodes[id]);
2174 [ + - ]: 1776114 : Trace("equality::evaluation")
2175 : 0 : << d_name << "::eq::processEvaluationQueue(): " << d_nodes[id]
2176 : 888057 : << " evaluates to " << nodeEvaluated << std::endl;
2177 [ - + ][ - + ]: 888057 : Assert(nodeEvaluated.isConst());
[ - - ]
2178 : 888057 : addTermInternal(nodeEvaluated);
2179 : 888057 : EqualityNodeId nodeEvaluatedId = getNodeId(nodeEvaluated);
2180 : :
2181 : : // Enqueue the semantic equality
2182 : 888057 : enqueue(MergeCandidate(
2183 : 1776114 : id, nodeEvaluatedId, MERGED_THROUGH_CONSTANTS, TNode::null()));
2184 : 888057 : }
2185 : :
2186 [ + - ]: 1055870 : Trace("equality::evaluation")
2187 : 527935 : << d_name << "::eq::processEvaluationQueue(): done" << std::endl;
2188 : 527935 : }
2189 : :
2190 : 56780469 : void EqualityEngine::propagate()
2191 : : {
2192 [ + + ]: 56780469 : if (d_inPropagate)
2193 : : {
2194 : : // We're already in propagate, go back
2195 : 47669 : return;
2196 : : }
2197 : :
2198 : : // Make sure we don't get in again
2199 : 56732800 : ScopedBool inPropagate(d_inPropagate, true);
2200 : :
2201 [ + - ]: 56732800 : Trace("equality") << d_name << "::eq::propagate()" << std::endl;
2202 : :
2203 [ + + ][ + + ]: 132349761 : while (!d_propagationQueue.empty() || !d_evaluationQueue.empty())
[ + + ]
2204 : : {
2205 [ + + ]: 75616964 : if (d_done)
2206 : : {
2207 : : // If we're done, just empty the queue
2208 [ + + ]: 7837606 : while (!d_propagationQueue.empty()) d_propagationQueue.pop_front();
2209 [ + + ]: 195935 : while (!d_evaluationQueue.empty()) d_evaluationQueue.pop();
2210 : 12514549 : continue;
2211 : : }
2212 : :
2213 : : // Process any evaluation requests
2214 [ + + ]: 75432805 : if (!d_evaluationQueue.empty())
2215 : : {
2216 : 527935 : processEvaluationQueue();
2217 : 527935 : continue;
2218 : : }
2219 : :
2220 : : // The current merge candidate
2221 : 74904870 : const MergeCandidate current = d_propagationQueue.front();
2222 : 74904870 : d_propagationQueue.pop_front();
2223 : :
2224 : : // Get the representatives
2225 : 74904870 : EqualityNodeId t1classId = getEqualityNode(current.d_t1Id).getFind();
2226 : 74904870 : EqualityNodeId t2classId = getEqualityNode(current.d_t2Id).getFind();
2227 : :
2228 : : // If already the same, we're done
2229 [ + + ]: 74904870 : if (t1classId == t2classId)
2230 : : {
2231 : 11743765 : continue;
2232 : : }
2233 : :
2234 [ + - ]: 126322210 : Trace("equality::internal")
2235 : 0 : << d_name << "::eq::propagate(): t1: "
2236 [ - - ]: 63161105 : << (d_isInternal[t1classId] ? "internal" : "proper") << std::endl;
2237 [ + - ]: 126322210 : Trace("equality::internal")
2238 : 0 : << d_name << "::eq::propagate(): t2: "
2239 [ - - ]: 63161105 : << (d_isInternal[t2classId] ? "internal" : "proper") << std::endl;
2240 : :
2241 : : // Get the nodes of the representatives
2242 : 63161105 : EqualityNode& node1 = getEqualityNode(t1classId);
2243 : 63161105 : EqualityNode& node2 = getEqualityNode(t2classId);
2244 : :
2245 [ - + ][ - + ]: 63161105 : Assert(node1.getFind() == t1classId);
[ - - ]
2246 [ - + ][ - + ]: 63161105 : Assert(node2.getFind() == t2classId);
[ - - ]
2247 : :
2248 : : // Add the actual equality to the equality graph
2249 : 126322210 : addGraphEdge(
2250 : 63161105 : current.d_t1Id, current.d_t2Id, current.d_type, current.d_reason);
2251 : :
2252 : : // If constants are being merged we're done
2253 [ + + ][ + + ]: 63161105 : if (d_isConstant[t1classId] && d_isConstant[t2classId])
[ + + ]
2254 : : {
2255 : : // When merging constants we are inconsistent, hence done
2256 : 58690 : d_done = true;
2257 : : // But in order to keep invariants (edges = 2*equalities) we put an
2258 : : // equalities in Note that we can explain this merge as we have a graph
2259 : : // edge
2260 : 58690 : d_assertedEqualities.push_back(Equality(null_id, null_id));
2261 : 58690 : d_assertedEqualitiesCount = d_assertedEqualitiesCount + 1;
2262 : : // Notify
2263 : 58690 : d_notify->eqNotifyConstantTermMerge(d_nodes[t1classId],
2264 : 58690 : d_nodes[t2classId]);
2265 : : // Empty the queue and exit
2266 : 58690 : continue;
2267 : : }
2268 : :
2269 : : // Vector to collect the triggered events
2270 : 63102415 : std::vector<TriggerId> triggers;
2271 : :
2272 : : // Figure out the merge preference
2273 : 63102415 : EqualityNodeId mergeInto = t1classId;
2274 [ + + ]: 63102415 : if (d_isInternal[t2classId] != d_isInternal[t1classId])
2275 : : {
2276 : : // We always keep non-internal nodes as representatives: if any node in
2277 : : // the class is non-internal, then the representative will be non-internal
2278 [ + + ]: 95904 : if (d_isInternal[t1classId])
2279 : : {
2280 : 56884 : mergeInto = t2classId;
2281 : : }
2282 : : else
2283 : : {
2284 : 39020 : mergeInto = t1classId;
2285 : : }
2286 : : }
2287 [ + + ]: 63006511 : else if (d_isConstant[t2classId] != d_isConstant[t1classId])
2288 : : {
2289 : : // We always keep constants as representatives: if any (at most one) node
2290 : : // in the class in a constant, then the representative will be a constant
2291 [ + + ]: 44296500 : if (d_isConstant[t2classId])
2292 : : {
2293 : 38970170 : mergeInto = t2classId;
2294 : : }
2295 : : else
2296 : : {
2297 : 5326330 : mergeInto = t1classId;
2298 : : }
2299 : : }
2300 [ + + ]: 18710011 : else if (node2.getSize() > node1.getSize())
2301 : : {
2302 : : // We always merge into the bigger class to reduce the amount of
2303 : : // traversing we need to do
2304 : 8109040 : mergeInto = t2classId;
2305 : : }
2306 : :
2307 [ + + ]: 63102415 : if (mergeInto == t2classId)
2308 : : {
2309 [ + - ]: 94272188 : Trace("equality") << d_name << "::eq::propagate(): merging "
2310 : 0 : << d_nodes[current.d_t1Id] << " into "
2311 : 47136094 : << d_nodes[current.d_t2Id] << std::endl;
2312 : 47136094 : d_assertedEqualities.push_back(Equality(t2classId, t1classId));
2313 : 47136094 : d_assertedEqualitiesCount = d_assertedEqualitiesCount + 1;
2314 [ + + ]: 47136094 : if (!merge(node2, node1, triggers))
2315 : : {
2316 : 13076 : d_done = true;
2317 : : }
2318 : : }
2319 : : else
2320 : : {
2321 [ + - ]: 31932642 : Trace("equality") << d_name << "::eq::propagate(): merging "
2322 : 0 : << d_nodes[current.d_t2Id] << " into "
2323 : 15966321 : << d_nodes[current.d_t1Id] << std::endl;
2324 : 15966321 : d_assertedEqualities.push_back(Equality(t1classId, t2classId));
2325 : 15966321 : d_assertedEqualitiesCount = d_assertedEqualitiesCount + 1;
2326 [ + + ]: 15966321 : if (!merge(node1, node2, triggers))
2327 : : {
2328 : 15482 : d_done = true;
2329 : : }
2330 : : }
2331 : :
2332 : : // If not merging internal nodes, notify the master
2333 [ + + ]: 16068618 : if (d_masterEqualityEngine && !d_isInternal[t1classId]
2334 [ + + ][ + + ]: 79171030 : && !d_isInternal[t2classId])
[ + + ]
2335 : : {
2336 : 27947598 : d_masterEqualityEngine->assertEqualityInternal(
2337 : 41921397 : d_nodes[t1classId], d_nodes[t2classId], TNode::null());
2338 : 13973799 : d_masterEqualityEngine->propagate();
2339 : : }
2340 : :
2341 : : // Notify the triggers
2342 [ + + ]: 63102412 : if (!d_done)
2343 : : {
2344 : 87716894 : for (size_t trigger_i = 0, trigger_end = triggers.size();
2345 [ + + ][ + + ]: 87716894 : trigger_i < trigger_end && !d_done;
[ + + ]
2346 : : ++trigger_i)
2347 : : {
2348 : : const TriggerInfo& triggerInfo =
2349 : 24643040 : d_equalityTriggersOriginal[triggers[trigger_i]];
2350 [ + + ]: 24643040 : if (triggerInfo.d_trigger.getKind() == Kind::EQUAL)
2351 : : {
2352 : : // Special treatment for disequalities
2353 [ + + ]: 21199773 : if (!triggerInfo.d_polarity)
2354 : : {
2355 : : // Store that we are propagating a diseauality
2356 : 10709008 : TNode equality = triggerInfo.d_trigger;
2357 : 10709008 : EqualityNodeId original = getNodeId(equality);
2358 : 10709008 : TNode lhs = equality[0];
2359 : 10709008 : TNode rhs = equality[1];
2360 : 10709008 : EqualityNodeId lhsId = getNodeId(lhs);
2361 : 10709008 : EqualityNodeId rhsId = getNodeId(rhs);
2362 : : // We use the THEORY_LAST as a marker for "marked as propagated,
2363 : : // reasons stored". This tag is added to an internal theories set
2364 : : // that is only inserted in, so this is safe. Had we iterated over,
2365 : : // or done other set operations this might be dangerous.
2366 [ + + ]: 10709008 : if (!hasPropagatedDisequality(THEORY_LAST, lhsId, rhsId))
2367 : : {
2368 [ + + ]: 10708203 : if (!hasPropagatedDisequality(lhsId, rhsId))
2369 : : {
2370 : 10673642 : d_deducedDisequalityReasons.push_back(
2371 : 21347284 : EqualityPair(original, d_falseId));
2372 : : }
2373 : 10708203 : storePropagatedDisequality(THEORY_LAST, lhsId, rhsId);
2374 [ + + ]: 10708203 : if (!d_notify->eqNotifyTriggerPredicate(triggerInfo.d_trigger,
2375 : 10708203 : triggerInfo.d_polarity))
2376 : : {
2377 : 4061 : d_done = true;
2378 : : }
2379 : : }
2380 : 10709008 : }
2381 : : else
2382 : : {
2383 : : // Equalities are simple
2384 [ + + ]: 10490765 : if (!d_notify->eqNotifyTriggerPredicate(triggerInfo.d_trigger,
2385 : 10490765 : triggerInfo.d_polarity))
2386 : : {
2387 : 120887 : d_done = true;
2388 : : }
2389 : : }
2390 : : }
2391 : : else
2392 : : {
2393 [ + + ]: 3443267 : if (!d_notify->eqNotifyTriggerPredicate(triggerInfo.d_trigger,
2394 : 3443267 : triggerInfo.d_polarity))
2395 : : {
2396 : 3154 : d_done = true;
2397 : : }
2398 : : }
2399 : : }
2400 : : }
2401 [ + + ]: 74904873 : }
2402 : 56732800 : }
2403 : :
2404 : 0 : void EqualityEngine::debugPrintGraph() const
2405 : : {
2406 [ - - ]: 0 : Trace("equality::internal") << std::endl << "Dumping graph" << std::endl;
2407 [ - - ]: 0 : for (EqualityNodeId nodeId = 0; nodeId < d_nodes.size(); ++nodeId)
2408 : : {
2409 [ - - ]: 0 : Trace("equality::internal") << d_nodes[nodeId] << " " << nodeId << "("
2410 : 0 : << getEqualityNode(nodeId).getFind() << "):";
2411 : :
2412 : 0 : EqualityEdgeId edgeId = d_equalityGraph[nodeId];
2413 [ - - ]: 0 : while (edgeId != null_edge)
2414 : : {
2415 : 0 : const EqualityEdge& edge = d_equalityEdges[edgeId];
2416 [ - - ]: 0 : Trace("equality::internal")
2417 : 0 : << " [" << edge.getNodeId() << "] " << d_nodes[edge.getNodeId()]
2418 : 0 : << ":" << edge.getReason();
2419 : 0 : edgeId = edge.getNext();
2420 : : }
2421 : :
2422 [ - - ]: 0 : Trace("equality::internal") << std::endl;
2423 : : }
2424 [ - - ]: 0 : Trace("equality::internal") << std::endl;
2425 : 0 : }
2426 : :
2427 : 0 : std::string EqualityEngine::debugPrintEqc() const
2428 : : {
2429 : 0 : std::stringstream ss;
2430 : 0 : eq::EqClassesIterator eqcs2_i = eq::EqClassesIterator(this);
2431 [ - - ]: 0 : while (!eqcs2_i.isFinished())
2432 : : {
2433 : 0 : Node eqc = (*eqcs2_i);
2434 : 0 : eq::EqClassIterator eqc2_i = eq::EqClassIterator(eqc, this);
2435 : 0 : ss << "Eqc( " << eqc << " ) : { ";
2436 [ - - ]: 0 : while (!eqc2_i.isFinished())
2437 : : {
2438 : 0 : if ((*eqc2_i) != eqc && (*eqc2_i).getKind() != Kind::EQUAL)
2439 : : {
2440 : 0 : ss << (*eqc2_i) << " ";
2441 : : }
2442 : 0 : ++eqc2_i;
2443 : : }
2444 : 0 : ss << " } " << std::endl;
2445 : 0 : ++eqcs2_i;
2446 : 0 : }
2447 : 0 : return ss.str();
2448 : 0 : }
2449 : :
2450 : 62256602 : bool EqualityEngine::areEqual(TNode t1, TNode t2) const
2451 : : {
2452 [ + - ]: 62256602 : Trace("equality") << d_name << "::eq::areEqual(" << t1 << "," << t2 << ")";
2453 : :
2454 [ - + ][ - + ]: 62256602 : Assert(hasTerm(t1));
[ - - ]
2455 [ - + ][ - + ]: 62256602 : Assert(hasTerm(t2));
[ - - ]
2456 : :
2457 : 62256602 : bool result = getEqualityNode(t1).getFind() == getEqualityNode(t2).getFind();
2458 [ + - ][ - - ]: 62256602 : Trace("equality") << (result ? "\t(YES)" : "\t(NO)") << std::endl;
2459 : 62256602 : return result;
2460 : : }
2461 : :
2462 : 22853014 : bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const
2463 : : {
2464 [ + - ]: 22853014 : Trace("equality") << d_name << "::eq::areDisequal(" << t1 << "," << t2 << ")";
2465 : :
2466 : : // Add the terms
2467 [ - + ][ - + ]: 22853014 : Assert(hasTerm(t1));
[ - - ]
2468 [ - + ][ - + ]: 22853014 : Assert(hasTerm(t2));
[ - - ]
2469 : :
2470 : : // Get ids
2471 : 22853014 : EqualityNodeId t1Id = getNodeId(t1);
2472 : 22853014 : EqualityNodeId t2Id = getNodeId(t2);
2473 : :
2474 : : // If we propagated this disequality we're true
2475 [ + + ]: 22853014 : if (hasPropagatedDisequality(t1Id, t2Id))
2476 : : {
2477 [ + - ]: 7633949 : Trace("equality") << "\t(YES)" << std::endl;
2478 : 7633949 : return true;
2479 : : }
2480 : :
2481 : : // Get equivalence classes
2482 : 15219065 : EqualityNodeId t1ClassId = getEqualityNode(t1Id).getFind();
2483 : 15219065 : EqualityNodeId t2ClassId = getEqualityNode(t2Id).getFind();
2484 : :
2485 : : // We are semantically const, for remembering stuff
2486 : 15219065 : EqualityEngine* nonConst = const_cast<EqualityEngine*>(this);
2487 : :
2488 : : // Check for constants
2489 [ + + ]: 19847676 : if (d_isConstant[t1ClassId] && d_isConstant[t2ClassId]
2490 [ + + ][ + + ]: 19847676 : && t1ClassId != t2ClassId)
[ + + ]
2491 : : {
2492 [ + + ]: 115691 : if (ensureProof)
2493 : : {
2494 : 13497 : nonConst->d_deducedDisequalityReasons.push_back(
2495 : 0 : EqualityPair(t1Id, t1ClassId));
2496 : 13497 : nonConst->d_deducedDisequalityReasons.push_back(
2497 : 0 : EqualityPair(t2Id, t2ClassId));
2498 : 13497 : nonConst->storePropagatedDisequality(THEORY_LAST, t1Id, t2Id);
2499 : : }
2500 [ + - ]: 115691 : Trace("equality") << "\t(YES)" << std::endl;
2501 : 115691 : return true;
2502 : : }
2503 : :
2504 : : // Create the equality
2505 : 15103374 : FunctionApplication eqNormalized(APP_EQUALITY, t1ClassId, t2ClassId);
2506 : : ApplicationIdsMap::const_iterator find =
2507 : 15103374 : d_applicationLookup.find(eqNormalized);
2508 [ + + ]: 15103374 : if (find != d_applicationLookup.end())
2509 : : {
2510 : 6230448 : if (getEqualityNode(find->second).getFind()
2511 [ + + ]: 6230448 : == getEqualityNode(d_falseId).getFind())
2512 : : {
2513 [ + + ]: 742317 : if (ensureProof)
2514 : : {
2515 : : const FunctionApplication original =
2516 : 8514 : d_applications[find->second].d_original;
2517 : 8514 : nonConst->d_deducedDisequalityReasons.push_back(
2518 : 8514 : EqualityPair(t1Id, original.d_a));
2519 : 8514 : nonConst->d_deducedDisequalityReasons.push_back(
2520 : 8514 : EqualityPair(find->second, d_falseId));
2521 : 8514 : nonConst->d_deducedDisequalityReasons.push_back(
2522 : 8514 : EqualityPair(t2Id, original.d_b));
2523 : 8514 : nonConst->storePropagatedDisequality(THEORY_LAST, t1Id, t2Id);
2524 : : }
2525 [ + - ]: 742317 : Trace("equality") << "\t(YES)" << std::endl;
2526 : 742317 : return true;
2527 : : }
2528 : : }
2529 : :
2530 : : // Check the symmetric disequality
2531 : 14361057 : std::swap(eqNormalized.d_a, eqNormalized.d_b);
2532 : 14361057 : find = d_applicationLookup.find(eqNormalized);
2533 [ + + ]: 14361057 : if (find != d_applicationLookup.end())
2534 : : {
2535 : 1257763 : if (getEqualityNode(find->second).getFind()
2536 [ + + ]: 1257763 : == getEqualityNode(d_falseId).getFind())
2537 : : {
2538 [ + + ]: 968611 : if (ensureProof)
2539 : : {
2540 : : const FunctionApplication original =
2541 : 3724 : d_applications[find->second].d_original;
2542 : 3724 : nonConst->d_deducedDisequalityReasons.push_back(
2543 : 3724 : EqualityPair(t2Id, original.d_a));
2544 : 3724 : nonConst->d_deducedDisequalityReasons.push_back(
2545 : 3724 : EqualityPair(find->second, d_falseId));
2546 : 3724 : nonConst->d_deducedDisequalityReasons.push_back(
2547 : 3724 : EqualityPair(t1Id, original.d_b));
2548 : 3724 : nonConst->storePropagatedDisequality(THEORY_LAST, t1Id, t2Id);
2549 : : }
2550 [ + - ]: 968611 : Trace("equality") << "\t(YES)" << std::endl;
2551 : 968611 : return true;
2552 : : }
2553 : : }
2554 : :
2555 : : // Couldn't deduce dis-equalityReturn whether the terms are disequal
2556 [ + - ]: 13392446 : Trace("equality") << "\t(NO)" << std::endl;
2557 : 13392446 : return false;
2558 : : }
2559 : :
2560 : 0 : size_t EqualityEngine::getSize(TNode t)
2561 : : {
2562 : : // Add the term
2563 : 0 : addTermInternal(t);
2564 : 0 : return getEqualityNode(getEqualityNode(t).getFind()).getSize();
2565 : : }
2566 : :
2567 : 220032 : std::string EqualityEngine::identify() const { return d_name; }
2568 : :
2569 : 7819244 : void EqualityEngine::addTriggerTerm(TNode t, TheoryId tag)
2570 : : {
2571 [ + - ]: 15638488 : Trace("equality::trigger") << d_name << "::eq::addTriggerTerm(" << t << ", "
2572 : 7819244 : << tag << ")" << std::endl;
2573 : :
2574 [ - + ][ - + ]: 7819244 : Assert(tag != THEORY_LAST);
[ - - ]
2575 : :
2576 [ + + ]: 7819244 : if (d_done)
2577 : : {
2578 : 3 : return;
2579 : : }
2580 : :
2581 : : // Add the term if it's not already there
2582 : 7819241 : addTermInternal(t);
2583 : :
2584 [ - + ]: 7819241 : if (!d_anyTermsAreTriggers)
2585 : : {
2586 : : // if we are not using triggers, we only add the term, but not as a trigger
2587 : 0 : return;
2588 : : }
2589 : :
2590 : : // Get the node id
2591 : 7819241 : EqualityNodeId eqNodeId = getNodeId(t);
2592 : 7819241 : EqualityNode& eqNode = getEqualityNode(eqNodeId);
2593 : 7819241 : EqualityNodeId classId = eqNode.getFind();
2594 : :
2595 : : // Possibly existing set of triggers
2596 : 7819241 : TriggerTermSetRef triggerSetRef = d_nodeIndividualTrigger[classId];
2597 : 7819241 : if (triggerSetRef != +null_set_id
2598 [ + + ][ + + ]: 7819241 : && getTriggerTermSet(triggerSetRef).hasTrigger(tag))
[ + + ]
2599 : : {
2600 : : // If the term already is in the equivalence class that a tagged
2601 : : // representative, just notify
2602 : 2133415 : EqualityNodeId triggerId = getTriggerTermSet(triggerSetRef).getTrigger(tag);
2603 [ + - ]: 4266830 : Trace("equality::trigger")
2604 : 0 : << d_name << "::eq::addTriggerTerm(" << t << ", " << tag
2605 : 0 : << "): already have this trigger in class with " << d_nodes[triggerId]
2606 : 2133415 : << std::endl;
2607 : 2133415 : if (eqNodeId != triggerId
2608 : 2133415 : && !notifyTriggerTermEquality(tag, t, d_nodes[triggerId], true))
2609 : : {
2610 : 1908 : d_done = true;
2611 : : }
2612 : : }
2613 : : else
2614 : : {
2615 : : // Check for disequalities by going through the equivalence class looking
2616 : : // for equalities in the uselists that have been asserted to false. All the
2617 : : // representatives appearing on the other side of such disequalities, that
2618 : : // have the tag on, are put in a set.
2619 : 5685826 : TaggedEqualitiesSet disequalitiesToNotify;
2620 : 5685826 : TheoryIdSet tags = TheoryIdSetUtil::setInsert(tag);
2621 : 5685826 : getDisequalities(
2622 : 5685826 : !d_isConstant[classId], classId, tags, disequalitiesToNotify);
2623 : :
2624 : : // Trigger data
2625 : : TheoryIdSet newSetTags;
2626 : : EqualityNodeId newSetTriggers[THEORY_LAST];
2627 : : unsigned newSetTriggersSize;
2628 : :
2629 : : // Setup the data for the new set
2630 [ + + ]: 5685826 : if (triggerSetRef != null_set_id)
2631 : : {
2632 : : // Get the existing set
2633 : 1309432 : TriggerTermSet& triggerSet = getTriggerTermSet(triggerSetRef);
2634 : : // Initialize the new set for copy/insert
2635 : 1309432 : newSetTags = TheoryIdSetUtil::setInsert(tag, triggerSet.d_tags);
2636 : 1309432 : newSetTriggersSize = 0;
2637 : : // Copy into to new one, and insert the new tag/id
2638 : 1309432 : unsigned i = 0;
2639 : 1309432 : TheoryIdSet tags2 = newSetTags;
2640 : : TheoryId current;
2641 [ + + ]: 3973185 : while ((current = TheoryIdSetUtil::setPop(tags2)) != THEORY_LAST)
2642 : : {
2643 : : // Remove from the tags
2644 : 2663753 : tags2 = TheoryIdSetUtil::setRemove(current, tags2);
2645 : : // Insert the id into the triggers
2646 : 2663753 : newSetTriggers[newSetTriggersSize++] =
2647 [ + + ]: 2663753 : current == tag ? eqNodeId : triggerSet.d_triggers[i++];
2648 : : }
2649 : : }
2650 : : else
2651 : : {
2652 : : // Setup a singleton
2653 : 4376394 : newSetTags = TheoryIdSetUtil::setInsert(tag);
2654 : 4376394 : newSetTriggers[0] = eqNodeId;
2655 : 4376394 : newSetTriggersSize = 1;
2656 : : }
2657 : :
2658 : : // Add it to the list for backtracking
2659 : 5685826 : d_triggerTermSetUpdates.push_back(TriggerSetUpdate(classId, triggerSetRef));
2660 : 5685826 : d_triggerTermSetUpdatesSize = d_triggerTermSetUpdatesSize + 1;
2661 : : // Mark the the new set as a trigger
2662 : 11371652 : d_nodeIndividualTrigger[classId] = triggerSetRef =
2663 : 5685826 : newTriggerTermSet(newSetTags, newSetTriggers, newSetTriggersSize);
2664 : :
2665 : : // Propagate trigger term disequalities we remembered
2666 [ + - ]: 11371652 : Trace("equality::trigger")
2667 : 0 : << d_name << "::eq::addTriggerTerm(" << t << ", " << tag
2668 : 5685826 : << "): propagating " << disequalitiesToNotify.size()
2669 : 5685826 : << " disequalities " << std::endl;
2670 : 5685826 : propagateTriggerTermDisequalities(
2671 : : tags, triggerSetRef, disequalitiesToNotify);
2672 : 5685826 : }
2673 : : }
2674 : :
2675 : 13591295 : bool EqualityEngine::isTriggerTerm(TNode t, TheoryId tag) const
2676 : : {
2677 [ + + ]: 13591295 : if (!hasTerm(t)) return false;
2678 : 13591186 : EqualityNodeId classId = getEqualityNode(t).getFind();
2679 : 13591186 : TriggerTermSetRef triggerSetRef = d_nodeIndividualTrigger[classId];
2680 : : return triggerSetRef != +null_set_id
2681 [ + + ][ + - ]: 13591186 : && getTriggerTermSet(triggerSetRef).hasTrigger(tag);
2682 : : }
2683 : :
2684 : 4519396 : TNode EqualityEngine::getTriggerTermRepresentative(TNode t, TheoryId tag) const
2685 : : {
2686 [ - + ][ - + ]: 4519396 : Assert(isTriggerTerm(t, tag));
[ - - ]
2687 : 4519396 : EqualityNodeId classId = getEqualityNode(t).getFind();
2688 : : const TriggerTermSet& triggerSet =
2689 : 4519396 : getTriggerTermSet(d_nodeIndividualTrigger[classId]);
2690 : 4519396 : unsigned i = 0;
2691 : 4519396 : TheoryIdSet tags = triggerSet.d_tags;
2692 [ + + ]: 7847172 : while (TheoryIdSetUtil::setPop(tags) != tag)
2693 : : {
2694 : 3327776 : ++i;
2695 : : }
2696 : 9038792 : return d_nodes[triggerSet.d_triggers[i]];
2697 : : }
2698 : :
2699 : 31275781 : void EqualityEngine::storeApplicationLookup(FunctionApplication& funNormalized,
2700 : : EqualityNodeId funId)
2701 : : {
2702 [ - + ][ - + ]: 31275781 : Assert(d_applicationLookup.find(funNormalized) == d_applicationLookup.end());
[ - - ]
2703 : 31275781 : d_applicationLookup[funNormalized] = funId;
2704 : 31275781 : d_applicationLookups.push_back(funNormalized);
2705 : 31275781 : d_applicationLookupsCount = d_applicationLookupsCount + 1;
2706 [ + - ]: 62551562 : Trace("equality::backtrack")
2707 : 0 : << "d_applicationLookupsCount = " << d_applicationLookupsCount
2708 : 31275781 : << std::endl;
2709 [ + - ]: 62551562 : Trace("equality::backtrack")
2710 : 31275781 : << "d_applicationLookups.size() = " << d_applicationLookups.size()
2711 : 31275781 : << std::endl;
2712 [ - + ][ - + ]: 31275781 : Assert(d_applicationLookupsCount == d_applicationLookups.size());
[ - - ]
2713 : :
2714 : : // If an equality over constants we merge to false
2715 [ + + ]: 31275781 : if (funNormalized.isEquality())
2716 : : {
2717 [ + + ]: 23918641 : if (funNormalized.d_a == funNormalized.d_b)
2718 : : {
2719 : 2470496 : enqueue(MergeCandidate(
2720 : 4940992 : funId, d_trueId, MERGED_THROUGH_REFLEXIVITY, TNode::null()));
2721 : : }
2722 [ + + ][ + + ]: 21448145 : else if (d_isConstant[funNormalized.d_a] && d_isConstant[funNormalized.d_b])
[ + + ]
2723 : : {
2724 : 1733054 : enqueue(MergeCandidate(
2725 : 3466108 : funId, d_falseId, MERGED_THROUGH_CONSTANTS, TNode::null()));
2726 : : }
2727 : : }
2728 : 31275781 : }
2729 : :
2730 : 10747084 : EqualityEngine::TriggerTermSetRef EqualityEngine::newTriggerTermSet(
2731 : : TheoryIdSet newSetTags,
2732 : : EqualityNodeId* newSetTriggers,
2733 : : unsigned newSetTriggersSize)
2734 : : {
2735 : : // Size of the required set
2736 : 10747084 : size_t size =
2737 : 10747084 : sizeof(TriggerTermSet) + newSetTriggersSize * sizeof(EqualityNodeId);
2738 : : // Align the size
2739 : 10747084 : size = (size + 7) & ~((size_t)7);
2740 : : // Reallocate if necessary
2741 [ - + ]: 10747084 : if (d_triggerDatabaseSize + size > d_triggerDatabaseAllocatedSize)
2742 : : {
2743 : 0 : d_triggerDatabaseAllocatedSize *= 2;
2744 : 0 : d_triggerDatabase =
2745 : 0 : (char*)realloc(d_triggerDatabase, d_triggerDatabaseAllocatedSize);
2746 : : }
2747 : : // New reference
2748 : 10747084 : TriggerTermSetRef newTriggerSetRef = d_triggerDatabaseSize;
2749 : : // Update the size
2750 : 10747084 : d_triggerDatabaseSize = d_triggerDatabaseSize + size;
2751 : : // Copy the information
2752 : 10747084 : TriggerTermSet& newSet = getTriggerTermSet(newTriggerSetRef);
2753 : 10747084 : newSet.d_tags = newSetTags;
2754 [ + + ]: 88467328 : for (unsigned i = 0; i < newSetTriggersSize; ++i)
2755 : : {
2756 : 77720244 : newSet.d_triggers[i] = newSetTriggers[i];
2757 : : }
2758 : : // Return the new reference
2759 : 10747084 : return newTriggerSetRef;
2760 : : }
2761 : :
2762 : 37418755 : bool EqualityEngine::hasPropagatedDisequality(EqualityNodeId lhsId,
2763 : : EqualityNodeId rhsId) const
2764 : : {
2765 : 37418755 : EqualityPair eq(lhsId, rhsId);
2766 : : bool propagated =
2767 : 37418755 : d_propagatedDisequalities.find(eq) != d_propagatedDisequalities.end();
2768 : : #ifdef CVC5_ASSERTIONS
2769 : : bool stored =
2770 : 37418755 : d_disequalityReasonsMap.find(eq) != d_disequalityReasonsMap.end();
2771 [ - + ][ - + ]: 37418755 : Assert(propagated == stored) << "These two should be in sync";
[ - - ]
2772 : : #endif
2773 [ + - ]: 74837510 : Trace("equality::disequality")
2774 : 0 : << d_name << "::eq::hasPropagatedDisequality(" << d_nodes[lhsId] << ", "
2775 [ - - ]: 37418755 : << d_nodes[rhsId] << ") => " << (propagated ? "true" : "false")
2776 : 37418755 : << std::endl;
2777 : 37418755 : return propagated;
2778 : : }
2779 : :
2780 : 31418194 : bool EqualityEngine::hasPropagatedDisequality(TheoryId tag,
2781 : : EqualityNodeId lhsId,
2782 : : EqualityNodeId rhsId) const
2783 : : {
2784 : 31418194 : EqualityPair eq(lhsId, rhsId);
2785 : :
2786 : : PropagatedDisequalitiesMap::const_iterator it =
2787 : 31418194 : d_propagatedDisequalities.find(eq);
2788 [ + + ]: 31418194 : if (it == d_propagatedDisequalities.end())
2789 : : {
2790 [ - + ][ - + ]: 24986607 : Assert(d_disequalityReasonsMap.find(eq) == d_disequalityReasonsMap.end())
[ - - ]
2791 : 0 : << "Why do we have a proof if not propagated";
2792 [ + - ]: 49973214 : Trace("equality::disequality")
2793 : 0 : << d_name << "::eq::hasPropagatedDisequality(" << tag << ", "
2794 : 0 : << d_nodes[lhsId] << ", " << d_nodes[rhsId] << ") => false"
2795 : 24986607 : << std::endl;
2796 : 24986607 : return false;
2797 : : }
2798 [ - + ][ - + ]: 6431587 : Assert(d_disequalityReasonsMap.find(eq) != d_disequalityReasonsMap.end())
[ - - ]
2799 : 0 : << "We propagated but there is no proof";
2800 : 6431587 : bool result = TheoryIdSetUtil::setContains(tag, (*it).second);
2801 [ + - ]: 12863174 : Trace("equality::disequality")
2802 : 0 : << d_name << "::eq::hasPropagatedDisequality(" << tag << ", "
2803 : 0 : << d_nodes[lhsId] << ", " << d_nodes[rhsId] << ") => "
2804 [ - - ]: 6431587 : << (result ? "true" : "false") << std::endl;
2805 : 6431587 : return result;
2806 : : }
2807 : :
2808 : 14591476 : void EqualityEngine::storePropagatedDisequality(TheoryId tag,
2809 : : EqualityNodeId lhsId,
2810 : : EqualityNodeId rhsId)
2811 : : {
2812 [ - + ][ - + ]: 14591476 : Assert(!hasPropagatedDisequality(tag, lhsId, rhsId))
[ - - ]
2813 : 0 : << "Check before you store it";
2814 [ - + ][ - + ]: 14591476 : Assert(lhsId != rhsId) << "Wow, wtf!";
[ - - ]
2815 : :
2816 [ + - ]: 29182952 : Trace("equality::disequality")
2817 : 0 : << d_name << "::eq::storePropagatedDisequality(" << tag << ", "
2818 : 14591476 : << d_nodes[lhsId] << ", " << d_nodes[rhsId] << ")" << std::endl;
2819 : :
2820 : 14591476 : EqualityPair pair1(lhsId, rhsId);
2821 : 14591476 : EqualityPair pair2(rhsId, lhsId);
2822 : :
2823 : : // Store the fact that we've propagated this already
2824 : 14591476 : TheoryIdSet notified = 0;
2825 : : PropagatedDisequalitiesMap::const_iterator find =
2826 : 14591476 : d_propagatedDisequalities.find(pair1);
2827 [ + + ]: 14591476 : if (find == d_propagatedDisequalities.end())
2828 : : {
2829 : 12506171 : notified = TheoryIdSetUtil::setInsert(tag);
2830 : : }
2831 : : else
2832 : : {
2833 : 2085305 : notified = TheoryIdSetUtil::setInsert(tag, (*find).second);
2834 : : }
2835 : 14591476 : d_propagatedDisequalities[pair1] = notified;
2836 : 14591476 : d_propagatedDisequalities[pair2] = notified;
2837 : :
2838 : : // Store the proof if provided
2839 [ + + ]: 14591476 : if (d_deducedDisequalityReasons.size() > d_deducedDisequalityReasonsSize)
2840 : : {
2841 [ + - ]: 25012342 : Trace("equality::disequality")
2842 : 0 : << d_name << "::eq::storePropagatedDisequality(" << tag << ", "
2843 : 0 : << d_nodes[lhsId] << ", " << d_nodes[rhsId] << "): storing proof"
2844 : 12506171 : << std::endl;
2845 [ - + ][ - + ]: 12506171 : Assert(d_disequalityReasonsMap.find(pair1) == d_disequalityReasonsMap.end())
[ - - ]
2846 : 0 : << "There can't be a proof if you're adding a new one";
2847 : : DisequalityReasonRef ref(d_deducedDisequalityReasonsSize,
2848 : 12506171 : d_deducedDisequalityReasons.size());
2849 : : #ifdef CVC5_ASSERTIONS
2850 : : // Check that the reasons are valid
2851 [ + + ]: 28663903 : for (unsigned i = ref.d_mergesStart; i < ref.d_mergesEnd; ++i)
2852 : : {
2853 [ - + ][ - + ]: 16157732 : Assert(
[ - - ]
2854 : : getEqualityNode(d_deducedDisequalityReasons[i].first).getFind()
2855 : : == getEqualityNode(d_deducedDisequalityReasons[i].second).getFind());
2856 : : }
2857 : : #endif
2858 [ - + ]: 12506171 : if (TraceIsOn("equality::disequality"))
2859 : : {
2860 [ - - ]: 0 : for (unsigned i = ref.d_mergesStart; i < ref.d_mergesEnd; ++i)
2861 : : {
2862 : 0 : TNode lhs = d_nodes[d_deducedDisequalityReasons[i].first];
2863 : 0 : TNode rhs = d_nodes[d_deducedDisequalityReasons[i].second];
2864 [ - - ]: 0 : Trace("equality::disequality")
2865 : 0 : << d_name << "::eq::storePropagatedDisequality(): because " << lhs
2866 : 0 : << " == " << rhs << std::endl;
2867 : 0 : }
2868 : : }
2869 : :
2870 : : // Store for backtracking
2871 : 12506171 : d_deducedDisequalities.push_back(pair1);
2872 : 12506171 : d_deducedDisequalitiesSize = d_deducedDisequalities.size();
2873 : 12506171 : d_deducedDisequalityReasonsSize = d_deducedDisequalityReasons.size();
2874 : : // Store the proof reference
2875 : 12506171 : d_disequalityReasonsMap[pair1] = ref;
2876 : 12506171 : d_disequalityReasonsMap[pair2] = ref;
2877 : : }
2878 : : else
2879 : : {
2880 [ - + ][ - + ]: 2085305 : Assert(d_disequalityReasonsMap.find(pair1) != d_disequalityReasonsMap.end())
[ - - ]
2881 : 0 : << "You must provide a proof initially";
2882 : : }
2883 : 14591476 : }
2884 : :
2885 : 131890656 : void EqualityEngine::getDisequalities(bool allowConstants,
2886 : : EqualityNodeId classId,
2887 : : TheoryIdSet inputTags,
2888 : : TaggedEqualitiesSet& out)
2889 : : {
2890 : : // Must be empty on input
2891 [ - + ][ - + ]: 131890656 : Assert(out.size() == 0);
[ - - ]
2892 : : // The class we are looking for, shouldn't have any of the tags we are looking
2893 : : // for already set
2894 [ + + ][ + - ]: 131890656 : Assert(d_nodeIndividualTrigger[classId] == null_set_id
[ - + ][ - + ]
[ - - ]
2895 : : || TheoryIdSetUtil::setIntersection(
2896 : : getTriggerTermSet(d_nodeIndividualTrigger[classId]).d_tags,
2897 : : inputTags)
2898 : : == 0);
2899 : :
2900 [ + + ]: 131890656 : if (inputTags == 0)
2901 : : {
2902 : 90541531 : return;
2903 : : }
2904 : :
2905 : : // Set of already (through disequalities) visited equivalence classes
2906 : 41349125 : std::set<EqualityNodeId> alreadyVisited;
2907 : :
2908 : : // Go through the equivalence class
2909 : 41349125 : EqualityNodeId currentId = classId;
2910 : : do
2911 : : {
2912 [ + - ]: 94887628 : Trace("equality::trigger")
2913 : 0 : << d_name << "::getDisequalities() : going through uselist of "
2914 : 47443814 : << d_nodes[currentId] << std::endl;
2915 : :
2916 : : // Current node in the equivalence class
2917 : 47443814 : EqualityNode& currentNode = getEqualityNode(currentId);
2918 : :
2919 : : // Go through the uselist and look for disequalities
2920 : 47443814 : UseListNodeId currentUseId = currentNode.getUseList();
2921 [ + + ]: 83982468 : while (currentUseId != null_uselist_id)
2922 : : {
2923 : 36538654 : UseListNode& useListNode = d_useListNodes[currentUseId];
2924 : 36538654 : EqualityNodeId funId = useListNode.getApplicationId();
2925 : :
2926 [ + - ]: 73077308 : Trace("equality::trigger") << d_name << "::getDisequalities() : checking "
2927 : 36538654 : << d_nodes[funId] << std::endl;
2928 : :
2929 : : const FunctionApplication& fun =
2930 : 36538654 : d_applications[useListNode.getApplicationId()].d_original;
2931 : : // If it's an equality asserted to false, we do the work
2932 : 73077308 : if (fun.isEquality()
2933 [ + + ][ + + ]: 64964998 : && getEqualityNode(funId).getFind()
2934 [ + + ][ + + ]: 64964998 : == getEqualityNode(d_false).getFind())
[ - - ]
2935 : : {
2936 : : // Get the other equality member
2937 : 6044643 : bool lhs = false;
2938 : 6044643 : EqualityNodeId toCompare = fun.d_b;
2939 [ + + ]: 6044643 : if (toCompare == currentId)
2940 : : {
2941 : 3398453 : toCompare = fun.d_a;
2942 : 3398453 : lhs = true;
2943 : : }
2944 : : // Representative of the other member
2945 : 6044643 : EqualityNodeId toCompareRep = getEqualityNode(toCompare).getFind();
2946 [ - + ]: 6044643 : if (toCompareRep == classId)
2947 : : {
2948 : : // We're in conflict, so we will send it out from merge
2949 : 0 : out.clear();
2950 : 0 : return;
2951 : : }
2952 : : // Check if we already have this one
2953 [ + + ]: 6044643 : if (alreadyVisited.count(toCompareRep) == 0)
2954 : : {
2955 : : // Mark as visited
2956 : 4902627 : alreadyVisited.insert(toCompareRep);
2957 : : // Get the trigger set
2958 : : TriggerTermSetRef toCompareTriggerSetRef =
2959 : 4902627 : d_nodeIndividualTrigger[toCompareRep];
2960 : : // We only care if we're not both constants and there are trigger
2961 : : // terms in the other class
2962 [ + + ]: 2277090 : if ((allowConstants || !d_isConstant[toCompareRep])
2963 [ + + ][ + + ]: 7179717 : && toCompareTriggerSetRef != null_set_id)
[ + + ]
2964 : : {
2965 : : // Tags of the other gey
2966 : : TriggerTermSet& toCompareTriggerSet =
2967 : 2414328 : getTriggerTermSet(toCompareTriggerSetRef);
2968 : : // We only care if there are things in inputTags that is also in
2969 : : // toCompareTags
2970 : 2414328 : TheoryIdSet commonTags = TheoryIdSetUtil::setIntersection(
2971 : : inputTags, toCompareTriggerSet.d_tags);
2972 [ + + ]: 2414328 : if (commonTags)
2973 : : {
2974 : 1680770 : out.push_back(TaggedEquality(funId, toCompareTriggerSetRef, lhs));
2975 : : }
2976 : : }
2977 : : }
2978 : : }
2979 : : // Go to the next one in the use list
2980 : 36538654 : currentUseId = useListNode.getNext();
2981 : : }
2982 : : // Next in equivalence class
2983 : 47443814 : currentId = currentNode.getNext();
2984 [ + - ][ + + ]: 47443814 : } while (!d_done && currentId != classId);
[ + + ]
2985 [ + - ]: 41349125 : }
2986 : :
2987 : 131890628 : bool EqualityEngine::propagateTriggerTermDisequalities(
2988 : : TheoryIdSet tags,
2989 : : TriggerTermSetRef triggerSetRef,
2990 : : const TaggedEqualitiesSet& disequalitiesToNotify)
2991 : : {
2992 : : // No tags, no food
2993 [ + + ]: 131890628 : if (!tags)
2994 : : {
2995 : 90541504 : return !d_done;
2996 : : }
2997 : :
2998 [ - + ][ - + ]: 41349124 : Assert(triggerSetRef != null_set_id);
[ - - ]
2999 : :
3000 : : // This is the class trigger set
3001 : 41349124 : const TriggerTermSet& triggerSet = getTriggerTermSet(triggerSetRef);
3002 : : // Go through the disequalities and notify
3003 : 41349124 : TaggedEqualitiesSet::const_iterator it = disequalitiesToNotify.begin();
3004 : 41349124 : TaggedEqualitiesSet::const_iterator it_end = disequalitiesToNotify.end();
3005 [ + + ][ + + ]: 42977365 : for (; !d_done && it != it_end; ++it)
[ + + ]
3006 : : {
3007 : : // The information about the equality that is asserted to false
3008 : 1647535 : const TaggedEquality& disequalityInfo = *it;
3009 : : const TriggerTermSet& disequalityTriggerSet =
3010 : 1647535 : getTriggerTermSet(disequalityInfo.d_triggerSetRef);
3011 : : TheoryIdSet commonTags =
3012 : 1647535 : TheoryIdSetUtil::setIntersection(disequalityTriggerSet.d_tags, tags);
3013 [ - + ][ - + ]: 1647535 : Assert(commonTags);
[ - - ]
3014 : : // This is the actual function
3015 : : const FunctionApplication& fun =
3016 : 1647535 : d_applications[disequalityInfo.d_equalityId].d_original;
3017 : : // Figure out who we are comparing to in the original equality
3018 [ + + ]: 1647535 : EqualityNodeId toCompare = disequalityInfo.d_lhs ? fun.d_a : fun.d_b;
3019 [ + + ]: 1647535 : EqualityNodeId myCompare = disequalityInfo.d_lhs ? fun.d_b : fun.d_a;
3020 : 1647535 : if (getEqualityNode(toCompare).getFind()
3021 [ + + ]: 1647535 : == getEqualityNode(myCompare).getFind())
3022 : : {
3023 : : // We're propagating a != a, which means we're inconsistent, just bail and
3024 : : // let it go into a regular conflict
3025 : 19294 : return !d_done;
3026 : : }
3027 : : // Go through the tags, and add the disequalities
3028 : : TheoryId currentTag;
3029 : 1628241 : while (
3030 : 4047701 : !d_done
3031 [ + + ][ + + ]: 4047701 : && ((currentTag = TheoryIdSetUtil::setPop(commonTags)) != THEORY_LAST))
[ + + ]
3032 : : {
3033 : : // Get the tag representative
3034 : 2419460 : EqualityNodeId tagRep = disequalityTriggerSet.getTrigger(currentTag);
3035 : 2419460 : EqualityNodeId myRep = triggerSet.getTrigger(currentTag);
3036 : : // Propagate
3037 [ + + ]: 2419460 : if (!hasPropagatedDisequality(currentTag, myRep, tagRep))
3038 : : {
3039 : : // Construct the proof if not there already
3040 [ + + ]: 159292 : if (!hasPropagatedDisequality(myRep, tagRep))
3041 : : {
3042 : 51047 : d_deducedDisequalityReasons.push_back(EqualityPair(myCompare, myRep));
3043 : 51047 : d_deducedDisequalityReasons.push_back(
3044 : 0 : EqualityPair(toCompare, tagRep));
3045 : 51047 : d_deducedDisequalityReasons.push_back(
3046 : 102094 : EqualityPair(disequalityInfo.d_equalityId, d_falseId));
3047 : : }
3048 : : // Store the propagation
3049 : 159292 : storePropagatedDisequality(currentTag, myRep, tagRep);
3050 : : // Notify
3051 [ + + ]: 318584 : if (!notifyTriggerTermEquality(
3052 : 318584 : currentTag, d_nodes[myRep], d_nodes[tagRep], false))
3053 : : {
3054 : 43 : d_done = true;
3055 : : }
3056 : : }
3057 : : }
3058 : : }
3059 : :
3060 : 41329830 : return !d_done;
3061 : : }
3062 : :
3063 : 15646875 : TheoryIdSet EqualityEngine::TriggerTermSet::hasTrigger(TheoryId tag) const
3064 : : {
3065 : 15646875 : return TheoryIdSetUtil::setContains(tag, d_tags);
3066 : : }
3067 : :
3068 : 6972335 : EqualityNodeId EqualityEngine::TriggerTermSet::getTrigger(TheoryId tag) const
3069 : : {
3070 : 6972335 : return d_triggers[TheoryIdSetUtil::setIndex(tag, d_tags)];
3071 : : }
3072 : :
3073 : : } // namespace eq
3074 : : } // Namespace theory
3075 : : } // namespace cvc5::internal
|
