Python Z3 cómo utilizar if sin else. La instrucción “if” en Python Z3 se utiliza para ejecutar un bloque de código si una condición se evalúa como verdadera. Si se desea utilizar solo “if” sin “else”, se puede realizar de la siguiente manera: “` from z3 import * x = Int(‘x’) y = Int(‘y’) s = Solver() s.add(x > 0) r = If(x > 10, y, 0) print(r) “` En el ejemplo anterior, se crea un “Solver” en Z3 y se agrega una restricción donde se especifica que “x” debe ser mayor que 0. Luego, se utiliza la instrucción “If” para evaluar si “x” es mayor que 10. Si esta condición se cumple, se asigna el valor de “y” a la variable “r”; de lo contrario, se le asigna el valor 0. Finalmente, se imprime el resultado. Espero que esta información sea de ayuda.

Answer

1. 

   davy.ai

   July 15, 2023 at 9:50 pm

   El error se produce porque la función If en z3py requiere tres argumentos, el primero es la condición, el segundo es el valor verdadero y el tercero es el valor falso. En el código dado, falta el tercer argumento.

   Aquí está el código corregido con una condición agregada usando And para verificar si s1[i] está dentro del rango ASCII:

   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(And(64 < s1[i], s1[i] <= 90), (s1[i] - 51) % 26 + 65, s1[i]) == key[i]
       con2 = If(And(96 < s1[i], s1[i] <= 122), (s1[i] - 79) % 26 + 97, s1[i]) == key[i]
       s.add(con1)
       s.add(con2)
   
   print(s.check())
   print(s.model())
   

   Este código debe mostrar el resultado del solucionador SMT, que indicará si las restricciones son satisfactorias o no. Si las restricciones son satisfactorias, también proporcionará un modelo que será una posible solución al problema.

Comments are closed.