Z3: Extracting Existential Model Values
I am playing with the Z3 QBVF solver and wondering if it is possible to extract values from an existential statement. Suppose I have the following:
(assert (exists ((x (_ BitVec 16))) (forall ((y (_ BitVec 16))) (bvuge y x))))
Basically it says there is a "least" unsigned 16-bit value. Then I can say:
(check-sat)
(get-model)
And Z3-3.0 happily replies:
sat
(model (define-fun x!0 () (_ BitVec 16)
#x0000)
)
Which is really cool. But what I want to do is to extract parts of this model via get-value. Unsurprisingly, none of the following works
(get-value (x))
(get-value (x!0))
In every case, Z3 rightly complains that there is no such constant. Obviously, the Z3 has such information, as evidenced by the answer to the call (check-sat)
. Is there a way to automatically access the existential meaning through get-value
or some other mechanism?
Thank..
source to share
The Z3 get-value
allows the user to link to "global" ads. An existential variable x
is a local declaration. Thus, it cannot be accessed with get-value
. By default, Z3 eliminates existential variables using a process called comemisation. 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)
converted to
forall y. P(x!1, y, z!1(y))
Note that z becomes a function since the choice of z may depend on y. Wikipedia has an entry in normal form
Thus, I have never found a satisfactory solution to the problem you described. For example, a formula can have many different existential variables with the same name. Thus, it is not clear how to refer to each instance in a command in an get-value
unambiguous way.
A possible workaround for this limitation is to apply the combo step "manually", or at least for the variables you want to know. For example,
(assert (exists ((x (_ BitVec 16))) (forall ((y (_ BitVec 16))) (bvuge y x))))
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)
You can use the fresh skolem function to get the value x
for each y
. Example above:
(declare-fun sx ((_ BitVec 16)) (_ BitVec 16))
(assert (forall ((y (_ BitVec 16))) (bvuge y (sx y))))
(check-sat)
(get-model)
In this example sx
, this is a new feature. The model generated by Z3 will assign an interpretation to sx
. In 3.0, interpretation is an identification function. This function can be used to get the value x
for each y
.
source to share