在 z3 的输入语言中使用 define-fun答案

【问题标题】：use of define-fun in z3's input language在 z3 的输入语言中使用 define-fun
【发布时间】：2014-03-25 17:03:48
【问题描述】：

this 发布后，define-fun 似乎是一个宏，它被 z3 的预处理器扩展，实际求解器看不到，但使输入文件可能更紧凑且更易于阅读。我之所以问，是因为我在同一问题上的令人满意的分配和性能方面看到了一些（显然是随机的）差异：一个使用 define-fun 而另一个不使用，这让我想知道它是否不仅仅是一个宏。在某些情况下是否必须小心define-fun 的激进使用？我在我遇到的一些 QF_NIRA、QF_LIRA 问题上观察到了这一点。

【问题讨论】：

标签： z3

【解决方案1】：

define-fun 在 Z3 中被视为宏。如果您使用等式和未解释的函数，Z3 的行为会有所不同。此外，如果您使用“declare-fun”，然后创建量化等式，问题不再出现在 QF_LIRA 片段中。

【讨论】：