Z3Py证明函数returns错误的反例

Question

我正在尝试使用 Z3Py 证明函数，但它似乎 return 是一个不正确的反例。问题是什么？？ (Z3-4.7.1-x86-win, Python-2.7.15)

>>> import z3
>>> A = z3.BitVec('A', 8)
>>> B = z3.BitVec('B', 8)
>>> C = z3.BitVec('C', 8)
>>> z3.prove((A*B)/C == A*(B/C))
counterexample
[A = 67, B = 86, C = 2]
>>> ((67*86)%256)/2
65
>>> (67*(86/2))%256
65

Answer 1

我认为您遇到了算术问题 "modulo 8"（8 位宽度）：A*B（均为 8 位值）无法表示为 8 位值，导致一些 wrap-around/clipping.

这些类型的等式一般不适用于固定宽度的数学。

Answer 2

让我们看看Z3在做什么：

import z3
A = z3.BitVec('A', 8)
B = z3.BitVec('B', 8)
C = z3.BitVec('C', 8)

s = z3.Solver()
s.add((A*B)/C == A*(B/C))
print s.sexpr()

当你运行这个脚本时，你会得到：

$ python a.py
(declare-fun C () (_ BitVec 8))
(declare-fun B () (_ BitVec 8))
(declare-fun A () (_ BitVec 8))
(assert (= (bvsdiv (bvmul A B) C) (bvmul A (bvsdiv B C))))

啊，它在 8 位向量上使用 bvmul 和 bvsdiv。事实证明，乘法对于有符号-无符号无关紧要，但除法却很重要。因此，实际上完成映射是为了将结果映射到 -128 到 127 的范围，而不是（正如我怀疑您可能已经预料到的那样）映射到 0 到 255。

所以，如果你做数学运算，左边会减少到 -63，因为乘法产生 5762，它被映射到有符号 8 位的 -126表示。然而，右侧被缩减为 65；从而给你合法的反例。

为避免这种情况，您可以使用旧的 Int 类型；或通过使用 UDiv 告诉 Python 不使用有符号除法，请参见此处：https://z3prover.github.io/api/html/namespacez3py.html#a64c02a843a4ac8781dd666a991797906

如果使用UDiv，可以得到更好的反例：

>>> import z3
>>> A = z3.BitVec('A', 8)
>>> B = z3.BitVec('B', 8)
>>> C = z3.BitVec('C', 8)
>>> z3.prove(z3.UDiv(A*B, C) == A*z3.UDiv(B, C))
counterexample
[A = 95, B = 140, C = 41]
>>> ((95*140)%256/41)%256
5
>>> (95*((140/41)%256))%256
29

我想这更符合您的预期。

Z3Py证明函数returns错误的反例

Z3Py prove function returns wrong counterexample

python

z3

z3py