한정 기호 및 배열에

Question

Z3 답변 배열을 통해 한정사를 사용하여이 코드를 부여 할 때 "알 수없는"

(declare-const ia Int) 
(declare-const ib Int) 
(declare-const la Int) 
(declare-const lb Int) 
(declare-const A (Array Int Int)) 
(declare-const a (Array Int Int)) 
(declare-const b (Array Int Int)) 

(assert 
    (exists 
     ((ia_1 Int) (ia_2 Int) (ib_1 Int) (la_0 Int) (lb_0 Int) (A_0 (Array Int Int)) (a_0 (Array Int Int)) (b_0 (Array Int Int))) 
     (and (= ia ia_2) (= ib ib_1) (= la la_0) (= lb lb_0) (= A A_0) (= a a_0) (= b b_0) (= ia_1 0) (= ib_1 0) (< ia_1 la_0) (< ib_1 lb_0) (< (select a_0 ia_1) (select b_0 ib_1)) (= ia_2 (+ ia_1 1))))) 

(assert 
    (not 
     (exists 
      ((ia_1 Int) (ib_1 Int) (la_0 Int) (lb_0 Int) (A_0 (Array Int Int)) (a_0 (Array Int Int)) (b_0 (Array Int Int))) 
      (and (= ia ia_1) (= ib ib_1) (= la la_0) (= lb lb_0) (= A A_0) (= a a_0) (= b b_0) (= ib_1 0))))) 

(check-sat) 

같은 경우 ("unsat") 정답을 얻을 수있는 방법이 있나요?

편집 : 예를 들어 제약 조건 (= ia_1 0)을 두 번째 연결에 추가하면 Z3이 "sat"로 올바르게 응답합니다.

Answer 1

여기에서 "알 수 없음"은 "올바른"대답입니다. 일반적으로 배열에 대한 한정 기호는 결정할 수 없습니다 (적어도 추가 가정하에는 아닙니다). Z3은 기본 quantifier 인스턴스화 방법이 올바른 인스턴스화 패턴을 선택하지 않기 때문에이 예제를 포기합니다. 자세한 내용은 quantifiers in the Z3 tutorial 섹션을 참조하십시오.

우리는 Z3을 돕기 위해 자체 인스턴스화 패턴을 지정할 수 있습니다. 또는 최소한 휴리스틱이 올바른 패턴을 자동으로 찾을 수 있도록 문제를 다시 설명 할 수 있습니다. 이 경우 내가 지금처럼 초 정량 다시 작성하여 성공 : 각 하위 정량에 적은 인수가

(assert 
    (forall ((la_0 Int) (lb_0 Int) (A_0 (Array Int Int))) 
      (and 
       (= A A_0) 
       (= la la_0) 
       (= lb lb_0) 
       (forall ((b_0 (Array Int Int)) (ib_1 Int)) 
        (and 
         (= b b_0) 
         (= ib ib_1) 
         (= ib_1 0) 
         (forall ((a_0 (Array Int Int)) (ia_1 Int)) 
          (not (and (= ia ia_1) (= a a_0))))      
         ))))) 

을, 기회는 뭔가 유용한 (내 생각) 픽업, 그러나 것 더 나은 과정의 의지 항상 충분하지는 않습니다.