Доказательство логического выражения

>>> 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) ??

Как это возможно?
Я хочу узнать подробную информацию о доказательстве этой формулы...


bit-manipulation z3 boolean-algebra
person ooo0o    schedule 18.11.2018    source источник
comment
что ты уже испробовал?   -  person Tobias Wilfert    schedule 18.11.2018

Ответы (1)


arrow_upward
2
arrow_downward

Вы можете отобразить (промежуточные) битовые векторы как наборы символов по 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  |

Шести бит будет достаточно, так как 62 можно выразить шестью битами.

Этап сложения не может создавать биты переноса, так как все соответствующие пары битов содержат по одному нулевому биту. Остальные операции имеют только побитовый эффект. Следовательно, можно анализировать эквивалентность битовой позиции за битовой позицией.

Последние две строки таблицы показывают, что выражения на самом деле эквивалентны.

person Axel Kemper    schedule 18.11.2018