Z3 C API 在运行时更改超时 [英] Z3 C API Changing Timeout at Runtime

问题描述

是否可以使用 C API 在运行时更改求解器的超时值?为了设置超时，可以执行以下操作 -

Is it possible to change the timeout value of the solver at runtime using C API? In order to set the timeout the following can be done -

Z3_config  cfg = Z3_mk_config();
Z3_set_param_value(cfg, "SOFT_TIMEOUT", "10000") // set timeout to 10 seconds
Z3_context ctx = Z3_mk_context(cfg);
....
Z3_check_and_get_model(ctx);
....
....
Z3_check_and_get_model(ctx);

但是，假设我们想在保留上下文的同时更改下一个查询的超时时间，是否可以更改其间的超时值?

However, suppose we want to change the timeout for next query while retaining the context, is it possible to change the timeout value in between?

推荐答案

考虑迁移到 Z3 4.0.Z3 4.0 具有新的 API，允许用户在相同的 Z3_context 中创建多个求解器.您可以为每个求解器设置不同的超时时间，并随时更新它们.Z3 4.0 还带有一个 C++ 层，使 C API 使用起来更加方便.这是一个设置超时的简短示例.在我的机器上，当使用 1 毫秒超时时，Z3 将返回 unknown，并在删除 s.set(p) 命令时返回 sat.

Consider moving to Z3 4.0. Z3 4.0 has new API that allows the user to create many solvers in the same Z3_context. You can set different timeouts for each solver, and update them whenever you want. Z3 4.0 also comes with a C++ layer that makes the C API much more convenient to use. Here is an short example that sets a timeout. On my machine, Z3 will return unknown when the 1 millisecond timeout is used, and sat when the s.set(p) command is removed.

context c;
expr x = c.real_const("x");
expr y = c.real_const("y");
solver s(c);

s.add(x >= 1);
s.add(y < x + 3);

params p(c);
p.set(":timeout", static_cast<unsigned>(1)); // in milliseconds
s.set(p);

std::cout << s.check() << std::endl;

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