Muito obrigado Josh e Leonardo por responderem à pergunta anterior.

Eu tenho mais algumas perguntas.

<1> Considere outro exemplo.

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

Isto tem uma solução simples i> 0. (tanto para o caso Int quanto para o Real)

No entanto, quando tentei 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 Não foi possível eliminar o quantificador aqui.

No entanto, poderia eliminar um caso real. (quando i e k são ambos reais) A eliminação do quantificador é mais difícil para números inteiros?

<2> Estou usando a API Z3 C no meu sistema. Eu estou adicionando algumas restrições não lineares em números inteiros com quantificadores no meu sistema. Atualmente, o Z3 verifica a satisfatibilidade e fornece um modelo correto quando o sistema é satisfatório.

Eu sei que após a eliminação do quantificador, essas restrições são reduzidas a restrições lineares.

Eu pensei que o z3 faz a eliminação do quantificador automaticamente antes de verificar a satisfatibilidade. Mas desde então, não poderia fazer isso no caso 1 acima, eu acho agora, que normalmente encontra um modelo sem a eliminação do quantificador. Estou correcto?

Atualmente o z3 pode resolver as restrições no meu sistema. Mas pode falhar em sistemas complexos. Nesse caso, é uma boa idéia fazer a eliminação do quantificador por algum outro método sem z3 e adicionar restrições ao z3 posteriormente?

<3> Eu posso pensar em adicionar restrições não-lineares reais em vez de restrições não-lineares inteiras no meu sistema. Nesse caso, como posso aplicar o z3 para fazer a eliminação do quantificador usando o C-API?

<4> Finalmente, é uma boa idéia aplicar o z3 para fazer a Quantifier Elimination? Ou normalmente encontra um modelo mais inteligentemente sem fazer a Quantifier Elimination?

Obrigado.