비트 벡터에서 어떻게 사용합니까?

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))는,674 S이 같을 때이 기능은 true를 반환 할 수 있다는 것을 의미. 함수의 이름으로 가면 정의가 (not (= (bvand e S) Empty)) 일 것으로 예상됩니다.