2

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

z3 ガイドの例では、そのような値にアクセスできます。
たとえば、次のような質問に対して

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

次のような答えが得られます

(((select my_array 0) 1))

の値が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 の応答は次のとおりです。

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))
4

1 に答える 1

3

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

  • 配列理論を含むロジックを指定します。(set-logic QF_AUFLIA)例: 例の先頭に追加します。

  • 自動構成を無効にします (Z3 は利用可能なすべての理論をインストールします)。コマンドを追加し(set-option :auto-config false)ます。

于 2011-12-30T15:55:53.237 に答える