Possible optimizations

[marcoeilers]

I think there are some possibilities to add additional constraints that reduce the search space for Z3 a bit. We could list them here.

At the moment, I have exactly one idea:

• If A is a subclass of B, that usually (i.e. in other OO languages) means that nothing in the definition of B may depend on A. I don't know if we want to be quite that strict, but USUALLY, if in class B, something could have either type A or type B, we want it to have type B. I think it could be worth restricting that, especially since this is a case that may happen a lot, since all operations possible on a variable of type B are always also possible on one of type A. So there might be a lot of disjunctions, and there will usually be no good reason for the SMT solver to choose one over the other. That might lead to performance problems especially when we're doing optimization.

[adsharma]

@marcoeilers - are you still interested in pursuing this idea? Do you have a test program that's slow? What changes need to happen to typpete to restrict the search space?

[marcoeilers]

This wasn't really motivated by a specific program that's slow, it was more of an idea that we could potentially explore if we get performance problems and there's a chance it would help. I'm not interested in looking into this at the moment.

Thanks for all your contribitions though, I'll try to look through those and properly respond to the issues next week.