Clarify overloading

[barrettcw]

From Levent Erkok, June 22, 2023:

z3 accepts the following script where <= is defined over a user-defined data-type:

(set-logic ALL)
(declare-datatype T ((a) (b)))
(define-fun <= ((x T) (y T)) Bool (= x a))

CVC5 rejects it:

(error "Parse Error: a.smt2:3.13: Symbol `<=' is shadowing a theory function symbol")

SMTLib document is a bit vague on this: It specifically says user-defined functions cannot be overloaded, but theory symbols can be. But it isn't clear if it explicitly allows them to be overloaded by user-space scripts, or is this only allowed from theory descriptions. I'm curious if this is something z3 supports and is well-defined (and hence CVC5 is not compliant), or if it just slips through the cracks in z3 and shouldn't be allowed (so a bug in z3).

In case it is allowed, what happens if I define <=, but it doesn't satisfy, say, transitivity. Is this supposed to work fine?

Cheers,

-Levent.

[barrettcw]

It is not allowed. As stated on p. 55 of the standard, "it is an error to declare or define a symbol that is already in the current signature." z3 is less strict than the standard in this case.

[barrettcw]

Thanks Clark. I believe you’re referring to the text:
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.

The way I read the second sentence above made me feel it was ambiguous: It’s clear overloading of user-defined symbols is not allowed, but not so for theory functions. At least it doesn’t explicitly seem to disallow it.

If I may suggest, perhaps make this point clear by explicitly stating that theory symbols can only be overloaded in other theories, as opposed to in user-space programs. That’d clear things up I think.

Cheers,

-Levent.

[barrettcw]

I can see why the second sentence might cause some confusion. I'll propose a fix to the team.