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

feat(util/trie): add for_each and display methods

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-05-13 18:23:27 -07:00
parent bfa6193bfe
commit 01eda46b69
2 changed files with 33 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/tests/util/trie.cpp
View file

@ -27,6 +27,7 @@ static void tst1() {
t2 = insert(t2, "help", 12);
lean_assert(*find(t2, "abd") == 11);
lean_assert(!find(t, "abd"));
t2.display(std::cout);
ctrie<int> t3 = *t2.find('a');
lean_assert(*find(t3, "bc") == 10);
lean_assert(*find(t3, "bd") == 11);
@ -54,6 +55,8 @@ static void tst2() {
lean_assert(*find(t1, "abd") == 12);
lean_assert(!find(t2, "abc"));
lean_assert(*find(t2, "abd") == 12);
std::cout << "---------\n";
t1.display(std::cout);
}
int main() {

30
src/util/trie.h
View file

@ -9,6 +9,7 @@ Author: Leonardo de Moura
#include <string>
#include "util/rb_map.h"
#include "util/optional.h"
#include "util/buffer.h"
namespace lean {
template<typename Key, typename Val, typename KeyCMP>
@ -83,6 +84,18 @@ class trie : public KeyCMP {
return new_t1;
}
template<typename F>
static void for_each(F && f, node const & n, buffer<Key> & prefix) {
if (n->m_value) {
f(prefix.size(), prefix.data(), *(n->m_value));
}
n->m_children.for_each([&](Key const & k, node const & c) {
prefix.push_back(k);
for_each(f, c, prefix);
prefix.pop_back();
});
}
node m_root;
trie(node const & n):m_root(n) {}
public:
@ -120,6 +133,23 @@ public:
void merge(trie const & t) {
m_root = merge(m_root.steal(), t.m_root);
}
template<typename F>
void for_each(F && f) const {
buffer<Key> prefix;
for_each(f, m_root, prefix);
}
// for debugging purposes
void display(std::ostream & out) const {
for_each([&](unsigned num_keys, Key const * keys, Val const & v) {
for (unsigned i = 0; i < num_keys; i++) {
if (i > 0) out << ", ";
out << keys[i];
}
out << " -> " << v << "\n";
});
}
};
struct char_cmp { int operator()(char c1, char c2) const { return c1 < c2 ? -1 : (c1 == c2 ? 0 : 1); } };