Z3表达式的导数

Question

我想取z3表达式的导数。我知道这个功能在Dreal4中是可能的，使用变量类型，但是我在z3中找不到任何类似特性的文档。在z3中有这样的方法吗？如果不是的话，下一步的最佳选择是什么？在交感和z3变量之间转换？

例如：

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

据我所知，z3目前不支持使用衍生品。但是，如果您选择这样做的话，它会公开足够多的API让您自己编写代码。最好的开始方式是查看z3py本身的内容：https://github.com/Z3Prover/z3/blob/master/src/api/python/z3/z3.py

然而，这将不仅仅是一个“下午”项目；您将不得不投资于学习细节，并准备好随着z3内部组件本身的变化而更新代码，这并不总是容易跟踪的。

您还可以在https://github.com/Z3Prover/z3/discussions上开始讨论，看看开发人员是否有其他建议。

另一种选择可能是留在dReal中，在那里使用派生函数，并使用dReal API遍历代码(假设它本身暴露得足够多，我不太熟悉)，并在z3 API中导出相同的代码；即，从dReal AST到z3 AST进行转换。如果你关心的一组表达式足够小，而困难的部分是做差异化，这可能会有回报。当然，如果您不想混合/匹配两个不同的系统，那么在z3中直接实现衍生工具可能是一种更好的方法。(因此，要面对维护代码的前景，因为这两个代码都会发生更改！)