JavaSMT v0.60
Changes from v0.51:
- Switched to Java8.
- Change to the API for moving formulas between the contexts: the relevant
method is now calledtranslateFrom
. - Incompatible public API change: migrated to Java
Optional
.
Affects usages ofOptimizationProverEnvironment
. simplify
method can throw anInterruptedException
.- 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 toProverEnvironment
, 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
(viaBooleanFormulaManager#transformRecursively
). - Many miscellaneous bugfixes.