Z3:在C ++中进行优化的超时 [英] Z3: timeout for optimize in C++

问题描述

我试图了解如何使用C ++ API为Z3的优化类设置超时.

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

这是我的代码:

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

但是我在opt.set(par)行上收到未知参数'timeout'"异常.是否可以为optimize类设置超时(超时后，我想获得找到的最佳解决方案)?

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

谢谢！

推荐答案

我知道这是一个老问题，但是如果有人仍在寻找答案，则需要:

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

Z3_global_param_set(超时"，超时);

Z3_global_param_set("timeout", timeout);

并且您的超时应以C字符串形式给出.

And your timeout should be given as a C string.

这篇关于Z3:在C ++中进行优化的超时的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！