Z3 - 배열 패턴 일치하기

Question

배열과 배열 목록을 매개 변수로 사용하고 목록의 배열 색인을 반환하는 함수를 형식화하려고합니다. 나는 매우 다른 접근법을 시도하고 Z3에서 "알려지지 않은"것을 얻는다.

이

(declare-fun SameArray ((Array Int Real) (Array Int Real)) Bool) 
(declare-fun Match ((Array Int Real) (Array Int (Array Int Real))) Int) 

(assert (forall ((array1 (Array Int Real)) (array2 (Array Int Real))) 
    (= 
     (SameArray array1 array2) 
     (ite (forall ((i Int)) (= (select array1 i) (select array2 i))) true false) 
    ) 
) 
) 

;(assert (forall ((pattern (Array Int Real)) (list (Array Int (Array Int Real)))) 
; (or 
; (exists ((index Int)) 
;  (and 
;  (= (SameArray pattern (select list index)) true) 
;  (forall ((j Int)) (or (= (SameArray pattern (select list j)) false) (>= j index))) 
;  (= (Match pattern list) index) 
;  ) 
; ) 
; (= (Match pattern list) (- 1)) 
; ) 
;)) 

(assert (forall ((pattern (Array Int Real)) (list (Array Int (Array Int Real)))) 
    (exists ((index Int)) 
    (and 
     (= (Match pattern list) index) 
     (or 
     (and 
      (= (SameArray pattern (select list index)) true) 
      (forall ((j Int)) (or (= (SameArray pattern (select list j)) false) (>= j index))) 
     ) 
     (= index (- 1)) 
    ) 
    ) 
) 
)) 

; Testing - SameArray 

(declare-const a1 (Array Int Real)) 
(declare-const a2 (Array Int Real)) 

(assert (= (store a1 1 1.1) a1)) 
(assert (= (store a1 2 1.2) a1)) 
(assert (= (store a1 3 1.3) a1)) 

(assert (= (store a2 1 2.1) a2)) 
(assert (= (store a2 2 2.2) a2)) 
(assert (= (store a2 3 2.3) a2)) 

(assert (= (SameArray a1 a1) true)) 
(assert (= (SameArray a1 a2) false)) 

(check-sat) 

; Testing - Match 

(declare-const aAll (Array Int (Array Int Real))) 

(assert (= (store aAll 1 a2) aAll)) 
(assert (= (store aAll 2 a1) aAll)) 

(assert (= (Match a1 aAll) 2)) 

(check-sat) 

편집 : 에도 매우 간단 더미 버전은 작동하지 않습니다 여기에

내가 첫 번째 나 두 번째 공리 작업 (여러 다른 여기에 포함되지 않았다)도 이에 시도하는 코드이다. 나는 패턴 (P => Q)과 (P => Q '가 아님)을가집니다. 왜 Z3이 나에게 unknwon을 주는지 나는 모른다.

(assert (forall ((pattern (Array Int Real)) (list (Array Int (Array Int Real)))) 
    (=> 
    (forall ((j Int)) (= (SameArray pattern (select list j)) false)) 
    (= (Match pattern list) (- 1)) 
) 
)) 

(assert (forall ((pattern (Array Int Real)) (list (Array Int (Array Int Real)))) 
    (=> 
    (not (forall ((j Int)) (= (SameArray pattern (select list j)) false))) 
    (= (Match pattern list) 1) 
) 
)) 

Answer 1

문제가 해결 될 수 있습니다. 가장 큰 문제점은 함수 Match이 방금 선언되었고 정의되지 않았으며 Z3이 추가 공리를 처리하는 데 문제가 있다는 것입니다. SameArray 함수에 문제가 없었지만 Match 함수가 실패했습니다. 올바른 정의는 다음과 같습니다.

(define-fun SameArray ((array1 (Array Int Real)) (array2 (Array Int Real))) Bool 
    (ite (forall ((i Int)) (= (select array1 i) (select array2 i))) true false) 
) 


(define-fun Match ((pattern (Array Int Real)) (list (Array Int (Array Int Real)))) Int 
    (ite 
    (exists ((index Int)) 
     (and 
     (= (SameArray pattern (select list index)) true) 
     (forall ((j Int)) (or (= (SameArray pattern (select list j)) false) (>= j index))) 
    ) 
    ) 
    1 0) 
) 

Answer 2

나는 코드의 this variant에서 수행대로 모두 MBQI 및 AUTO_CONFIG을 비활성화 느낌을 얻을. 첫 번째 check-sat은 unknown이고 두 번째 것은 unsat입니다. set-option 두 가지를 모두 언급하면 ​​sat 및 unsat이 표시됩니다.

push/pop 범위 내의 어설 션이 첫 번째 공리와 모순되기 때문에 unsat이 필요합니다.

unknown 대 sat에 대해서는 약간 추측해야합니다. 내 이해에 따르면 MBQI은 해석되지 않은 모든 기호에 대한 해석을 찾으려고합니다. 즉, 주어진 어설 션을 만족시킬 수있는 모델을 찾으려고 시도합니다.

MBQI이 없으면 Z3은 전자 매칭을 사용합니다. 즉, 해석되지 않은 기호에 대한 해석을 찾지 않습니다. Z3은 모순을 찾으려고 노력하지만, 첫 번째 점 check-sat의 주장은 서로 모순되지 않습니다. 문제에는 유도 할 수있는 모순이 포함되어 있지 않으므로 Z3에서 알 수없는 해석되지 않은 기호가 포함되어 있으므로 Z3에서보고 할 수있는 코드는 모두 unsat입니다.