z3py：私はZ3のPythonのAPIを使用しています具体的な値

Question

でネストされた店舗を簡素化し、[バージョン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

シンプリはアレイ上の最も安い書き換えを適用します。 したがって、同じキーに対して2つの隣接するストアが見つかると、最も内側のキーを押しつぶすことがわかります。 一般に、重複するキーを見つけるのに高いコストがかかります。さらに、キーが重複しているかどうかを判断できない変数もあります。