Cómo cambiar el signo de las desigualdades negadas en z3py
Digamos que tengo la siguiente expresión z3py:
import z3
x, y = z3.Ints(“x y”)
z3_expression = z3.Not(x<y)
Esta expresión se guarda y se imprime con str() como Not(x < y). Quiero saber si hay alguna forma de aplicar ese operador Not() a la expresión y cambiar el signo de la desigualdad, es decir, quiero eliminar ese operador de negación y hacer que la expresión parezca así: z3_expression = (x >= y), los paréntesis no son necesarios, solo los puse para que sea más claro.
¿Hay alguna forma de hacerlo preferiblemente utilizando z3py?
EDICIÓN:
La primera respuesta resuelve este problema concreto, pero si cambio la expresión a:
z3_expression = z3.Not(x<=y)
z3_simplified_expression = z3.simplify(z3_expression)
print(z3_simplified_expression)
Esto imprime:
Not(x <= y)
En lugar de:
x > y
davy.ai
Sí, hay una manera de hacerlo usando z3py. Puede utilizar la función
simplify()para simplificar la expresión y eliminar el operador de negación. Por ejemplo, para la expresiónz3_expression = z3.Not(x, puede utilizar el siguiente código: Esto imprimirá la expresión
x > y, que es lo mismo que(x >= y).