14

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.

pad
  • 41,040
  • 7
  • 92
  • 166

1 Answers1

16

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.

Leonardo de Moura
  • 21,065
  • 2
  • 47
  • 53
  • Thank you for the detailed answer. Using universal quantifier is definitely a neat trick. I wonder about the cost of using universal quantifiers and uninterpreted functions. My constraints in the form of quantified LIAs now turns into quantified UFLIA formulas. Is this change heavily affected the solving time of Z3? – pad Oct 12 '11 at 23:36
  • Yes, the formula will be in `UFLIA`, but it is in a decidable fragment of UFLIA. If you use option 1 (`MACRO_FINDER=true`), then the performance impact should be very small. Z3 will detect these quantifiers as macros, and will eliminate the quantifiers and all occurrences of the auxiliary uninterpreted functions. Thus, after preprocessing the resultant problem will be in `QF_LIA`. The performance impact of option 2 (`MBQI`) is not clear, in some problems Z3 may be faster, but in others much slower. – Leonardo de Moura Oct 13 '11 at 00:41
  • Thanks! Just to clarify, my original formulas are LIA with quantifiers, and I want to use LIA quantifier elimination to solve them. The option 1 seems to be more compelling to me, and I'm going to experiment with it soon. – pad Oct 13 '11 at 07:02