Z3 C API Изменение времени ожидания во время выполнения

Можно ли изменить значение времени ожидания решателя во время выполнения, используя 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);

Однако предположим, что мы хотим изменить время ожидания для следующего запроса при сохранении контекста. Можно ли изменить значение времени ожидания между ними?

Ответы на вопрос(1)

Решение Вопроса

Подумайте о переходе на Z3 4.0. Z3 4.0 имеет новый API, который позволяет пользователю создавать множество решателей в одном и том же Z3_context. Вы можете установить различные таймауты для каждого решателя и обновлять их, когда захотите. Z3 4.0 также поставляется с уровнем C ++, который делает C API намного более удобным в использовании. Вот короткий пример, который устанавливает время ожидания. На моей машине Z3 вернетсяunknown когда используется таймаут в 1 миллисекунду, иsat когда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;

Ваш ответ на вопрос