매개 변수화 된 정렬

Question

매개 변수화 된 정렬 값에 어떻게 액세스합니까? 예를 들어

, 나는 다음과 같은 선언이있는 경우 : 나는 x가 나타내는 쌍의 첫 번째 요소에 액세스하려면 어떻게

(declare-sort Pair 2) 
(declare-const x (Pair Int Int)) 

를?

Answer 1

해당 필드에 액세스하기 위해 first 및 second이라는 두 개의 선택자를 사용하여 매개 변수 레코드를 만들 수 있습니다. 여기

는 an example입니다 : Z3 SMT 가이드 algebraic datatypes에 대한 포괄적 인 소개도 있습니다

(declare-datatypes (T1 T2) ((Pair (mk-pair (first T1) (second T2))))) 
(declare-const p1 (Pair Bool Int)) 
(declare-const p2 (Pair Int Int)) 
(assert (first p1)) 
(assert (> (first p2) 2)) 
(assert (= (second p1) (second p2))) 
(check-sat) 
(get-model) 

.