如何声明常量以在Z3_mk_forall_const中用作约束变量？

假设我要普遍量化x和y满足下述公式：如何声明常量以在Z3_mk_forall_const中用作约束变量？

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

使用Z3_mk_forall_const。我将不得不首先构造上面的公式，它需要Z3_ast类型的常量x和y。使用Z3_mk_const在全局声明中创建x和y结果。我希望避免这种情况。有其他选择吗？

来源

2014-03-25 Gowtham Kaki

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

来源

2014-03-26 11:46:37

谢谢，克里斯多弗。我了解_'Z3_mk_forall'_可用于创建具有de-Brujin索引作为绑定变量的通用量化公式。但是，对于嵌套量词来说，这种方法非常麻烦，因为它需要“移动”索引。另一方面，具有唯一约束变量的量化公式可以平凡地组成。所以，我最好在不创建全局声明的情况下使用_'Z3_mk_forall_const'_。 –

恐怕没有直接的做法。然而，用于创建量词的常量仅仅是为了便于使用;内部任何东西无论如何都会被转化为de-Brujin指数。所以，一旦你创建了量词，在其他地方重新使用常量应该是安全的。 –

如何声明常量以在Z3_mk_forall_const中用作约束变量？

回答

相关问题