Доступ к элементам сортировки с несколькими полями

У меня возникли проблемы с использованием сортировки в формате SMTlib2. Например, я определяю интервал как:

(declare-sort Pair 2)
(define-sort Interval () (Pair Int Int))

Теперь, как я могу вернуть новый интервал из функции? например.:

(define-fun getInterval ((a Int) (b Int)) Interval
  (Interval a b))

Это не работает. Мой вопрос: как я могу создавать и создавать экземпляры объектов данного типа и как я могу получить доступ к их полям?

Прямо сейчас я использую 2 UF, которые я создал как геттеры полей, но я до сих пор не знаю, как иметь конструктор:

(declare-fun L (Interval) Int)
(declare-fun H (Interval) Int)

Спасибо, Нуно


z3 smt
person Nuno Lopes    schedule 21.11.2012    source источник

Ответы (1)


arrow_upward
0
arrow_downward

Вам следует изучить подраздел "Запись", раздел "Типы данных" в руководстве Z3 SMT. По сути, вы можете создать тип записи с конструктором mk-pair и двумя селекторами first и second для доступа к его полям.

Вот примерссылки наrise4fun:

(set-option :macro-finder true)

(declare-datatypes (T1 T2) ((Pair (mk-pair (first T1) (second T2)))))

(define-sort Interval () (Pair Int Int))
(define-fun getInterval ((a Int) (b Int)) Interval
  (mk-pair a b))

(declare-const p1 Interval)
(declare-const p2 Interval)

;construct objects of a give sort
(assert (= p1 (getInterval 2 2)))

;accessing their fields
(assert (= (first p1) (second p2)))

(check-sat)
(get-model)
person pad    schedule 21.11.2012
comment
Спасибо. Мне все еще интересно, в чем польза сортов, состоящих из нескольких подвидов. - person Nuno Lopes; 21.11.2012
comment
Это хороший момент. Я согласен с вами, они по сути бесполезны с точки зрения пользователя. Z3 поддерживает их, поскольку они являются частью стандарта SMT-LIB 2.0. Однако они полезны для определения семантики фоновых теорий (см.: smtlib.cs.uiowa .edu/theories/ArraysEx.smt2). Однако ваша точка зрения по-прежнему верна, поскольку конструкция par может использоваться только в определении фоновых теорий и не может использоваться пользователями SMT 2.0. - person Leonardo de Moura; 21.11.2012