Home
last modified time | relevance | path

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

/dports/math/cvc4/CVC4-1.7/src/theory/uf/
H A Dequality_engine.cpp228 d_nodeIndividualTrigger.push_back(+null_set_id); in newNode()
354 d_triggerTermSetUpdates.push_back(TriggerSetUpdate(tId, null_set_id)); in addTermInternal()
474 if (aTriggerRef != +null_set_id && bTriggerRef != +null_set_id) { in assertEquality()
564 …Theory::Set class1Tags = class1triggerRef == null_set_id ? 0 : getTriggerTermSet(class1triggerRef)… in merge()
685 if (class2triggerRef != +null_set_id) { in merge()
686 if (class1triggerRef == +null_set_id) { in merge()
690 d_triggerTermSetUpdates.push_back(TriggerSetUpdate(class1Id, +null_set_id)); in merge()
1772 if (triggerSetRef != +null_set_id && getTriggerTermSet(triggerSetRef).hasTrigger(tag)) { in addTriggerTerm()
1796 if (triggerSetRef != null_set_id) { in addTriggerTerm()
1836 return triggerSetRef != +null_set_id && getTriggerTermSet(triggerSetRef).hasTrigger(tag); in isTriggerTerm()
[all …]
H A Dequality_engine.h587 static const TriggerTermSetRef null_set_id = (TriggerTermSetRef)(-1); variable
610 TriggerSetUpdate(EqualityNodeId classId = null_id, TriggerTermSetRef oldValue = null_set_id)
689 …EqualityNodeId equalityId = null_id, TriggerTermSetRef triggerSetRef = null_set_id, bool lhs = tru…