mirror of
https://github.com/Z3Prover/z3
synced 2025-04-05 17:14:07 +00:00
add note about opt.incremental
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
ac822acb0f
commit
cd416ee9a9
|
@ -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
|
||||
==============
|
||||
|
|
Loading…
Reference in a new issue