Doing a lot of repetitive z3.Store() ops

[Notselwyn]

Hi all, is there an efficient way to do bulk z3.Store() operations? For example, I may want to do 1000 store operations, but it feels really inefficient. Perhaps a z3.StoreMany(arr: z3.ArrayRef, start: ..., value: ..., len: ...) is an idea? like C's memset()

[Notselwyn]

Tips from anyone would really be appreciated, as this is currently the bottleneck of my application. This behaviour could turn my application from O(n^2) into O(n) so it would be really awesome if some sort of z3.Store mechanism with a dynamic/z3 size could be implemented

[NikolajBjorner]

You could try to use a "Lambda" construct instead of Store.

[Notselwyn]

Great, thank you so much! This looks exactly like what I need. Is it perchance possible to use nameless variables for the index? I need to dynamically generate these z3.Lambda objects, and I fear that dynamically generating unique names is a bit tricky in my algorithm

Edit: just found the "Fresh<..>" funcs, thanks again for the help! :-)

[Notselwyn]

Oh wow, this really saves a lot of performance! You're a legend for developing all this :-)