我正在浏览Z3py,并对如何在特定情况下使用API有疑问。下面的代码是我最终希望使用Z3的简化版本。我的一些问题是: 1.有没有办法像下面的变量'a'一样创建任意长度的数组值? 2.您可以通过Z3py访问循环中的数组中的每个元素吗? 3.是否可以将结果分配回原始变量或是需要新变量?转换为CNF会自动添加一个唯一的ID吗? (即a + = b)学习Z3py - 是否支持数组和循环
总体而言,我迷失在如何将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"
我想检查我是否理解这个问题。看来你想用Z3Py来解决这个问题:给定'a'和'd',找到'b',这样你就可以打印出好的。是吗? –
是的,这就对了。 – daybreak