如何在位向量中使用所有向量

Question

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

我想知道的是，如果我做得很好（在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等於這個函數只能返回true。按照函數的名稱，我希望定義爲(not (= (bvand e S) Empty))。