From ae707ffff7b3a4e4f33c4dae114362a2709d4376 Mon Sep 17 00:00:00 2001
From: Clemens Eisenhofer <56730610+CEisenhofer@users.noreply.github.com>
Date: Wed, 2 Nov 2022 18:02:29 +0100
Subject: [PATCH] Added 64-bit "1" counting (#6434)

* Memory leak in .NET user-propagator
The user-propagator object has to be manually disposed (IDisposable), otherwise it stays in memory forever, as it cannot be garbage collected automatically

* Throw an exception if variable passed to decide is already assigned instead of running in an assertion violation

* Added 64-bit "1" counting
---
 src/util/util.h | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/src/util/util.h b/src/util/util.h
index f08558f37..9d129f9a7 100644
--- a/src/util/util.h
+++ b/src/util/util.h
@@ -103,6 +103,7 @@ unsigned uint64_log2(uint64_t v);
 static_assert(sizeof(unsigned) == 4, "unsigned are 32 bits");
 
 // Return the number of 1 bits in v.
+// see e.g. http://en.wikipedia.org/wiki/Hamming_weight
 static inline unsigned get_num_1bits(unsigned v) {
 #ifdef __GNUC__
     return __builtin_popcount(v);
@@ -122,6 +123,25 @@ static inline unsigned get_num_1bits(unsigned v) {
 #endif
 }
 
+static inline unsigned get_num_1bits(uint64_t v) {
+#ifdef __GNUC__
+    return __builtin_popcountll(v);
+#else
+#ifdef Z3DEBUG
+    unsigned c;
+    uint64_t v1 = v;
+    for (c = 0; v1; c++) {
+        v1 &= v1 - 1; 
+    }
+#endif
+    v = v - (v >> 1) & 0x5555555555555555;
+    v = (v & 0x3333333333333333) + ((v >> 2) & 0x3333333333333333); 
+    v = (v + (v >> 4)) & 0x0F0F0F0F0F0F0F0F;
+    uint64_t r = (v * 0x0101010101010101) >> 56;
+    SASSERT(c == 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
 static inline uint64_t shift_right(uint64_t x, uint64_t y) {