Derivative of Z3 expression

Question

I would like to take the derivative of z3 expression. I know this functionality is possible in Dreal4, using the Variable type, however I cant find any documentation of a similar feature in z3. Is there a method for this in z3? If not what is the next best option? convert between sympy and z3 vars?

For example:

from z3 import *
x = Real('x')
f = x**2

#next line takes the derivative of f with respect to x
#f_prime = f.differentiate(f,x)

Answer 1

As far as I know, z3 does not currently support taking derivatives. However, it exposes enough API for you to code this up yourself, if you choose to do so. The best way to start would be to look at the contents of z3py itself: https://github.com/Z3Prover/z3/blob/master/src/api/python/z3/z3.py

However, this isn't going to be just an "afternoon" project; you'll have to invest in learning the details, and also be ready to update your code as z3 internals itself change, which isn't always easy to track.

You can also start a discussion at https://github.com/Z3Prover/z3/discussions to see if the developers have any other advice for you.

Another alternative might be to stay in dReal, take the derivative there, and walk the code using dReal API (assuming it exposes enough of itself, I'm not too familiar), and export the same in z3 API; i.e., do a translation from dReal AST to z3 AST. This might pay off if the set of expressions you care about is sufficiently small and the hard part is doing the differentiation. Definitely something to try, though implementing derivatives directly in z3 might be a better approach if you don't want to mix/match two separate systems. (And hence, face the prospect of maintaining your code with respect to changes in both of them!)