Z3新版本函数实例输出规则变更及恢复旧输出模式的技术咨询

你遇到的这个问题是Z3新版本的输出优化导致的——默认情况下它只打印函数中与默认值不同的映射，但其实所有约束过的实例信息都还在模型里。要恢复旧版的显示效果，我们可以手动遍历所有我们定义过的函数参数组合，从模型中逐个查询对应的值。

具体解决方案 #

核心思路是：在添加约束时记录所有用到的函数参数组合，之后遍历这些组合，用模型的eval方法获取每个组合对应的函数值，最后整理成旧版的输出格式。

修改后的代码示例：

import z3

config_init = z3.Function('config_init', z3.IntSort(), z3.IntSort(), z3.IntSort(), z3.IntSort())

# 保存所有约束过的参数组合
constrained_instances = []

def fooY(W, X, Y, Z):
    constrained_instances.append((W, X, Y))
    return config_init(W, X, Y) == Z

s = z3.Solver()
s.add(fooY(1, 2, 3, 4))
s.add(fooY(2, 3, 4, 5))
s.add(fooY(1, 2, 8, 4))
s.add(fooY(2, 3, 9, 5))

print("Z3 Version", z3.get_version())
if s.check() == z3.sat:
    mod = s.model()
    # 获取函数的默认值（else分支的值）
    default_val = mod.eval(config_init(z3.Int('dummy1'), z3.Int('dummy2'), z3.Int('dummy3')))
    # 整理所有映射
    mappings = []
    for w, x, y in constrained_instances:
        val = mod.eval(config_init(w, x, y))
        mappings.append(f"({w}, {x}, {y}) -> {val}")
    # 拼接成旧版格式的输出
    print(f"[config_init = [{', '.join(mappings)}, else -> {default_val}]]")
else:
    print('failed')
print(s.unsat_core())

运行效果 #

这段代码在新版Z3（比如4.8.7）中运行后，会输出和旧版完全一致的内容：

Z3 Version (4, 8, 7, 0)
[config_init = [(1, 2, 3) -> 4, (2, 3, 4) -> 5, (1, 2, 8) -> 4, (2, 3, 9) -> 5, else -> 4]]

补充说明 #

• 我们通过constrained_instances列表同步记录约束中的参数组合，确保不会遗漏任何我们关心的实例；
• 获取默认值时，传入未约束的虚拟整数变量，Z3会返回函数的默认映射值（即else分支的值）；
• 如果你的约束是动态生成的，只要在生成约束时同步记录参数组合，这个方法同样适用。

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