I'm curious what the limitations on z3's map operator are. According to the z3 tutorial (http://rise4fun.com/z3/tutorial), "Z3 provides a parametrized map function on arrays. It allows applying arbitrary functions to the range of arrays."
Map appears to work when I'm mapping built-in functions or functions declared with (declare-fun ...) syntax. When I attempt to use map with function (really macros) defined with (define-fun ...) syntax, I receive the error invalid function declaration reference, named expressions (aka macros) cannot be referenced.
Is there a standard way to map user-defined functions over arrays?
Here is some code that illustrates my confusion:
;simple function, equivalent to or
(define-fun my-or ((x Bool) (y Bool)) Bool (or x y))
(assert (forall ((x Bool) (y Bool)) (= (my-or x y) (or x y))))
(check-sat)
;mapping or with map works just fine
(define-sort Set () (Array Int Bool))
(declare-const a Set)
(assert ( = a ((_ map or) a a) ))
(check-sat)
;but this fails with error
(assert ( = a ((_ map my-or) a a) ))
I'm currently hacking around the problem like this:
(define-fun my-or-impl ((x Bool) (y Bool)) Bool (or x y))
(declare-fun my-or (Bool Bool) Bool)
(assert (forall ((x Bool) (y Bool)) (= (my-or x y) (my-or-impl x y))))
(check-sat)
But I'm hoping that there's a way to solve this which doesn't involve universal quantifiers.