Draft: Prepare Release 6.0.0

[baierd]

To prepare the release of 6.0.0 we should discuss all changes that we included and want to include, as well as update our README and info material to reflect the current state of JavaSMT.

TODO:

• [ ] All breaking changes that we plan to do should be included in this PR. For example #491.
• [ ] We need to discuss which changes currently under development are supposed to be finished for this release.
• [ ] We need to update our info material to reflect the current version of JavaSMT. We should be clear about future developments (e.g. we want to update to Java 17 soon and 21 next year), as well as the current requirements and dependencies (i.e. what is needed to run or build our solvers).
• [ ] We need to write a thorough release message with the many changes that piled up, as well as our plans for the future regarding Java versions etc.

[kfriedberger]

This issue is a good first step towards the next release. Thanks for making the steps transparent.

[baierd]

Note: Version 6 will be the last mayor release for Java 11. We will move to Java 17 soon after and aim to adopt Java 21 in 2026.

Changelog (WIP):

• Many API calls in the Model and ProverEnvironment now throw SolverException and InterruptedException, as some solvers can throw these exceptions when executing the changed operations. MathSAT5 now throws a SolverException in cases in which model generation fails when requesting a model, instead of the previous IllegalArgumentException. Warning: Model.iterator() may throw the checked exceptions SolverException and InterruptedException although these exceptions are not declared with throws due to API restrictions.
• ProverEnvironment, InterpolatingProverEnvironment, and OptimizationProverEnvironment can now be created with an optional ShutdownNotifier, allowing the re-use of the creating SolverContext after the shutdown of the ProverEnvironment. This is currently supported for the following solvers: Bitwuzla, CVC4, MathSAT5, Z3, Yices2, and OpenSMT2.

[daniel-raffler]

(from https://github.com/sosy-lab/java-smt/pull/508#issuecomment-3636432860)

• Added 2 methods to FloatingPointFormulaManager to allow access to the rounding mode of floating point formulas. Use fromRoundingModeFormula to get the rounding mode of a formula, and makeRoundingMode to create new rounding mode formulas