es.davy.ai

Preguntas y respuestas de programación confiables

¿Tienes una pregunta?

Si tienes alguna pregunta, puedes hacerla a continuación o ingresar lo que estás buscando.

  • es.davy.ai/
  • Programación /
  • ¿Cómo evalúo una expresión de cuantificación dentro de una evaluación de modelo de Z3?

¿Cómo evalúo una expresión de cuantificación dentro de una evaluación de modelo de Z3?

14 Jul, 2023 Programación

Considere lo siguiente, que crea un modelo simple donde una cadena es igual a un valor específico:

from z3 import *

s = Solver()
x = String('x')
s.add(x == StringVal('foo'))
s.check()

Luego, quiero preguntar si existe una cadena que sea igual al valor del modelo de x:

y = String('y')
expr = Exists(y, y == x)
print(s.model().evaluate(expr))

Esperaría que esto devolviera un valor booleano, pero en cambio, la salida es en sí misma una expresión:

Exists(y, y == "foo")

¿Cómo puedo hacer que esta expresión sea evaluada realmente dentro del método evaluate, en lugar de ser devuelta tal cual? Asumo que evaluate no le gusta el hecho de que introduje una nueva variable no asignada, pero seguramente poner esa variable dentro de un Exists (o en eso caso, un ForAll) es suficiente para que la expresión sea evaluada. ¿Hay alguna forma de escribir métodos de cuantificación sin introducir una nueva variable no asignada?

Tags:  ,

Answer

  1. Avatar for davy.ai
    davy.ai

    Para evaluar la expresión dentro del método evaluate, puedes utilizar el método substitute para reemplazar la variable y por su valor actual en el modelo:

    y = String('y')
expr = Exists(y, y == x)
result = s.model().evaluate(expr)
evaluated_result = simplify(expr.substitute(y, result))
print(evaluated_result)

    Esto imprimirá la cadena de texto "true", indicando que la expresión es verdadera en el modelo actual.

    En cuanto al problema de introducir nuevas variables no asignadas, puedes utilizar el método ForAll en lugar de Exists para evitar introducir variables que no estén ya en el contexto actual:

    expr = ForAll(x, x == StringVal('foo'))
print(s.check(expr)) # Devolverá "sat"

    Esto comprobará si la expresión dada es verdadera para todos los posibles valores de x y devolverá si el resultado es satisfactorio o no.

Comments are closed.