mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

release notes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-06-15 14:59:33 -07:00
parent 6fc08e9c9f
commit 1debbc29c4
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
RELEASE_NOTES
View file

@ -26,12 +26,16 @@ Version 4.8.0
(known as ACCE, ABCE, CCE). Asymmetric branching also uses features introduced in Lingeling by exploiting binary implication graphs. (known as ACCE, ABCE, CCE). Asymmetric branching also uses features introduced in Lingeling by exploiting binary implication graphs.
Use sat.acce=true to enable the full repertoire of inprocessing methods. By default, clauses that are "eliminated" by acce are tagged Use sat.acce=true to enable the full repertoire of inprocessing methods. By default, clauses that are "eliminated" by acce are tagged
as lemmas (redundant) and are garbage collected if their glue level is high. as lemmas (redundant) and are garbage collected if their glue level is high.
- Substantial overhaul of the spacer horn clause engine.
- Removed features: - Removed features:
- interpolation API - interpolation API
- duality engine for constrained Horn clauses. - duality engine for constrained Horn clauses.
- pdr engine for constrained Horn clauses. The engine's functionality has been
folded into spacer as one of optional strategies.
- long deprecated API functions have been removed from z3_api.h - long deprecated API functions have been removed from z3_api.h
Version 4.7.1 Version 4.7.1
============= =============