smt - Z3: Extracting existential model-values

Question

I'm playing around with Z3's QBVF solver, and wondering if it's possible to extract values from an existential assertion. To wit, let's say I have the following:

(assert (exists ((x (_ BitVec 16))) (forall ((y (_ BitVec 16))) (bvuge y x))))

This basically says that there is a "least" 16-bit unsigned value. Then, I can say:

(check-sat)
(get-model)

And Z3-3.0 happily responds:

sat
(model  (define-fun x!0 () (_ BitVec 16)
#x0000)
)

Which is really cool. But what I want to do is to be able to extract pieces of that model via get-value. Unsurprisingly, none of the following seem to work

(get-value (x))
(get-value (x!0))

In each case Z3 rightly complains there's no such constant. Clearly Z3 has that information as evidenced by the response to the (check-sat) call. Is there any way to access the existential value automatically via get-value, or some other mechanism?

Thanks..

Answer 1

In Z3, get-value only allows the user to reference “global” declarations. The existential variable x is a local declaration. Thus, it can’t be accessed using get-value. By default, Z3 eliminates existential variables using a process called “skolemization”. The idea is to replace existential variables with fresh constants and function symbols. For example, the formula

exists x. forall y. exists z. P(x, y, z)

is converted into

forall y. P(x!1, y, z!1(y))

Note that z becomes a function because the choice of z may depend on y. Wikipedia has an entry on skolem normal form

That being said, I never found a satisfactory solution for the problem you described. For example, a formula may have many different existential variables with the same name. So, it is not clear how to reference each instance in the get-value command in a non-ambiguous way.

A possible workaround for this limitation is to apply the skolemization step “by hand”, or at least for the variables you want to know the value. For example,

(assert (exists ((x (_ BitVec 16))) (forall ((y (_ BitVec 16))) (bvuge y x))))

is written as:

(declare-const x (_ BitVec 16))
(assert (forall ((y (_ BitVec 16))) (bvuge y x)))
(check-sat)
(get-value x)

If the existential variable is nested in a universal quantifier such as:

(assert (forall ((y (_ BitVec 16))) (exists ((x (_ BitVec 16))) (bvuge y x))))
(check-sat)
(get-model)

A fresh skolem function can be used to obtain the value of x for each y. The example above becomes:

(declare-fun sx ((_ BitVec 16)) (_ BitVec 16))
(assert (forall ((y (_ BitVec 16))) (bvuge y (sx y))))
(check-sat)
(get-model)

In this example, sx is the fresh function. The model, produced by Z3, will assign an interpretation for sx. In version 3.0, the interpretation is the identity function. This function can be used to obtain the value of x for each y.