Z3 QBVF问题

Question

继之前的讨论之后：Z3：提取存在模型值

有什么区别之间：

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

至于

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

Z3呢？也就是说，我仍然会自动获得后者的 QBVF 求解器吗？

另外，经过实验，我发现如果我发出：

(eval (sx #x8000))

在 (check-sat) 调用之后，它工作正常（这很棒）。 那就更好了

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

如果我还可以说：唉，对于该查询，Z3 抱怨它是一个无效的函数应用程序， 。有没有办法以这种方式使用eval函数？

谢谢！

Answer 1

脚本

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

和

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

并不等效。第二个实际上可以满足

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

关于eval命令，您可以引用任何未解释的常量和函数符号。因此，您可以编写：

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

命令 (eval (sx y)) 对于第一个脚本不起作用，因为 y 是通用变量。