z3モデルの配列用語の値

Question

私は私の研究にz3を使用していますが、私は以下の問題があります。私は配列と未解釈関数を含む充足可能な数式のモデルを分析しています。私は特定の配列のエントリを検査してみたいと思います。

z3ガイドの例では、このような値にアクセスできます。
例えば、

(get-value ((select my_array 0))) 

のような質問のための位置0でmy_arrayの値が1であることを示す

(((select my_array 0) 1)) 

ような回答を得ます。

しかし、私が得る答えは全く非常に有用ではありません

(((select my_array 0) (select Array!val!0 0))) 

のように見えます。私はこのようになりますブロックを取得するモデルの冒頭にも

、：

;; universe for (Array Int Int): 
    ;; Array!val!10 Array!val!6 Array!val!0 Array!val!5 Array!val!9 Array!val!1 Array!val!11 Array!val!4 Array!val!2 Array!val!7 Array!val!3 Array!val!8 
    ;; ----------- 
    ;; definitions for universe elements: 
    (declare-fun Array!val!10() (Array Int Int)) 
    (declare-fun Array!val!6() (Array Int Int)) 
    (declare-fun Array!val!0() (Array Int Int)) 
    (declare-fun Array!val!5() (Array Int Int)) 
    (declare-fun Array!val!9() (Array Int Int)) 
    (declare-fun Array!val!1() (Array Int Int)) 
    (declare-fun Array!val!11() (Array Int Int)) 
    (declare-fun Array!val!4() (Array Int Int)) 
    (declare-fun Array!val!2() (Array Int Int)) 
    (declare-fun Array!val!7() (Array Int Int)) 
    (declare-fun Array!val!3() (Array Int Int)) 
    (declare-fun Array!val!8() (Array Int Int)) 
    ;; cardinality constraint: 
    (forall ((x (Array Int Int))) 
      (and (= x Array!val!10) 
       (= x Array!val!6) 
       (= x Array!val!0) 
       (= x Array!val!5) 
       (= x Array!val!9) 
       (= x Array!val!1) 
       (= x Array!val!11) 
       (= x Array!val!4) 
       (= x Array!val!2) 
       (= x Array!val!7) 
       (= x Array!val!3) 
       (= x Array!val!8))) 
    ;; ----------- 

私は本当にこの意味を理解していない、何とかこれは私の問題に関連しているようで、同様のブロックはではありません。はガイドの簡単な例を示しています。誰がz3のこの動作を引き起こすのか、それを回避する方法を知っていますか？

実験の結果、望ましくない動作を示す「最小」の例が見つかりました。それは、インデックス式で未解釈の関数を使うことと関係しているようです。これに

(declare-fun my_function ((Int)(Int)) Int) 
(declare-fun my_array() (Array Int Int)) 

(assert 
    (= 
    (select my_array (my_function 0 1)) 
    (select my_array (my_function 1 0)) 
) 
) 

(check-sat) 
(get-model) 
(get-value ((select my_array (my_function 0 1)))) 
(get-value ((my_function 0 1))) 

Z3の応答は次のとおりです。SMTで

sat 
(model 
;; universe for (Array Int Int): 
;; Array!val!0 
;; ----------- 
;; definitions for universe elements: 
(declare-fun Array!val!0() (Array Int Int)) 
;; cardinality constraint: 
(forall ((x (Array Int Int))) (= x Array!val!0)) 
;; ----------- 
(define-fun my_array() (Array Int Int) 
Array!val!0) 
(define-fun my_function ((x!1 Int) (x!2 Int)) Int 
(ite (and (= x!1 0) (= x!2 1)) 2 
(ite (and (= x!1 1) (= x!2 0)) 3 
2))) 
) 
(((select my_array (my_function 0 1)) (select Array!val!0 2))) 
(((my_function 0 1) 2)) 

Answer 1

、 "論理" 式を構築するために利用可能な理論を指定します。たとえば、コマンド(set-logic QF_UFLIA)が使用されている場合、解釈されない関数と線形整数演算が使用できます。コマンドset-logicを使用してロジックが指定されていない場合。 Z3は自動的にユーザーのロジックを推測し、必要な理論だけをインストールします。あなたの例では、Z3はあなたの例が配列理論を必要としていないと誤って推測しています。したがって、(Array Int Int)は未解釈のソートとして扱われます。 これは、Z3が（Array Int Int）が解釈されていないソートであると仮定し、生成されたモデルでその解釈を提供する理由です。これはバグです。私は次のリリースで修正します。一方 、あなたはこのバグを回避するために、次のいずれかの方法を使用することができます。

• は、配列の理論が含まれているロジックを指定します。例：例の先頭に(set-logic QF_AUFLIA)を追加します。

• 自動設定を無効にします（利用可能なすべての理論がインストールされます）。コマンド(set-option :auto-config false)を追加します。