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