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

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

1 голос
/ 12 марта 2012

Предполагается использование нескольких встроенных и определенных пользователем типов 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)))))

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

1 Ответ

3 голосов
/ 12 марта 2012

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

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

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

...