<p>让我们看看Z3在做什么:</p>
<pre><code>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()
</code></pre>
<p>运行此脚本时,将得到:</p>
<pre><code>$ 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))))
</code></pre>
<p>啊,它在8位向量上使用<code>bvmul</code>和<code>bvsdiv</code>。结果发现乘法对有符号无符号不重要,但除法对有符号无符号有影响。因此,映射实际上是为了将结果映射到范围<code>-128</code>到<code>127</code>而不是(正如我猜想的那样)到<code>0</code>到<code>255</code>。你知道吗</p>
<p>所以,如果你做数学运算,左边会减少到<code>-63</code>,因为乘法会产生<code>5762</code>,它会以有符号8位表示映射到<code>-126</code>。然而,右手边被简化为<code>65</code>;从而给出了一个合理的反例。你知道吗</p>
<p>为了避免这种情况,您可以使用良好的旧<code>Int</code>类型;或者通过使用<code>UDiv</code>告诉Python不要使用有符号除法,请参见这里:<a href="https://z3prover.github.io/api/html/namespacez3py.html#a64c02a843a4ac8781dd666a991797906" rel="nofollow noreferrer">https://z3prover.github.io/api/html/namespacez3py.html#a64c02a843a4ac8781dd666a991797906</a></p>
<p>如果您使用<code>UDiv</code>,您可以得到一个更好的反例:</p>
<pre><code>>>> 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
</code></pre>
<p>我想这正是你所期待的。你知道吗</p>