получить промежуточные результаты от z3opt

Question

решение большой проблемы оптимизации с z3, что вряд ли достигнет оптимального в разумные сроки. Любой способ получить промежуточные решения? возможно, установить внутренний тайм-аут, чтобы он дал мне лучшее решение, которое он нашел до сих пор? Спасибо, Ofer

Answer 1

Вы можете прервать Z3 напрямую из API или установить таймаут. Из текстового интерфейса вы можете прервать его (CTRL^C) или установить тайм-аут. Он возвращает диапазон верхней/нижней границы и модели наилучшей привязки, найденной до сих пор.