2

继续前面的讨论: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功能?

谢谢!

4

1 回答 1

2

脚本

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

于 2011-09-09T14:08:09.223 回答