满足Z3Py中的K/N约束
满足Z3Py中的K/N约束
提问于 2019-10-21 22:11:52
我有一个带有逻辑的程序，如下面的伪代码所述。x是一个字符串，x[k]将返回索引k处字符的十进制字符代码。^运算符返回操作数的十进制异或结果。
x = input
int checksum = x[0] ^ x[1] ^ x[2]
int sum = 0
sum += x[36] ^ x[23] == 111
sum += x[23] ^ x[29] == 101
sum += x[29] ^ x[30] == 116
sum += x[30] ^ x[9] == 115
sum += x[9] ^ x[25] == 0
return sum == checksum and x[0] ^ x[29] == 100 and x[1] ^ x[30] == 200我希望找到使此程序返回true的输入。如果我想用Z3Py解决这个问题，有没有办法呢？我需要一些K of N约束，它允许我将约束表达为表达式，但我还没有找到对此的支持。
我想用Z3做什么的伪代码：
int checksum = x[0] ^ x[1] ^ x[2]
bools = []
bools.append(Bool(x[36] ^ x[23] == 111))
bools.append(Bool(x[23] ^ x[29] == 101))
bools.append(Bool(x[29] ^ x[30] == 116))
bools.append(Bool(x[30] ^ x[9] == 115))
bools.append(Bool(x[9] ^ x[25] == 0))
state.add(bools[0])
state.add(bools[1])
state.add(bools[2])
state.add(bools[3])
state.add(bools[4])
state.add(x[0] ^ x[29] == 100)
state.add(x[1] ^ x[30] == 200)
state.add(PbEq([boolean for boolean in bools], checksum))回答 1
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/58488120
复制相关文章
相似问题
腾讯云开发者
