bottleneck on `Mappings.encode_expr`

[redianthus]

It is taking 16% of the whole execution time on Test-Comp.

We discussed this a little bit with @filipeom and there are various fixes:

1. Add a cache to avoid recomputing the representation all the time.
2. Maybe we could make this cache weak to avoid using too much space (that is, when an expression is not used anymore, the entry in the cache should be garbage collected). I'm afraid this is not going to play well with multi-core so maybe we should try this only after trying 1.
3. Attach the solver representation directly to expression, this is annoying because it requires changing the type of expressions but I'm also afraid it will not work well with smtzilla...

[redianthus]

As an additional data point, the time is mostly spent in: (Z3_)Mappings.{cvtop,make_symbol,distinct,extract,ite,logand,logor,of_z,zero_extend,mk_int_expr}.

We could maybe also try to improve those directly when possible with micro-optimizations.

[filipeom]

As an additional data point, the time is mostly spent in: (Z3_)Mappings.{cvtop,make_symbol,distinct,extract,ite,logand,logor,of_z,zero_extend,mk_int_expr}.

We could maybe also try to improve those directly when possible with micro-optimizations.

Yeah, but maybe these are also most of the expressions that probably end up in the solver. So it may be biased towards them. But we should indeed try to optimize these as much as possible.

[redianthus]

Yes, I think it depends a lot on the compiler used and what kind of Wasm instructions it generates. It would be interesting to test with other languages to see if the compiler produces really different code, for instance with Go we could end-up with something quite different.