z3python：使用數學庫

Question

我試圖用與z3python python的數學庫，我所做的就是

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

返回的錯誤信息是AttributeError的：ArithRef實例沒有屬性「浮」。

我的目的並不是真的在Z3中使用階乘函數，而是我很好奇數學函數庫中的函數是否可以與Z3一起使用。任何建議表示讚賞。

Answer 1

一般來說，不，這是不可能的。原因是Python函數沒有翻譯成邏輯約束（理論上可以通過fixed-point engine來完成），但是它需要大量的工作，並且本質上是（通常不可判定的）模型檢查問題的編碼。另見Leo對相關問題的出色答案here）。

在這個特定的例子中，請注意a是符號，即它代表任何可能的實數。 math.factorial不知道如何處理這些信息，因爲它的實現只能處理具體的實數。

對於某些特定的功能，當然可以爲Z3提供精確的編碼。例如，Z3支持指數運算，Python API提供__pow__運算符。但是，該運算符可能與Python的__pow__（浮點抽象的）實數的語義完全不同，它不是從Python的__pow__實現派生的。