Как я могу получить доступ к значениям параметризованных сортировок?
Например, если у меня есть следующие объявления:
(declare-sort Pair 2)
(declare-const x (Pair Int Int))
Как мне получить доступ к первому элементу в паре, которую представляет x?
Вы можете создать параметрическую запись с двумя селекторами first и second для доступа к ее полю.
Вот пример:
(declare-datatypes (T1 T2) ((Pair (mk-pair (first T1) (second T2)))))
(declare-const p1 (Pair Bool Int))
(declare-const p2 (Pair Int Int))
(assert (first p1))
(assert (> (first p2) 2))
(assert (= (second p1) (second p2)))
(check-sat)
(get-model)
В руководстве по Z3 SMT также есть подробное введение в алгебраические типы данных.
