Closed BenSpencer closed 9 years ago
To check: will we have any solver support for this?
There is no direct solver support for either case-insensitive-comparisons or tolowercase/touppercase functions, although they are in-principle interested in this.
Their suggested workaround: Create a char_tolower method with a big if/then/else chain which maps 'A' to 'a', 'B' to 'b', etc. and then use this to define a case-insensitive-eq by checking each character in the two strings with char_tolower. This could also be used to define a string_tolower function.
Fixed in 84e8d375, with real-world tests in c5540105 (jquery-on-demo) and 2a6a0b90 (prototype-on-tutorial).
We have some constraint rewriting to generate constraints which use a "relational" str_tolower_bounded(input, output)
predicate, with output
being a new temporary variable which is used in the remainder of the constraints. str_tolower_bounded
is defined as described above to check for matching length and that the first 5 characters of input
converted to lowercase are the first 5 characters of output
.
See test
target-id-toLowerCase-check
in a35b8551.Also include any other sensible-seeming properties, most obviously `toUpperCase()'.