Z3py - 配列変数の制約を解く際に生成される関数k！0

Question

研究活動中、z3pyの配列（Python API for Z3 v4.4.2）を調べています。
なぜz3が結果としてより多くの配列関数を提供するのか疑問に思っていました。 ！Z3はKを使用していますように思え

>>> A = Array('A', IntSort(), IntSort()) 
>>> solve(A[0] == 0) 
[A = [0 -> 0, else -> 0], k!0 = [0 -> 0, else -> 0]] 

補助機能として0が、我々は、ドキュメントで何かを見つけるdid'nt：！たとえば、ここでK 0飛び出します。
これに関する参考情報はありますか？

Answer 1

Z3は、値にInt（配列インデックス）から関数k!0を作成し、配列にキャストします。 Pythonバインディングでは印刷されませんが、これはZ3 REPLから見ることができます。

これは、アレイモデルサブセクションhttp://rise4fun.com/Z3/tutorialcontent/guide#h26で簡単に説明されています。

(declare-const a1 (Array Int Int)) 
(assert (= (select a1 0) 0)) 
(check-sat) 
;=> sat 

(get-model) 
;=> (model 
;  (define-fun a1() (Array Int Int) 
;  (_ as-array k!0)) 
;  (define-fun k!0 ((x!0 Int)) Int 
;  (ite (= x!0 0) 0 
;   0)) 
; )