Z3 만족 모델을 출력하는 솔버?

Question

Z3에서 입력 스크립트가 SMTLib 형식으로 작성된 경우 모델을 출력 할 수 있습니까 (모델을 만족하는 값 할당)? get-model은 제약 조건을 만족시키는 해석을 반환합니다. 이 해석들로부터 구체적인 가치를 추출 할 방법이 있습니까? 파이썬/C++ API를 사용하여 모델 값을 얻을 수 있다는 것을 알고 있습니다.

가

Answer 1

당신은 아마 get-value를 사용하려면

가 여기에 최소한의 예입니다 (rise4fun 링크 : http://rise4fun.com/Z3/wR81) : 당신은 잠재적으로 다음이 당신이 등을하려고하는지에 따라 구문 분석해야 할 것

(declare-fun x() Int) 
(declare-fun y() Int) 
(declare-fun z() Int) 
(assert (>= (* 2 x) (+ y z))) 
(declare-fun f (Int) Int) 
(declare-fun g (Int Int) Int) 
(assert (< (f x) (g x x))) 
(assert (> (f y) (g x x))) 
(check-sat) ; sat 
(get-model) ; returns: 
; (model 
; (define-fun z() Int 
; 0) 
; (define-fun y() Int 
; (- 38)) 
; (define-fun x() Int 
; 0) 
; (define-fun g ((x!1 Int) (x!2 Int)) Int 
; (ite (and (= x!1 0) (= x!2 0)) 0 
;  0)) 
; (define-fun f ((x!1 Int)) Int 
; (ite (= x!1 0) (- 1) 
; (ite (= x!1 (- 38)) 1 
;  (- 1)))) 
;) 
(get-value (x)) ; returns ((x 0)) 
(get-value ((f x))) ; returns (((f x) (- 1))) 

자세한 내용은

의 SMT-LIB 표준 체크 아웃 :

http://smtlib.cs.uiowa.edu/language.shtml

최신을 버전은 http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.0-r12.09.09.pdf

get-value 페이지의 39/그림 3.5에 나와 있습니다.