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 гораздо удобнее в использовании. Вот краткий пример, который устанавливает тайм-аут. На моей машине 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;