0

我正在使用以下 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

更新：感谢克里斯托夫的回答。这是一个快速修复：

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

1 回答 1

0

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

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

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

此外，这些Extract(...)术语提取 1 位向量，这意味着和Ex.. + Ex..还是一个 1 位值，而2作为 1 位向量的数字是0(模 2^1)，即确实是这样的情况Ex... + Ex... = 2。

于 2015-08-07T12:05:31.223 回答