奇怪的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，可以通过包括

解决此漏洞（设置选项：自动配置错误）

在脚本的开头

。