How to check in Z3py whether the expression contains a specific variable or expression?

I'm using z3py, how do I check whether an expression contains a given variable or expression? For example,

x = Int('x')
expr = x + 1

So, expr should contains variable x.

I've checked the z3.py source code, but I didn't find a solution. Any idea? Thanks.

Solution

You can write a simple recursive descent walk over the expression:

from z3 import *

def contains(x, e):
    return x.__repr__() == e.__repr__() or any([contains(x, c) for c in e.children()])

x, y, z = Ints('x y z')
expr = x + 2 * y

print(contains(x, expr))
print(contains(y, expr))
print(contains(z, expr))
print(contains(x+2, expr))
print(contains(2*y, expr))
print(contains(y*2, expr))
print(contains(1, IntVal(2)))
print(contains(1, IntVal(1)))
print(contains(x, x))
print(contains(x, y))

This prints:

True
True
False
False
True
False
False
True
True
False

However, I should caution that in typical z3 programming you already know what your variables are. (After all, you have to declare them explicitly!) So, unless you're writing some high-level library code, you should simply keep track of what variables you have and just check in this list. Recursive-descents like this can be expensive for large expressions.