使用量词会影响Z3的性能吗？

Question

在对this question 的回答中，Leo 建议使用量词来定义函数。假设我只需要应用函数1次，使用量词会影响Z3的性能吗？

与我声明一个不带参数且不带量词的函数（因为我只使用该函数仅 1 次）的情况相比如何？

Answer 1

您可以尝试使用选项 smt.macro_finder=true 将量化等式转换为宏。默认情况下它是关闭的，因此最好为只应用一次的函数定义宏。这也意味着 Z3 最终使用了基于通用量词的求解器。在某些情况下，使用“define-fun”命令由宏定义的函数对于纯位向量或纯线性算术的公式很方便。在这些情况下，Z3 使用更有效的设置。例如，Z3 使用“相关性”传播来避免多余的量词实例化。相关性传播有其自身的开销，这对于量化公式是可以容忍的，但对于无量词公式来说不是一个好主意。