Z3 Iterate over String to add up Only Numbers (Python api)

I want my Z3 Script to be able to generate a string where all digits multiplied equal a certain value. Therefore it needs to iterate over said String and take only the digits and multiply them together. It should skip other chars.

For example "a1b2c3" results to 6

Now I know that I need to rebuild my snippet, but this is what I wanted to do:

from z3 import *

s = Solver()

def mul_only_numbers(w):
    res = 1
    for elem in str(w):
        if elem.isdigit():
            res *= int(elem)
    return res

word = String("word")
s.add(mul_only_numbers(word) == 6)

res = s.check()
if res == sat:
    st = str(s.model()[word])
    print(st)
else:
    print("Solver said:", res)

Of course this doesn't work because str(w) = "word".

But how can I still achieve, what I'm trying to do?

Solution

You cannot use recursion (or iteration) in Python to go over the elements of a symbolic string. The recursion has to be done at the z3-level, for which you can use RecFunction facility:

from z3 import *

s = Solver()

def digitValue(c):
    dv = StrToInt(c)
    return If(dv == -1, 1, dv)

mul_only_numbers = RecFunction('mul_only_numbers', StringSort(), IntSort())
w = FreshConst(StringSort())
RecAddDefinition( mul_only_numbers
                , [w]
                , If ( Length(w) == 0
                     , 1
                     , digitValue(Extract(w, 0, 1)) * mul_only_numbers(Extract(w, 1, Length(w) - 1))
                     )
                )

word = String("word")
s.add(mul_only_numbers(word) == 6)
s.add(Length(word) >= 8)

res = s.check()
if res == sat:
    print(s.model()[word])
else:
    print("Solver said:", res)

Note that I added an extra constraint that the string should have unicode length of >= 8 to make the model interesting. This prints:

"61\u{0}\u{0}\u{0}\u{0}\u{0}\u{0}"

which satisfies the constraint that the digits in the string multiplied gives you 6.

Note that this sort of recursive definition, while possible, will not be performant; and it can cause decidability issues. By that, I mean the solver might end up responding unknown, or take very long to come back. If you know the length of the string in advance, then you'd be better served modeling each character separately instead. Or you can iteratively increase the length: Try length 1, length 2, ... etc., until you find a model that satisfies your constraints. Or even do a binary search on the length. One usually needs to experiment with different encodings to find one that works the best for each individual problem.