5.0.0
JavaSMT 5.0.0
This major release brings support for the SMT solver Bitwuzla (version 0.4.0), some bugfixes,
and includes several changes in the API.
New Features and Breaking Changes:
- User propagation can be used to provide a strategy when solving satisfiability (only Z3).
- Array theory supports the creation of constant arrays, e.g., specifying a default value for all indices.
- Bitvector theory provides rotation and improved modulo/remainder operations.
- Floating-point theory has better model evaluation.
Updated Solvers:
- Bitwuzla 0.4.0
- OpenSMT 2.6.0
- Z3 4.12.5
We slowly abandon Ubuntu 18.04 as build platform and will use Ubuntu 22.04 in the future.
What's Changed (Auto-generated list of PRs)
- #352 Add model evaluation on FloatingPointFormula by @kfriedberger in #356
- #349 Add user propagator feature by @ThomasHaas in #349
- #355 Replace Z3 phantom reference map by doubly-linked list. by @ThomasHaas in #355
- #363 Add fp.rem operation to FloatingPointFormulaManager by @leventeBajczi in #363
- #364 Add new floating point literal constructor using IEEE754 bitpattern by @leventeBajczi in #364
- #365 Deprecate .modulo(), add .smod(), .rem() by @leventeBajczi in #365
- #368 Add support for const array literals by @kfriedberger in #368
- #332 Add bitwuzla by @kfriedberger in #332
- #369 Adding missing features to the Bitwuzla bindings by @daniel-raffler in #369
- #370 Add the SMT solver Bitwuzla to JavaSMT by @baierd in #370
- #342 add a debug mode by @daniel-raffler in #348
- #376 Example: Add Binoxxo-Solver as another example implementation. by @kfriedberger in #376
- #375 Add support for UNSAT core to the OpenSMT backend by @daniel-raffler in #375
- #377 Improve bitwuzla build scripts and documentation by @kfriedberger in #378
- #381 Improve interpolation behaviour by @kfriedberger in #382
New Contributors
- @ThomasHaas made their first contribution in #349
- @leventeBajczi made their first contribution in #363
Full Changelog: 4.1.1...5.0.0