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

fix(CMakeLists): remove tests for dead module, fixes #883

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-19 07:59:57 -08:00
parent 093a212ed4
commit 4bb58a04db
3 changed files with 0 additions and 65 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/CMakeLists.txt
View file

@ -389,7 +389,6 @@ add_subdirectory(tests/util/numerics)
add_subdirectory(tests/util/interval)
add_subdirectory(tests/kernel)
add_subdirectory(tests/library)
add_subdirectory(tests/library/blast)
add_subdirectory(tests/frontends/lean)
add_subdirectory(tests/shell)
# The DLL (shared library) is not being generated correctly when we use cross-compilation (i.e., generate the Windows DLL using Linux).

3
src/tests/library/blast/CMakeLists.txt
View file

@ -1,3 +0,0 @@
add_executable(union_find union_find.cpp $<TARGET_OBJECTS:util>)
target_link_libraries(union_find ${EXTRA_LIBS})
add_test(union_find "${CMAKE_CURRENT_BINARY_DIR}/union_find")

61
src/tests/library/blast/union_find.cpp
View file

@ -1,61 +0,0 @@
/*
Copyright (c) 2015 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <algorithm>
#include "util/test.h"
#include "util/init_module.h"
#include "library/blast/union_find.h"
using namespace lean;
typedef union_find<unsigned, unsigned, unsigned_cmp> uf;
static void check_explain(uf const & m, unsigned n1, unsigned n2, std::initializer_list<unsigned> const & expected_js) {
buffer<unsigned> js1;
bool r = m.explain(n1, n2, js1);
lean_assert(r);
lean_assert(m.rep(n1) == m.rep(n2));
std::sort(js1.begin(), js1.end());
buffer<unsigned> js2;
js2.append(expected_js.size(), expected_js.begin());
std::sort(js2.begin(), js2.end());
lean_assert(js1.size() == js2.size());
for (unsigned i = 0; i < js1.size(); i++) {
lean_assert(js1[i] == js2[i]);
}
}
static void tst1() {
uf m;
m.join(1, 2, 0);
lean_assert(m.is_eq(1, 1));
lean_assert(m.is_eq(1, 2));
m.join(1, 3, 1);
lean_assert(m.is_eq(2, 3));
check_explain(m, 2, 3, {0, 1});
check_explain(m, 2, 1, {0});
check_explain(m, 1, 3, {1});
m.join(3, 4, 2);
m.join(5, 1, 3);
m.join(6, 2, 4);
lean_assert(m.rep(6) == m.rep(4));
check_explain(m, 2, 3, {0, 1});
check_explain(m, 6, 4, {0, 1, 2, 4});
check_explain(m, 5, 6, {0, 3, 4});
lean_assert_eq(m.size(1), 6);
for (unsigned i = 10; i < 30; i++)
m.join(i, i+1, i);
check_explain(m, 10, 15, {10, 11, 12, 13, 14});
lean_assert_eq(m.size(10), 21);
}
int main() {
save_stack_info();
initialize_util_module();
tst1();
finalize_util_module();
return has_violations() ? 1 : 0;
}