在z3中如何获取字符串的上部？

Question

我想断言我的字符串变量的上限等于字符串值。例如

> v = z3.String('var')
> v.upper() == z3.StringVal('HELLO')

但是，我没有看到从z3的string API上升的方法。我该如何做到这一点？

我发现两个类似的问题1和2似乎很痛苦。这还是最先进的吗？

Answer 1

是的，这是最先进的。使用z3提供的字符串API没有其他方法可以做到这一点。

请注意，这对于字符串和序列都是一个问题，问题的关键在于没有API来访问某个位置的“元素”。 （在Z3中，字符串只是宽度为8的位向量序列。）

很久以前，z3提交了一个请求，要求添加此API：https://github.com/Z3Prover/z3/issues/1302

您可能希望在那里发出请求，以便他们倾向于添加支持！

（请注意，一些较高级别的API通过提供一种简单的方式来访问该位置的元素，从而隐藏了用户的复杂性。以下是它在SBV库中的完成方式：https://github.com/LeventErkok/sbv/blob/master/Data/SBV/List.hs#L135-L171。但这对于某些事情来说有很多工作要做很简单，我希望基础解算器得到支持。）