python - z3python : using math library

Question

我试图在 z3python 中使用 python 的数学库，我所做的是

import z3
import math
a,b = z3.Reals('a b')
solve(b == math.factorial(a), b == 6)

它返回的错误信息是 AttributeError: ArithRef instance has no attribute 'float'。

我的目的并不是真正在 Z3 中使用阶乘函数，而是我很好奇数学库中的函数是否可以在一般情况下与 Z3 一起使用。任何建议表示赞赏。

Answer 1

一般来说，不，这是不可能的。原因是 Python 函数没有转换为逻辑约束(理论上可以完成，例如，通过 fixed-point engine )，但它需要大量的努力，并且本质上是(通常不可判定的)模型检查的编码问题。另请参阅 Leo 对相关问题的出色回答 here ).

在这个特定的例子中，请注意 a 是符号的，即它代表任何可能的实数。 math.factorial 不知道如何处理这些信息，因为它的实现只处理具体的实数。

对于某些特定的功能，当然可以为 Z3 提供精确的编码。例如，Z3 支持求幂，Python API 提供了一个 __pow__ 运算符。但是请注意，此运算符可能与 Python 对实数(的浮点抽象)的 __pow__ 具有完全相同的语义，并且它不是派生自 Python 的 __pow__ 实现>.