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

Question

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

Answer 1

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