Упростите выражение z3 bitvector, но избегайте извлечения и конкатата - PullRequest
Новая
       73

Упростите выражение z3 bitvector, но избегайте извлечения и конкатата

2 голосов
/ 27 июня 2019

Мне было интересно, можно ли заставить z3 не использовать Extract и Concat в выходном выражении, когда к выражению с битовыми векторами применено simplify.

Например, вместо 

>>> x = BitVector("x", 32)
>>> simplify(x ^ 7 ^ 6)
Concat(Extract(31, 1, x), ~Extract(0, 0, x))

Я хотел бы получить 

>>> x = BitVector("x", 32)
>>> simplify(x ^ 7 ^ 6)
x ^ 1

Я посмотрел на help_simplify, но не смог найти такой "вариант".

1 Ответ

2 голосов
/ 27 июня 2019

не легко. z3 преобразует XOR с цифрами в маску довольно рано в переписывающем устройстве, и, похоже, нет простого способа контролировать это поведение. Смотрите здесь: https://github.com/Z3Prover/z3/blob/master/src/ast/rewriter/bv_rewriter.cpp#L1817-L1823

Сказав это, преимущество программируемого API состоит в том, что z3 предоставляет вам все инструменты для самостоятельного кодирования таких преобразований. Это не означает, что это легко сделать, но, по крайней мере, оно предоставляет все необходимые фрагменты. Несмотря на то, что выполнение всей работы по переписыванию именно того, что вы хотите, может быть большой задачей, вы можете избежать неприятностей с помощью чего-то простого: 

def constFold(e):
    try:
       if is_app(e) and all([is_bv_value(c) for c in e.children()]):
          return simplify(e)
       else:
          return e
    except:
        return e

Это чрезвычайно простодушно; и это даже не решает проблему, которую вы поставили: 

>>> constFold(x^6^7)
x ^ 6 ^ 7

Но он справляется с этим: 

>>> constFold(x^(6^7))
x ^ 1

Но для 8 строк кода это не так уж плохо! Дело в том, что вы можете улучшить его, пройдя по структуре выражений, узнав ассоциативность / коммутативность и т. Д., И выполнив любые преобразования, которые вы хотите использовать в AST, как показано в программируемом API.

Имейте в виду, что если вы используете это в контексте решателя, вы должны поддерживать кучу инвариантов, и если вы делаете «неправильное» преобразование, вы можете легко сделать решатель несостоятельным. С большой властью приходит большая ответственность! Тем не менее, с помощью простого программирования можно многого достичь, если вы хотите изучить API и совершить глубокое погружение.

Удачи!

...