extracting decimal value from a character in a Z3

问题:

Let s1 be an arbitrary string in Z3Str. I can check if the third character in it is a lower case letter:

(declare-const s1 String)
(assert (= s1 "74b\x00!!###$$"))
(assert (str.in.re (str.at s1 2) (re.range "a" "z")))
(check-sat)
(get-value (s1))

Now suppose it really is, and I want to replace that third letter with its upper case (the new string s2 will contain the replaced version). Inspired by standard programming languages, I might be tempted to do something like this:

(declare-const s1 String)
(declare-const s2 String)
(declare-const b1 Bool)
(assert (= s1 "74b\x00!!###$$"))
(assert (= b1 (str.in.re (str.at s1 2) (re.range "a" "z"))))
(assert (= (str.substr s2 0 2) (str.substr s1 0 2)))
(assert (= (str.substr s2 3 8) (str.substr s1 3 8)))
(assert (= (str.len s2) (str.len s1)))
(assert (= (str.at s2 2) (ite b1 (- (str.at s1 2) 32) (str.at s1 2))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 32 = 'a'-'A'
(check-sat)
(get-value (s1 s2 b1))

But, of course, this doesn't work because of the types:

(error "line 9 column 52: Sort mismatch at argument #1 for function 
(declare-fun - (Int Int) Int) supplied sort is String")

Is there any straight forward way of manipulating the decimal value of a character in a Z3 string? I mean other than a giant switch-case on all lower case letters ... There seems to be some hope, because the API does support "\x61" as an alternative representation of "a". Any help is very much appreciated, thanks!!

回答1:

The following works:

(declare-const s1 String)
(declare-const s2 String)
(declare-const b1 Bool)
(assert (= s1 "74b\x00!!###$$"))
(assert (= b1 (str.in.re (str.at s1 2) (re.range "a" "z"))))
(assert (= (str.substr s2 0 2) (str.substr s1 0 2)))
(assert (= (str.substr s2 3 8) (str.substr s1 3 8)))
(assert (= (str.len s2) (str.len s1)))

(declare-const subSecElt (_ BitVec 8))
(declare-const eltUpCase (_ BitVec 8))
(assert (= (bvsub subSecElt #x20) eltUpCase))
(assert (= (seq.unit subSecElt) (str.at s1 2)))
(assert (= (str.at s2 2) (ite b1 (seq.unit eltUpCase) (str.at s1 2))))

(check-sat)
(get-value (s1 s2 b1))

It would indeed be nice if this can be simplified further, though I don't see an easy way to do that since the API doesn't seem to allow accessing the elements directly from a sequence. It lets you get subsequences, but not elements, which is what you really need here: Note that a subsequence of length 1 is different than the underlying element at that position, which explains the rightful type-error you got.

This is the answer I get for this query:

sat
((s1 "74b\x00!!###$$")
 (s2 "74B\x00!!###$$")
 (b1 true))