【发布时间】：2021-01-27 00:20:16
【问题描述】：
有没有办法将 Z3PY 数据类型转换为原生 Python 数据类型？
当我的公式被 Z3 求解后，我可以通过调用 model() 函数将其打印出来。但是如何将模型输出保存为变量中的普通整数？所以我可以使用它们。
我可以将它们转换为普通整数，以便在程序的其余 Python 代码中使用它们吗？
我使用求解器的全部目的是将结果作为另一个 Python 程序的输入。所以我需要它来处理它。
【问题讨论】：
【发布时间】：2021-01-27 00:20:16
【问题描述】：
假设你声明的变量是x:
x = z3.Int("x")
你会得到它作为一个 Python int 像这样：
model[x].as_long()
z3 模型也是可迭代的。检索列表推导中的所有参数：
[model[v] for v in model]
【讨论】：
-
谢谢！我尝试检索列表中的所有参数。它是一种获取变量名的方法吗？现在我得到了变量的值。
-
好吧，我不需要那个。变量始终具有相同的名称，因此我可以自己编写代码。感谢您的帮助，正是我需要的！干杯
-
如果您需要变量名，最简单的方法（虽然不是很简单）是查看
model字典本身。不过，这可能会变得相当复杂。最著名的方法是自己跟踪变量，这几乎总是可行的。 （除非您正在编写适用于任意程序的实用程序。）