z3py는 : 콘크리트 값

Question

내가 Z3의 파이썬 API를 사용하고 [버전 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

simplifier은 배열에서 가장 저렴한 재 작성을 적용합니다. 그래서 같은 키에 대해 두 개의 인접한 저장소를 찾으면 가장 안쪽의 키를 스쿼시하는 것을 알고 있습니다. 일반적으로 중복되는 키를 찾는 데는 많은 비용이 들며, 또한 키가 겹치는 지 여부를 결정할 수없는 변수가 될 수 있습니다.