parametric functions in smtlib

Question

I understand that there is a way to declare parametric datatypes in SMTLIB. Is there a way to define a function that takes in such type? For instance the standard doc has:

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

Now how can I declare a function that takes in a parametric Pair type?

Answer 1

SMTLib does not allow for parametric function definitions. Note that internal functions, like +, - etc., can be many-sorted/parametric, they work on Integers and Reals just fine, for instance. But user-defined functions aren't allowed to be many-sorted. That is, you can write a function that takes a (Pair Int Bool), but not one that takes (Pair a b) where a and b are type-variables; i.e., polymorphic.

This is explained in Section 4.1.5 of https://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf:

Well-sortedness checks, required for commands that use sorts or terms, are always done with respect to the current signature. It is an error to declare or define a symbol that is already in the current signature. This implies in particular that, contrary to theory function symbols, user-defined function symbols cannot be overloaded.(29)

And later on in Footnote 29, it says:

The motivation for not overloading user-defined symbols is to simplify their processing by a solver. This restriction is significant only for users who want to extend the signature of the theory used by a script with a new polymorphic function symbol—i.e., one whose rank would contain parametric sorts if it was a theory symbol. For instance, users who want to declare a “reverse” function on arbitrary lists, must define a different reverse function symbol for each (concrete) list sort used in the script. This restriction might be removed in future versions.

TLDR; No you cannot define parametric functions in SMTLib. But this might change in the future as the logic gets richer. The current workaround is the process of "monomorphisation," i.e, generate a new version of the function at each concrete-type that you use. This can be done by hand, or it can be automated by a higher-level tool that generates the SMTLib for you.