Add patterns to MapProxy

[delcypher]

The MapProxy class only looks for non alias expressions that match the pattern <var> + <const> when handling non-aliasing expressions that are used as indices. We can generalise this to

• <expr> + <const> and <expr> - <const> (these can co-exist and do not alias). We can also the same for bitvectors provided we check that we don't allow overflowing bitvector constants (I don't think we do).
• <expr> * <const> (need to be careful when <const> == 0 as this aliases <expr>)