Z3 SMT Sovler中的Hamming权方程

Question

我有一个方程组要解，其中有一些hamming权的方程。汉明权重通常是一个数字的二进制表示中的1的个数。我试图在Z3 SMT Solver中求解，但它输出一个错误，说明"；b"没有当前的模型"；。我试图找到一个32位的数字，给定的hamming权和一些方程。

在下面的例子中，我试图找到一个hamming权重等于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"没有当前的模型"；。

有人能帮我解决这个问题吗？

编辑：我把hamming方程弄错了；它将是

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。