Сортировочно-параметрические функции-обертки

Предполагая использование нескольких встроенных и определяемых пользователем сортировок Z3, например. Int, Bool, S1, S2, ..., есть ли способ написать общую функцию сортировки и распаковки, которая выполняет преобразование из сортировки A в сортировку B и обратно? Например

(declare-const a S1)
(declare-const b S2)
(declare-const c Int)

(WRAP[S1] b) ; Expression is of sort S1
(WRAP[S1] c) ; Expression is of sort S1
(WRAP[Int] (WRAP[S1] c)) ; Expression is of sort Int

В настоящее время я рассматриваю каждый случай вручную, например.

(declare-fun $boolToInt (Bool) Int)
(declare-fun $intToBool (Int) Bool)

(assert (forall ((x Int))
  (= x ($boolToInt($intToBool x)))))

(assert (forall ((x Bool))
  (= x ($intToBool($boolToInt x)))))

Такие оболочки могут быть созданы автоматически из заданного набора сортов, но я бы предпочел универсальное решение из возможных.


types wrapper parametric-polymorphism z3
person Malte Schwerhoff    schedule 12.03.2012    source источник

Ответы (1)


arrow_upward
3
arrow_downward

Вы можете использовать типы данных для кодирования «типов объединения». Вот пример:

(declare-sort S1)
(declare-sort S2)

(declare-datatypes () ((S1-S2-Int (WRAP-S1 (S1-Value S1))
                                  (WRAP-S2 (S2-Value S2))
                                  (WRAP-Int (Int-Value Int)))))

(declare-const a S1)
(declare-const b S2)
(declare-const c Int)

(simplify (WRAP-S1 a))
(simplify (= (WRAP-S1 a) (WRAP-Int 10)))
(simplify (S1-Value (WRAP-S1 a)))
(simplify (is-WRAP-S2 (WRAP-S1 a)))
(simplify (is-WRAP-S1 (WRAP-S1 a)))
(simplify (is-WRAP-Int (WRAP-Int c)))
(simplify (S1-Value (WRAP-S2 b)))

Дополнительную информацию о типах данных можно найти в руководстве по Z3. Тип данных S1-S2-Int имеет три конструктора: WRAP-S1, WRAP-S2 и WRAP-Int. Z3 автоматически генерирует предикаты распознавателя: is-WRAP-S1, is-WRAP-S2 и is-WRAP-Int. Методы доступа S1-Value, S2-Value и Int-Value используются для «деконструкции» значения S1-S2-Int. Например, для всех a, (S1-Value (WRAP-S1 a)) = a. Значение (S1-Value (WRAP-S2 b)) занижено. В этом случае Z3 рассматривает S1-Value как неинтерпретируемую функцию.

Кстати, аксиома

(assert (forall ((x Int))
  (= x ($boolToInt($intToBool x)))))

эквивалентно ложному. По сути, он пытается ввести целые числа в логические значения.

person Leonardo de Moura    schedule 12.03.2012
comment
Спасибо, Лео! Я не заметил, что аксиома $boolToInt эквивалентна false, но, к счастью, она никогда не срабатывала. Ваше решение по-прежнему требует создания типа данных union для всех соответствующих сортировок заранее, но я думаю, что нет никакого способа обойти это. - person Malte Schwerhoff; 26.03.2012