From af0207fce34573166edc13151081fa9c54514840 Mon Sep 17 00:00:00 2001 From: George Karpenkov Date: Fri, 10 Jun 2016 22:36:17 +0200 Subject: [PATCH] Adding CHANGELOG. --- CHANGELOG.md | 30 ++++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) create mode 100644 CHANGELOG.md diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 index 0000000000..358e32472e --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,30 @@ +# JavaSMT ChangeLog + +## JavaSMT 0.60 + + - Switched to Java8. + - Change to the API for moving formulas between the contexts: the relevant + method is now called `translateFrom`. + - Incompatible public API change: migrated to Java `Optional`. + Affects usages of `OptimizationProverEnvironment`. + - `simplify` method can throw an `InterruptedException`. + - Supported options are checked when creating a `ProverEnvironment`. + - Our custom Z3 JNI is dropped, official JNI bindings from Z3 are used instead. + `z3java` solver is dropped as well, since with the same JNI code other Java + bindings only provide an extra wrapping layer. + - Custom fork of Z3 is no longer required, using custom classloader to load + Z3 Java bindings. + - Adds `getModelAssignments` method to `ProverEnvironment`, which serializes + the model to a list of assignments. + - Switches to manual closing (try-with-resources) for `Model` objects. + - Exposes API for calculating UNSAT core over assumptions. + Assumptions feature is emulated in solvers which do not support it natively. + - More descriptive name for prover options: `GENERATE_MODELS`, + `GENERATE_UNSAT_CORE`, `GENERATE_UNSAT_CORE_OVER_ASSUMPTIONS`. + - Adds support for floating point theory in Z3. + - Adds recursive transformation visitor for boolean formulas, which does not + use recursion in its implementation + (via `BooleanFormulaManager#transformRecursively`). + - Many miscellaneous bugfixes. + +## JavaSMT 0.51