From d36cecc2f328cdd742c601cee6bc803dca1b2b14 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <a-nlopes@microsoft.com>
Date: Fri, 19 Sep 2014 15:51:08 +0100
Subject: [PATCH] make use of count population intrinsincs on MSVC/gcc/clang

Signed-off-by: Nuno Lopes <a-nlopes@microsoft.com>
---
 src/util/util.h | 16 +++++++++-------
 1 file changed, 9 insertions(+), 7 deletions(-)

diff --git a/src/util/util.h b/src/util/util.h
index 0aa8f881d..58120b2f2 100644
--- a/src/util/util.h
+++ b/src/util/util.h
@@ -95,7 +95,12 @@ unsigned uint64_log2(uint64 v);
 COMPILE_TIME_ASSERT(sizeof(unsigned) == 4);
 
 // Return the number of 1 bits in v.
-inline unsigned get_num_1bits(unsigned v) {
+static inline unsigned get_num_1bits(unsigned v) {
+#ifdef _MSC_VER
+    return __popcnt(v);
+#elif defined(__GNUC__)
+    return __builtin_popcount(v);
+#else
 #ifdef Z3DEBUG
     unsigned c;
     unsigned v1 = v;
@@ -108,15 +113,16 @@ inline unsigned get_num_1bits(unsigned v) {
     unsigned r = (((v + (v >> 4)) & 0xF0F0F0F) * 0x1010101) >> 24; 
     SASSERT(c == r);
     return r;
+#endif
 }
 
 // Remark: on gcc, the operators << and >> do not produce zero when the second argument >= 64.
 // So, I'm using the following two definitions to fix the problem
-inline uint64 shift_right(uint64 x, uint64 y) {
+static inline uint64 shift_right(uint64 x, uint64 y) {
     return y < 64ull ? (x >> y) : 0ull;
 }
 
-inline uint64 shift_left(uint64 x, uint64 y) {
+static inline uint64 shift_left(uint64 x, uint64 y) {
     return y < 64ull ? (x << y) : 0ull;
 }
 
@@ -255,10 +261,6 @@ inline std::ostream & operator<<(std::ostream & out, std::pair<T1, T2> const & p
     return out;
 }
 
-#ifndef _WINDOWS
-#define __forceinline inline
-#endif
-
 template<typename IT>
 bool has_duplicates(const IT & begin, const IT & end) {
     for (IT it1 = begin; it1 != end; ++it1) {