대수 2를 Z3의 비트 벡터로 계산하는 방법은 무엇입니까?

Question

z3이 Bitvectors에 대한 대수를 직접 계산하는 함수가 있습니까?

그렇지 않으면 어떻게 로그를 효율적으로 구현할 수 있습니까?

Answer 1

나는 최선의 방법은 본질적으로 룩업 테이블 인 if-then-else 체인으로 코드화하는 것입니다. 로그 천천히 성장하기 때문에

(ite (< x 2) 0 
    (ite (< x 4) 1 
      (ite (< x 8) 2 
      .... etc ... 

, 당신은 등 32 비트 벡터 32 가지, 다른 기지 유사하다 만이 필요한 것 : 기본-2를 가정하면, (lg 0 = 0 가정) 같은이있을 것이다. 자동으로이 코드를 쉽게 생성 할 수 있습니다.