Usage: How to Encode Derivatives

[chelseas]

I would like to do some proofs of the form:
f is an uninterpreted function
fp is the derivative of f -- an uninterpreted function such that fp(x) = df/dx (x)
g is some function (defined) of f and fp
And then reason about properties like the minimizer of g and such.
I am having trouble figuring out how to encode f and fp. I thought that I might be able to encode/define f and fp using the define-ode macro or the integral macro...but I have not yet come across any minimal examples that I could apply.

Is this type of relation definable in dreal? If so, can you direct me to an example that would be relevant in the codebase? I see there are a lot of examples for ode work in the dreal3 repo.

[chelseas]

My attempt at a minimal example produced syntax error, unexpected symbol errors

(set-logic QF_NRA_ODE)
(declare-fun f () Real)
(declare-fun fp () Real)
(define-ode flow1 ((= d/dt[f] fp)))
(check-sat)
(get-model)
(exit)

[scungao]

Differentiation in general is not a computable operator (its output can be discontinuous). So we don’t directly support d/dx in the theory and you need to explicitly define it with its own function form. The ODEs theory can numerically integrate but you’ll still need the derivative in function form first.

…

On Tue, Feb 9, 2021 at 23:37 Chelsea Sidrane ***@***.***> wrote: I would like to do some proofs of the form: f is an uninterpreted function fp is the derivative of f -- an uninterpreted function such that fp(x) = df/dx (x) g is some function (defined) of f and fp And then reason about properties like the minimizer of g and such. I am having trouble figuring out how to encode f and fp. I thought that I might be able to encode/define f and fp using the define-ode macro or the integral macro...but I have not yet come across any minimal examples that I could apply. Is this type of relation definable in dreal? If so, can you direct me to an example that would be relevant in the codebase? I see there are a lot of examples for ode work in the dreal3 repo. — You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub <#238>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ABI3GEWSN5JUEJXAXXHRFUTS6IZUZANCNFSM4XMOIE4Q> .

[chelseas]

What about differentiation only for smooth (infinitely differentiable) functions?
What do you mean by "you need to explicitly define it with its own function form"?