z3 - Z3 SMT Sovler 中的汉明权重方程

Question

我有一个方程组要求解，其中有一些汉明权重方程。汉明权重通常是数字的二进制表示中 1 的数量。我试图在 Z3 SMT Solver 中求解，但它输出一个错误，指出“b'there is no current model”。我试图找到一个具有给定汉明权重和一些方程的 32 位数字。

在下面的示例中，我试图找到一个汉明权重等于 3 的数字（0 到 2^5-1）。

from z3 import *
s = Solver()
K = [BitVec('k%d'%i,5) for i in range(3)]    

Eq = [K[0]&0x1 + K[0]&0x2 + K[0]&0x4 + K[0]&0x8 + K[0]&0x10 == 3]  #
s.add(Eq)
s.check()
print(s.model())

这给出了错误“b'没有当前模型”。

谁能帮我解决这个问题？

编辑：我把汉明方程弄错了；这将是

Eq = [(K[0]&0x1) +  ((K[0]&0x2)>>1) +  ((K[0]&0x4)>>2) +  ((K[0]&0x8)>>3) +  ((K[0]&0x10)>>4) == 3 ]

谢谢

Answer 1

这是 Python 中的运算符优先级。这有效：

Eq = [(K[0]&0x1) + (K[0]&0x2) + (K[0]&0x4) + (K[0]&0x8) + (K[0]&0x10) == 3]

但是，您实际上并没有以这种方式计算汉明权重。每个术语都需要转换。例如K[0]&0x8，不是零或一，而是0x8或0x0。