量词消去 - 更多问题(Quantifier Elimination - More question

非常感谢Josh和莱昂纳多回答前面的问题。

我有几个问题。

<1>考虑另一个例子。

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

这具有一个简单的解决方案I> 0。（都为INT和实际案例）

然而，当我尝试以下，

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

Z3无法消除这里量词。

但是，它可以消除对一个真实的案例。（当i和k都是实数）是量词消除了整数比较困难？

<2>我使用在我的系统Z3 C API。我加入的整数部分非线性约束，在我的系统量词。 Z3目前检查可满足并给我一个正确的模型时，该系统是满足的。

我知道，量词消除后，这些限制就减少了线性约束。

我认为，Z3自动执行量词消去检查可满足之前。但是，因为，它不能做，在上述情况1，我现在想，那它通常没有找到消除量词的模型。我对么？

目前Z3可以解决在我的系统的约束。但它可能无法在复杂的系统。在这种情况下，它是一个好主意，通过一些其他的方法做量词消除不Z3和添加约束后来到Z3？

<3>我能想到在我的系统中加入实非线性约束，而不是整数非线性约束。在这种情况下，我怎么能强制使用Z3 C-API做量词消除？

<4>最后，这是一个好主意，执行Z3做量词消除？或者，它通常发现的模型更明智而不做量词消除？

谢谢。

<1>非线性整数算术的理论不承认量词消去（QE）。此外，非线性整数运算的决策问题是不可判定。

回想一下，Z3拥有量词消除非线性真正的算术公式的有限的支持。当前程序是基于虚拟术语替换。未来的版本，可能有非线性实际运算的全力支持。

<2>量词消除不默认启用。用户必须提出要求。即使未启用量词消去Z3可以找到满足的公式模型。它使用一种叫做基于模型的量词实例（MBQI）。在Z3在线教程具有描述这种技术的能力和限制的几个例子。

<3>你必须在创建Z3_context对象来启用它。可以Z3_context对象创建过程中提供了在命令行上设置的任何选项。下面是一个例子，它使模型构建和量词消除：

Z3_config cfg = Z3_mk_config();
Z3_context ctx;
Z3_set_param_value(cfg, "MODEL", "true");
Z3_set_param_value(cfg, "ELIM_QUANTIFIERS", "true");
Z3_set_param_value(cfg, "ELIM_NLARITH_QUANTIFIERS", "true");
ctx = mk_context_custom(cfg, throw_z3_error);
Z3_del_config(cfg);

在此之后， ctx指向支持模型构建和量词消去一个Z3上下文对象。

<4> MBQI模块甚至没有用于线性算术片段完成。 Z3的在线教程介绍的片段是完整的。 MBQI模块是包含未解释的功能问题的一个很好的选择。如果你的问题只用算术运算，然后量词消去通常是更好和更有效。话虽这么说，几个问题都可以用MBQI得以迅速解决。