mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

updated release notes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-07-03 21:42:14 -07:00
parent e8e786ae64
commit e622022bf9
1 changed files with 14 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

14
RELEASE_NOTES
View file

@ -31,6 +31,20 @@ Version 4.8.0
- Added model compression to eliminate local function definitions in models when
inlining them does not incur substantial overhead. The old behavior, where models are left
uncompressed can be replayed by setting the top-level parameter model_compress=false.
- Integration of a new solver for linear integer arithmetic and mixed linear integer arithmetic by Lev Nachmanson.
It incorporates several improvements to QF_LIA solving based on
. using a better LP engine, which is already the foundation for QF_LRA
. including cuts based on Hermite Normal Form (thanks to approaches described
in "cuts from proofs" and "cutting the mix").
. extracting integer solutions from LP solutions by tightening bounds selectively.
We use a generalization of Bromberger and Weidenbach that allows avoiding selected
bounds tighthenings (https://easychair.org/publications/paper/qGfG).
It solves significantly more problems in the QF_LIA category and may at this point also
be the best solver for your problem as well.
The new solver is enabled only for select SMT-LIB logics. These include QF_LIA, QF_IDL, and QF_UFLIA.
Other theories (still) use the legacy solver for arithmetic. You can enable the new solver by setting
the parameter smt.arith.solver=6 to give it a spin.
- Removed features:
- interpolation API