我的Python程序使用Z3 Python API。它使用以下命令生成许多假设，以供Z3检查：
check(P1, P2,....Pn)
然后我使用以下命令获得unsat核心：
unsat_core()
有没有一种方法可以在我的python程序中使用该命令check(P1, P2,....Pn)而无需事先知道断言的数量？假设的数量在代码运行期间定义，并且每次运行都会更改。
提前致谢！
当然。您可以将假设放入一个元组，而只需使用元组拆包。
例如。
my_assumptions = (P1, P2, ...Pn)
check(*my_assumptions)
根据程序的结构，您可能需要先将假设创建/追加到列表，然后再将列表转换为元组
本文收集自互联网，转载请注明来源。
如有侵权，请联系[email protected] 删除。
我来说两句