Как использовать кортежи в SMT-lib?

Я совершенно уверен, что можно будет описывать кортежи с использованием синтаксиса SMT-lib, особенно для решателя Z3. Однако я не могу найти способ сделать это. Я нашел только эту страницу документации , но не понимаю, как ее использовать в z3 -in.

Мои проблемы до сих пор:

      (declare-const t (Prod Int Bool))
(error "line 1 column 19: unknown sort 'Prod'")
(declare-const t (Tuple Int Bool))
(error "line 2 column 18: unknown sort 'Tuple'")
(declare-const t (Pair Int Bool))
(error "line 3 column 18: unknown sort 'Pair'")
Источник

2 ответа

В дополнение к тому, что сказал Кристоф, прямо в документе SMTLib есть пример: http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf

В Разделе 4.2.3 вы можете найти:

      (declare-datatype Pair (par (X Y) ((pair (first X) (second Y)))))

Если ты просто хочешь IntxBool, то вы можете упростить:

      (declare-datatype PairIntBool (par () ((pair (first Int) (second Bool)))))

В общем, вы должны прочитать Раздел 4.2.3, чтобы узнать, как объявлять и использовать новые типы данных.

Источник

Ваша ссылка указывает на OCAML API, т.е. это не имеет ничего общего с SMT. Кортежи - это особый случай типов данных, для которых есть раздел в по РуководствеZ3 .

Источник
Другие вопросы по тегам