python Z3如何使用if而不使用else

Question

我试着用z3做一些简单的数学运算，条件是如果没有其他。

for (i = 0; i <= 15; ++i)
{
if (s1[i] > 64 && s1[i] <= 90)
s1[i] = (s1[i] - 51) % 26 + 65;
if (s1[i] > 96 && s1[i] <= 122)
s1[i] = (s1[i] - 79) % 26 + 97;
}
for (i = 0; i <= 15; ++i)
{
result = key[i];
if (s1[i] != result)
return result;
}

from z3 import *
key = list(b"Qsw3sj_lz4_Ujw@l")
s1 = [BitVec('s1_%d' % i, 8) for i in range(len(key))]
s = Solver()
for i, n in enumerate(key):
con1 = If(Or(64 < s1[i], s1[i] <= 90), (s1[i] - 51) % 26 + 65 == key[i])
con2 = If(Or(96 < s1[i], s1[i] <= 122), (s1[i] - 79) % 26 + 97 == key[i])
s.add(con1)
s.add(con2)
print(s.check())
print(s.model())

出现错误。TypeError: If() missing 1 required positional argument: 'c'

Answer 1

If接受三个参数；(1( 条件、(2(then结果和(3(else结果。你只提供了两个。如果您不关心else的情况约束，可以替换True：

con1 = If(Or(64 < s1[i], s1[i] <= 90), (s1[i] - 51) % 26 + 65 == key[i], True)

并且类似地用于CCD_ 7。

注意，z3中没有else的If。虽然这将修复您的"；语法"；错误，它不会修复你在模型中犯的错误；如果有的话。(如前所述，你的条件是unsat，我认为这不是你所期望的。(你应该真正考虑当条件为假时，程序是如何改变(或不改变(的，而不是像这样的约束，你应该在将变量放入SSA(单静态赋值形式(后，对变量本身的变化进行建模