michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

refactor(util/name_set): implement name_sets using red black trees instead of hashtables

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-04-22 11:09:13 -07:00
parent cc1cfba8ad
commit ad43d9177b
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/util/name_set.cpp
View file

@ -11,7 +11,7 @@ name mk_unique(name_set const & s, name const & suggestion) {
name n = suggestion; name n = suggestion;
int i = 1; int i = 1;
while (true) { while (true) {
if (s.find(n) == s.end()) if (!s.contains(n))
return n; return n;
n = name(suggestion, i); n = name(suggestion, i);
i++; i++;

4
src/util/name_set.h
View file

@ -5,10 +5,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura Author: Leonardo de Moura
*/ */
#pragma once #pragma once
#include <unordered_set> #include "util/rb_tree.h"
#include "util/name.h" #include "util/name.h"
namespace lean { namespace lean {
typedef std::unordered_set<name, name_hash, name_eq> name_set; typedef rb_tree<name, name_quick_cmp> name_set;
/** /**
\brief Make a name that does not occur in \c s, based on \brief Make a name that does not occur in \c s, based on
the given suggestion. the given suggestion.