z3 - smtlib 中的 define-fun 与 define-funs-rec

Question

这似乎是根据SMTLIB 标准define-funs-rec可以做什么的严格超集。如果是这样，是否有理由不总是使用，也许除了语法简单之外？define-fundefine-funs-rec

Answer 1

严格来说; 不。Butdefine-fun-rec相当新（相对于 good old 而言define-fun），因此如果您想要更大的可移植性并且不需要递归定义，那么您应该坚持使用define-fun.

可以想象，define-fun-rec除非你真的有一个递归定义，例如一个有根据的检查器，否则它可能还会在一个并不真正需要的求解器中带来更重的机器。这最终可能会花费一些性能周期；尽管我怀疑这会引起太大的关注。