Z3: timeout for optimize in C++

2019-07-22 07:29发布

问题:

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!

回答1:

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.