Z3Py 证明函数返回错误的反例答案

【问题标题】：Z3Py prove function returns wrong counterexampleZ3Py 证明函数返回错误的反例
【发布时间】：2018-10-11 14:08:27
【问题描述】：

我正在尝试使用 Z3Py 证明函数，但它似乎返回了一个不正确的反例。问题是什么？？ (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

【问题讨论】：

标签： python z3 z3py

【解决方案1】：

让我们看看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))))

啊，它使用 bvmul 和 bvsdiv 超过 8 位向量。事实证明，乘法对于有符号无符号无关紧要，但除法确实如此。因此，映射实际上是为了将结果映射到-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

这更符合我的预期。

【讨论】：

【解决方案2】：

我认为您看到算术“模 8”（8 位宽度）存在问题：A*B（两个 8 位值）不能表示为 8 位值，导致一些环绕/剪辑。

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

【讨论】：