SSA에서 z3 bvsmod 동작 이해

Question

z3을 사용하여 배우려고합니다. 그래서이 질문은 어리석은 일입니다.

다음 코드에서 bvsmod를 bvadd와 비교했을 때 Z3에서 x___0에 대한 예기치 않은 값이 나타나는 이유는 무엇입니까? SSA를 사용하여 여기에서 실행 흐름을 구현합니다.

Z3 지침 :

(set-option :pp.bv-literals false) 
; 
; The code 
; x %= 5 
; x * 2 == 8 
; Implement SSA 
; x1 = x0 % 5 
; x1 * 2 == 8 
; 
(push) 
(set-info :status unknown) 
(declare-const x___0 (_ BitVec 32)) 
(declare-const x___1 (_ BitVec 32)) 
(assert (= x___1 (bvsmod x___0 (_ bv5 32)))) 
(assert (= (bvmul x___1 (_ bv2 32)) (_ bv8 32))) 
(check-sat) 
(get-model) 
(pop) 
; 
; The code 
; x += 1 
; x * 2 == 8 
; Implement SSA 
; x1 = x0 + 1 
; x1 * 2 == 8 
; 
(push) 
(declare-const x___0 (_ BitVec 32)) 
(declare-const x___1 (_ BitVec 32)) 
(assert (= x___1 (bvadd x___0 (_ bv1 32)))) 
(assert (= (bvmul x___1 (_ bv2 32)) (_ bv8 32))) 
(check-sat) 
(get-model) 
(pop) 

결과 :

sat 
(model 
    (define-fun x___1() (_ BitVec 32) 
     (_ bv4 32)) 
    (define-fun x___0() (_ BitVec 32) 
     (_ bv3720040335 32)) 
) 
sat 
(model 
    (define-fun x___1() (_ BitVec 32) 
     (_ bv4 32)) 
    (define-fun x___0() (_ BitVec 32) 
     (_ bv3 32)) 
) 

내가 의미가 값 3를 얻을 x___0 bvadd 사용 방정식의 경우.

bvsmod의 경우 값이 인데, 예상되는 값 근처의 값, 즉 4로 끝나는 값이없는 이유는 무엇입니까?

Answer 1

(... 평가)을 할 수 있습니다. 인코딩은 괜찮습니다.

bvsmod에 대한 호출을 통해 암시 적으로 암시 된 32 비트 부호있는 정수를 사용하고 있음을 알 수 있습니다. 리턴 된 모델은 십진법으로 등가가 3720040335 인 32 비트 비트 벡터 값을 제공합니다. 부호가있는 값으로 해석하면 실제로는 -574926961이며 요청한대로 은 실제로 4과 동일 함을 확인할 수 있습니다.

솔버는 제약 조건을 만족하는 모델을 무료로 제공합니다. 좀 더 구체적인 가치를 원한다면 "단순한"형식적으로 의미해야하는 것을 인코딩하기 위해 제약 조건을 추가해야합니다.

Answer 2

이와 같은 수식을 작성하려면 한정 기호가 필요합니다. 대신 SMT 표현식을 사용하는 것이 좋습니다. 공유는 무료로 이루어질 것입니다. 당신이 중간 값이 필요한 경우 쓰기 예컨대는 : (assert (= (bvmul (bvadd x___0 (_ bv1 32)) (_ bv2 32)) (_ bv8 32)))

, 당신은 항상 나중에 점점 값으로 아무 문제가 없다