1

我正在使用最新的 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。

4

1 回答 1

1

这已在 Z3 4.0 中修复。Z3 4.0 即将发布。同时，您可以在线使用它：http ://rise4fun.com/Z3/75y

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

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

（设置选项：自动配置假）

在脚本的开头。

于 2012-04-17T21:08:58.950 回答