问题描述
我有一个方程组要求解，其中有一些汉明重量方程。汉明权通常是一个数字的二进制表示中 1 的数量。 我试图在 Z3 SMT Solver 中求解，但它输出一个错误，指出“b'没有当前模型”。我试图找到一个具有给定汉明权重和一些方程的 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 ]
谢谢
解决方法
这是 Python 中的运算符优先级。这有效：
Eq = [(K[0]&0x1) + (K[0]&0x2) + (K[0]&0x4) + (K[0]&0x8) + (K[0]&0x10) == 3]
但是，您实际上并没有以这种方式计算汉明重量。每个术语都需要转换。例如。 K[0]&0x8 不是零或一，而是 0x8 或 0x0。