Can theory symbols be overloaded by user scripts?

[LeventErkok]

z3 accepts the following script:

(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. I'm curious if this is something z3 supports and is well-defined, or if it just slips through the cracks and shouldn't be allowed.

In other words, is it safe to overload theory-symbols in z3? Does it work as one would expect? For instance, the definition of <= may not be transitive for the data-type I define it for. Is this going to cause trouble internally?

[LeventErkok]

I've posted a query on the SMTLib mailing list, and Clark confirmed that overloading of theory-symbols in user-space programs isn't allowed. See: https://groups.google.com/g/smt-lib/c/1qGiNqodg4g

I'm still curious if z3 is being lenient on purpose here, and if this is expected to work fine. As a side point, perhaps it should be caught and flagged by smtlib2_compliant=true parameter; currently z3 doesn't complain about it even with this setting.

[LeventErkok]

Turned it into an issue: #6789