Z3 : 실존 적 모델 값 추출하기

Question

저는 Z3의 QBVF 솔버를 가지고 놀고 있으며 실존 적 어설 션에서 값을 추출 할 수 있는지 궁금합니다. 재치하기 위해, 다음과 같은 I가 있다고 가정 해 봅시다 :

는

(assert (exists ((x (_ BitVec 16))) (forall ((y (_ BitVec 16))) (bvuge y x)))) 

이 기본적으로 "최소"16 비트 부호없는 값이 있음을 말한다.

(check-sat) 
(get-model) 

을 그리고 Z3-3.0 행복하게 응답 : 그럼, 내가 말할 수있는 정말 멋진

sat 
(model (define-fun x!0() (_ BitVec 16) 
#x0000) 
) 

합니다. 그러나 내가하고 싶은 것은 get-value를 통해 해당 모델의 조각을 추출 할 수 있어야한다는 것입니다. 당연히, 다음 중 어느 것도 Z3는 바로 그러한 상수가 없습니다 불평 각각의 경우에

(get-value (x)) 
(get-value (x!0)) 

을 제대로 작동하지 않습니다. 분명히 Z3은 (check-sat) 호출에 대한 응답으로 입증 된 정보를 가지고 있습니다. get-value 또는 다른 메커니즘을 통해 실존 값에 자동으로 액세스 할 수 있습니까?

감사합니다 .. Z3에서

Answer 1

는 get-value는 사용자가 "전역"선언을 참조 할 수 있습니다. 실존 변수 x은 로컬 선언입니다. 따라서 get-value을 사용하여 액세스 할 수 없습니다. 기본적으로 Z3은 "skolemization"이라는 프로세스를 사용하여 실존 변수를 제거합니다. 아이디어는 실존하는 변수를 새로운 상수와 함수 기호로 대체하는 것입니다. 예를 들어 수식

exists x. forall y. exists z. P(x, y, z) 

는 Z의 선택 예에 따라 달라질 수 있기 때문에, Z는 함수가되도록

forall y. P(x!1, y, z!1(y)) 

참고로 변환된다. 위키 피 디아에는 skolem normal form

에 관한 항목이 있습니다. 나는 당신이 설명한 문제에 대한 만족스러운 해결책을 찾지 못했습니다. 예를 들어, 수식에는 동일한 이름을 가진 많은 다른 존재 변수가있을 수 있습니다. 따라서 get-value 명령의 각 인스턴스를 불분명하게 참조하는 방법이 명확하지 않습니다.

이 제한에 대한 가능한 해결 방법은 "손으로"스콜화 단계를 적용하거나 적어도 값을 알고 자하는 변수에 적용하는 것입니다. 예를 들어 ,

(assert (exists ((x (_ BitVec 16))) (forall ((y (_ BitVec 16))) (bvuge y x)))) 

같이 기입된다 :

(declare-const x (_ BitVec 16)) 
(assert (forall ((y (_ BitVec 16))) (bvuge y x))) 
(check-sat) 
(get-value x) 

실존 변수와 같은 범용 정량에 중첩되는 경우

(assert (forall ((y (_ BitVec 16))) (exists ((x (_ BitVec 16))) (bvuge y x)))) 
(check-sat) 
(get-model) 

신선한 skolem 기능으로 사용될 수있다 각 y에 대해 x의 값을 얻으십시오. 예는 상술된다 :

(declare-fun sx ((_ BitVec 16)) (_ BitVec 16)) 
(assert (forall ((y (_ BitVec 16))) (bvuge y (sx y)))) 
(check-sat) 
(get-model) 

를이 예에서, sx는 새로운 함수이다. Z3에서 제작 한이 모델은 sx에 대한 해석을 할당합니다. 버전 3.0에서는 해석이 ID 함수입니다. 이 함수는 각 y에 대해 x의 값을 얻는 데 사용할 수 있습니다.