1

I'm trying to understand how to set a timeout for the optimize class of Z3 using C++ API.

This i my code:

context c;
optimize opt(c);
z3::params par(c);
par.set("timeout", 1000);
opt.set(par);

But I get "unknown parameter 'timeout'" exception on the line opt.set(par). Is it possible to set the timeout for the optimize class (after the timeout, I would like to obtain the best solution found)?

Thank you!

Daniele Ferone
  • 55
  • 4
  • you mean like a sleep? or something specific to Z3 – Charlie Jul 30 '16 at 12:43
  • ["z3 minimization and timeout"](https://stackoverflow.com/questions/35203432/z3-minimization-and-timeout) is basically the same question, but using the Python API. The user there doesn't seem to have found a good solution. For the C++ API, using `set_param("smt.timeout", 1000);` works on my system for timing out during `opt.check()`, but maybe it only works while solving the hard constraints. From the other question it sounds like the optimal model will not be returned using an approach like that anyway. I deleted my partial answer so maybe the Z3 devs will see this question as unanswered. – Douglas B. Staple Aug 02 '16 at 12:09

1 Answers1

0

I know this is an old question, but if anyone's still looking for an answer, you need:

Z3_global_param_set("timeout", timeout);

And your timeout should be given as a C string.

Noran H. Azmy
  • 88
  • 8