python - z3python：使用数学库

Question

我试图将python的数学库与z3python一起使用，我所做的是

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 一起使用。任何建议表示赞赏。

score 2 · Accepted Answer

一般来说，不，这是不可能的。原因是没有将 Python 函数转换为逻辑约束（理论上可以通过定点引擎完成），但它需要大量的努力并且本质上是（通常无法确定的）模型的编码 -检查问题。另请参阅 Leo在此处对相关问题的出色回答）。

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

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

1 回答 1