非常感谢乔希和莱昂纳多回答上一个问题.
我还有几个问题.
<1>考虑另一个例子.
(exists k) i * k > = 4 and k > 1.
这有一个简单的解决方案i> 0.(对于Int和Real案例)
但是,当我尝试跟随时,
(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.我在我的系统中使用量词在Integers上添加了一些非线性约束.Z3目前检查可满足性,并在系统满意时给我一个正确的模型.
我知道在量化消除后,这些约束会减少到线性约束.
我认为z3在检查可满足性之前会自动进行量化消除.但是,因为,我现在认为,在上面的案例1中,它通常找不到没有量词消除的模型.我对么？
目前z3可以解决我系统中的约束.但它可能在复杂系统上失败.在这种情况下,在没有z3的情况下通过其他方法进行量化消除是一个好主意,并在以后添加约束到z3？
<3>我可以考虑在我的系统中添加Real非线性约束而不是Integer非线性约束.在这种情况下,如何使用C-API强制z3进行Quantifier Elimination？
<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可以快速解决几个问题.