Rewrites for substr of strings of length one (#1712)

Rewrites for substr of strings of length one (#1712)

This commit adds a rewrite for substrings of strings of length one to
the empty string if it can be shown that it is not possible that the
start position and the length are both greater than zero:

```
(str.substr "A" x y) --> "" if x = 0 |= 0 >= y
```

The commit introduces a set of functions to check such entailments
with assumptions.