Z3 4.0 模型中的额外输出答案

【问题标题】：Z3 4.0 Extra Output in ModelZ3 4.0 模型中的额外输出
【发布时间】：2012-06-11 15:24:09
【问题描述】：

当我尝试获取模型字符串以及我定义的变量时，我会在模型中获得额外的输出 -

 z3name!0=3, z3name!1=-2, z3name!10=0, z3name!11=0, z3name!12=0, z3name!13=0, z3name!14=0, z3name!15=0, z3name!2=0, z3name!3=0, z3name!4=2, z3name!5=2, z3name!6=0, z3name!7=-3, z3name!8=2, z3name!9=0

我想知道这是错误的输出吗？还是Z3正在使用的一些中间变量？

因为我定义的变量的值对我来说似乎没问题。我以前没有见过任何这样的输出，因此我有这个疑问。

【问题讨论】：

标签： z3

【解决方案1】：

我意识到这是一个老话题，但我发现自己遇到了和莱昂纳多所说的一样的“错误”。由于 OP 没有发布他的代码，我认为我的可能可以帮助修复它（即使只要确实保留了正确性，这个额外的输出对我来说不是问题）。

看来，如果我将最终断言中的“/”更改为“+”运算符，问题就会消失。

(declare-fun fun0!0 () Int)
(declare-fun fun0!-1 () Int)
(declare-fun var0 () Int)

(assert (and
    (and
        (or (= fun0!0 0) (= fun0!0 1) (= fun0!0 2))
        (or (= fun0!-1 0) (= fun0!-1 1) (= fun0!-1 2))
        (or (= var0 1) (= var0 -1))
    )
    (and (or (= var0 0) (= var0 -1)))
))

(define-fun fun0 ((i! Int)) Int
    (ite
        (= i! 0)
        fun0!0
        (ite
            (= i! -1)
            fun0!-1
            (- 0 1)
        )
    )
)

(assert (=
    (fun0 var0)
    (/ var0 var0)
))
(check-sat)

【讨论】：

【解决方案2】：

Z3 有几个预处理步骤。其中一些引入了新变量。新变量通常会从结果模型中删除。如果不是，这是一个错误。但是，此错误不会影响正确性。这只是一个不便。

如果您能发布您的问题，那就太好了。我们将能够确定哪个预处理步骤没有消除引入的辅助变量。

【讨论】：