奇怪的Z3模型值 [英] strange Z3 model value

问题描述

我使用的是最新的 Z3 3.2 版.我从get-value"命令中得到了意外的响应.这是我在 SMT-LIB2 兼容模式下运行的小脚本:

(set-option :produce-models true)(declare-datatypes () ((Object o0 null)))(声明有趣的 IF (Object) Int)(declare-fun i2() Int)(断言(=(IF o0)i2))(断言 (= (IF null) 0))(检查周六)(获取值(i2))

回复是:

((i2 (IF o0)))

我希望只返回0".有什么办法可以让Z3将返回项计算为一个宇宙常数吗?

这是完整的模型:

(型号;;对象的宇宙:;;对象!val!0;;-----------;;Universe 元素的定义:(declare-fun Object!val!0 () Object);;基数约束:(forall ((x Object)) (= x Object!val!0));;-----------(define-fun i2() int(如果 o0))(define-fun IF ((x!1 Object)) Int(ite (= x!1 Object!val!0) 00)))

我也很困惑为什么 o0 没有在模型中定义.

解决方案

此问题已在 Z3 4.0 中修复.Z3 4.0即将发布.同时，您可以在线使用:http://rise4fun.com/Z3/75y>

此链接可用于执行您的示例.Z3 4.0 产生了预期的结果.

关于该错误，主要问题是 Z3 将 Object 视为未解释的排序.在 Z3 3.2 中，您可以通过包含

来解决此错误<块引用>

(设置选项:自动配置假)

在脚本的开头.

I'm using the latest Z3 version 3.2. I get an unexpected response from the "get-value" command. Here is the little script that I run in SMT-LIB2 compliant mode:

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

The response is:

((i2 (IF o0)))

I expect to get just "0" back. Is there any way to ask Z3 to evaluate the returned term to a universe constant?

Here is the full model:

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

I'm also puzzled why o0 is not defined in the model.

解决方案

This has been fixed in Z3 4.0. Z3 4.0 will be released soon. In the meantime, you can use it online: http://rise4fun.com/Z3/75y

This link can be used to execute your example. Z3 4.0 produces the expected result.

Regarding the bug, the main problem is that Z3 is treating Object as an uninterpreted sort. In Z3 3.2, you can workaround this bug by including

(set-option :auto-config false)

in the beginning of your script.

这篇关于奇怪的Z3模型值的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！