Z3 : Z3 소개 int2bv?

Question

Z3 (smt2 형식) 작업과 다소 혼동 스럽습니다 int2bv. 나는 그런 smt2 표현 쓴 : 나는 Z3와 그것을 해결 때

(declare-const t1 Int) 
(assert (= ((_ int2bv 2) t1) #b11)) 
(check-sat) 
(get-model) 

를, 그것을 가지고 :

sat 
(model 
    (define-fun t1() Int 
    0) 
) 

올바른인가요? 3일까요? 나는 int2bv 연산이 int 값을 동등한 bitvector 값으로 변환한다고 생각했습니다. 그러나 그렇지 않은 것 같습니다!

감사합니다.

Answer 1

기능은 기본적으로 해석되지 않은 것으로 취급되므로 (문서에 명시된대로) 의미가 정확하지 않습니다. 이전에 그 변환 기능에 대한 몇 가지 질문이 있었다, 그들도 여기에 도움이 될 수 있습니다

Z3: an exception with int2bv

Check overflow with Z3

bv-enable-int2bv-propagation option