Map over Array with min or max

[andrewthad]

Z3 lets users map over multiple arrays together. For example:

(define-fun array_and ((s1 (Array Int Bool)) (s2 (Array Int Bool))) (Array Int Bool) ((_ map and) s1 s2))
(define-fun array_gt ((s1 (Array Int Int)) (s2 (Array Int Int))) (Array Int Bool) ((_ map (> (Int Int) (Int))) s1 s2))
(define-fun array_plus ((s1 (Array Int Int)) (s2 (Array Int Int))) (Array Int Int) ((_ map (+ (Int Int) (Int))) s1 s2))

This works because and, >, and + are built-in functions. I have not been able to figure out a way to do the same with a user-defined min or max (binary functions of type (Int Int) (Int)). According to https://stackoverflow.com/a/19338192/1405768, using define-fun is not an option. Here's an attempt with lambda, which I'm not familiar with:

(define-fun array_max ((s1 (Array Int Int)) (s2 (Array Int Int))) (Array Int Int) ((_ map (lambda ((x Int) (y Int)) (ite (> x y) x y))) s1 s2))

Z3 rejects this with

(error "line 10 column 100: unknown sort 'x'")

And I don't believe that lambda is even intended to be used this way.

It is possible to work around this by supplying an uninterpreted function and guiding its interpretation by using assert everywhere. I'm hoping that doing this is not necessary though.

Here is an example of the workaround I described:

(declare-fun my_max (Int Int) (Int))
(define-fun array_max ((s1 (Array Int Int)) (s2 (Array Int Int))) (Array Int Int) ((_ map my_max) s1 s2))

[andrewthad]

I think I've figured this out. Using lambda to build an array, it's possible to write:

(define-fun true_array_max ((s1 (Array Int Int)) (s2 (Array Int Int))) (Array Int Int) (lambda ((i Int)) (ite (> (select s1 i) (select s2 i)) (select s1 i) (select s2 i))))

Are there any caveats to this, or should it work as expected?

[NikolajBjorner]

There is a difference between using map and lambda:

• the built-in decision procedure for arrays with map know when formulas are satisfied and can then acta as a decision procedure. You can use define-fun or define-fun-rec for the functions passed to map. Passing in an expression (lambda) is not supported. Somehow the error message makes no sense.
• the formulation using lambda is handled on a best effort manner. It depends on how you use true_array_max. If you start comparing arrays (use extensionality) then the solver may not be able to conclude satisfiability.

[andrewthad]

Thanks. I had forgotten that extensionality necessarily becomes undecidable once lambda is introduced. Also, I figured out a better way to formulate my original function without using lambda:

(define-fun better_array_max ((s1 (Array Int Int)) (s2 (Array Int Int))) (Array Int Int)
  ((_ map (ite (Bool Int Int) (Int))) ((_ map (> (Int Int) (Bool))) s1 s2) s1 s2)
)