Expr & Sort class hierarchy #2
Conversation
We want sort-specific operator overloading, but Python operator overloading is based on classes. Thus, we create (a) class hierarchies which match the Sort hierarchy (b) functions to construct the correct class based on the sort Expr hierarchy also has elements for concrete values. This will be useful for interacting with models. Actual overloading is still a ways off...
There was a problem hiding this comment.
It looks pretty good to me, I left a few general comments. One higher-level question is about the class hierarchy: is that from the Z3 API? It makes sense, although you could also do a case split within the comparison operator. I suppose that might be less efficient.
I'm wondering when would you do the cast to the specific sort class? Will all sort objects that a user interacts with be an instance of one of the specific classes?
I'm interested in the rationale, although if this is just to best match the API, then I recognize that we don't really have a choice.
| True | ||
| >>> is_sort(Int('x')) | ||
| False | ||
| >>> is_expr(Int('x')) |
There was a problem hiding this comment.
Do you have an is_expr? Maybe remove that from the example if not.
There was a problem hiding this comment.
We don't have it yet, but we will.
My instinct is to leave this here for now; that will ensure that we're reminded of this when we enable doc-testing. Thoughts?
Yeah, this class hierarchy is from the Z3 API, so we're stuck with it. I'm not sure about the comparative efficiency of this approach v. a case-split. Perhaps Leo thought this approach would produce better error messages (e.g., a boolean expression doesn't have a "+" operation). It might make for nicer code, too. While I generally prefer the case-split (FP) approach to the sub-class (OO) approach, the latter is the strongest when you want extensibility to new kids of data, which is our situation here.
Anything given the user will be run through |
We want sort-specific operator overloading, but Python operator
overloading is based on classes. Thus, we create
(a) class hierarchies which match the Sort hierarchy
(b) functions to construct the correct class based on the sort
Expr hierarchy also has elements for concrete values.
This will be useful for interacting with models.
Actual overloading is still a ways off...