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

Question

Я пытаюсь определить теорию множеств (объединение, пересечение и т. Д.) для 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,...} (вот почему я пытаюсь получить эту функциональность с помощью квантификаторов.) Верно ли это? Или есть другой маршрут?

Спасибо!

Ranjit.

Answer 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) оператор карты. This paper описывает расширенную теорию массивов и как ее кодировать с помощью этого набора операций, таких как объединение и пересечение. На сайте rise4fun есть примеры. Это хорошая альтернатива, если это единственные кванторы в вашей проблеме, потому что проблема теперь в разрешимом фрагменте. С другой стороны, если у вас есть дополнительные количественные формулы, содержащие множества, то это, вероятно, будет работать плохо. Проблема в том, что модель, построенная по теории массивов, не знает о существовании дополнительных кванторов.

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

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