timeout - Z3 JAVA-API 用于求解器超时

Question

如何为 Z3 JAVA API 设置求解器的超时时间？

再次回到这个问题：

这是我的代码：

    Context ctx = getZ3Context();
    solver = ctx.MkSolver();
    Params p = ctx.MkParams();
    p.Add("timeout", 1);
    solver.setParameters(p);

不起作用，求解器只是永远运行查询。对此有任何想法吗？

Answer 1

我没有使用过 Java API，但是从查看官方Java 示例和此代码段中，我假设以下内容应该可以工作：

Solver s = ctx.MkSolver();
Params p = ctx.MkParams();
p.Add("timeout", valueInMilliseconds); /* "SOFT_TIMEOUT" or ":timeout"? */
s.setParameters(p);

Answer 2

好的，终于自己找到了解决办法：

Context ctx = getZ3Context();
solver = ctx.MkSolver();
Params p = ctx.MkParams();
/* Also tried
 * p.Add("timeout", 1),
 * p.Add(":timeout", 1), 
 * neither worked.
 */
p.Add("soft_timeout", 1);
solver.setParameters(p);