Home
last modified time | relevance | path

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

/dports/math/cvc4/CVC4-1.7/src/theory/uf/
H A Dequality_engine_types.h290 struct FunctionApplication { struct
297 …FunctionApplication(FunctionApplicationType type = APP_EQUALITY, EqualityNodeId a = null_id, Equal… argument
301 bool operator == (const FunctionApplication& other) const { argument
323 size_t operator () (const FunctionApplication& app) const { in operator() argument
336 FunctionApplication original;
337 FunctionApplication normalized;
339 …FunctionApplicationPair(const FunctionApplication& original, const FunctionApplication& normalized) in FunctionApplicationPair()
H A Dequality_engine.cpp176 FunctionApplication funOriginal(type, t1, t2); in newApplicationNode()
180 FunctionApplication funNormalized(type, t1ClassId, t2ClassId); in newApplicationNode()
647 FunctionApplication funNormalized(fun.type, aNormalized, bNormalized); in merge()
862 const FunctionApplication& app = d_applications[i].original; in backtrack()
1132 const FunctionApplication& f1 = d_applications[currentNode].original; in getExplanation()
1133 const FunctionApplication& f2 = d_applications[edgeNode].original; in getExplanation()
1181 const FunctionApplication& eq = d_applications[eqId].original; in getExplanation()
1697 FunctionApplication eqNormalized(APP_EQUALITY, t1ClassId, t2ClassId); in areDisequal()
1702 const FunctionApplication original = d_applications[find->second].original; in areDisequal()
1719 const FunctionApplication original = d_applications[find->second].original; in areDisequal()
[all …]
H A Dequality_engine.h257 …typedef std::unordered_map<FunctionApplication, EqualityNodeId, FunctionApplicationHashFunction> A…
266 std::vector<FunctionApplication> d_applicationLookups;
274 void storeApplicationLookup(FunctionApplication& funNormalized, EqualityNodeId funId);