z3：获取模型的决策变量。

在使用Z3求解器时，可以使用z3.Model类的decl()方法来获取模型中的决策变量。

以下是一个使用Z3求解器求解模型并获取决策变量的示例代码：

from z3 import *

# 创建整数变量 x 和 y
x = Int('x')
y = Int('y')

# 创建求解器
solver = Solver()

# 添加约束条件
solver.add(x > 0)
solver.add(y < 10)

# 求解模型
if solver.check() == sat:
    # 获取模型
    model = solver.model()

    # 获取决策变量的值
    x_value = model[x]
    y_value = model[y]

    print(f"x = {x_value}")
    print(f"y = {y_value}")
else:
    print("无解")

在上面的示例中，我们创建了两个整数变量 x 和 y，并添加了约束条件 x > 0 和 y < 10。然后我们使用求解器求解模型，并通过 solver.model() 方法获取模型。最后，我们可以使用 model[变量] 来获取决策变量的值，并打印出来。

运行上面的代码，将会输出模型中决策变量的值。如果没有解，则输出 "无解"。

注意：Z3求解器返回的模型中只包含被限制条件约束的变量。如果某个变量没有被约束到具体的值，那么在获取模型时将无法获取到该变量的值。