diff options
| author | Tim King <taking@cs.nyu.edu> | 2012-05-10 14:50:45 +0000 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2012-05-10 14:50:45 +0000 |
| commit | 021d68c157ee698e706096fc9f4a112f17cd0128 (patch) | |
| tree | e6444a4978d25c9942b35234aafb896e7874738a /src/theory/uf | |
| parent | cb7a91be1a29c31d607e6287101f490b0cc7f731 (diff) | |
Removing now unneeded (as of r3425) typenames from EqualityEngine. trunk now compiles on Debian.
Diffstat (limited to 'src/theory/uf')
| -rw-r--r-- | src/theory/uf/equality_engine.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp index b78015c00..ec0a8fce3 100644 --- a/src/theory/uf/equality_engine.cpp +++ b/src/theory/uf/equality_engine.cpp @@ -119,7 +119,7 @@ EqualityNodeId EqualityEngine::newApplicationNode(TNode original, EqualityNodeId d_applications[funId] = FunctionApplicationPair(funOriginal, funNormalized); // Add the lookup data, if it's not already there - typename ApplicationIdsMap::iterator find = d_applicationLookup.find(funNormalized); + ApplicationIdsMap::iterator find = d_applicationLookup.find(funNormalized); if (find == d_applicationLookup.end()) { // When we backtrack, if the lookup is not there anymore, we'll add it again Debug("equality") << "EqualityEngine::newApplicationNode(" << original << ", " << t1 << ", " << t2 << "): no lookup, setting up" << std::endl; @@ -362,7 +362,7 @@ bool EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vect EqualityNodeId aNormalized = getEqualityNode(fun.a).getFind(); EqualityNodeId bNormalized = getEqualityNode(fun.b).getFind(); FunctionApplication funNormalized(aNormalized, bNormalized); - typename ApplicationIdsMap::iterator find = d_applicationLookup.find(funNormalized); + ApplicationIdsMap::iterator find = d_applicationLookup.find(funNormalized); if (find != d_applicationLookup.end()) { // Applications fun and the funNormalized can be merged due to congruence if (getEqualityNode(funId).getFind() != getEqualityNode(find->second).getFind()) { |