Z3：超时参数无效

Question

为Z3求解器设置了超时参数，执行数千次求解后，发现超时参数无效，求解过程不会在预定时间停止。

我们使用Z3 C API来设置超时参数和其他一些参数。

timeout_param = Z3_mk_params(ctx);
Z3_params_inc_ref(ctx, timeout_param);
Z3_params_set_uint(ctx, timeout_param, Z3_mk_string_symbol(ctx, "timeout"), 20000);
                     
Z3_global_param_set("model.partial", "true");
Z3_global_param_set("smt.ematching", "true");
Z3_global_param_set("smt.mbqi.max_iterations", "10000");
Z3_global_param_set("rewriter.hi_fp_unspecified", "true");

具体来说，我们记录了每次求解的时间，发现都是严格按照参数设定的时间进行的。然而，出错的求解花费的时间比参数长了几十倍。

这可能是什么原因？

Answer 1

z3 中的超时是一个相当棘手的问题。这是一位开发人员之前说过的话：https://github.com/Z3Prover/z3/issues/5568#issuecomment-927139409

引用那里：

并非所有活动都可以安全中断。 Z3 内部轮询 是否存在取消/超时/资源过剩状态。这 轮询仅在安全的地方进行。例如，如果它执行 “推”，可以响应内部或外部动作，它 无法安全中断，因为状态不安全 可回溯的。根据高级报告，我必须假设它是 由于解算器被设置为无法进行的状态 被打断了。

因此，您的用例完全有可能属于 z3 不轮询的情况之一。

如果您减少问题并创建一个简单的重现器，您可以将其发布到 https://github.com/Z3Prover/z3/issues/ 并获得一些反馈。

如果你真的想完全停止求解，使用类似 setrlimit 的东西可能更合适。或者，您可以为求解器启动一个单独的线程，如果它在一定时间后没有返回，则从父级终止它。这完全取决于您想做什么。