SMTLIBアレイ理論Z3の奇妙さ

Question

SMTLIBアレイを使用している間、私はZ3の理論と鉱山の理解の違いに気づいた。私は公式サイト[1]にあるSMTLIBアレイ理論[0]を使用しています。

私の問題は、単純な例で最もよく説明されていると思います。

(store (store (store ((as const (Array Int Int)) 0) 0 1) 1 2) 0 0) 
     (store (store ((as const (Array Int Int)) 0) 0 1) 1 2) 

最初の配列は、他のすべてのインデックスのインデックス1と0 2を返す必要があり、第二は、すべての他の指標のインデックス1、及び0のインデックス0、2に1を返すべきです。インデックス0 selectを呼び出すと、これを確認しているようだ：

(assert 
    (= 
     (select (store (store (store ((as const (Array Int Int)) 0) 0 1) 1 2) 0 0) 0) 
     0 
    ) 
) 
(assert 
    (= 
     1 
     (select  (store (store ((as const (Array Int Int)) 0) 0 1) 1 2)  0) 
    ) 
) 

Z3は、両方のためのsatを返します。予想通り

(assert 
    (= 
     (select (store (store (store ((as const (Array Int Int)) 0) 0 1) 1 2) 0 0) 0) 
     (select  (store (store ((as const (Array Int Int)) 0) 0 1) 1 2)  0) 
    ) 
) 

、Z3は（それは、私は、Linux-AMD64上のバージョン3.2を使用しています重要な場合には）、この場合にunsatに答えます。次は、これら二つの配列を比較してみましょう：

(assert 
    (= 
     (store (store (store ((as const (Array Int Int)) 0) 0 1) 1 2) 0 0) 
       (store (store ((as const (Array Int Int)) 0) 0 1) 1 2) 
    ) 
) 

Z3は、私は、「これら二つの配列の比較結果が等しく」と解釈され、sat私に語りました。しかし、私はこれらの配列が等価でないと予想します。私が言うSMTLIBアレイ理論、でこれを基礎：

- (forall ((a (Array s1 s2)) (b (Array s1 s2))) 
    (=> (forall ((i s1)) (= (select a i) (select b i))) 
      (= a b))) 

ので、平易な英語で、このようなものを意味するであろう「もし等しいとならない2つのアレイを、そして、彼らはすべてのインデックスに対して同じである場合にのみ」。誰も私にこれを説明できますか？私は何かを見逃したり、理論を誤解していますか？あなたがこの問題について考えていることに感謝します。

敬具、 レオン

[0] http://goedel.cs.uiowa.edu/smtlib/theories/ArraysEx.smt2 問題を報告するための[1] http://smtlib.org

Answer 1

感謝。これは配列プリプロセッサのバグです。プリプロセッサは、実際のソルバが呼び出される前に配列式を単純化します。このバグは、定数配列を使用する問題（例：((as const (Array Int Int)) 0)）にのみ影響します。定数配列を使用しないことでバグを回避することができます。私はバグを修正し、修正は次のリリースで利用可能になります。