改进 String -> String 函数的 Z3 模型输出答案

【问题标题】：Improving Z3 model output for String -> String functions改进 String -> String 函数的 Z3 模型输出
【发布时间】：2021-12-29 20:22:25
【问题描述】：

考虑以下代码，指定从字符串到字符串的简单函数：

from z3 import *
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())

模型输出如下：

[map = [Concat(Unit(Char),
               Concat(Unit(Char),
                      Concat(Unit(Char), Unit(Char)))) ->
        "value1",
        Concat(Unit(Char),
               Concat(Unit(Char),
                      Concat(Unit(Char), Unit(Char)))) ->
        "value2",
        Concat(Unit(Char),
               Concat(Unit(Char),
                      Concat(Unit(Char), Unit(Char)))) ->
        "value3",
        Concat(Unit(Char),
               Concat(Unit(Char),
                      Concat(Unit(Char), Unit(Char)))) ->
        "value4",
        else -> "value1"]]

如何让它输出实际的键而不是Concat(Unit(Char), Concat(Unit(Char), ...))？

【问题讨论】：

标签： python z3 z3py

【解决方案1】：

这似乎是最近 z3py 中的一个问题。如果我使用 2021 年 8 月 3 日从他们的 GitHub 大师编译的 z3 运行你的程序，我会得到：

sat
[map = ["key2" -> "value2",
        "key3" -> "value3",
        "key4" -> "value4",
        else -> "value1"]]

但是，如果我使用 2021 年 11 月 15 日编译的 z3 运行它，那么我会看到您看到的输出；这显然是假的。

请在https://github.com/Z3Prover/z3/issues将此作为错误报告

【讨论】：

奇怪，因为我使用的是 7 月 13 日发布的 4.8.12。这也是 4.8.13 的问题。
序列逻辑在夏天进行了一次大改写；其中重新设计了字符串和序列以支持新的 SMTLib 字符串逻辑。（过去字符串只是 8 位位向量的序列。现在不再是这种情况了；现在它们有自己的单独类型，现在支持 unicode。）所以，如果事情有点复杂，我不会感到惊讶关于模型的打印方式，整个夏天都是片状的。我怀疑这是一个“大”错误，一旦报告他们应该能够很快修复它。
很高兴知道它现在支持 unicode！我在这里打开了一个问题：github.com/Z3Prover/z3/issues/5674
@ahelwer 看起来 Nikolaj 已经在 GitHub master 中修复了这个问题。在发布新版本之前，您将不得不从源代码进行编译。