CODEWITHSUNDEEP
z3
Mae Milano
Mae Milano

Reputation: 754

mapping user-defined functions in z3

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.

Upvotes: 1

Views: 1241

Answers (2)

jnfoster
jnfoster

Reputation: 31

The best option is to use (_ map or).

Unless one wants to map a non-built-in function over an array... I guess declare-fun plus assert is the only way to go?

Upvotes: 0

Leonardo de Moura
Leonardo de Moura

Reputation: 21475

Unfortunately, define-fun is just a macro definition in Z3. They are implemented in the Z3 SMT 2.0 parser. They are not part of the Z3 kernel. That is, Z3 solvers do not even "see" these definitions. The approach using declare-fun and quantifiers works, but as you said we should avoid quantifiers since they create performance problems, and it is really easy to create problems with quantifiers that Z3 can't solve. The best option is to use (_ map or).

Upvotes: 1

Related Questions