Home
last modified time | relevance | path

Searched refs:bSharedId (Results 1 – 1 of 1) sorted by relevance

/dports/math/cvc4/CVC4-1.7/src/theory/uf/
H A Dequality_engine.cpp495 EqualityNodeId bSharedId = bTriggerTerms.triggers[b_i++]; in assertEquality() local
497 if (!hasPropagatedDisequality(aTag, aSharedId, bSharedId)) { in assertEquality()
499 if (!hasPropagatedDisequality(aSharedId, bSharedId)) { in assertEquality()
501 d_deducedDisequalityReasons.push_back(EqualityPair(bSharedId, b)); in assertEquality()
505 storePropagatedDisequality(aTag, aSharedId, bSharedId); in assertEquality()
507 … notifying " << aTag << " for " << d_nodes[aSharedId] << " != " << d_nodes[bSharedId] << std::endl; in assertEquality()
508 … if (!d_notify.eqNotifyTriggerTermEquality(aTag, d_nodes[aSharedId], d_nodes[bSharedId], false)) { in assertEquality()