|
|
# Detección de intersección de dominios en funciones
|
|
|
|
|
|
Para habilitar la detección de intersección de dominios en funciones por partes, se debe activar la detección mediante la opción `-d`. Esta opción utiliza el resultado de satisfacibilidad otorgado por Z3 para determinar si hay intersección en los dominios.
|
|
|
|
|
|
En caso de intersección de dominios en funciones, se muestra en pantalla cuales son los dominios que se intersectan.
|
|
|
|
|
|
Si además se activa la opción de modo detallado (`-v`), se puede visualizar cual es el string pasado como entrada a Z3 para evaluar la satisfacibilidad de cada par de condiciones. Esta opción es de utilidad para desarrolladores al poder facilmente encontrar las evaluaciones realizadas por Z3 y verificar su resultado.
|
|
|
|
|
|
Estos strings brindados por el modo detallado pueden ser evaluados mediante entrada y salida estándar de Z3 rápidamente con el comando:
|
|
|
````
|
|
|
z3 -in
|
|
|
```` |
|
|
\ No newline at end of file |