Как устранить битвекторную арифметику в Z3

Question

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

not ((not x) add y)

что равно

x sub y

по этому коду:

(declare-const x (_ BitVec 32))
(declare-const y (_ BitVec 32))
(assert (= (bvnot (bvadd (bvnot x) y)) (bvsub x y)))
(check-sat)
(simplify (bvnot (bvadd (bvnot x) y)))

Я хочу получить результат как:

sat
(bvsub x y) 

Тем не менее, результат:

sat
(bvnot (bvadd (bvnot x) y))

Кто-нибудь поможет мне?

Answer 1

Мы можем доказать это (bvnot (bvadd (bvnot x) y)) эквивалентно (bvsub x y) используя следующий скрипт.

(declare-const x (_ BitVec 32))
(declare-const y (_ BitVec 32))
(assert (not (= (bvnot (bvadd (bvnot x) y)) (bvsub x y))))
(check-sat)

В этом сценарии мы использовали Z3, чтобы показать, что (not (= (bvnot (bvadd (bvnot x) y)) (bvsub x y))) неудовлетворительно. То есть невозможно найти значения для x а также y такой, что значение (bvnot (bvadd (bvnot x) y)) отличается от значения (bvsub x y),

В Z3 simplify Команда просто применяет правила перезаписи и игнорирует набор утвержденных выражений. simplify Команда намного быстрее, чем проверка соответствия с помощью check-sat, Более того, учитывая два эквивалентных выражения F а также G, нет гарантии, что результат (simplify F) будет равен (simplify G), Например, в Z3 v4.3.1 команда упрощения дает разные результаты для (= (bvnot (bvadd (bvnot x) y) а также (bvsub x y), хотя они являются эквивалентными выражениями. С другой стороны, он дает тот же результат для (= (bvneg (bvadd (bvneg x) y) а также (bvsub x y),

(simplify (bvnot (bvadd (bvnot x) y)))
(simplify (bvneg (bvadd (bvneg x) y)))
(simplify (bvsub x y))

Вот полный скрипт для приведенных выше примеров.

Кстати, эти примеры гораздо более читабельны, если мы используем интерфейс Z3 Python.

x, y = BitVecs('x y', 32)
prove(~(~x + y) == x - y)
print simplify(x - y)
print simplify(~(~x + y))
print simplify(-(-x + y))

Наконец, Z3 имеет более сложные процедуры упрощения. Они доступны как Тактика. Учебники в формате Python и SMT 2.0 предоставляют дополнительную информацию.

Другая возможность состоит в том, чтобы изменить Z3 проще / переписать. Как вы указали, not x эквивалентно -x -1, Мы можем легко добавить это правило переписывания: not x --> -x - 1 переписчику Z3. В качестве примера, в этом коммите я добавил новую опцию "bvnot2arith", которая включает это правило. Реальная реализация очень мала (5 строк кода).