CODEWITHSUNDEEP
setz3
Eneelk
Eneelk

Reputation: 97

Applying a function on the domain of a Z3 set

Is there a way in Z3 to apply a function to each element of a set in order to obtain a new set? In a usual programming language, such a function looks like this: map :: (a -> b) -> Set a -> Set b

I am aware of the map function but it applies an arbitrary function to the range of arrays. The map I'm looking for works with the domain of arrays (given the way of Z3 sets are built).

Upvotes: 0

Views: 401

Answers (1)

alias
alias

Reputation: 30460

This is not possible in SMTLib. Note that the map function you want is a higher-order function, and SMTLib does not support higher-order logic. There are some proposed extensions to include such features, but at least z3 doesn't support such features yet. Some references:

Having said that, you can sometimes get away by simulating higher-ordered features using quantified axioms. Of course, introducing quantifiers make the logic semi-decidable, so the prover can return unknown (and it most likely will for any interesting use case), but it is one way to handle such problems. Here's an example:

; declare two Int sets
(declare-fun S1 () (Array Int Bool))
(declare-fun S2 () (Array Int Bool))

; Function to increment "domain" by 1
(define-fun f ((a Int)) Int (+ a 1))

; Relate S2 to S1 by "mapping" on the domain
; In a higher-order language, this would be:
;      S2 = map f S1
(assert (forall ((x Int)) (= (select S2 x)
                             (select S1 (f x))
                          )))

; some tests:
(assert (= (select S2 4) (select S1 3)))

(check-sat)
(get-model)

Note how I used a forall assertion to express the relationship between S1 and S2. This may not be possible in general; and you might have to also specify the inverse of f in the general case, but it can address basic uses. Note that you will not be able to "pass" a function to any of these: Just like f in the example above, all the functions used in a "higher-order" position will have to be explicitly named. It's rather limited, but can get the job done in simple cases.

Also, while Z3 quickly solves this particular benchmark, I wouldn't expect it to handle arbitrary quantified cases. For reasoning with higher-order functions, Z3 (or any other SMT solver) is just not the right tool. If that's your goal, look into theorem provers like Isabelle, HOL, Coq, Agda, Lean; which are designed from the ground to deal with higher-order features. They also have strong connections (i.e., oracles and proof-replay mechanisms) so they can use SMT solvers as background engines as they complete proofs. The downside is, of course, they are not push-button, and thus require manual guidance. (Though automation has become really good in recent years.)

Upvotes: 1

Related Questions