Add a z3 constraint, such that the value of a z3 variable equals to the return value of some function

Question

I have a Python function that takes a real number and returns a string, e.g.

def fun(x):
    if x == 0.5:
        return "Hello"
    else:
        return "Bye"

I start a z3 solver:

from z3 import *

r = Real('r')
s = Solver()

Now I want to tell the solver find a value of r, such that fun(r) returns "Hello". I am facing the following problems:

1. If r = Real('r'), then I cannot call fun(r), because r is a z3 variable
2. I cannot say s.add(StringVal("Hello") == StringVal(fun(r))) as a constraint, because 1) r is a z3 variable, 2) the interpretation of r is not known yet. Hence, I have no model from which I could extract a value and pass it to the fun.

Is it possible to implement what I want?

Answer 1

There's no out-of-the box way to do this in z3, unless you're willing to modify the definition of fun so z3 can understand it. Like this:

from z3 import *

def fun(x):
    return If(x == 0.5, StringVal("Hello"), StringVal("Bye"))

r = Real('r')
s = Solver()

s.add(fun(r) == StringVal("Hello"))
print(s.check())
print(s.model())

This prints:

sat
[r = 1/2]

So, we changed the function fun to use the z3 idioms that correspond to what you wanted to write. A few points:

• Obviously, not every Python construct will be easy to translate in this way. While you can express most every construct, the complexity of the hand-transformation will get higher as you work on more complicated functions.

• So far as I know, there's no automatic way to do this translation for you. However, take a look at this blog post for some ideas on how to do so via the disassembler.

• PyExZ3 is a now-defunct symbolic simulator for Python, using z3 as the backend solver. While the project is no longer active, you might be able to resurrect the source-code or get some ideas from it.

• You have used Real to model the parameter x. Z3's Real values are true mathematical reals. (Strictly speaking, they are algebraic reals, but that's besides the point for now.) Python, however, doesn't have those; instead it uses double-precision floats. But luckily, z3 understands floats, so for a more realistic encoding use the Float64 sort. See here for details.