Z3에서 비트 벡터를 제로/부호 확장하는 방법은 무엇입니까?

Question

Z3 SMT 인터페이스를 사용하여 비트 벡터에서 제로 확장을 수행 할 수 없습니다. 소스를 읽음으로써 배운 것을 보면, 다양한 바인딩 (C, C++, Python 등)을 사용할 수 있지만, SMT 인터페이스의 튜토리얼에는 호출 방법이 없습니다.

SMT QF_BV 로직 표준의 zero_extend을 사용하면 Z3이 unsupported으로 표시됩니다.

Answer 1

그것은 zero_extend 및 다른 기능 파라 메트릭 사람, C에서 foo<T> 같은 아마 뭔가 ++ 것으로 밝혀졌다. 특수 구문을 사용하는 등의 기능을 하나 개의 필요를 호출하려면 : 절대적으로 맞습니다, zero_extend (다른 사람의 사이에서) 파라 메트릭

sat 
(model 
    (define-fun a() (_ BitVec 1) #b0) 
    (define-fun b() (_ BitVec 2) #b00) 
)