Valores mínimos y máximos de variable entera.
Supongamos una restricción muy simple:solve(x > 0 && x < 5)
.
¿Puede Z3 (o cualquier otro solucionador de SMT, o cualquier otra técnica automática) calcular los valores mínimo y máximo de la variable (entero)?x
que satisface las restricciones dadas?
En nuestro caso, el mínimo es 1 y el máximo es 4.