Z3 найти правильную перестановку

Question

Я пытаюсь заставить Z3 найти все возможные перестановки последовательности фиксированного размера, которые удовлетворяют некоторым ограничениям.Однако, я столкнулся с ошибкой тайм-аута с кодом, который я разработал до сих пор:

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

; --------------- Basic Definitions -------------------
(declare-datatypes () ((Obj A B C)))

; --------------- 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))))


; Two difference permutations of the same list
(declare-const l0 MyList)
(declare-const l1 MyList)

(assert (= 2 (seq.len l0)))
(assert (= 2 (seq.len l1)))
(assert (not (= l1 l0)))
(assert (permutation l0 l1))

; --------------- Verify -------------------
(check-sat)
(get-model)

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

Answer 1

Вы сталкиваетесь с ограничениями возможностей Z3 при наличии квантификаторов.

Возможно, вы захотите взглянуть на этот вопрос: Определение теории множеств с помощью Z3 / SMT-LIB2

В этом случае вопрос касается общих операций над множествами, но я думаю, что вы найдете ответы и на ваш случай.(Короче говоря, отключите MBQI и посмотрите, можете ли вы использовать функции вместо последовательностей.)