python - Z3PY 将整数转换为 Python 整数

Question

有没有办法将 Z3PY 数据类型转换为原生 Python 数据类型？
当我的公式被 Z3 求解时，我可以通过调用 model() 函数将其打印出来。但是如何将模型输出保存为变量中的普通整数？所以我可以使用它们。
我可以将它们转换为普通整数，以便我可以在程序的其余 Python 代码中使用它们吗？
我使用求解器的全部目的是将结果作为另一个 Python 程序的输入。所以我需要它来处理它。

Answer 1

假设您声明的变量是 x :

x = z3.Int("x")

你会得到它作为一个 Python int 像这样:

model[x].as_long()

z3 模型也是可迭代的。检索列表推导式中的所有参数:

[model[v] for v in model]