Generating and evaluating models for String -> String functions in Z3

Question

I have the following program that applies simple key = value constraints to a function from String to String:

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

The output of the model 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"]]

This is sort of strange, but presumably it is just a limitation of Z3's representation of elements of the domain of a function.

The hope is I can evaluate a Z3 expression on a concrete constant value of a function in a model; however, I cannot figure out how to do that. The Eval method from the Python reference docs is nowhere to be found in the namespace. I've done something like this before with the C# bindings so I know it is possible.

Answer 1

As is essentially tradition for my Z3 questions at this point, a few more minutes of messing around revealed you can do this as follows:

s.model().eval(expr)

The Eval function in the python documentation is actually listed as a member function of Model, which is easy to miss.

Per the comment from @alias it is actually best practice to use

s.model().evaluate(expr, model_completion = True)

to reduce surprises.