Frontend.downsize()

[yaroslavyaroslav]

Question

What's the purpose of this method if any? I see that it actually doesn't implemented here:

def downsize(self): #pylint:disable=no-self-use
        pass

i'm just digging in an app that uses your lib and this method specifically, so it would be very helpful to me to get what's its intention and where it's implementation, to get what original z3 API it wraps.

[rhelmot]

Frontends are implemented with a mixin pattern, meaning their behavior is split up over many classes which are combined into one class via multiple inheritance. You're looking at the frontend base class, but there are many more derived classes which add behavior. In particular, FullFrontend has an implementation which clears its internal caches, allowing the z3 solver (the backend) to be garbage collected. This is the intended behavior of downsize - to clear caches to reduce memory footprint.

[yaroslavyaroslav]

Thanks, @rhelmot can I say, that this is rather the python specific methods, not z3 one?

[rhelmot]

Indeed - there is no corresponding z3 api call. The equivalent if you're rewriting this in raw z3 would be to delete your solver instance.

[yaroslavyaroslav]

Thanks a lot, this really helped me out!