title: extracting decimal value from a character in a Z3 string
body: <p>Let s1 be an arbitrary string in Z3Str.
  I can check if the third character in it is a lower case letter:</p>
  
  <pre><code>(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))
  </code></pre>
  
  <p>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:</p>
  
  <pre><code>(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))
  </code></pre>
  
  <p>But, of course, this doesn't work because of the types:</p>
  
  <pre><code>(error "line 9 column 52: Sort mismatch at argument #1 for function 
  (declare-fun - (Int Int) Int) supplied sort is String")
  </code></pre>
  
  <p>Is there any <strong>straight forward</strong> way of manipulating the decimal
  value of a character in a Z3 string? I mean other than a giant switch-case on <strong>all</strong> 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!!</p>