如何在 Z3py 中定义函数？

Question

如何使用 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 定义)

Answer 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 的使用示例：

How to define a function in Z3py?