CODEWITHSUNDEEP
timeoutz3java
Betsy
Betsy

Reputation: 95

Z3 JAVA-API for solver timeout

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

Back to this question again:

Here is my code:

    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?

Upvotes: 1

Views: 868

Answers (2)

Betsy
Betsy

Reputation: 95

Okay, finally found a solution myself:

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);

Upvotes: 0

Malte Schwerhoff
Malte Schwerhoff

Reputation: 12852

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);

Upvotes: 1

Related Questions