最新の Z3 バージョン 3.2 を使用しています。「get-value」コマンドから予期しない応答が返されました。SMT-LIB2 準拠モードで実行する小さなスクリプトを次に示します。
(set-option :produce-models true)
(declare-datatypes () ((Object o0 null)))
(declare-fun IF (Object) Int)
(declare-fun i2 () Int)
(assert (= (IF o0) i2))
(assert (= (IF null) 0))
(check-sat)
(get-value (i2))
応答は次のとおりです。
((i2 (IF o0)))
ちょうど「0」が返ってくると思います。返された項をユニバース定数に評価するように Z3 に依頼する方法はありますか?
完全なモデルは次のとおりです。
(model
;; universe for Object:
;; Object!val!0
;; -----------
;; definitions for universe elements:
(declare-fun Object!val!0 () Object)
;; cardinality constraint:
(forall ((x Object)) (= x Object!val!0))
;; -----------
(define-fun i2 () Int
(IF o0))
(define-fun IF ((x!1 Object)) Int
(ite (= x!1 Object!val!0) 0
0))
)
モデルで o0 が定義されていない理由にも困惑しています。