z3 - Z3 C API 在运行时更改超时

Question

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

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

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

Answer 1

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

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;