限定排序范围

【问题标题】：Limit scope of defined sort限定排序范围
【发布时间】：2019-09-18 07:51:58
【问题描述】：

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

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

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

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

【问题讨论】：

(forall ... 是不可满足的，因为并非所有实数都大于 0。您可能正在寻找暗示，例如(forall ... (implies (< 0 x) (some other constraint)) 这样其他一些约束只需要在 x 大于 0 时为真。

标签： z3 smt

【解决方案1】：

不幸的是，这在 SMTLib 中是不可能的。详情见这个答案：Is there an UnsignedIntSort in Z3?

正如 Christoph 指出的那样，您的查询是 unsat，因为量化的断言是错误的；这将求解器置于unsat 状态，而不管您可能有什么其他约束。

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

【讨论】：