奇怪的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評估返回的宇宙常數？

以下是完整的模式：

(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未在模型中定義。

Answer 1

這已在Z3 4.0中修復。 Z3 4.0即將發佈。同時，您可以在線使用它：http://rise4fun.com/Z3/75y

此鏈接可用於執行您的示例。 Z3 4.0產生預期的結果。

關於這個bug，主要問題是Z3將對象視爲未解釋的類型。 在Z3 3.2，可以通過包括

解決此漏洞（設置選項：自動配置錯誤）

在腳本的開頭

。