如何在 Z3py 中定义一个函数？答案

【问题标题】：How to define a function in Z3py?如何在 Z3py 中定义一个函数？
【发布时间】：2021-08-06 15:20:38
【问题描述】：

如何使用 Z3 python API 编写与此代码等效的代码？

(define-fun mymax ((a Int) (b Int)) Int
  (ite (> a b) a b))

(assert (= (mymax 100 7) 100))

(check-sat)
(get-model)

不幸的是，Function 方法是 Python 中的 declare_fun，而不是 define_fun：它不接受包含函数定义的参数。如果我们能写这样的东西就好了：

mymax = Function('mymax', IntSort(), IntSort(), IntSort(),
                 Lambda([a,b], If(a>b, a, b))

(我可以声明mymax并为其添加适当的约束，但是当函数大而复杂时，z3必须搜索它的定义，这看起来效率不高。我宁愿给z3定义)

【问题讨论】：

标签： z3py

【解决方案1】：

通常，Function 声明旨在将未解释的名称引入环境。也就是说，你告诉求解器有这个函数，也许它遵守一些规则；如交换性、结合性等；但这就是你关心的全部，即没有实际定义。

如果您确实知道定义，这似乎是您的用例，推荐的方法实际上是直接使用 Python 函数本身；它操纵符号表达式。在您的示例中，它将是：

def symMax(a, b):
  return If(a>b, a, b)

然后只需在您的代码中使用它，它就会扩展到正确的定义。

对此有一个例外：如果您的函数是递归的，会发生什么：您可以使用递归 Python 函数，但在这种情况下扩展可能不起作用，因为“终止”条件可能是象征性的。在这些情况下，请使用RecAddDefinition：https://z3prover.github.io/api/html/namespacez3py.html#a7029cec3faf5bd7cdd9d9e0365f8a3b5

请注意，当您的定义根本不是递归时，您也可以使用RecAddDefinition；也许这就是你的想法。但在这些情况下，定义 Python 函数是首选方式，因为您可以更轻松地操作这些术语。

有关RecAddDefinition 的使用示例，请参阅此问题：https://stackoverflow.com/a/68457868/936310

【讨论】：

感谢您的提示。我猜python函数和RecAddDefinition在处理上很相似，但是当函数复杂且经常使用时，我怀疑`RecAddDefinition`会相对更快，因为对它的调用将在C++中而不是在Python中解释.
这两种方法其实有很大的不同。使用RecAddDefinition，您将其注册为求解器的函数；它将按原样处理它并根据求解器的需要扩展定义。在 Python 版本中，每次调用都将在您将其传递给求解器之前完全展开。（因此，如果递归并且不象征性地终止，则会出现问题。）在任何一种方法中都不能合理地谈论“效率”。我实际上认为如果总是应用于基本术语，Python 版本会更快。它们是互补的技术。