1
Ich versuche zu verstehen, wie Sie ein Timeout für die Optimierung der Klasse von Z3 mit C++ API festlegen.Z3: Zeitüberschreitung für die Optimierung in C++
Der i mein Code:
context c;
optimize opt(c);
z3::params par(c);
par.set("timeout", 1000);
opt.set(par);
Aber ich bekomme "unbekannte Parameter 'timeout'" Ausnahme auf der Linie opt.set (par). Ist es möglich, das Zeitlimit für die Optimierungsklasse festzulegen (nach dem Timeout möchte ich die beste gefundene Lösung erhalten)?
Vielen Dank!
Sie meinen wie ein Schlaf? oder etwas, das spezifisch für Z3 ist – Charlie
["z3 Minimierung und Timeout"] (https://Stackoverflow.com/questions/35203432/z3-minimization-and-timeout) ist im Grunde die gleiche Frage, aber mit der Python-API. Der Benutzer scheint dort keine gute Lösung gefunden zu haben. Für die C++ API, 'set_param (" smt.timeout ", 1000);' funktioniert auf meinem System für das Zeitlimit während 'opt.check()', aber vielleicht funktioniert es nur, während die harten Einschränkungen gelöst werden. Aus der anderen Frage klingt es, als ob das optimale Modell mit einem solchen Ansatz nicht zurückgegeben wird. Ich habe meine unvollständige Antwort gelöscht, sodass die Z3-Entwickler diese Frage möglicherweise unbeantwortet sehen. –