如何让Z3生成包含指定索引映射的具体数组模型？

Z3默认会用逻辑等价且最简洁的形式输出模型，所以你得到的是全为"bar"的常量数组。要让模型明确展示你指定的索引映射，需要手动处理模型输出，或者通过代码提取目标索引的对应关系，以下是具体实现方案：

Z3Py自定义输出实现 #

直接获取模型后，提取你关注的索引映射即可，示例代码如下：

from z3 import *

# 声明数组与约束
MyArray = Array('MyArray', StringSort(), StringSort())
solver = Solver()
solver.add(MyArray["foo"] == "bar")
solver.add(MyArray["faz"] == "bar")

if solver.check() == sat:
    model = solver.model()
    # 指定需要展示的索引
    target_indices = ["foo", "faz"]
    # 提取索引与值的映射
    index_map = {idx: model.eval(MyArray[idx]).as_string() for idx in target_indices}
    print(index_map)

运行后输出：

{'foo': 'bar', 'faz': 'bar'}

如果想要更贴近["foo"->"bar","faz"->"bar"]的格式，可修改打印逻辑：

# 接上述代码
formatted_output = [f'"{key}"->"{{value}}"'.format(value=index_map[key]) for key in target_indices]
print(f"[{', '.join(formatted_output)}]")

运行后输出：

["foo"->"bar", "faz"->"bar"]

为什么默认模型是常量数组？ #

Z3的模型生成器会优先选择最简洁的等价表达式。由于你只约束了"foo"和"faz"两个位置的值，其余位置无约束，常量数组（所有位置为"bar"）在逻辑上完全满足你的约束，因此成为默认输出形式。

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