mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-02 21:36:09 +00:00
Code Activity

next release notes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-02-18 21:30:08 -08:00
parent 33d4d38dee
commit 9f91380b7d
1 changed files with 12 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

18
RELEASE_NOTES.md
View file

@ -1,11 +1,17 @@
RELEASE NOTES RELEASE NOTES
Version 4.next
================ Version 4.17.0
- Planned features ==============
- sat.euf - A FiniteSets theory solver
- CDCL core for SMT queries. It extends the SAT engine with theory solver plugins. FiniteSets is a theory with a sort (FiniteSet S) for base sort S.
- add global incremental pre-processing for the legacy core. Inhabitants of (FiniteSet S) are finite sets of elements over S.
The main operations are creating empty sets, singleton sets, union, intersection, set difference, ranges of integers, subset modulo a predicate.
Constraints are: membership, subset.
The size of a set is obtained using set.size.
It is possible to map a function over elements of a set using set.map.
Support for set.range, set.map is partial.
Support for set.size exists, but is without any optimization. The source code contains comments on ways to make it more efficient. File a GitHub issue if you want to contribute.s
Version 4.16.0 Version 4.16.0
============== ==============