(Z3Py) concat, 한정 기호 및 비트 벡터

Question

비트 벡터 및 연결과 함께 수량 기호를 사용할 수 있습니까? 최신 Z3에서 다음 코드를 실행, 설명하기 :

a = BitVec('a', 8) 
b = Concat(BitVec('b', 4), BitVec('c', 4)) 

prove(ForAll(a, Exists(b, a == b))) 

다음과 같은 오류가 발생합니다 :

BitVecRef instance has no attribute '__len__' 

나는 BitVecRef에 간단한 __len__ 방법을 추가하는 시도했지만 또 다른 문제가 발생했다.

Concat이 없으면 코드가 예상대로 작동합니다. 예를 들어

a = BitVec('a', 8) 
b = BitVec('b', 8) 

prove(ForAll(a, Exists(b, a == b))) 

올바른 출력 : proved

Answer 1

내 예 B 연접 속기로서 값을 정의한다. 한정어 Exists (b, a == b)에 대한 바운드 변수로 전달됩니다. 한정자는 아래의 a, b, c와 같은 기본 상수의 목록을 예상하지만 d와 같은 compound 식은 포함하지 않습니다. 아래는 처리 된 퍼즐의 버전입니다.

a = BitVec('a', 8) 
b = BitVec('b', 4) 
c = BitVec('c', 4) 
d = Concat(b, c) 

prove(ForAll(a, Exists(b, a == d)))