Z3Py中已求值模型下如何直接获取ArithRef表达式的数值？

完全可以直接获取ArithRef类型表达式的求值结果，不需要手动重新计算。当优化模型求解完成后，只需通过求解得到的Model对象调用eval()方法，传入目标表达式即可得到该表达式在当前模型下的具体取值，甚至可以进一步转换为Python原生数值类型。

举个具体的代码示例：

from z3 import *

# 定义变量与表达式
x = Real('x')
y = If(x > 5, 0, 0.5 * x)

# 创建优化器并设置求解规则
opt = Optimize()
opt.add(x <= 8)  # 添加约束：x不超过8
opt.maximize(x)   # 设置目标：最大化x

# 执行求解
if opt.check() == sat:
    model = opt.model()
    # 获取x的取值
    x_result = model.eval(x)
    # 直接获取y的求值结果
    y_result = model.eval(y)
    
    print(f"x的取值：{x_result}")
    print(f"y的求值结果：{y_result}")
    # 转换为Python原生float类型
    print(f"y的float值：{float(y_result)}")

运行这段代码后，因为x被约束为≤8且最大化，所以x的取值是8，此时y会触发x>5的分支，结果为0，Z3会自动完成这个逻辑判断与计算，无需手动代入x的值重新推导y的结果。

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