Используя Z3 с текстовым форматом, я могу использоватьdefine-fun определить функции для повторного использования позже. Например:

(define-fun mydiv ((x Real) (y Real)) Real
  (if (not (= y 0.0))
      (/ x y)
      0.0))

Интересно как создатьdefine-fun с Z3 API (я использую F #) вместо повторения тела функции везде. Я хочу использовать его, чтобы избежать дублирования и отладки формул. Я пробовал сContext.MkFuncDecl, но, кажется, генерирует только неинтерпретированные функции.