Extending `z3` with one way functions

Question

I'm looking to use a one-way function in a z3 Python program. I'd like z3 to respect the following properties/tactics:

• if x = y, then f(x) = f(y)
• f is a computable Python function that I can provide when x is known
• if f(x) = y, attempt to resolve by matching f(*y) = f(x) implying x = *y from prior assignments (never attempt to guess x that computes to y)

Are there built in features to support this construct or anything else that may help introduce it?