Z3의 배열에 대한 제약

Question

배열과 관련하여 Z3의 작동 방식에 대한 두 가지 질문이 있습니다.

1) 모델에서 배열에는 해당 값과 함께 "else"요소가 있습니다. 수식에서 배열의 "else"요소에 대한 제약 조건을 지정하는 방법이 있습니까? 예를 들어 배열의 첫 번째 요소가 5보다 크고 다른 모든 요소가 5보다 작도록 지정할 수 있습니까? 커맨드 라인에서 Z3 통해 다음 식을 확인하면

2)

(set-logic QF_AX) 
(declare-sort Index 0) 
(declare-sort Element 0) 
(declare-fun a1() (Array Index Element)) 
(declare-fun i0() Index) 
(declare-fun i1() Index) 
(assert 
    (let 
    (
     (?v_1 (select a1 i0)) 
     (?v_2 (select a1 i1)) 
    ) 
    (
     not(= ?v_1 ?v_2) 
    ) 
) 
) 

Z3는 다음과 같은 출력을 생성한다.

sat 
(model 
    ;; universe for Index: 
    ;; Index!val!1 Index!val!0 
    ;; ----------- 
    ;; definitions for universe elements: 
    (declare-fun Index!val!1() Index) 
    (declare-fun Index!val!0() Index) 
    ;; cardinality constraint: 
    (forall ((x Index)) (or (= x Index!val!1) (= x Index!val!0))) 
    ;; ----------- 
    ;; universe for Element: 
    ;; Element!val!1 Element!val!0 
    ;; ----------- 
    ;; definitions for universe elements: 
    (declare-fun Element!val!1() Element) 
    (declare-fun Element!val!0() Element) 
    ;; cardinality constraint: 
    (forall ((x Element)) (or (= x Element!val!1) (= x Element!val!0))) 
    ;; ----------- 
    (define-fun i1() Index 
    Index!val!1) 
    (define-fun a1() (Array Index Element) 
    (_ as-array k!0)) 
    (define-fun i0() Index 
    Index!val!0) 
    (define-fun k!0 ((x!1 Index)) Element 
    (ite (= x!1 Index!val!0) Element!val!0 
    (ite (= x!1 Index!val!1) Element!val!1 
     Element!val!0))) 
) 

Z3py를 통해 동일한 수식을 검사하면 다음 모델이 생성됩니다.

[i1 = Index!val!1, 
a1 = [Index!val!0 -> Element!val!0, 
     Index!val!1 -> Element!val!1, 
     else -> Element!val!0], 
i0 = Index!val!0, 
k!0 = [Index!val!0 -> Element!val!0, 
     Index!val!1 -> Element!val!1, 
     else -> Element!val!0]] 

흥미롭게 a1k!0에 대한 참조는 Z3py에서 "역 참조", 즉이 a1FuncInterp는 개체를 의미한다. 항상 그렇습니까? 특히 프로그램이 Z3py에서 제공하는 모델을 따라 걷는 경우 모든 as_array 표현식이 기본 함수 정의로 해석된다고 가정하는 것이 안전합니까?

Answer 1

배열은 func_interp를 모델로 가지고 있기 때문에 약간 특별한 경우입니다. 파이썬 API에서 우리는 dereferenced이라는 것을 의지 할 수 있습니다.

def get_interp(self, decl): 
... 
    if decl.arity() == 0: 
     r = _to_expr_ref(Z3_model_get_const_interp(self.ctx.ref(), self.model, decl.ast), self.ctx) 
     if is_as_array(r): 
      return self.get_interp(get_as_array_func(r)) # <-- Here. 
     else: 
      return r