Можно ли в smtlib объявить сортировку функций?

Question

Например,

      $ z3 -in
(declare-fun f (Int Real) Int)
(assert (= f f))
(check-sat)
sat

Хорошо.

Однако я бы хотел квалифицировать это as?

      $ z3 -in
(declare-fun f (Int Real) Int)
(assert (= (as f ???) (as f ???)))
(check-sat)
sat

Что я должен заполнить ????

Это должен быть сорт, но какой сорт мне использовать?

я пытался ((Int Real) Int) или (-> (Int Real) Int) или (_ (Int Real) Int), но ни один из них не является правильным.

Можно ли в smtlib объявить сортировку функций?

Если невозможно объявить функцию сортировки, как устранить неоднозначность f в следующей программе:

      $ z3 -in
(declare-fun f (Int Real) Real)
(declare-fun f (Int Bool) Real)
(assert (= f f))
(error "line 3 column 11: ambiguous constant reference, more than one constant with the same sort, use a qualified expression (as <symbol> <sort>) to disambigua
te f")

Обратите внимание: если я не использую функции, это не проблема:

      $ z3 -in
(declare-fun f () Int)
(assert (= (as f Int) (as f Int)))
(check-sat)
sat

Спасибо.

Answer 1

Аннотация

      (as f Int)

правильно, хотя (как вы заметили) очень сбивает с толку. Эта аннотация не обязательно означает «есть». Скорее, это означает Int, так что это также может быть функция.

Это действительно очень сбивает с толку, но соответствует стандарту http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf, стр. 27:

Напомним, что каждый функциональный символ f отдельно связан с одним или несколькими рангами, каждый из которых определяет типы аргументов и результатов f. Чтобы упростить проверку сортировки, функциональный символ в термине может быть аннотирован одной из сортировок результата σ. Такой аннотированный функциональный символ является квалифицированным идентификатором формы (как f σ).

Как указано выше в (as f σ), тип σявляется результатом сортировки по f.

Также обратите внимание, что поддержка этих аннотаций решателем довольно непоследовательна. Предыдущее обсуждение этого вопроса см. Https://github.com/Z3Prover/z3/issues/2135.