这是我使用 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) ?
In Z3, Int是无限的。你是对的，结果一定是sat. The unsat结果是由于 Z3 模块之一中的错误造成的。我已经修复了这个错误。实施中的一个临时缓存没有被重置。该修复将在下一版本中提供。
同时，您可以在脚本开头使用以下命令来禁用有缺陷的模块。
(set-option :mbqi false)
顺便说一句，该错误仅影响包含以下形式文字的示例(= x y) where x and y是通用变量。
顺便说一句，虽然你的例子是令人满意的，但 Z3 无法为其构建模型（即使在错误修复之后）。事实上，在bug修复之后，Z3给出了答案unknown。
模型查找器（Z3 中使用）只能查找未解释排序（例如 PZ）的解释有限的模型。此限制将来可能会改变。
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
