z3 - 「array-ext」を含むモデルから具体的な値を取得する

Question

配列と量指定子を組み合わせると、Z3 は のアプリケーションを含むモデルを生成することがよくありますarray-ext。たとえば、このテスト ケースは次のモデルを生成します。

(define-fun pipeid () (Array Int Int)
  (_ as-array k!2))
(define-fun valid () (Array Int Bool)
  (_ as-array k!0))
(define-fun ispipe () (Array Int Bool)
  (_ as-array k!1))
(define-fun pipeid_ab () Int
  2)
(define-fun fd () Int
  0)
(define-fun k!3 ((x!1 Int)) Int
  (ite (= x!1 0) 0
    (array-ext (_ as-array k!0) (_ as-array k!1))))
(define-fun k!0!4 ((x!1 Int)) Bool
  (ite (= x!1 3) false
    true))
(define-fun k!0 ((x!1 Int)) Bool
  (k!0!4 (k!3 x!1)))
(define-fun k!1 ((x!1 Int)) Bool
  true)
(define-fun k!2!5 ((x!1 Int)) Int
  (ite (= x!1 3) 4
    1))
(define-fun k!2 ((x!1 Int)) Int
  (k!2!5 (k!3 x!1)))

まず、array-extin とはk!3どういう意味ですか? a [ x ] != b [ x(array-ext a b) ] であるインデックスxをつなぎ合わせましたが、つなぎ合わせたものが正しくないか、以上の循環定義に頭を包むことができません。k!0k!3

第二に、そのようなモデルから具体的な値を抽出するにはどうすればよいですか? 一般に、配列の具体的な値をモデルで直接表現することはできないことはわかっていますが、少なくともその具体的な値が何であるかを理解し、モデルから何らかの形で抽出できるようにしたいと考えています。個々の配列インデックスをクエリしても役に立たないようです。

 model.evaluate(pipeid[1]) => If(array-ext(as-array, as-array) = 3, 4, 1)

ありがとう。