z3 中如何定义 Int 排序（SMT-LIB 2.0 Ints 理论）和动态声明排序？
这是我使用 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 的回答是不饱和。
您能帮我理解这个结果吗？具体来说，z3 如何解释排序 Int ？它真的被认为是无限的吗？动态声明的排序（这里是排序 PZ）怎么样？
Here is an SMT-LIB 2.0 benchmark which I executed with z3 :
(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)
I expected the result to be sat, with at least a model where PZ is the powerset of Z (integers) and MS is a predicate which tests the membership of an integer into a subset of Z (an element of the sort PZ).
But z3 answered unsat.
Could you help me understanding this result please ? Specifically, how does z3 interprets the sort Int ? Is it really considered infinite ? What about dynamically declared sort (here the sort PZ) ?
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（1）
在 Z3 中，
Int是无限的。你是对的，结果一定是sat。unsat结果是由于 Z3 模块之一中的错误造成的。我已经修复了这个错误。实施中的一个临时缓存没有被重置。该修复将在下一版本中提供。同时，您可以在脚本开头使用以下命令来禁用有缺陷的模块。
顺便说一句，该错误仅影响包含
(= xy)形式文字的示例，其中x和y是通用变量。顺便说一句，虽然你的例子是令人满意的，但 Z3 无法为其构建模型（即使在错误修复之后）。实际上，在错误修复后，Z3 生成的答案是
未知。模型查找器（Z3 中使用）只能查找未解释排序（例如 PZ）的解释有限的模型。此限制将来可能会改变。
In Z3,
Intis infinite. You are correct, the result must besat. Theunsatresult is due to a bug in one of the Z3 modules. I've already fixed the bug. One temporary cache in the implementation was not being reset. The fix will be available in the next release.In the meantime, you can disable the buggy module by using the following command in the beginning of your script.
BTW, the bug only affects examples that contain literals of the form
(= x y)wherexandyare universal variables.BTW, although your example is satisfiable, Z3 can't build a model for it (even after the bug fix). Actually, after the bug fix, Z3 produces the answer
unknown.The model finder (used in Z3) is only capable of finding models where the interpretation of uninterpreted sorts (such as PZ) is finite. This limitation may change in the future.