有没有办法将 Z3PY 数据类型转换为原生 Python 数据类型？
当我的公式由 Z3 求解时，我可以通过调用 model() 函数将其打印出来。但是如何将模型输出保存为变量中的普通整数呢？这样我就可以使用它们。
我可以将它们转换为普通整数，以便我可以在程序的其余 Python 代码中使用它们吗？
我使用求解器的全部目的是将结果作为另一个 Python 程序的输入。所以我需要它能够处理它。
最佳答案
假设您声明的变量是 x:
x = z3.Int("x")
你会得到像这样的Python int:
model[x].as_long()
z3 模型也是可迭代的。检索列表理解中的所有参数:
[model[v] for v in model]
关于python - Z3PY 将 Int 转换为 Python int，我们在Stack Overflow上找到一个类似的问题： https://stackoverflow.com/questions/65911213/