Use str.subtr in str.to.int/int.to.str reduction (#3544)

Use str.subtr in str.to.int/int.to.str reduction (#3544)

Previously, we were using UFs to encode substrings in the
`str.to.int`/`int.to.str` reductions. Our experiments have shown,
however, that using `str.substr` is more efficient instead.