SMT: further simplify exponentiation expressions

[d-xo]

The SMT backend currently performs some very simple preprocessing of expressions involving exponentation (see here). These could be extended to allow the SMT encoding of any exponentiation where the RHS is concrete, by either:

• fully evaluating the result of the exponentation if both the RHS & LHS are concrete
• encoding the exponentiation as a chain of multiplications if the RHS is concrete, but the LHS is symbolic

We will need to write a simple evaluator for act expressions to do this properly.