From a7707dd669415f321546a46224c105c44667f858 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 25 Sep 2013 20:55:23 -0700
Subject: [PATCH] test(bit_tricks): add tests for log2

---
 src/tests/util/CMakeLists.txt |  3 +++
 src/tests/util/bit_tricks.cpp | 33 +++++++++++++++++++++++++++++++++
 2 files changed, 36 insertions(+)
 create mode 100644 src/tests/util/bit_tricks.cpp

diff --git a/src/tests/util/CMakeLists.txt b/src/tests/util/CMakeLists.txt
index 7d24eb8ed..73388220b 100644
--- a/src/tests/util/CMakeLists.txt
+++ b/src/tests/util/CMakeLists.txt
@@ -46,3 +46,6 @@ add_test(trace ${CMAKE_CURRENT_BINARY_DIR}/trace)
 add_executable(exception exception.cpp)
 target_link_libraries(exception ${EXTRA_LIBS})
 add_test(exception ${CMAKE_CURRENT_BINARY_DIR}/exception)
+add_executable(bit_tricks bit_tricks.cpp)
+target_link_libraries(bit_tricks ${EXTRA_LIBS})
+add_test(bit_tricks ${CMAKE_CURRENT_BINARY_DIR}/bit_tricks)
diff --git a/src/tests/util/bit_tricks.cpp b/src/tests/util/bit_tricks.cpp
new file mode 100644
index 000000000..c31c586e3
--- /dev/null
+++ b/src/tests/util/bit_tricks.cpp
@@ -0,0 +1,33 @@
+/*
+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 "util/test.h"
+#include "util/bit_tricks.h"
+using namespace lean;
+
+static void tst1() {
+    lean_assert(log2(255) == 7);
+    lean_assert(log2(256) == 8);
+    lean_assert(log2(257) == 8);
+    lean_assert(log2(321) == 8);
+    lean_assert(log2(520) == 9);
+    lean_assert(log2(65535) == 15);
+    lean_assert(log2(65536) == 16);
+    lean_assert(log2(65537) == 16);
+    lean_assert(log2(5203939) == 22);
+    lean_assert(log2(10309482) == 23);
+    lean_assert(log2(41039392) == 25);
+    lean_assert(log2(213469392) == 27);
+    lean_assert(log2(1293828727) == 30);
+    lean_assert(log2(1073741824) == 30);
+    lean_assert(log2(2147483648u) == 31);
+    lean_assert(log2(4294967295u) == 31);
+}
+
+int main() {
+    tst1();
+    return has_violations() ? 1 : 0;
+}