Z3Py prove函数返回错误的counterexamp

Question

我试图使用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

Answer 1

我认为您看到了算术“模8”（8位宽度）的一个问题：a*B（两个8位值）不能表示为8位值，导致一些环绕/剪裁。你知道吗

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

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

我想这正是你所期待的。你知道吗