mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

Added 64-bit "1" counting (#6434)

Browse source 
* 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
This commit is contained in:
Clemens Eisenhofer 2022-11-02 18:02:29 +01:00 committed by GitHub
parent 0d97d2214c
commit ae707ffff7
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 20 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

20
src/util/util.h
View file

@ -103,6 +103,7 @@ unsigned uint64_log2(uint64_t v);
static_assert(sizeof(unsigned) == 4, "unsigned are 32 bits"); static_assert(sizeof(unsigned) == 4, "unsigned are 32 bits");
// Return the number of 1 bits in v. // 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) { static inline unsigned get_num_1bits(unsigned v) {
#ifdef __GNUC__ #ifdef __GNUC__
return __builtin_popcount(v); return __builtin_popcount(v);
@ -122,6 +123,25 @@ static inline unsigned get_num_1bits(unsigned v) {
#endif #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. // 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 // So, I'm using the following two definitions to fix the problem
static inline uint64_t shift_right(uint64_t x, uint64_t y) { static inline uint64_t shift_right(uint64_t x, uint64_t y) {