31 мая 2012 г., 14:47 от Raj

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

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

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

31 мая 2012 г., 16:32 от Leonardo de Moura

Подумайте о переходе на 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;

ВАШ ОТВЕТ НА ВОПРОС