mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

Merge branch 'master' of https://github.com/z3prover/z3

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-11-02 17:32:32 -07:00
commit e0bbe8dfc0
1 changed files with 20 additions and 0 deletions
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");
// 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) {