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

feat(util/rb_tree): add max (element) method

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2014-08-30 10:22:51 -07:00
parent a47dada27f
commit 658e0780a6
1 changed files with 10 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/util/rb_tree.h
View file

@ -207,6 +207,15 @@ class rb_tree : public CMP {
return &it->m_value;
}
static T const * max(node const & n) {
node_cell const * it = n.m_ptr;
if (!it)
return nullptr;
while (it->m_right)
it = it->m_right.m_ptr;
return &it->m_value;
}
node erase(node && n, T const & v) {
lean_assert(n);
node h = ensure_unshared(n.steal());
@ -349,6 +358,7 @@ public:
}
T const * min() const { return min(m_root); }
T const * max() const { return max(m_root); }
bool contains(T const & v) const { return find(v) != nullptr; }
template<typename F>