用于求解器超时的 Z3 JAVA-API [英] Z3 JAVA-API for solver timeout

问题描述

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

How to set solver's timeout for Z3 JAVA API?

再次回到这个问题:

这是我的代码:

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

不起作用，求解器只是永远运行查询.对此有什么想法吗?

Not work, the solver just running the query forever. Any idea about this?

推荐答案

Java API 没用过，但是从官方看Java 示例 和 这个代码段，我认为以下几行应该可以工作:

I haven't used the Java API, but from Looking at the official Java example and at this snippet, I'd assume that something along the following lines should work:

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

这篇关于用于求解器超时的 Z3 JAVA-API的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！