奇妙なZ3モデル値

Question

私は最新の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に依頼する方法はありますか？ O0がモデルに定義されていない理由を私も困惑してい

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

：

はここでフルモデルです。

Answer 1

これはZ3 4.0で修正されています。 Z3 4.0はすぐにリリースされる予定です。その間、オンラインで使用できます。http://rise4fun.com/Z3/75y

このリンクは、あなたの例を実行するために使用できます。 Z3 4.0は期待される結果をもたらします。

主な問題は、Z3がObjectを未解釈のソートとして扱っていることです。 はZ3 3.2では、あなたは

を含めることによって、このバグを回避することができます（セットオプション：偽自動設定）あなたのスクリプトの先頭で

を。