Z3 QBVF questions

Question

Following up to the previous discussion: Z3: Extracting existential model-values

Is there a difference between:

(declare-fun sx ((_ BitVec 16)) (_ BitVec 16))
(assert (forall ((y (_ BitVec 16))) (bvuge y (sx y))))

And

(declare-fun sx ((_ BitVec 16)) (_ BitVec 16))
(declare-fun y () (_ BitVec 16))
(assert (bvuge y (sx y)))

As far as Z3 is concerned? That is, will I still get the QBVF solver for the latter automatically?

Also, upon experimentation I found that if I issue:

(eval (sx #x8000))

After a (check-sat) call, it works fine (which is great). What would be better is if I could also say:

(eval (sx (get-value (y))))

Alas, for that query Z3 complains that it's an invalid function application. Is there a way to use the eval function in that manner?

Thanks!

Answer 1

The scripts

(declare-fun sx ((_ BitVec 16)) (_ BitVec 16))
(assert (forall ((y (_ BitVec 16))) (bvuge y (sx y))))

and

(declare-fun sx ((_ BitVec 16)) (_ BitVec 16))
(declare-fun y () (_ BitVec 16))
(assert (bvuge y (sx y)))

are not equivalent. The second is actually equisatisfiable to

(declare-fun sx ((_ BitVec 16)) (_ BitVec 16))
(assert (exists ((y (_ BitVec 16))) (bvuge y (sx y))))

Regarding the eval command, you can reference any uninterpreted constant and function symbol. Thus, you can write:

(declare-fun sx ((_ BitVec 16)) (_ BitVec 16))
(declare-fun y () (_ BitVec 16))
(assert (bvuge y (sx y)))
(check-sat)
(eval (sx y))

The command (eval (sx y)) will not work for the first script because y is a universal variable.