z3 - 使用 Datalog 输入格式在 Z3 中的 BitVec 中计数

Question

是否有一种紧凑的方法可以使用 Datalog 输入格式计算 Z3 中 BitVec 中设置为 1 的位数？

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

目前接受的这个问题的答案：Count one in Z3 in BitVec with SMT 2 input format指出在 SMT 2 输入格式中没有很好的方法。

这个问题目前接受的答案：Sum of all the bits in a Bit Vector of Z3展示了如何在 Python 中执行此操作。

标签： z3datalog

Answer 1

对于32 bit向量，您可以尝试将以下伪代码转换为 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

这被称为Bit Twiddling Hack并且也被张贴在这里。