Improving Z3 model output for String -> String functions-CodePudding

Consider the following code specifying a simple function from strings to strings:

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())

The model output is as follows:

[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"]]

How can I get it to output the actual keys instead of Concat(Unit(Char), Concat(Unit(Char), ...))?

CodePudding user response：

This seems to be a recent breakage in z3py. If I run your program with z3 compiled on August 3rd 2021 from their GitHub master, I get:

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

But if I run it with z3 compiled on November 15th 2021, then I see the output you are seeing; which is clearly bogus.

Please report this as a bug at https://github.com/Z3Prover/z3/issues