非常感谢乔希和莱昂纳多回答上一个问题.
我还有几个问题.
<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做量词消除是一个好主意吗？或者它通常在不进行量词消除的情况下更智能地找到模型？
谢谢.
我想使用Z3 C API解决包含量词的约束.我正在努力使用像"Z3_mk_exists()"这样的函数,因为我没有找到任何在线或tar文件中的测试示例中的示例.我并不完全理解这些函数所需的所有参数以及它们的确切含义.有人可以帮忙吗？
谢谢.Kaustubh.
我在Linux上使用Z3 4.1 C-API。我想为求解器指定一个超时。
我正在使用以下命令，但是在命令Z3_solver_set_params（）中出现分段错误。
Z3_context ctx = mk_context();
Z3_solver s = Z3_mk_solver(ctx);
Z3_params params = Z3_mk_params(ctx);
Z3_symbol r = Z3_mk_string_symbol(ctx, ":timeout");
Z3_params_set_uint(ctx, params, r, static_cast<unsigned>(10));
Z3_solver_set_params(ctx, s, params);
看来我没有正确使用API。
我在包含示例的test_capi.c文件中找不到用于C-API设置求解器超时的任何示例。有人可以帮忙吗？
z3 ×3