Zeitüberschreitung bei Änderung der Z3 C-API zur Laufzeit
Ist es möglich, den Timeout-Wert des Solvers zur Laufzeit mithilfe der C-API zu ändern? Um das Timeout einzustellen, kann folgendes gemacht werden:
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);
Angenommen, wir möchten das Zeitlimit für die nächste Abfrage ändern, während der Kontext beibehalten wird. Ist es möglich, den Zeitlimitwert dazwischen zu ändern?