python Z3 how to use if without else

Question

I try to use z3 do some easy math, condition is if without else.

........................................

  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())

Got error. TypeError: If() missing 1 required positional argument: 'c'

Answer 1

If takes three arguments; (1) condition, (2) then result, and (3) else result. You've only provided two. You can substitute True if you don't care about the else case constraint:

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

and similarly for con2.

Note that there's no such thing as an If without else in z3. While this will fix your "syntax" error, it won't fix the mistake you're making in your model; if any, of course. (As stated, your conditions are unsat, which I presume wasn't what you were expecting.) You should really consider what how the program changes (or doesn't change) when the condition is false, and instead of constraints like this, you should model how the variables themselves change after putting them into SSA (single-static assignment form.)