我的Python程序使用Z3 Python API。它使用以下命令生成许多假设，以供Z3检查：
check(P1, P2,....Pn)
然后我使用以下命令获得unsat核心：
unsat_core()
有没有一种方法可以在我的python程序中使用命令
check(P1, P2,....Pn)而不预先知道断言的数量？假设的数量在代码运行期间定义，并且每次运行都会更改。
提前致谢！
最佳答案
当然。您可以将您的假设放入一个元组，而只需使用tuple unpacking。
例如。
my_assumptions = (P1, P2, ...Pn)
check(*my_assumptions)
根据程序的结构，您可能需要先将假设创建/追加到列表，然后再将列表转换为元组
关于python - 在Z3中，是否有一种方法可以生成不确定数量的假设要检查？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/26025519/