Z3 및/또는 SMT (v2.6)

Question

에 대한 일반 데이터 유형 모델링 SMT v2.6에서 일반 데이터 유형의 동작을 모델링하고 싶습니다. 저는 Z3를 구속 조건 해결사로 사용하고 있습니다. 나는 official example, 다음과 같은 방법으로 매개 변수화 데이터 형과 같은 일반적인 목록을 기반으로, 모델 : 나는 데이터 유형에 대한 일반적인 될 목록을 원하는

(declare-datatypes (T) ((MyList nelem (cons (hd T) (tl MyList))))) 

. 지금은 그래서 (... 예를 들면, 길이 작업, 빈 운전) 일반 데이터 형식 MyList에 함수를 정의하고 싶은, 그러나

(declare-const x (MyList Int)) 
(declare-const y (MyList Real)) 

: 나중에, 나는 상수에게 다음과 같은 방법을 선언하고 싶습니다 그들은 T님께 재사용 가능합니다. 내가 어떻게이 일을 성취 할 수 있을지 생각해? 나는 다음과 같은 것을 시도했다 :

(declare-sort K) 
(define-fun isEmpty ((in (MyList K))) Bool 
    (= in nelem) 
) 

그러나 이것은 나에게 오류 메시지를 준다; 이 예제가 작동하려면 Z3이 일부 형식 유추를 수행해야합니다.

나에게 힌트를 줄 수 있다면 좋을 것입니다.

Answer 1

SMT-Lib에서는 다형성 사용자 정의 함수를 사용할 수 없습니다. http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf 제 4.1.5 상태 : 종류의 용어를 사용하는 명령에 필요한

잘 정렬도 검사가, 는 항상 현재의 서명과 관련하여 수행됩니다. 이미 서명에있는 기호를 선언하거나 정의하려면 오류 이 발생합니다. 이는 특히 이론 기호 인 기능 심볼과 달리 사용자 정의 함수 심볼을 오버로드 할 수 없음을 의미합니다. 상기 각주-29로 확장된다

는 :

사용자 정의 심볼 오버로딩되지 용 동기는 솔버 그들의 프로세싱을 단순화하는 것이다. 이 제한은 스크립트 에 사용되는 이론의 서명을 새로운 다형 함수 기호 (즉, 이론 기호 인 경우 매개 변수 정렬을 포함하는 순위가 인 계급)로 확장하고자하는 사용자에게만 중요합니다. 예를 들어 사용자는 임의의 목록에 대해 "역"기능을 선언하려는 경우 은 스크립트에 사용 된 각 (콘크리트) 목록 정렬에 대해 다른 역 기능 기호를 정의해야합니다. 이 제한 사항은 이후 버전에서 제거 될 수 있습니다.

사용자가 생각하기에 사용자 수준에서 "다형성"기능을 정의 할 수 없습니다. 그러나 각주에서 알 수 있듯이 SMT 솔버가 더 널리 배포됨에 따라 이러한 제한이 제거 될 가능성이 있습니다. 그러나 그 일이 일어날 때 정확히 누군가의 추측입니다.