Overloading theory symbols in user programs

[LeventErkok]

It appears z3 allows overloading of theory symbols in user-space:

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

z3 accepts the above without complaint. Is this intentional? CVC5 rejects it:

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

I also checked with SMTLib folks and they confirmed SMTLib does not allow such overloading. (https://groups.google.com/g/smt-lib/c/1qGiNqodg4g)

• Is this intentionally supported in z3? i.e., would doing the above cause any internal issues? (For instance, the user definition of <= may not be transitive or even reflexive. Would that cause any problems?)

• Assuming support for this is intentional, I think the smtlib2_compliant=true option should check and reject this. Currently, z3 allows the above even with the smtlib2_compliant=true setting given at the command-line.

[NikolajBjorner]

z3 performs overload resolution across user and non-user functions. Producing errors for smtlib2_compliant is extra liability and only serves the purpose of a filter so there are no plans to support this.