From cd416ee9a96271f92c9f61db35ceca1385cff185 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 5 Jul 2022 08:20:46 -0700 Subject: [PATCH] add note about opt.incremental Signed-off-by: Nikolaj Bjorner --- RELEASE_NOTES.md | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md index 19ac57ecb..6cec47b5a 100644 --- a/RELEASE_NOTES.md +++ b/RELEASE_NOTES.md @@ -35,7 +35,12 @@ Version 4.9.0 totalizer encoding or built-in cardinality constraints. The default engine is still maxres, so you have to set opt.maxsat_engine=rc2 to enable the rc2 option at this point. The engines maxres-bin and rc2bin are experimental should not be used - (they are inferior to default options). + (they are inferior to default options). +- Incremental constraints during optimization set option opt.incremental = true + - The interface `Z3_optimize_register_model_eh` allows to monitor incremental results during optimization. + It is now possible to also add constraints to the optimization context during search. + You have to set the option opt.incremental=true to be able to add constraints. The option + disables some pre-processing functionality that removes variables from the constraints. Version 4.8.17 ==============