부분적 Z3에서 Z3

Question

에서 헌장을 해석, 하나는과 같이 const 완전히 해석의를 선언 할 수

(declare-const x Int) 

을 마찬가지로, 하나가 정의 할 수있는이 같은 하나의 완전 해석 :

(define-fun y() Int 3) 
; y == 3 

을 감안할 때 대수 데이터 유형 인 경우 다음과 같이 완전히 해석 된 튜플을 가질 수 있습니다.

(declare-datatypes() ((Item (mk-item (size Int) (weight Int))))) 
(define-fun z() Item (mk-item 3 4)) 
; z == Item(size=3, weight=4) 

... 또는 온 해석 아래와 같은 하나

가

(declare-const i1 (Item Int Int)) 

앞의 예에 따라, 그래서 지금은, 부분적으로 해석 데이터 형식을 가질 수 있습니다, weight 각 항목에 대한 수정 될 것이며 size는 다를 수 있습니까?

; (bad syntax, but I hope you get the idea) 
; in this case the size is varying, but weight is fixed to 5 
(declare-const i2 (Item Int 5)) 

당신은 단순히 declare-fun로를 선언하고 당신이 알고있는 부분에 대한 평등을 주장한다

Answer 1

:

(declare-datatypes() ((Item (mk-item (size Int) (weight Int))))) 

(declare-fun x() Item) 
(assert (= (weight x) 5)) 

(check-sat) 
(get-model) 

이 생성됩니다

sat 
(model 
    (define-fun x() Item 
    (mk-item 0 5)) 
) 

을