alt-ergo icon indicating copy to clipboard operation
alt-ergo copied to clipboard
verified publisher icon OCamlPro

Fix 1023

Open Halbaroth opened this issue 10 months ago • 6 comments

This PR addresses the issue #1023 about inconsistent SAT environments after optimization.

The basic idea is simple. Before optimizing the model in Satml_frontend, we push an additional assertion level. The first-order model, the boolean model and the objectives are saved before asserting any new formula during the optimization. The latest consistent models are restored after popping the assertion level.

This PR also includes a refactoring of the optimization implementation in Satml_frontend which improves the readability.

Halbaroth avatar Feb 11 '25 13:02 Halbaroth