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

Add is_prefix_of for hierarchical names

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-19 11:43:09 -07:00
parent b2c877b0c3
commit 90ad0ba3b3
3 changed files with 50 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
src/tests/util/name.cpp
View file

@ -67,9 +67,25 @@ static void tst3() {
lean_assert(n == name(name(name("foo"), "bla"), "tst"));
}
static void tst4() {
lean_assert(is_prefix_of(name{"foo", "bla"}, name{"foo", "bla"}));
lean_assert(is_prefix_of(name{"foo", "bla"}, name{"foo", "bla", "foo"}));
lean_assert(is_prefix_of(name{"foo"}, name{"foo", "bla", "foo"}));
lean_assert(!is_prefix_of(name{"foo"}, name{"fo", "bla", "foo"}));
lean_assert(!is_prefix_of(name{"foo", "bla", "foo"}, name{"foo", "bla"}));
lean_assert(is_prefix_of(name{"foo", "bla"}, name(name{"foo", "bla"}, 0u)));
lean_assert(is_prefix_of(name(name(0u), 1u), name(name(0u), 1u)));
lean_assert(!is_prefix_of(name(name(0u), 3u), name(name(0u), 1u)));
lean_assert(is_prefix_of(name(name(0u), 1u), name(name(name(0u), 1u), "foo")));
lean_assert(!is_prefix_of(name(name(2u), 1u), name(name(name(0u), 1u), "foo")));
lean_assert(!is_prefix_of(name(name(0u), 3u), name(name(name(0u), 1u), "foo")));
lean_assert(!is_prefix_of(name(name("bla"), 1u), name(name(name(0u), 1u), "foo")));
}
int main() {
tst1();
tst2();
tst3();
tst4();
return has_violations() ? 1 : 0;
}

35
src/util/name.cpp
View file

@ -11,6 +11,7 @@ Author: Leonardo de Moura
#include "name.h"
#include "debug.h"
#include "rc.h"
#include "buffer.h"
#include "hash.h"
#include "trace.h"
@ -66,7 +67,7 @@ struct name::imp {
display_core(out, p);
}
friend void copy_limbs(imp * p, std::vector<name::imp *> & limbs) {
friend void copy_limbs(imp * p, buffer<name::imp *> & limbs) {
limbs.clear();
while (p != nullptr) {
limbs.push_back(p);
@ -194,13 +195,41 @@ bool operator==(name const & a, name const & b) {
}
}
bool is_prefix_of(name const & n1, name const & n2) {
buffer<name::imp*> limbs1, limbs2;
name::imp* i1 = n1.m_ptr;
name::imp* i2 = n2.m_ptr;
copy_limbs(i1, limbs1);
copy_limbs(i2, limbs2);
unsigned sz1 = limbs1.size();
unsigned sz2 = limbs2.size();
if (sz1 > sz2)
return false;
else if (sz1 == sz2 && n1.hash() != n2.hash())
return false;
auto it1 = limbs1.begin();
auto it2 = limbs2.begin();
for (; it1 != limbs1.end(); ++it1, ++it2) {
i1 = *it1;
i2 = *it2;
if (i1->m_is_string != i2->m_is_string)
return false;
if (i1->m_is_string) {
if (strcmp(i1->m_str, i2->m_str) != 0)
return false;
} else if (i1->m_k != i2->m_k) {
return false;
}
}
return true;
}
bool operator==(name const & a, char const * b) {
return a.m_ptr->m_is_string && strcmp(a.m_ptr->m_str, b) == 0;
}
int cmp(name::imp * i1, name::imp * i2) {
static thread_local std::vector<name::imp *> limbs1;
static thread_local std::vector<name::imp *> limbs2;
buffer<name::imp *> limbs1, limbs2;
copy_limbs(i1, limbs1);
copy_limbs(i2, limbs2);
auto it1 = limbs1.begin();

2
src/util/name.h
View file

@ -31,6 +31,8 @@ public:
static name const & anonymous();
name & operator=(name const & other);
name & operator=(name && other);
/** \brief Return true iff \c n1 is a prefix of \c n2. */
friend bool is_prefix_of(name const & n1, name const & n2);
friend bool operator==(name const & a, name const & b);
friend bool operator!=(name const & a, name const & b) { return !(a == b); }
friend bool operator==(name const & a, char const * b);