我有一个具有如下伪代码中所述逻辑的程序。 x是一个字符串，x[k]将返回索引k处的字符的十进制字符。 ^运算符返回操作数的十进制XOR结果。
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 && x[20] ^ x[10] == 100 && x[21] ^ x[22] == 200
我想找到使该程序返回true的输入。如果我想在Z3Py中解决此问题，有什么办法可以解决？我需要N个约束中的K个，使我可以将约束表达为表达式，但我对此没有支持。