Z3 字符串/字符异或? [英] Z3 String/Char xor?

问题描述

我正在 Python 中使用 Z3，并试图弄清楚如何进行字符串操作.通常，我将 z3.String 作为对象进行了尝试，执行了诸如 str1 + str2 == 'hello world' 之类的操作.但是，我一直无法完成以下行为:

I'm working with Z3 in Python and am trying to figure out how to do String operations. In general, I've played around with z3.String as the object, doing things like str1 + str2 == 'hello world'. However, I have been unable to accomplish the following behavior:

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

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

So basically add the constraint that character 1 xor character 2 equals 12. My understanding is that the string is defined as a sequence of 8-bit BitVectors under the hood, and BitVectors should be able to be xor'd.

谢谢！

推荐答案

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

So far I don't expose ways to access characters with a function. You would have to define auxiliary functions and axioms that capture extraction. The operator [] extracts a sub-sequence, which is of length 1 if the index is within bounds.

这是一种访问元素的方法:

Here is a way to access the elements:

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)

这篇关于Z3 字符串/字符异或?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！