Я пытаюсь использовать 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))
Кто-нибудь поможет мне?
Мы можем доказать, что (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 имеет более сложные процедуры упрощения. Они доступны как Tactics. Учебники по Python и SMT 2.0 предоставляют дополнительную информацию.
Другая возможность состоит в том, чтобы модифицировать Z3, упрощая/переписывая. Как вы указали, not x эквивалентно -x -1. Мы можем легко добавить это правило перезаписи: not x --> -x - 1 к переписывателю Z3. Например, в этом коммите я добавил новый параметр под названием "bvnot2arith", который включает это правило. Фактическая реализация очень мала (5 строк кода).
bvnot и bvneg. Что мне здесь нужно, IS побитовая операция "не". Как мы все знаем, в бит-векторной арифметике -x = not x + 1 => not x = -x - 1, таким образом, not ((not x) + y) = -((-x - 1) + y) - 1 = x + 1 - y - 1 = x - y. Тем не менее, Tactics, о которых вы упомянули, действительно помогают мне, согласно Пользовательские упростители, вопрос, на который вы уже ответили. Похоже, мне нужна собственная тактика, верно? В любом случае, спасибо за вашу помощь.
- person bwdeng; 28.12.2012
not x --> -x -1 в качестве примера того, как взломать переписчик Z3 (z3.codeplex. com/SourceControl/changeset/8515044f8bec)
- person Leonardo de Moura; 28.12.2012
