Muchas gracias Josh y Leonardo por responder la pregunta anterior.

Tengo algunas preguntas más.

<1> Considera otro ejemplo.

<code>(exists k) i * k > = 4 and k > 1.
</code>

Esto tiene una solución simple i> 0. (Tanto para el caso Int y Real)

Sin embargo, cuando intenté seguir,

<code>(declare-const i Int)
(assert (exists ((k Int)) (and (>= (* i k)  4) (> k 1))))
(apply (using-params qe :qe-nonlinear true))
</code>

Z3 No se pudo eliminar el cuantificador aquí.

Sin embargo, podría eliminarse por un caso real. (cuando i y k son reales) ¿Es más difícil la eliminación del cuantificador para los enteros?

<2> Estoy usando Z3 C API en mi sistema. Estoy agregando algunas restricciones no lineales en enteros con cuantificadores en mi sistema. Actualmente, Z3 comprueba si es satisfactoria y me da un modelo correcto cuando el sistema es satisfactorio.

Sé que después de la eliminación del cuantificador, estas restricciones se reducen a restricciones lineales.

Pensé que z3 hace la eliminación del cuantificador automáticamente antes de verificar la satisfacibilidad. Pero como no podía hacer eso en el caso 1 de arriba, ahora creo que generalmente encuentra un modelo sin la Eliminación de Quantifier. ¿Estoy en lo correcto?

Actualmente z3 puede resolver las restricciones en mi sistema. Pero puede fallar en sistemas complejos. En tal caso, ¿es una buena idea hacer la eliminación del cuantificador por algún otro método sin z3 y agregar restricciones a z3 más adelante?

<3> Puedo pensar en agregar restricciones no lineales reales en lugar de restricciones no lineales enteras en mi sistema. En ese caso, ¿cómo puedo hacer que z3 realice la eliminación de Quantifier utilizando C-API?

<4> Finalmente, ¿es una buena idea imponer z3 para hacer la Eliminación de Quantifier? ¿O usualmente encuentra un modelo de manera más inteligente sin hacer la Eliminación de Quantifier?

Gracias.