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