z3 모델의 배열 용어 값

Question

제 연구에 z3을 사용하고 있는데 다음과 같은 문제가 있습니다. 배열과 해석되지 않은 함수가 포함 된 만족스러운 수식 모델을 분석합니다. 특정 배열 항목을 검사하고 싶습니다.

z3 가이드의 예제에서 이러한 값에 액세스 할 수 있습니다.
예컨대,

(get-value ((select my_array 0))) 

같은 질문에 대한 위치 0에서 my_array의 값이 1 것을 나타내는

(((select my_array 0) 1)) 

같은 답변을 얻을 수 있습니다.

그러나, 내가 할 대답은 전혀 매우 도움이되지 않습니다

(((select my_array 0) (select Array!val!0 0))) 

것 같습니다. ,

;; universe for (Array Int Int): 
    ;; Array!val!10 Array!val!6 Array!val!0 Array!val!5 Array!val!9 Array!val!1 Array!val!11 Array!val!4 Array!val!2 Array!val!7 Array!val!3 Array!val!8 
    ;; ----------- 
    ;; definitions for universe elements: 
    (declare-fun Array!val!10() (Array Int Int)) 
    (declare-fun Array!val!6() (Array Int Int)) 
    (declare-fun Array!val!0() (Array Int Int)) 
    (declare-fun Array!val!5() (Array Int Int)) 
    (declare-fun Array!val!9() (Array Int Int)) 
    (declare-fun Array!val!1() (Array Int Int)) 
    (declare-fun Array!val!11() (Array Int Int)) 
    (declare-fun Array!val!4() (Array Int Int)) 
    (declare-fun Array!val!2() (Array Int Int)) 
    (declare-fun Array!val!7() (Array Int Int)) 
    (declare-fun Array!val!3() (Array Int Int)) 
    (declare-fun Array!val!8() (Array Int Int)) 
    ;; cardinality constraint: 
    (forall ((x (Array Int Int))) 
      (and (= x Array!val!10) 
       (= x Array!val!6) 
       (= x Array!val!0) 
       (= x Array!val!5) 
       (= x Array!val!9) 
       (= x Array!val!1) 
       (= x Array!val!11) 
       (= x Array!val!4) 
       (= x Array!val!2) 
       (= x Array!val!7) 
       (= x Array!val!3) 
       (= x Array!val!8))) 
    ;; ----------- 

난 정말 이것의 의미를 이해하지 않지만, 어떻게 든이 내 문제에 관련이있는 것으로 보인다

또한, 모델의 시작 부분에 I는 다음과 같다 블록을 얻을 비슷한 블록이 이 아니기 때문에이 가이드의 간단한 예를 들어보십시오. 누구든지 z3의 이러한 동작을 어떻게 유발하는지 또는 피할 수있는 방법을 알고 있습니까?

몇 가지 실험을 한 후 원하지 않는 동작을 나타내는 "최소"예제를 발견했습니다. 그것은 인덱스 표현식에서 해석되지 않은 함수를 사용하는 것과 관련이있는 것 같습니다. 이것에

(declare-fun my_function ((Int)(Int)) Int) 
(declare-fun my_array() (Array Int Int)) 

(assert 
    (= 
    (select my_array (my_function 0 1)) 
    (select my_array (my_function 1 0)) 
) 
) 

(check-sat) 
(get-model) 
(get-value ((select my_array (my_function 0 1)))) 
(get-value ((my_function 0 1))) 

Z3의 반응은 다음과 같습니다

SMT에서

sat 
(model 
;; universe for (Array Int Int): 
;; Array!val!0 
;; ----------- 
;; definitions for universe elements: 
(declare-fun Array!val!0() (Array Int Int)) 
;; cardinality constraint: 
(forall ((x (Array Int Int))) (= x Array!val!0)) 
;; ----------- 
(define-fun my_array() (Array Int Int) 
Array!val!0) 
(define-fun my_function ((x!1 Int) (x!2 Int)) Int 
(ite (and (= x!1 0) (= x!2 1)) 2 
(ite (and (= x!1 1) (= x!2 0)) 3 
2))) 
) 
(((select my_array (my_function 0 1)) (select Array!val!0 2))) 
(((my_function 0 1) 2)) 

Answer 1

, 어떤 이론은 "논리"지정 수식을 구성 할 수 있습니다. 예를 들어, (set-logic QF_UFLIA) 명령을 사용하면 해석되지 않은 함수와 선형 정수 연산을 사용할 수 있습니다. 논리가 명령 set-logic을 사용하여 지정되지 않은 경우. Z3은 사용자에 대한 논리를 자동으로 추측하고 필요한 이론 만 "설치"합니다. 귀하의 예제에서 Z3은 귀하의 예제가 배열 이론을 필요로하지 않는다고 잘못 추측합니다. 따라서 (Array Int Int)은 해석되지 않은 정렬로 처리됩니다. Z3에서 (Array Int Int)가 해석되지 않은 정렬이라고 가정하고 생성 된 모델에서 해석을 제공하는 이유가 여기에 있습니다. 이 버그는 다음 릴리스에서 해결할 것입니다. 한편 ,이 버그를 방지하기 위해 다음 방법 중 하나를 사용할 수 있습니다

• 배열 이론을 포함하는 로직을 지정합니다. 예 : (set-logic QF_AUFLIA)을 예제 앞에 추가하십시오.

• 자동 구성을 사용하지 않도록 설정하십시오 (사용 가능한 모든 이론을 설치합니다). 명령 (set-option :auto-config false)을 추가하십시오.