Can theory symbols be overloaded by user scripts?

[erk...@gmail.com]

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.

[Clark Barrett]

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.

-Clark

--
You received this message because you are subscribed to the Google Groups "SMT-LIB" group.
To unsubscribe from this group and stop receiving emails from it, send an email to smt-lib+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/929d30f1-4d84-4089-8327-028f17900884n%40googlegroups.com.

[Levent Erkok]

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.

You received this message because you are subscribed to a topic in the Google Groups "SMT-LIB" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/smt-lib/1qGiNqodg4g/unsubscribe.
To unsubscribe from this group and all its topics, send an email to smt-lib+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/CAFOm5sRAVB-Ovy9ZoQmq1Uh1ajoz6_wUyeOkrdH4x-DmUdnCEQ%40mail.gmail.com.

[Clark Barrett]

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

-Clark

To view this discussion on the web visit https://groups.google.com/d/msgid/smt-lib/F5C99210-ED48-4E8A-930F-1B1F0211C09B%40gmail.com.