Allow empty String ranges

[daniel-raffler]

Hello,
I've noticed that there is a precondition the char override for StringFormulaManager.range:

* @return formula denoting the range regular expression over two chars.
* @see #range(StringFormula, StringFormula)
*/
default RegexFormula range(char start, char end) {
  Preconditions.checkArgument(
      start <= end,
      "Range from start '%s' (%s) to end '%s' (%s) is empty.",
      start,
      (int) start,
      end,
      (int) end);
  return range(makeString(String.valueOf(start)), makeString(String.valueOf(end)));
}

However, the JavaDoc for the (general) range method does not mention this restriction:

/**
 * @return formula denoting the range regular expression over two sequences of length 1.
 */
RegexFormula range(StringFormula start, StringFormula end);

And, according to SMTLIB, empty ranges should be fine:

; RE range
; (re.range s₁ s₂) is the set of all *singleton* strings s such that
; (str.<= s₁ s s₂) provided s₁ and s₂ are singleton. Otherwise, it 
; is the empty language.
(re.range String String RegLan)

I've tried it out with different solvers, and only CVC4 seems to cause issues when the precondition in the default method is simply removed. CVC5 and Princess still assume that the bounds are single character Strings and will throw an exception otherwise. However, they can handle the case when the lower bound is larger than the upper bound and simply return the empty language. Z3 supports both cases, and will also return the empty language when one of the bounds is not a single character String.

In this PR I removed the precondition from the default override to make sure it matches the behavior of the general method. I also added some checks to prevent crashes on CVC5 and Princess if either of the bounds is not a single character Strings, and fixed two bugs for Princess. Note that there are still some issues on CVC4, but this will be hard to fix as the solver is no longer maintained.

[kfriedberger]

It is good to match our API against the SMTLIB standard.
Looks good for me.

[kfriedberger]

lgtm.