pdr: improve `expr_at_step` to re-use more of the definitions that are provided by the encoding

[ekiwi]

The TransitionSystem encoding will already have a bunch of thing predefined, so we should not have to re-create the whole expression.
Also, this seems ripe for caching.

[michael-zhang-lambda]

I see that there is a function expr_in_step that has similar functionality to expr_at_step in UnrollSmtEncoding. However, this seems to not be exposed in the public TransitionSystemEncoding interface. Should we expose something like expr_in_step in the public interface?

[michael-zhang-lambda]

My plan would to probably factor out UnrollSmtEncoding and TransitionSystemEncoding into its own file (since it currently seems that both are coupled with BMC, which is not the case now). Then, we could cache stepped expressions internally in UnrollSmtEncoding to improve performance and prevent PDR or BMC implementations from having to consider this.