Searched refs:t1Id (Results 1 – 3 of 3) sorted by relevance
| /dports/math/cvc4/CVC4-1.7/src/theory/uf/ |
| H A D | equality_engine.cpp | 413 EqualityNodeId t1Id = getNodeId(t1); in assertEqualityInternal() local
940 EqualityNodeId t1Id = getNodeId(t1); in explainEquality() local
945 getExplanation(t1Id, t2Id, equalities, eqp); in explainEquality()
953 EqualityPair pair(t1Id, t2Id); in explainEquality()
1044 …Warning() << d_nodes[t1Id] << " with find " << d_nodes[getEqualityNode(t1Id).getFind()] << std::en… in getExplanation()
1051 if (t1Id == t2Id){ in getExplanation()
1053 …if ((d_nodes[t1Id].getKind() == kind::BUILTIN) && (d_nodes[t1Id].getConst<Kind>() == kind::SELECT)… in getExplanation()
1072 bfsQueue.push_back(BfsData(t1Id, null_id, 0)); in getExplanation()
1393 EqualityNodeId t1Id = getNodeId(t1); in addTriggerEqualityInternal() local
1669 EqualityNodeId t1Id = getNodeId(t1); in areDisequal() local
[all …]
|
| H A D | equality_engine_types.h | 112 EqualityNodeId t1Id, t2Id; member
116 : t1Id(x), t2Id(y), type(type), reason(reason) in MergeCandidate()
|
| H A D | equality_engine.h | 523 …void getExplanation(EqualityEdgeId t1Id, EqualityNodeId t2Id, std::vector<TNode>& equalities, EqPr…
|