Равные списки являются перестановками друг друга. Почему Z3 отвечает «неизвестно»?

Question

Я пытаюсь проверить алгоритм сортировки и решил отобразить списки из языка программирования в виде кортежей (размер как Int, содержимое как Array Int -> Obj) и назвал их MyList.

Потом я наткнулся на следующую проблему:

l0 и l1 такие MyLists.

На вопрос (assert (not (permutation l0 l0))), Z3 отвечает unsat быстро.

На вопрос (assert (not (permutation l1 l1))), Z3 отвечает unsat быстро.

Но когда я прошу

(assert (= l1 l0)) 
(assert (not (permutation l1 l0))) 

Он отвечает unknown через несколько секунд. Как это может быть? Этот вопрос намного сложнее? Массивы AFAIK являются экстенсиональными в Z3, поэтому приравнивание двух списков должно привести к отказу от рефлексивного случая, не так ли?

Вот полный код (SMT-Lib2):

(set-option :produce-unsat-cores true) 
(set-option :produce-models true) 

; --------------- Basic Definitions ------------------- 

(declare-sort Obj 0) 

; --------------- Predicates ------------------------------- 

(declare-datatypes() ((MyList (mk-pair (size Int) (contents (Array Int Obj)))))) 

(define-fun size_list ((l MyList) (size Int)) Bool 
         (and 
         (<= 0 size) 
         (= (size l) size) 
        ) 
) 

(define-fun select_list ((l MyList) (index Int) (result Obj)) Bool 
         (and 
          (exists ((sl Int)) 
          (and 
           (size_list l sl) 
           (>= index 0) 
           (< index sl) 
          ) 
         ) 
          (= (select (contents l) index) result) 
         ) 
) 

(define-fun in_list ((o Obj) (l MyList)) Bool 
        (exists ((i Int)) (select_list l i o))) 


(define-fun permutation ((l1 MyList) (l2 MyList)) Bool 
         (forall ((o Obj)) (= (in_list o l1) (in_list o l2)))) 

(declare-const l0 MyList) 
(declare-const l1 MyList) 

;(assert (not (permutation l0 l0))) ; unsat 
;(assert (not (permutation l1 l1))) ; unsat 

(assert (= l1 l0)) 
(assert (not (permutation l1 l0))) ; unknown 

; --------------- Verify ------------------- 
(check-sat) 

также: Как вы поступаете, когда решатель отвечает unknown? Модели и Unsat-сердечники недоступны в этом случае ...

Заранее спасибо.

Answer 1

Да, это ограничение того, как квантификаторы обрабатываются во время предварительной обработки, а Z3 не может получить простую конгруэнтность.

Возможно, вам удастся воспользоваться новой поддержкой последовательностей. Тогда эта проблема, и, возможно, связанные с теми, стало намного проще:

(set-option :produce-unsat-cores true) 
(set-option :produce-models true) 

; --------------- Basic Definitions ------------------- 

(declare-sort Obj 0) 

; --------------- Predicates ------------------------------- 

(define-sort MyList() (Seq Obj)) 

(define-fun in_list ((o Obj) (l MyList)) Bool (seq.contains l (seq.unit o))) 


(define-fun permutation ((l1 MyList) (l2 MyList)) Bool 
        (forall ((o Obj)) (= (in_list o l1) (in_list o l2)))) 

(declare-const l0 MyList) 
(declare-const l1 MyList) 

;(assert (not (permutation l0 l0))) ; unsat 
;(assert (not (permutation l1 l1))) ; unsat 

(assert (= l1 l0)) 
(assert (not (permutation l1 l0))) ; unknown 

; --------------- Verify ------------------- 
(check-sat) 

См http://rise4fun.com/z3/tutorial/sequences для более подробной информации.