z3 - 如何在位向量中使用 forall

Question

我打算做的是去所有的向量，并在每一位上做不同的事情。

我想知道的是我是否表现良好（in define-fun LT....）？

因为结果与预期不符：S

此链接中的代码：http ://rise4fun.com/Z3/xrFK

Answer 1

我不确定您的公式的预期语义是什么，但直觉上似乎您的定义is_in可能是罪魁祸首：

(define-fun is_in ((e (_ BitVec 9)) (S (_ BitVec 9))) Bool
    ;; True if e is an element of the "set" S.
    (= (bvand e S) e))

约束(= (bvand e S) e))意味着这个函数只有在S等于时才能返回真e。按照函数的名称，我希望定义是(not (= (bvand e S) Empty)).