等于列表是彼此的排列。为什么Z3的回答是“未知”？ [英] Equal lists are permutations of one another. Why does Z3 answer 'unknown'?

问题描述

我想验证一个排序算法，并决定将名单从编程语言（大小如int，内容阵列诠释 - > OBJ）的元组模型，并叫他们MYLIST

I am trying to verify a sorting algorithm and decided to model lists from the programming language as tuples of (size as Int, contents as Array Int -> Obj) and called them MyList.

然后我就翻过了以下问题：

Then I came accross the following problem:

10和L1是这样MyLists

l0 and l1 are such MyLists.

当问（断言（不（置换10 10））），Z3的答案不饱和度快。

当问（断言（不（置换L1 L1））），Z3的答案不饱和度快。

但是，当我问

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

它回答未知几秒钟​​后。怎么可能？这是查询更加困难？ AFAIK数组是伸展在Z3，所以等同的两个名单应该让归结为反身的情况下，shoudn't呢？

It answers unknown after a few seconds. How can that be? Is this query that much more difficult? AFAIK Arrays are extensional in Z3, so equating the two lists should make it boil down to the reflexive case, shoudn't it?

下面是完整的code（SMT-LIB2）：

Here is the full code (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)

另外：你如何进行时，求解答案未知？模型和不满意的巴氏-内核不可在这种情况下...

Also: How do you proceed when the solver answers unknown? Models and Unsat-cores are not available in this case...

先谢谢了。

推荐答案

是的，这是量词是如何被pre-处理过程中处理的限制和Z3是无法检索简单的一致性。

Yes, this is a limitation of how quantifiers get handled during pre-processing and Z3 is unable to retrieve the simple congruence.

也许你可以从序列新的支持中获益。那么这个问题，并且可能与那些，变得容易多了：

Maybe you could benefit from the new support for sequences. Then this problem, and probably related ones, become much easier:

(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 了解更多详情。

See http://rise4fun.com/z3/tutorial/sequences for more details.

这篇关于等于列表是彼此的排列。为什么Z3的回答是“未知”？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！