Implementing a symbolic string capitalization method

[davidmrdavid]

This is a follow-up to #39 and the goal of this thread is to brainstorm a design to implement capitalization as a symbolic string method.

So, if we assume that we already have a symbolic version of upper implemented, we can probably implement capitalize as follows:

def capitalize(self):
    size = len(self)
    smt_str = self.var
    first_letter = z3.SubString(self.var, 0, 1) # first letter
    rest = z3.SubString(self.var, 1, end) # rest of string
    rest = SmtStr(rest) # because we want to return a SmtStr type

    # make first letter uppercase, not sure if the types align here
    upper_first_letter = self.upper(SmtStr(smt_mystr))
    return upper_first_letter + rest 

Assuming this is more-or-less correct, all it means is that we need to implement upper. To implement upper, I see two options:
(1) We could create a dictionary of the english alphabet that maps lowercase letters to their uppercase variants. A failed index to this dictionary would return the input itself (this would occur, say, if you were trying to uppercase a string representing a number)

(2) Extracting the ASCII-number out of the symbolic string and adding 32 so long as the ASCII number is between [32, and 96]. All other inputs would remain unchanged. Now I'm unsure if we can even access the numeric representation of a z3 string so maybe this is a dead end...

The first case seems easiest to me, although I'm unsure if there are performance implications to it. I would love to hear y'alls thoughs, maybe there's something I haven't thought about. If all looks good, I'll go ahead and implement upper using approach (1) and then use that as the backbone for capitalize.

Thanks again!

[pschanely]

Very exciting. I've got a few thoughts for you, but this approach is a good start. May I assume that you're interested in this work partly as a learning experience? If so, I think I should hold back and let you explore the problem a little first.

First, some related links: 1, 2, 3. (note you'll find stuff sometimes with the python API and sometimes in SMTLIB format; you can generally call .sexpr() on any Z3 value to see the corresponding SMTLIB code) Some of these links talk about the ord() capability that you're looking for; another uses a deep list of Z3 if-then-else expressions to translate each possible letter.

A few tempting things that I recommend you avoid: (1) quantifiers, that is z3.ForAll and z3.Exists - these tend to quickly drive Z3 to "unknown satisfiability" which essentially causes CrossHair to give up on the current execution iteration (2) function definitions in Z3 (if you find yourself wanting a Z3 function, try to instead create a regular python function that generates constraints for Z3 just-in-time). Having a lot of constraints is sometimes fine; much more important is the kind of constraint. Just as background, the word "logic" is used in SMT to describe kinds of constraints that are effectively solvable.

At any rate, your starting code looks good to me, and I think some of those links above will give you ideas about how to implement upper()? Feel free to reach out anytime, either here or in the chat.

[pschanely]

A minor update for folks stumbling upon this discussion: CrossHair now supports all case-changing methods, albeit slowly, even over unicode.