证明布尔表达式

Question

>>> import z3  
>>> X = z3.BitVec('X', 32)  
>>> z3.prove( X^18 == ((X|(~44)) & (X^62)) + (X&44) )  
proved

x^18 等同于 ((x|(~44))&(x^62))+(x&44)[=18= 】？？

这怎么可能？
我想知道关于证明这个公式的详细信息...

Answer 1

您可以将（中间）位向量显示为每个 8 位的符号集：

| X                       |   x7 |   x6 |   x5 |   x4 |   x3 |   x2 |   x1 |   x0  |
| 44                      |    0 |    0 |    1 |    0 |    1 |    1 |    0 |    0  |
| ~44                     |    1 |    1 |    0 |    1 |    0 |    0 |    1 |    1  |
| X|(~44)                 |    1 |    1 |   x5 |    1 |   x3 |   x2 |    1 |    1  |
| 62                      |    0 |    0 |    1 |    1 |    1 |    1 |    1 |    0  |
| X^62                    |   x7 |   x6 |  !x5 |  !x4 |  !x3 |  !x2 |  !x1 |   x0  |
| (X|(~44))&(X^62)        |   x7 |   x6 |    0 |  !x4 |    0 |    0 |  !x1 |   x0  |
| X&44                    |    0 |    0 |   x5 |    0 |   x3 |   x2 |    0 |    0  |
| (X|(~44))&(X^62)+(X&44) |   x7 |   x6 |   x5 |  !x4 |   x3 |   x2 |  !x1 |   x0  |
| X^18                    |   x7 |   x6 |   x5 |  !x4 |   x3 |   x2 |  !x1 |   x0  |

6位就够了，62可以用6位表示。

加法步骤不能产生进位，因为所有对应的位对各有一个零位。其他操作仅具有按位效果。因此，可以逐位分析等价位。

最后两行 table 表明表达式实际上是等价的。

证明布尔表达式

Proving boolean expression

bit-manipulation

z3

boolean-algebra