z3 - 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 抱怨它是一个invalid function application. 有没有办法以这种方式使用该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它是一个通用变量。