Блог

Я пытаюсь использовать z3, чтобы сделать простую математику, условие-если без чего-либо еще.

………………………………….

 for (i = 0; i lt;= 15;   i)  {  if (s1[i] gt; 64 amp;amp; s1[i] lt;= 90)  s1[i] = (s1[i] - 51) % 26   65;  if (s1[i] gt; 96 amp;amp; s1[i] lt;= 122)  s1[i] = (s1[i] - 79) % 26   97;  }  for (i = 0; i lt;= 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 lt; s1[i], s1[i] lt;= 90), (s1[i] - 51) % 26   65 == key[i])  con2 = If(Or(96 lt; s1[i], s1[i] lt;= 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'

If требуется три аргумента; (1) условие, (2) then результат и (3) else результат. Вы предоставили только два. Вы можете заменить True , если вас не волнует else ограничение по делу:

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

и точно так же для con2 .

Обратите внимание, что в z3 нет такого понятия, как If «без else «. Хотя это исправит вашу «синтаксическую» ошибку, это не исправит ошибку, которую вы допускаете в своей модели; если таковая имеется, конечно. (Как уже говорилось, ваши условия таковы unsat , что, я полагаю, было не то, что вы ожидали.) Вам действительно следует подумать о том, как изменяется (или не изменяется) программа, когда условие ложно, и вместо подобных ограничений вы должны смоделировать, как изменяются сами переменные после их помещения в SSA (форма одностатического назначения).