Блог

Я использую 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)
  

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