정렬 매개변수 래퍼 함수

Question

여러 내장 및 사용자 정의 Z3 정렬을 사용한다고 가정합니다.Int, Bool, S1, S2, ... A 정렬에서 B 정렬로 캐스트하는 일반적인 정렬 래핑 및 래핑 해제 함수를 작성하는 방법이 있습니까?예를 들어

(declare-const a S1)
(declare-const b S2)
(declare-const c Int)

(WRAP[S1] b) ; Expression is of sort S1
(WRAP[S1] c) ; Expression is of sort S1
(WRAP[Int] (WRAP[S1] c)) ; Expression is of sort Int

나는 현재 각 사례를 수동으로 다루고 있습니다.

(declare-fun $boolToInt (Bool) Int)
(declare-fun $intToBool (Int) Bool)

(assert (forall ((x Int))
  (= x ($boolToInt($intToBool x)))))

(assert (forall ((x Bool))
  (= x ($intToBool($boolToInt x)))))

이러한 래퍼는 지정된 종류 집합에서 자동으로 생성될 수 있지만 가능한 일반적인 솔루션을 선호합니다.

Answer 1

데이터 유형을 사용하여 "공용체 유형"을 인코딩할 수 있습니다.예는 다음과 같습니다.

(declare-sort S1)
(declare-sort S2)

(declare-datatypes () ((S1-S2-Int (WRAP-S1 (S1-Value S1))
                                  (WRAP-S2 (S2-Value S2))
                                  (WRAP-Int (Int-Value Int)))))

(declare-const a S1)
(declare-const b S2)
(declare-const c Int)

(simplify (WRAP-S1 a))
(simplify (= (WRAP-S1 a) (WRAP-Int 10)))
(simplify (S1-Value (WRAP-S1 a)))
(simplify (is-WRAP-S2 (WRAP-S1 a)))
(simplify (is-WRAP-S1 (WRAP-S1 a)))
(simplify (is-WRAP-Int (WRAP-Int c)))
(simplify (S1-Value (WRAP-S2 b)))

데이터 유형에 대한 자세한 내용은 다음에서 찾을 수 있습니다. Z3 가이드.데이터 유형 S1-S2-Int 세 개의 생성자가 있습니다. WRAP-S1, WRAP-S2 그리고 WRAP-Int.Z3은 인식기 조건자를 자동으로 생성합니다. is-WRAP-S1, is-WRAP-S2 그리고 is-WRAP-Int.접근자 S1-Value, S2-Value 그리고 Int-Value "해체"하는 데 사용됩니다. S1-S2-Int 값.예를 들어, 모든 사람에게 a, (S1-Value (WRAP-S1 a)) = a.의 가치 (S1-Value (WRAP-S2 b)) 과소 지정되었습니다.이 경우 Z3는 다음을 처리합니다. S1-Value 해석되지 않은 함수로.

그런데 공리

(assert (forall ((x Int))
  (= x ($boolToInt($intToBool x)))))

거짓과 동일합니다.본질적으로 부울에 정수를 주입하려고 합니다.