Доступ к членам составных сортировок (типов данных) в SMT-LIBv2

Согласно разд. 3.9.3 из Язык и инструменты SMT-LIBv2: учебное пособие возможно чтобы объявить составную сортировку, подобную этой, в SMT-LIBv2:

(set-logic QF_UF)
(declare-sort Triple 3)
(declare-fun state () (Triple Bool Bool Bool))

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

(assert (_ state 1))
(assert (select 1 state))

Но похоже, что эти операторы работают только с векторами и массивами. Я не могу найти ни одного примера, в котором используются такие составные сортировки, и ничего не могу найти о доступе к этим элементам в учебнике или языковом стандарте. Как это делается? Или я совсем не понял, для чего эта функция?

Мое приложение: я хочу закодировать временную проблему и хочу сделать это в форме функции перехода состояния, которая преобразует старое состояние в новое состояние, поэтому я могу написать что-то вроде следующего, экспериментируя с системой:

....
(declare-fun initial_state () MyStateSort)
(declare-fun state_after_step_1 () MyStateSort)
(declare-fun state_after_step_2 () MyStateSort)
(assert (= (MyTransitionFunc initial_state) state_after_step_1)
(assert (= (MyTransitionFunc state_after_step_1) state_after_step_2)

smt model-checking cvc4
person CliffordVienna    schedule 22.12.2014    source источник

Ответы (1)


arrow_upward
0
arrow_downward

Это ответ на мой собственный вопрос. Если кто-нибудь может опубликовать пример использования определяемой пользователем сортировки с арностью > 0, я с радостью приму это как ответ.

После более внимательного прочтения стандарта SMT-LIBv2 я теперь думаю, что объявления сортировки с арностью> 0 имеют применение только в теоретических определениях (для объявления сортировок, таких как Array), а не в пользовательском коде. Пример в Учебнике Дэвида Кока, кажется, вводит в заблуждение, поскольку предполагает, что его можно использовать для объявления составных сортировок. Я не нашел никаких указаний на это где-либо еще. Это включает в себя полный тест SMT-LIB, который не содержит ни одного объявления сортировки с арностью > 0.

Вместо «составных сортировок» следует использовать неинтерпретируемые функции для создания эквивалента сложных структур данных. Пример:

(set-logic QF_UF)
(declare-sort CONTAINER_SORT 0)
(declare-fun CONTAINER_MEMBER_1 (CONTAINER_SORT) Bool)
(declare-fun CONTAINER_MEMBER_2 (CONTAINER_SORT) Bool)
(declare-fun INSTANCE_1 () CONTAINER_SORT)
(declare-fun INSTANCE_2 () CONTAINER_SORT)

Это эффективно объявит следующие 4 независимых логических выражения.

(CONTAINER_MEMBER_1 INSTANCE_1)
(CONTAINER_MEMBER_2 INSTANCE_1)

(CONTAINER_MEMBER_1 INSTANCE_2)
(CONTAINER_MEMBER_2 INSTANCE_2)
person CliffordVienna    schedule 24.12.2014
comment
Это в основном правильно. Команда declare-sort создает новые функции сортировки. Их можно применять для создания новых сортов. Однако, если сортировка не имеет связанной теории, она не интерпретируется. Итак, (Array CONTAINER_SORT CONTAINER_SORT) — это приложение функции Array к созданному пользователем постоянному символу сортировки CONTAINER_SORT. Поскольку у Array есть теория, все имеет смысл. Тройка, которую вы объявили выше, не работает, поэтому приложение генерирует новый символ сортировки с неинтерпретируемым доменом. - person Tim; 06.01.2015
comment
Что касается кодирования простых типов данных, я бы рекомендовал изучить теорию индуктивного типы данных. В smt2 cvc4 следует за расширением z3 для этого. (cvc3/4 поддерживает эту теорию на языке CVC, а также в API. Кроме того, синтаксис yices поддерживает нерекурсивные типы данных.) См. следующие примеры: rise4fun, cvc4 примеры ввода и пример API cvc4. - person Tim; 06.01.2015