Z3 字符串/字符异或？

Question

我正在使用 Python 中的 Z3 并试图弄清楚如何进行字符串操作。一般来说，我以z3.String 为对象，做str1 + str2 == 'hello world' 之类的事情。但是，我一直无法完成以下行为：

solver.add(str1[1] ^ str1[2] == 12) # -- or --
solver.add(str1[1] ^ str1[2] == str2[1])

所以基本上添加了字符 1 xor 字符 2 等于 12 的约束。我的理解是字符串被定义为引擎盖下的 8 位 BitVectors 序列，并且 BitVectors 应该能够被异或。

谢谢！

Answer 1

到目前为止，我还没有公开使用函数访问字符的方法。您必须定义捕获提取的辅助函数和公理。运算符 [] 提取一个子序列，如果索引在边界内，则该子序列的长度为 1。

这是访问元素的一种方式：

from z3 import *

nth = Function('nth', StringSort(), IntSort(), BitVecSort(8))

k = Int('k')
str1, str2, s = Strings('str1 str2 s')

s = Solver()
s.add(ForAll([str1, k], Implies(And(0 <= k, k < Length(str1)), Unit(nth(str1, k)) == str1[k])))

s.add( ((nth(str1, 1)) ^ (nth(str2, 2))) == 12)