z3, z3py:我可以定义一个包含一组整数的排序吗?

Question

这是我之前的问题"是否有可能从本质上减少Function的搜索空间"的后续问题。

我在想是否有可能定义一个包含一组整数的排序，例如整数1-10。

我的直觉是，为了减少函数的搜索空间，我想定义一个函数，它的域排序和范围排序是IntSort，而不是定义一个函数，它的域排序和范围排序是一个只包含我感兴趣的整数集的排序。

假设

Answer 1

这听起来像位向量可能是建模问题的好选择，至少您的整数集相对较小且大小有限。Z3可以处理与量词和未解释函数相结合的位向量，它有一些自定义的预处理器，因此它在一些问题上表现得很好;这绝对值得一试。