Use let expression in copySlice to decrease expression size

[samalws-tob]

Description

This PR changes copySlice so that it returns an expression of the form (let ((src [value of src])) (store (store [value of dst] 0 (select src 0)) 1 (select src 1)), rather than (store (store [value of dst] 0 (select [value of src] 0)) 1 (select [value of src] 1)). This reduces the number of times src has to be written out in the SMT expression from size times to only 1 time. This can drastically reduce the size of the resulting SMT expression, especially in the case of nested CopySlices.
Fixes #487 .

Checklist

• tested locally
• added automated tests
• updated the docs
• updated the changelog

[arcz]

I think it looks good and it's a great catch. @d-xo @msooseth @zoep would you take a look too?

[zoep]

This looks good to me too! But I'd like @d-xo or @msooseth to have a look too

[ggrieco-tob]

I'm wondering what is the status of this PR?

[samalws-tob]

@ggrieco-tob PR is ready but waiting for review from @d-xo or @msooseth

[d-xo]

In general a positive review from @zoep or @arcz is imo enough to merge.

[d-xo]

I am a little confused why the common sub expression elimination pass isn't handling this during smt generation?

[zoep]

I am a little confused why the common sub expression elimination pass isn't handling this during smt generation?

The copySlice expansion happens post-CSE, which happens at the Expr level, so this repeating subterm will not be eliminated.

Regarding SMT encoding, is there any difference between local let and a top-level constant declaration (e.g., in terms of performance)?