z3의 상호 재귀 적 데이터 유형과 내장 유형과의 상호 작용

Question

현재 Z3을 사용하여 유형이 다른 언어에 대한 간단한 프로그램 논리를 다형성 목록으로 인코딩하려고합니다.

내가 이해하는 한, the Z3 tutorial by Moura and Bjorner에서 "배열과 같은 다른 유형 안에 재귀 적 데이터 유형 정의를 중첩 할 수 없습니다." 그래서

, 나는 다음과 같은 OCaml의 유형이 있다고 가정 : 내가 사용 Z3이 형식을 인코딩하고 싶습니다 이상적으로

type value = 
    | Num of float 
    | String of string 
    | List of value list 

을 내장 Z3List 유형,하지만 난이 불가능하다고 생각 Z3 때문에 재귀 적 데이터 유형과 다른 유형 사이의 상호 재귀를 지원하지 않습니다. 누군가 이것이 이것이 사실인지 확인할 수 있습니까?

그렇다면 값 목록, my_list 및 my_list 및 value가 상호 재귀적일 수있는 고유 한 형식을 정의 할 수있는 유일한 방법이라고 생각합니다. OCaml의에서 :

type value = 
    | Num of float 
    | String of string 
    | List of my_list 
and my_list = 
    | Cons of value * my_list 
    | nil 

그러나 이것은 내가 Z3는 Z3Lists에 대한 지원 내장 된 추론 인프라를 활용할 수 없음을 의미합니다. 이 작업을 수행하는 더 좋은 방법이 있습니까?

Answer 1

my_list와 함께 병합 된 버전을 사용해야하는 것은 맞습니다. 좋은 소식은 Z3의 목록에 내장 된 추론은 다른 데이터 유형과 동일한 메커니즘을 사용하므로 플랫 데이터 유형 선언과 동일한 추론 지원을 얻을 수 있다는 것입니다.