如何优化Z3中String→String函数的模型输出显示

Z3默认的打印配置会将字符串常量展开为字符拼接的底层表示输出，不会直接展示可阅读的字符串字面量，这属于打印格式化的问题，不是模型本身的逻辑错误。

在代码初始化阶段调整Z3的全局打印参数，开启字符串字面量打印开关即可：

from z3 import *
# 新增两行配置参数
set_option(pp_string_literals=True)
set_option(model_compress=False)

map = Function('map', StringSort(), StringSort())
c1 = map(StringVal('key1')) == StringVal('value1')
c2 = map(StringVal('key2')) == StringVal('value2')
c3 = map(StringVal('key3')) == StringVal('value3')
c4 = map(StringVal('key4')) == StringVal('value4')
s = Solver()
s.add(And(c1, c2, c3, c4))
print(s.check())
print(s.model())

修改配置后运行代码，模型输出的键就会直接显示为"key1"、"key2"等实际的字符串字面量，不会再出现Concat拼接的表达式。

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