[SMT-LIB] overloading

[cok@frontiernet.net]

Cesare et al.

This bullet on page 11 regards overloading:

Theory function symbols can now be overloaded arbitrarily, although in ambiguous
cases their occurrences within a term must be annotated with a return sort. (User-defined function symbols cannot overload any already defined symbol.)

I understood that to mean that the user cannot add definitions of theory functions, even with a different signature.

The benchmark AUFLIRA/nasa/fol_simplify/cl5_nebula_array_0001.fof.smt2 (among others)
includes as a user-definition

(declare-fun abs (Real) Real)

But the logic also includes the Reals_Ints theory, which defines 'abs' for an Int argument,
but not for a Real argument.

Can you clarify whether the benchmark is incorrect or whether the statement about user-defined overloading needs elaboration?

- David