параметрические функции в smtlib

Question

Я понимаю, что есть способ объявить параметрические типы данных в SMTLIB. Есть ли способ определить функцию, которая принимает такой тип? Например, в стандартном документе есть:

      ( declare - datatypes ( ( Pair 2) ) (
( par ( X Y ) ( ( pair ( first X ) ( second Y )) ))))

Теперь, как я могу объявить функцию, которая принимает параметрический Pair тип?

Answer 1

SMTLib не позволяет определять параметрические функции. Обратите внимание, что внутренние функции, такие как +, - и т. д., могут быть многосортными/параметрическими, например, они отлично работают с целыми и вещественными числами. Но пользовательские функции не могут быть отсортированы по множеству. То есть вы можете написать функцию, которая принимает , но не тот, который занимает куда а также являются переменными типа; т. е. полиморфный.

Это объясняется в разделе 4.1.5 https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf:

Проверки правильности сортировки, необходимые для команд, использующих сортировку или термины, всегда выполняются в отношении текущей сигнатуры. Объявление или определение символа, который уже есть в текущей подписи, является ошибкой. Это подразумевает, в частности, что, в отличие от теоретических функциональных символов, определяемые пользователем функциональные символы не могут быть перегружены.(29)

А позже в сноске 29 говорится:

Причина отказа от перегрузки определяемых пользователем символов заключается в упрощении их обработки решателем. Это ограничение имеет значение только для пользователей, которые хотят расширить сигнатуру теории, используемой сценарием, новым полиморфным функциональным символом, т. е. тем, чей ранг содержал бы параметрические сортировки, если бы это был символ теории. Например, пользователи, которые хотят объявить «обратную» функцию для произвольных списков, должны определить разные символы обратной функции для каждой (конкретной) сортировки списка, используемой в сценарии. Это ограничение может быть снято в будущих версиях.

TLDR; Нет, вы не можете определять параметрические функции в SMTLib. Но это может измениться в будущем, когда логика станет богаче. Текущий обходной путь — это процесс «мономорфизации», т. е. создание новой версии функции для каждого конкретного типа, который вы используете. Это можно сделать вручную или автоматизировать с помощью инструмента более высокого уровня, который генерирует для вас SMTLib.