Кванторы и Массивы в Z3

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») в таком случае?

Редактировать: Z3 правильно отвечает с "sat", если добавить, например, ограничение (= ia_1 0) во второе соединение.

Answer 1

Здесь «неизвестный» является «правильным» ответом. В общем, кванторы по массивам не разрешимы (по крайней мере, не при дополнительных предположениях). Z3 отказывается от этого примера, потому что эвристика эмулирования квантификатора по умолчанию не подбирает правильные шаблоны создания. Для получения дополнительной информации см. Раздел на странице 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))))      
         ))))) 

С меньшим количеством аргументов для каждого суб-квантора, скорее всего, лучше, что это будет подобрать что-то полезное (я думаю), но это будет, конечно, не всегда бывает достаточно.