Z3中String→String函数的模型生成与求值方法咨询

展示异常原因 #

你看到的模型输出异常仅为Z3 Python API默认打印未解释函数时的展示层问题，并非约束逻辑错误或定义域存在限制。Z3默认不会将字符串类型的模式匹配项序列化为可读字面量，会展开为Concat+Unit的内部AST结构，你看到的多个相同的Concat项只是渲染bug，实际模型内部的匹配逻辑完全符合你添加的key=value约束。

具体实现方法 #

Z3 Python API提供小写开头的Model.eval()方法，可直接传入任意Z3表达式，返回该表达式在当前模型下的求值结果，无需手动解析模型的函数映射项。

修改后的可直接获取指定key对应值的示例代码如下：

from z3 import *
# 避免使用map作为变量名，防止覆盖Python内置map函数
map_func = Function('map', StringSort(), StringSort())
c1 = map_func(StringVal('key1')) == StringVal('value1')
c2 = map_func(StringVal('key2')) == StringVal('value2')
c3 = map_func(StringVal('key3')) == StringVal('value3')
c4 = map_func(StringVal('key4')) == StringVal('value4')

s = Solver()
s.add(And(c1, c2, c3, c4))
print("求解结果：", s.check())
model = s.model()

# 批量测试不同key的返回值
test_keys = ["key1", "key2", "key3", "key4", "key5"]
for key in test_keys:
    eval_result = model.eval(map_func(StringVal(key)))
    # 如需转换为Python原生字符串，可调用as_string方法
    # native_str = as_string(eval_result)
    print(f"map('{key}') = {eval_result}")

运行后输出结果如下：

求解结果： sat
map('key1') = "value1"
map('key2') = "value2"
map('key3') = "value3"
map('key4') = "value4"
map('key5') = "value1"

其中不在约束列表中的key5返回值对应模型中else分支的默认值。

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