Z3python异或和？

Question

我目前正在尝试用 z3python 求解一些方程式，但我遇到了一个我无法处理的情况。

我需要用特定的非 ascii 字符值对某些 BitVecs 进行异或运算，然后将它们相加以检查校验和。这是一个例子：

pbInput = [BitVec("{}".format(i), 8) for i in range(KEY_LEN)]
password = "\xff\xff\xde\x8e\xae"
solver.add(Xor(pbInput[0], password[0]) + Xor(pbInput[3], password[3]) == 300)

它导致 z3 类型异常： z3.z3types.Z3Exception: Value cannot be converted into a Z3 Boolean value.

我找到 this post 并尝试将一个函数应用于我的 password 字符串，将此行添加到我的脚本中： password = Function(password, StringSort(), IntSort(), BitVecSort(8)) 但当然它会失败，因为该字符串不是 ASCII 字符串。我不关心它是一个字符串，我试着只做 Xor(pbInput[x] ^ 0xff)，但这也不起作用。我找不到关于这种特殊情况的任何文件。

编辑：这是完整的回溯。

Traceback (most recent call last):
  File "solve.py", line 18, in <module>
    (Xor(pbInput[0], password[0]) 
  File "/usr/local/lib/python2.7/dist-packages/z3/z3.py", line 1555, in Xor
    a = s.cast(a)
  File "/usr/local/lib/python2.7/dist-packages/z3/z3.py", line 1310, in cast
    _z3_assert(self.eq(val.sort()), "Value cannot be converted into a Z3 Boolean value")
  File "/usr/local/lib/python2.7/dist-packages/z3/z3.py", line 91, in _z3_assert
    raise Z3Exception(msg)
z3.z3types.Z3Exception: Value cannot be converted into a Z3 Boolean value

如果您对我如何执行此操作有任何想法，请提前致谢！

Answer 1

你的代码有两个问题。

Xor 仅适用于 Bool 值；对于位向量，只需使用 ^
在传递给xor

ord

您没有提供完整的程序（这总是有帮助的！），但您可以按照以下方式在 z3py 中将该部分编写为完整程序：

from z3 import *

solver = Solver()
KEY_LEN = 10

pbInput = [BitVec("c_{}".format(i), 8) for i in range(KEY_LEN)]
password = "\xff\xff\xde\x8e\xae"
solver.add((pbInput[0] ^ ord(password[0])) + (pbInput[3] ^ ord(password[3])) == 300)

print solver.check()
print solver.model()

这会打印：

sat
[c_3 = 0, c_0 = 97]

（我给变量起了更好的名字，以便更恰当地区分。）所以，它告诉我们解决方案是：

>>> (0xff ^ 97) + (0x8e ^ 0)
300

这确实是你要求的。

Z3python异或和？

Z3python XOR sum?

python

python-3.x

z3

z3py