Searched refs:disequalityInfo (Results 1 – 1 of 1) sorted by relevance
2092 const TaggedEquality& disequalityInfo = *it; in propagateTriggerTermDisequalities() local2093 const TriggerTermSet& disequalityTriggerSet = getTriggerTermSet(disequalityInfo.triggerSetRef); in propagateTriggerTermDisequalities()2097 const FunctionApplication& fun = d_applications[disequalityInfo.equalityId].original; in propagateTriggerTermDisequalities()2099 EqualityNodeId toCompare = disequalityInfo.lhs ? fun.a : fun.b; in propagateTriggerTermDisequalities()2100 EqualityNodeId myCompare = disequalityInfo.lhs ? fun.b : fun.a; in propagateTriggerTermDisequalities()2118 … d_deducedDisequalityReasons.push_back(EqualityPair(disequalityInfo.equalityId, d_falseId)); in propagateTriggerTermDisequalities()