Z3 QBVF 问题

Question

跟进之前的讨论：Z3: Extracting existential model-values

有没有区别：

(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 是一个通用变量。