Macro to calculate maximum value

Question

I found the macro to calculate the maximum value in Z3 Sat Solver.

(define-fun max_integ ((x Int) (y Int)) Int 
    (ite (< x y) y x)) 

How to program the same using C-API in Z3 Sat Solver?

Thank You,

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 max_integ 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. This issue is discussed in the following posts:

• Equivalent of define-fun in Z3 API

• Z3 SMT 2.0 vs Z3 py implementation