함수는 생성자에서 2 개의 매개 변수를 사용하여 정렬을 수신합니다.

Question

4 가지 (작업, 역할, 사용자 및 실행)를 만들었습니다. 마지막 매개 변수는 2 개의 매개 변수를받은 다음 실행, 호출 P Run의 "인스턴스"를 만들기 위해 2 개의 파라미터를 받는다. 그런 다음 사용자 역할 "관계"(Privs)와 역할 - 태스크 "관계"(역할)가 포함 된 두 개의 배열을 만들었습니다. 이 두 배열을 사용하여 사용자 u를 볼 때 Priv.r에서 역할 r을 갖고 역할에서 역할 r을 찾을 때 작업 t를 갖는지를 확인합니다. 지금까지 나는이 같은 별도의 라인에서이 작업을 수행하기 위해 관리 :

(declare-sort Task) 
(declare-sort Role) 
(declare-sort User) 
(declare-sort Run 2) 
(define-sort P (User Role) (Run User Role)) 
(declare-fun t() Task) 
(declare-fun r() Role) 
(declare-fun u() User) 
(declare-const Privs (Array User Role)) 
(declare-const Roles (Array Role Task)) 


(assert (= (select Privs u) r)) 
(assert (= (select Roles r) t)) 

을하지만 지금은 실행을받는 재미 (사용자, 역할 쌍)을 만들려고 노력하고 함수 내에서 같은 주장하지만, 모든 사용자입니다 P와 그 모든 역할. 실행 정렬 변수를 함수에 전달하여 수행 할 수 있습니까 ?? .. 내부의 요소 (사용자, 역할)에 액세스하기 위해 ??

Answer 1

"사용자"와 "역할"로 인스턴스화 된 정렬과 함께 "실행"만 사용하면 매개 변수 유형을 사용하게됩니다. 그렇다면 "Run"을 매개 변수화해야하는 이유는 무엇입니까? 매개 변수 정렬 및 사용 사례에 대한 정의는 http://smtlib.org에 자세하게 설명되어 있습니다. Z3은이 공통 형식을 구현하므로 질문에 대한 Z3에는 특별한 것이 없습니다.