Count ones in BitVec in Z3 with Datalog input format

Question

Is there a compact way of counting the number of bits that are set to 1 in a BitVec in Z3 using Datalog input format?

$ z3 -h  # most of the lines below omited for clarity
Input format:
  -dl         use parser for Datalog input format.

The currently accepted answer for this question: Count ones in BitVec in Z3 with SMT 2 input format states that there is no nice way to do in SMT 2 input format.

The currently accepted answer for this question: Sum of all the bits in a Bit Vector of Z3 shows how to do this in Python.

Axel Kemper Axel Kemper · Accepted Answer · 2018-07-04T06:59:39

For 32 bit vectors, you could try to translate the following pseudo code to SMT:

v = v - ((v >> 1) & 0x55555555);                    // reuse input as temporary
v = (v & 0x33333333) + ((v >> 2) & 0x33333333);     // temp
c = ((v + (v >> 4) & 0xF0F0F0F) * 0x1010101) >> 24; // count

This is called Bit Twiddling Hack and was also posted here.

Count ones in BitVec in Z3 with Datalog input format

1 Answers