Определение теории множеств с Z3/SMT-LIB2

Я пытаюсь определить теорию множеств (объединение, пересечение и т.д.), для Z3 с использованием интерфейса SMTLIB. К сожалению, мой текущий определение зависает z3 для тривиального запроса, поэтому, я думаю, я не хватает некоторые простые опции/флаги.

здесь постоянная ссылка: http://rise4fun.com/Z3/JomY

(declare-sort Set)
(declare-fun emp () Set)
(declare-fun add (Set Int) Set)
(declare-fun cup (Set Set) Set)
(declare-fun cap (Set Set) Set)
(declare-fun dif (Set Set) Set)
(declare-fun sub (Set Set) Bool)
(declare-fun mem (Int Set) Bool)
(assert (forall ((x Int)) (not (mem x emp))))
(assert (forall ((x Int) (s1 Set) (s2 Set)) 
            (= (mem x (cup s1 s2)) (or (mem x s1) (mem x s2)))))
(assert (forall ((x Int) (s1 Set) (s2 Set)) 
            (= (mem x (cap s1 s2)) (and (mem x s1) (mem x s2)))))
(assert (forall ((x Int) (s1 Set) (s2 Set)) 
            (= (mem x (dif s1 s2)) (and (mem x s1) (not (mem x s2))))))
(assert (forall ((x Int) (s Set) (y Int)) 
            (= (mem x (add s y)) (or (mem x s) (= x y)))))

(declare-fun z3v8 () Bool)
(assert (not z3v8))
(check-sat)

Какой-нибудь намек на то, что мне не хватает?

Кроме того, из того, что я могу сказать, нет стандартного SMT-LIB2 кодирование заданных операций, например. Z3.mk_set_{add,del,empty,...} (вот почему я пытаюсь получить эту функциональность с помощью кванторов). Это верно? Или есть другой маршрут?

Спасибо!

Ранджит.

Ответы

Ответ 1

Ваша формула является выполнимой, и Z3 не способен создать модель для такого вида формулы. Обратите внимание, что он должен будет генерировать интерпретацию для неинтерпретированного сорта Set. Есть несколько альтернатив, которые вы можете рассмотреть.

1- Отключить модуль создания квантификатора (MBQI) на основе модели. BTW, все инструменты на основе Boogie (VCC, Dafny, Coral и т.д.) Делают это. Чтобы отключить модуль MBQI, мы должны использовать

(set-option :auto-config false)
(set-option :mbqi false)

Примечание: в ветке "незавершенное производство" опция :mbqi была переименована в :smt.mbqi.

Минусы: когда модуль MBQI отключен, Z3 обычно возвращает unknown для выполнимых формул, содержащих квантификатор.

2- Кодировать наборы T как массивы от T до Boolean. Z3 поддерживает теорию расширенных массивов. Расширенная теория имеет два новых оператора: ((_ const T) a) постоянные массивы, оператор отображения ((_ map f) a b). В этой статье описывается теория расширенных массивов и как ее кодировать, например, объединение и пересечение. На веб-сайте rise4fun есть примеры. Это хорошая альтернатива, если это единственные кванторы в вашей проблеме, потому что проблема теперь в разрешимом фрагменте. С другой стороны, если у вас есть дополнительные количественные формулы, содержащие множества, то это, вероятно, будет работать плохо. Проблема в том, что модель, построенная по теории массивов, не знает о существовании дополнительных кванторов.

Например, как кодировать вышеуказанные операторы, используя const и map, см. ниже: http://rise4fun.com/Z3/DWYC

3- Представляем множества T как функции от T до Bool. Этот подход обычно хорошо работает, если у нас нет наборов множеств или неинтерпретируемых функций, которые принимают множества в качестве аргументов. в онлайн-учебнике Z3 есть пример (раздел Quantifiers).