小编day*_*eak的帖子

我正在浏览Z3py,并在一些特定情况下对如何使用API​​提出疑问.下面的代码是我最终想要使用Z3的简化版本.我的一些问题是:1.有没有办法创建一个任意长的值数组,如下面的变量'a'？2.你能通过Z3py在循环中访问数组的每个元素吗？3.是否可以将结果分配回原始变量或是否需要新变量？转换为CNF会自动添加唯一ID吗？(即a + = b)

总的来说,我迷失了如何将Z3py API应用于以下算法,其中解决方案依赖于'b'.任何帮助或提示都表示赞赏,谢谢.

import sys
import struct

a = "\xff\x33\x01\x88\x02\x11\x03\x55"
b = sys.stdin.read(1) #a byte of user input - value 'a' is good
c = ''
d = ''

for x in range(len(a)):
    c +=  struct.pack( 'B', int(a[x].encode('hex'), 16)^int(b.encode('hex'), 16) )

print c.encode('hex')

second = '\x23\x23'
x = 0
while x < len(c):
    d += struct.pack( 'h', int(c[x:x+1].encode('hex'), 16)^int(second.encode('hex'), 16) )
    x += 2

print d.encode('hex')

if d == '\xbd\x23\x43\x23\x40\x23\x41\x23':
    print "Good"
else:
    print "Bad"

我正在通过Python读取文件,并且存在为文件中的最后500个字节左右创建标识符的问题.我希望标识符对于在该块中共享相同确切字节的任何文件都是相同的,但实际字节可以是任何顺序.如果丢失或添加了一个字节,我希望标识符不同.我正在寻找人们可能拥有的任何设计或实施建议,因为速度很重要.

谢谢您的帮助.