해당 필드 중 하나가 함수가되도록 레코드를 선언하는 방법

Question

저는 Z3에 매우 익숙하므로 어리석은 질문을해서 유감입니다.

일부 필드가 기능을하도록 레코드를 정의하려고합니다. dom으로 의도

(선언 - 데이터 유형 (DOM의 RAN) ((PFun (MK-pfun (DOM (DOM) BOOL) (법 (DOM) RAN)))))

: 나는이 시도 그리고 run은 두 개의 필드가 있는데, 그 타입은 함수입니다 (DOM에서 Bool 로의 함수, DOM에서 RAN으로의 함수의 법칙). 또한 함수 유형을 괄호로 묶으려고했습니다.

(선언 데이터 유형 (DOM RAN) ((PFun (mk-pfun (dom (DOM) Bool)) (law (DOM) RAN)))))))))))

bun 이러한 작품이 없습니다.

자습서를 검색했지만 이에 대한 예는 없습니다.

도와 주시겠습니까?

미리 답변 해 주셔서 감사합니다.

모든 맥시, 최고의

Answer 1

Z3는 1 차 논리에 근거한다. 따라서 함수는 데이터 유형 생성자 또는 다른 함수의 인수가 될 수 없습니다. 배열을 사용하여 고차원 기능을 "시뮬레이션"할 수 있습니다. p이 PFun 및 d 종류 DOM의 일정은 다음 (select (dom p) d) 쓰기가 dom(p)(d)를 얻을하자 당신은

(declare-datatypes (DOM RAN) ((PFun (mk-pfun (dom (Array DOM Bool)) 
               (law (Array DOM RAN)))))) 

로 데이터 유형을 작성할 수 있으며, (select (law p) d)이 law(p)(d)을 얻었다.