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

Add hierarchical names tests

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-08-22 08:48:52 -07:00
parent 1b5fcb80ee
commit fbd25cac9f
2 changed files with 30 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -4,8 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include "name.h"
#include <cstring>
#include <sstream>
#include "test.h"
#include "name.h"
using namespace lean;
static void tst1() {
@ -82,10 +84,35 @@ static void tst4() {
lean_assert(!is_prefix_of(name(name("bla"), 1u), name(name(name(0u), 1u), "foo")));
}
static void tst5() {
name n(0u);
lean_assert(n.size() == 1);
lean_assert(name().size() > 0);
lean_assert(name({"foo", "bla", "boing"}).get_prefix() == name({"foo", "bla"}));
lean_assert(!name({"foo", "bla", "boing"}).is_atomic());
lean_assert(name({"foo"}).is_atomic());
lean_assert(strcmp(name({"foo", "bla", "boing"}).get_string(), "boing") == 0);
lean_assert(name(name(0u), 1u).get_numeral() == 1u);
lean_assert(name(2u).get_numeral() == 2u);
lean_assert(name::anonymous().is_anonymous());
name n1("foo");
name n2 = n1;
lean_assert(n2 == n1);
std::cout << name::anonymous() << "\n";
std::cout << name({"foo", "bla", "boing"}).get_prefix() << "\n";
lean_assert(name("foo").is_string());
lean_assert(name(0u).is_numeral());
lean_assert(name(name(0u), "foo").is_string());
lean_assert(name(name("foo"), 0u).is_numeral());
lean_assert(name(name(0u), "foo").get_prefix().is_numeral());
lean_assert(name(name("foo"), 0u).get_prefix().is_string());
}
int main() {
tst1();
tst2();
tst3();
tst4();
tst5();
return has_violations() ? 1 : 0;
}

4
src/util/debug.cpp
View file

@ -25,7 +25,7 @@ static std::unique_ptr<std::set<std::string>> g_enabled_debug_tags;
bool has_violations() {
return g_has_violations;
}
// LCOV_EXCL_START
void enable_assertions(bool f) {
g_enable_assertions = f;
}
@ -102,5 +102,5 @@ void invoke_debugger() {
}
}
}
// LCOV_EXCL_STOP
}