Z3 Python如何从ModelRef中移除追踪变量且无需两次运行求解器

你使用assert_and_track时绑定的追踪变量本质是Z3自动添加的布尔常量，求解后会默认出现在模型结果里，不需要二次执行求解器，直接对返回的ModelRef对象做过滤重打包即可实现需求，具体方案如下：

核心实现代码 #

正常求解得到原始模型后，执行以下过滤逻辑即可：

from z3 import *

# 前置逻辑：你已完成solver.assert_and_track、solver.check()调用
original_model = solver.model()

# 过滤所有名称匹配tracker前缀的追踪变量
keep_decls = [
    decl for decl in original_model.decls() 
    if not decl.name().startswith("tracker")
]

# 基于保留的变量构造新的ModelRef对象
filtered_model = Model([(decl, original_model[decl]) for decl in keep_decls])

说明 #

• 得到的filtered_model和原生求解得到的ModelRef对象完全兼容，所有取值、遍历操作都可以正常使用，无任何差异
• 如果你的追踪变量使用了自定义前缀，只需要修改startswith中的匹配字符串即可，也可以替换为正则匹配适配更复杂的命名规则
• 该操作仅对已有模型结果做本地处理，不会触发二次求解，性能开销可以忽略

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