如何从Python Z3 Solver模型中提取指定变量的值？

你的问题核心在于：用exec在函数内部创建的Z3变量仅存在于函数的局部作用域，外部代码无法直接访问这些变量名，因此直接调用solver_model[X_307_1_W]会触发NameError——因为当前作用域根本没有定义X_307_1_W这个变量。

下面提供两种可行的解决方案：

方案1：修改函数，用字典跟踪创建的变量 #

这种方法更安全可控，避免exec带来的作用域问题，同时能明确管理所有创建的Z3变量：

from z3 import Solver, Real, sat

def my_eval(equations):
    var_dict = {}  # 存储所有创建的Z3变量
    solver = Solver()
    for eqn in equations:
        parts = eqn.split()
        if parts[0].startswith('X'):
            # 创建第一个变量并存入字典
            var_name = parts[0]
            var_dict[var_name] = Real(var_name)
            # 创建去掉最后两位的变量并存入字典
            other_var_name = var_name[:-2]
            var_dict[other_var_name] = Real(other_var_name)
        # 使用eval和变量字典添加方程，避免exec的安全风险
        solver.add(eval(eqn, {"__builtins__": None}, var_dict))
    
    if solver.check() == sat:
        return solver.model(), var_dict
    else:
        return None, var_dict  # 处理无解情况

使用示例：

# 假设equations是你的方程组列表
model, var_map = my_eval(equations)
if model:
    # 通过字典获取目标变量，再从模型中提取值
    target_val = model[var_map['X_307_1_W']]
    print(f"X_307_1_W的值为: {target_val}")
else:
    print("方程组无解")

方案2：直接创建同名Z3变量取值 #

如果不想修改原函数，可直接创建与目标变量同名的Z3变量，再从模型中取值——Z3通过变量名称来匹配模型中的赋值：

from z3 import Real

model = my_eval(equations)
# 创建同名的Real变量
target_var = Real('X_307_1_W')
# 检查变量是否在模型中
if target_var in model:
    val = model[target_var]
    print(f"X_307_1_W的值为: {val}")
else:
    print("该变量不存在于模型中")

为什么原方法会报错？ #

你用exec在my_eval函数内部创建的变量，属于函数的局部命名空间。当函数执行完毕返回模型后，这些局部变量会被销毁，外部代码无法访问X_307_1_W这个变量名，自然会触发NameError。

内容的提问来源于stack exchange，提问作者Coder Boy