z3py - 我想将 BitVec 的 hammingWeight 添加到求解器，但它有问题

Question

我首先给BitVec添加了约束，然后将这些BitVec的汉明权重添加到约束中，但是汉明权重的约束不起作用

我将解放入约束中，解满足第一部分的约束，但不满足汉明权重的约束

    from z3 import *

    s=Solver()

    def hammingWeight(x,n):
        return sum(ZeroExt(n,Extract(i,i,x)) for i in range(n))

    rounds=3
    weight=3

    x=[BitVec('x'+str(i),16) for i in range(rounds+1)]
    y=[BitVec('y'+str(i),16) for i in range(rounds+1)]
    z=[BitVec('z'+str(i),16) for i in range(rounds)]
    hw=[BitVec('z'+str(i),16) for i in range(rounds)]

    def round(r,x,y,z,hw):
        varbits=RotateLeft(x[r],8)|RotateLeft(x[r],1)
        doublebits=RotateLeft(x[r],1)&(~(RotateLeft(x[r],8))&RotateLeft(x[r],15))
        y[r+1]=x[r]
        x[r+1]=y[r]^z[r]^RotateLeft(x[r],2)
        hw[r]=varbits^doublebits
        s.add(z[r]&varbits==0,(z[r]^RotateLeft(z[r],7))&doublebits==0)

    for r in range(rounds):
        round(r,x,y,z,hw)
    s.add(hammingWeight(x[0],16)+hammingWeight(y[0],16)!=0)
    hw=0
    for r in range(rounds):
        hw+=hammingWeight(hw[r],16)

    s.add(hw<=weight)
    print(s.check())
    print(s.model())

解决方案找到一个模型，但模型未满足约束：hw<=weight

标签： z3py

Answer 1

当我运行你的程序时，我得到：

Traceback (most recent call last):
  File "a.py", line 29, in <module>
    hw+=hammingWeight(hw[r],16)
TypeError: 'int' object has no attribute '__getitem__'

这是因为您hw已从位向量列表重新定义，然后将其分配给0. 也许是剪切粘贴错误？请先修复后重新发布。