时间戳

首页 > 解决方案 > 限定排序范围

z3 - 限定排序范围

问题描述

我试图通过 SMT-LIB 限制新定义的排序范围。这样做可以通过减少必要断言的数量来简化我的脚本。

为此，我使用了define-sort和forall。

(define-sort R () Real)
(assert (forall ((x R)) (< 0 x)))
(declare-const r R)
(check-sat)

但是无论如何 z3 总是返回unsat。所以我想这是不可能的。是吗？

标签： z3smt

解决方案

不幸的是，这在 SMTLib 中是不可能的。有关详细信息，请参阅此答案：Z3 中是否存在 UnsignedIntSort？

正如克里斯托夫指出的那样，您的查询是unsat因为量化的断言是错误的；unsat无论您可能有什么其他约束，这都会使求解器处于状态。

以我的经验，处理这些场景的最好方法是不直接使用 SMTLib；而是使用更高级别的 API 并使用这些环境提供的编程功能来根据需要吐出所有> 0约束。它毛茸茸且丑陋，但它是目前在 SMTLib 中处理这些问题的唯一方法。唯一支持这种“谓词子类型化”的求解器是 Yices v1.0，它有自己的输入语言，不再受支持。

推荐阅读