如何在 z3 中定义 Int 排序（SMT-LIB 2.0 Ints 理论）和动态声明的排序？答案

【问题标题】：How are Int sort (of SMT-LIB 2.0 Ints theory) and dynamically declared sorts defined in z3?如何在 z3 中定义 Int 排序（SMT-LIB 2.0 Ints 理论）和动态声明的排序？
【发布时间】：2011-12-31 11:14:11
【问题描述】：

这是我使用 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，至少有一个模型，其中PZ 是Z（整数）的幂集，MS 是一个谓词，用于测试一个整数转换为 Z 的子集（PZ 排序的元素）。

但是z3回答了unsat。

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

【问题讨论】：

标签： types set z3 smt

【解决方案1】：

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

(set-option :mbqi false)

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

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

【讨论】：

感谢您的回答@Leonardo，我期待着使用下一个版本。但是，当我禁用 MBQI 模块（使用 z3-3.2）时，答案仍然是 unsat。你也一样吗？
你也应该使用(set-option :auto-config false)。对外发布时开启自动配置，会开启mbqi。