使用 Z3、Z3py 的 sum int-casted BitVec 结果不正确

Question

我正在使用以下 python 代码来查找两个二进制数：

• 求和到某个数
• 它们转换为整数的最高位总和必须为 2

第二个约束对我来说更重要；在我的情况下，它会扩展：假设它可能变成 [N] 数的最高位必须总和为 [M]。

我不确定为什么 z3 没有给出正确的结果。有什么提示吗？非常感谢。

def BV2Int(var):
    return ArithRef(Z3_mk_bv2int(ctx.ref(), var.as_ast(), 0), var.ctx)

def main():
    s = Solver()
    s.set(':models', True) 
    s.set(':auto-cfgig', False) 
    s.set(':smt.bv.enable_int2bv',True) 

    x = BitVec('x',4)
    y = BitVec('y',4)
    s = Solver()
    s.add(x+y == 16, Extract(3,3,x) + Extract(3,3,y) == 2)
    s.check()
    print s.model()
    # result: [y = 0, x = 0], fail both constraint

    s = Solver()
    s.add(x+y == 16, BV2Int(Extract(3,3,x)) + BV2Int(Extract(3,3,y)) == 2)
    s.check()
    print s.model()
    # result: [y = 15, x = 1], fail the second constraint

更新：感谢 Christoph 的回答。这是一个快速修复：

• Extract(3,3,x) -> ZeroExt(SZ, Extract(3,3,x)) 其中 SZ 是 RHS 的位宽减 1。

Answer 1

（旁白：auto-cfgig 应该是自动配置。）

请注意，bv2int 和 int2bv 本质上被视为未解释，因此如果这部分对您的问题至关重要，请不要使用它们（请参阅 documentation 和 previous questions）。

这个例子的问题是位向量的宽度。 x 和 y 都是 4 位变量，作为 4 位向量的数字 16 是 0（模 2^4），所以，确实 x + y 等于 16 当x=0 和 y=0。

此外，Extract(...) 项提取 1 位向量，这意味着和 Ex.. + Ex.. 再次是 1 位值，而数字 2 作为 1 位向量是 0（模 2 ^1)，即Ex... + Ex... = 2确实是这样。