z3py: упростить вложенные хранилища с конкретными значениями

Я использую python API Z3 [версия 4.4.2 - 64 бит] и пытаюсь понять, почему z3 упрощает выражение в этом случае:

>>> a = Array('a', IntSort(), IntSort())
>>> a = Store(a, 0, 1)
>>> a = Store(a, 0, 3)
>>> simplify(a)
Store(a, 0, 3)

но это не в этом случае:

>>> a = Array('a', IntSort(), IntSort())
>>> a = Store(a, 0, 1)
>>> a = Store(a, 1, 2)
>>> a = Store(a, 0, 3)
>>> simplify(a) 
Store(Store(Store(a, 0, 1), 1, 2), 0, 3)

python z3 z3py
person Bageyelet    schedule 17.10.2016    source источник

Ответы (1)


arrow_upward
0
arrow_downward

Упрощение применяет только самые дешевые перезаписи массивов. Поэтому, если он находит два соседних хранилища для одного и того же ключа, он знает, что нужно раздавить самый внутренний ключ. Как правило, поиск перекрывающихся ключей требует больших затрат, и, кроме того, ключи могут быть переменными, когда невозможно определить, перекрываются ли они.

person Nikolaj Bjorner    schedule 17.10.2016
comment
Спасибо за ответ! Есть ли способ упростить выражение во втором случае? - person Bageyelet; 20.10.2016