Equivalent of define-fun in Z3 API

Question

Using Z3 with the textual format, I can use define-fun to define functions for reuse later on. For example:

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

I wonder how to create define-fun with Z3 API (I use F#) instead of repeating the body of the function everywhere. I want to use it to avoid duplication and debug formulas easier. I tried with Context.MkFuncDecl, but it seems to generate uninterpreted functions only.

Answer 1

The define-fun command is just creating a macro. Note that the SMT 2.0 standard doesn’t allow recursive definitions. Z3 will expand every occurrence of my-div during parsing time. The command define-fun may be used to make the input file simpler and easier to read, but internally it does not really help Z3.

In the current API, there is no support for creating macros. This is not a real limitation, since we can define a C or F# function that creates instances of a macro. However, it seems you want to display (and manually inspect) formulas created using the Z3 API. In this case, macros will not help you.

One alternative is to use quantifiers. You can declare an uninterpreted function my-div and assert the universally quantified formula:

(declare-fun mydiv (Real Real) Real)
(assert (forall ((x Real) (y Real))
                (= (mydiv x y)
                   (if (not (= y 0.0))
                       (/ x y)
                       0.0))))

Now, you can create your formula using the uninterpreted function mydiv.

This kind of quantified formula can be handled by Z3. Actually, there are two options to handle this kind of quantifier:

1. Use the macro finder: this preprocessing step identifies quantifiers that are essentially defining macros and expand them. However, the expansion only happens during preprocessing time, not during parsing (i.e., formula construction time). To enable the model finder, you have to use MACRO_FINDER=true
2. The other option is to use MBQI (model based quantifier instantiation). This module can also handle this kind of quantifier. However, the quantifiers will be expanded on demand.

Of course, the solving time may heavily depend on which approach you use. For example, if your formula is unsatisfiable independently of the “meaning” of mydiv, then approach 2 is probably better.