Difference between macro and quantifier in Z3

Question

I would like to know what is the difference between following 2 statements -

Statement 1

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

Statement 2

(declare-fun max_integ ((Int)(Int)) Int)
(assert (forall ((x Int) (y Int)) (= (max_integ x y) (if (< x y) y x))))

I observed that when I use Statement1, my z3 constraints give me a result in 0.03 seconds. Whereas when I used Statement2, it does not finish in 2 minutes and I terminate the solver. I would like also to know how achieve it using C-API.

Thanks !

Answer 1

Statement 1 is a macro. Z3 will replace every occurrence of max_integ with the ite expression. It does that during parsing time. In the second statement, by default, Z3 will not eliminate max_integ, and to be able to return sat it has to build an interpretation for the uninterpreted symbol max_integ that will satisfy the quantifier for all x and y. Z3 has an option called :macro-finder, it will detect quantifiers that are essentially encoding macros, and will eliminate them. Here is an example (also available online here):

(set-option :macro-finder true)
(declare-fun max_integ ((Int)(Int)) Int)
(assert (forall ((x Int) (y Int)) (= (max_integ x y) (if (< x y) y x))))
(check-sat)
(get-model) 

That being said, we can easily simulate macros in a programmatic API by writing a function that given Z3 expressions return a new Z3 expression. Here in an example using the Python API (also available online here):

def max(a, b):
   # The function If builds a Z3 if-then-else expression
   return If(a >= b, a, b)

x, y = Ints('x y')
solve(x == max(x, y), y == max(x, y), x > 0)

Yet another option is to use the C API: Z3_substitute_vars. The idea is to an expression containing free variables. Free variables are created using the API Z3_mk_bound. Each variable represents an argument. Then, we use Z3_substitute_vars to replace the variables with other expressions.