在Z3中，是否有一種方法可以生成未定義數量的假設來檢查？

Question

我的Python程序使用Z3 Python API。產生要通過Z3使用命令查了一些假設：

check(P1, P2,....Pn) 

然後我用命令得到不飽和度的核心：

unsat_core() 

有沒有一種方法，我可以在我的Python程序中使用不知道提前斷言的次數的命令check(P1, P2,....Pn)？ 假設的數量是在代碼運行過程中定義的，並且每次運行都會發生變化。

在此先感謝！

Answer 1

當然。你可以把你的假設放到一個元組中，並使用tuple unpacking。

例如。

my_assumptions = (P1, P2, ...Pn) 
check(*my_assumptions) 

取決於你的程序是如何組織的，您可能需要創建/假設添加到列表第一則列表轉換爲一個元組