types - 如何在 z3 中定义 Int 排序(SMT-LIB 2.0 Ints 理论)和动态声明的排序？

Question

这是我使用 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)怎么样？

Answer 1

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

(set-option :mbqi false)

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

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