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

test(hash): add missing tests

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-09-29 17:03:48 -07:00
parent 57b6148bbb
commit 1179b6b52b
2 changed files with 26 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/tests/util/CMakeLists.txt
View file

@ -52,3 +52,6 @@ add_test(bit_tricks ${CMAKE_CURRENT_BINARY_DIR}/bit_tricks)
add_executable(lazy_list lazy_list.cpp)
target_link_libraries(lazy_list ${EXTRA_LIBS})
add_test(lazy_list ${CMAKE_CURRENT_BINARY_DIR}/lazy_list)
add_executable(hash hash.cpp)
target_link_libraries(hash ${EXTRA_LIBS})
add_test(hash ${CMAKE_CURRENT_BINARY_DIR}/hash)

23
src/tests/util/hash.cpp Normal file
View file

@ -0,0 +1,23 @@
/*
Copyright (c) 2013 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
*/
#include <iostream>
#include "util/test.h"
#include "util/hash.h"
using namespace lean;
static void tst1() {
int a[] = {0, 1, 2};
unsigned h3 = hash(3, [&](unsigned i) { return a[i]; });
lean_assert(h3 == hash(3, [&](unsigned i) { return a[i]; }));
unsigned h1 = hash(1, [&](unsigned i) { return a[i]; });
lean_assert(h1 != h3);
}
int main() {
tst1();
return has_violations() ? 1 : 0;
}