Используйте z3 для подтверждения идентичности булевой/арифметической формулы

Я пытаюсь использовать z3 для подтверждения следующей личности:

х+у == х^у + 2*(х&у)

То есть мы можем заменить любое дополнение смесью логических и арифметических инструкций (пример взят из главы 2.2, Hacker's Delight). ).

Я использую следующий фрагмент z3 python:

from z3 import *

x = BitVec("x", 32)
y = BitVec("y", 32)

lhs = x ^ y + (2*(x&y))
rhs = x + y
s = Solver()
s.add(lhs != rhs)
print s.check()
print s.model()

Однако z3 дает мне это:

Суббота

[y = 1509949440, x = 1040187384]

Так что я полагаю, что я как-то неправильно использую API. Есть идеи, в чем моя ошибка?


python z3 z3py
person newgre    schedule 02.02.2015    source источник

Ответы (1)


arrow_upward
2
arrow_downward

По-видимому, это проблема с приоритетом оператора ^. С использованием

lhs = (x ^ y) + (2*(x&y))

заставляет пример работать на меня.

person ErikR    schedule 02.02.2015
comment
Если я изменю выражение в переменной rhs в своем коде на x-y, z3 все равно выведет SAT, даже если эта формула не эквивалентна x-y. Есть идеи, что происходит? - person newgre; 03.02.2015
comment
Можете ли вы где-нибудь предоставить полный код, чтобы убедиться, что я точно знаю, что вы пытаетесь сделать? Обратите внимание, что когда z3 находит решение lhs != rhs, это означает, что он нашел контрпример к предложению lhs == rhs. - person ErikR; 03.02.2015
comment
Приведенный выше код является полным кодом. Единственное, что я изменил, это выражения для правой стороны. до: rhs = x + y, после изменения: rhs = x - y Вывод SAT после изменения (что не может быть правдой, верно?) - person newgre; 03.02.2015
comment
SAT означает, что lhs == rhs в общем случае неверно, потому что z3 нашел контрпример, который должен распечатать. Например, (x-y) != (x^y) + (2*(x&y)) выполняется при x=1, y=1, а это означает, что x-y == (x^y) + 2*(x&y) в общем случае неверно. - person ErikR; 03.02.2015