如何在 Z3_mk_forall_const 中声明常量以用作绑定变量？

【问题标题】：How to declare constants to use as bound variables in Z3_mk_forall_const?如何在 Z3_mk_forall_const 中声明常量以用作绑定变量？
【发布时间】：2014-03-25 19:07:14
【问题描述】：

假设我想在下面的公式中普遍量化 x 和 y：

f(x,y) <=> x=y

使用 Z3_mk_forall_const 。我必须首先构造上面的公式，它需要 Z3_ast 类型的常量 x 和 y。使用 Z3_mk_const 创建 x 和 y 会导致全局声明。理想情况下，我希望避免这种情况。有其他选择吗？

【问题讨论】：

标签： z3

【解决方案1】：

是的，还有其他选择；你可以使用Z3_mk_forall，它使用de-Brujin variable indexes。您可以使用创建索引变量而不是常量 Z3_mk_bound 然后将它们的排序 (sorts) 和名称 (decl_names) 的数组传递给 mk_forall 或 mk_exists。

【讨论】：

谢谢，克里斯托夫。我了解 Z3_mk_forall 可用于创建以 de-Brujin 指数作为绑定变量的通用量化公式。但是，这种方法对于嵌套量词来说很麻烦，因为它需要“移动”索引。另一方面，具有唯一绑定变量的量化公式可以简单地组成。因此，理想情况下，我希望在不创建全局声明的情况下使用 Z3_mk_forall_const。
恐怕没有直接的方法可以做到这一点。但是，用于创建量词的常量只是为了方便。无论如何，在内部，一切都被转化为 de-Brujin 指数。所以，一旦你创建了量词，在别处重用常量应该是安全的。