забава в Z3, возвращающая более одного элемента

Насколько я понимаю, я могу объявить функцию, которая возвращает более одного элемента. скажем, у меня есть функция x, которая получает сортировку T и возвращает сортировку U и сортировку R.

(объявление-сортировка T) (объявление-сортировка R) (объявление-сортировка U)

(заявить-весело х (Т) (У Р))

как я могу тогда получить доступ при вызове функции x к возвращаемым элементам... скажем, мне нужно подтвердить передачу U одной функции и R другой... можно ли это сделать?


z3 z3py theorem-proving
person user3723800    schedule 10.06.2014    source источник

Ответы (1)


arrow_upward
2
arrow_downward

Ваш пример не является правильно сформированным SMT-LIB2. Не разбирает. (ошибка "строка 3, столбец 23: неверное количество параметров для конструктора сортировки") http://www.smtlib.org подробно описывает синтаксис и семантику SMT-LIB2.

person Nikolaj Bjorner    schedule 10.06.2014
comment
Спасибо Николай!! Я знаю, что это неправильно, я прошу прощения за то, что я должен упомянуть, что это просто псевдокод для попытки объяснить, что я хочу сделать. Я пытаюсь сказать, что если есть функция x, которая получает T и возвращает (UR), есть какой-либо способ поймать результат вызова x (он же (UR)) и затем использовать их по отдельности, сделал ли я свою точку зрения ?? - person user3723800; 10.06.2014
comment
Вы можете определить тип данных, который содержит несколько объектов, например, в соответствии с определением Pair в Руководстве Z3 по типам данных (rise4fun.com/z3/tutorial/guide) - person Christoph Wintersteiger; 10.06.2014