4

这是我使用 z3 执行的 SMT-LIB 2.0 基准测试：

(set-logic AUFLIA)
(declare-sort PZ 0)
(declare-fun MS (Int PZ) Bool)

(assert (forall ((x Int)) (exists ((X PZ)) 
            (and (MS x X) 
                 (forall ((y Int)) (=> (MS y X) (= y x)))))))
(check-sat)

我预计结果是sat，至少有一个模型，其中ZPZ的幂集（整数）是一个谓词，用于测试整数在Z的子集（排序的元素）中的成员资格。MSPZ

但是z3回答了unsat。

你能帮我理解这个结果吗？具体来说，z3 如何解释 sort Int？它真的被认为是无限的吗？那么动态声明的排序（这里是排序PZ）呢？

4

1 回答 1

3

在 Z3 中，Int是无限的。你是对的，结果一定是sat。结果unsat是由于 Z3 模块之一中的错误造成的。我已经修复了这个错误。实施中的一个临时缓存没有被重置。该修复程序将在下一个版本中提供。同时，您可以在脚本开头使用以下命令禁用错误模块。

(set-option :mbqi false)

顺便说一句，该错误仅影响包含(= x y)wherex和y是通用变量形式的文字的示例。

顺便说一句，尽管您的示例令人满意，但 Z3 无法为其构建模型（即使在错误修复之后）。实际上，在修复错误之后，Z3 会产生答案unknown。模型查找器（在 Z3 中使用）仅能够查找未解释类型（例如 PZ）的解释是有限的模型。此限制将来可能会改变。

于 2011-11-17T17:21:54.897 回答