从 Z3 字符串中的字符中提取十进制值 [英] extracting decimal value from a character in a Z3 string

问题描述

设 s1 是 Z3Str 中的任意字符串.我可以检查其中的第三个字符是否是小写字母:

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))

现在假设它真的是，我想替换第三个字母大写(新字符串 s2 将包含替换的版本).受标准编程语言的启发，我可能会想做这样的事情:

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")

是否有任何直接操作小数的方法Z3 字符串中字符的值?我的意思是除了 所有 小写字母上的一个巨大的 switch-case ......似乎有一些希望，因为 API 确实支持\x61"作为a"的替代表示.非常感谢任何帮助，谢谢！！

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!!

推荐答案

以下作品:

(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))

如果可以进一步简化这确实很好，尽管我没有看到一种简单的方法来做到这一点，因为 API 似乎不允许直接从序列访问元素.它允许您获得子序列，但不能获得元素，而这正是您在这里真正需要的:请注意，长度为 1 的子序列与该位置的底层元素不同，这解释了您获得的正确类型错误.

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))

这篇关于从 Z3 字符串中的字符中提取十进制值的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！