Version 4.8.9
=============
- New features
- significant improvements to regular expression solving
- expose user theory plugin. It is a leaner user theory plugin that was once available.
It allows for registering callbacks that react to when bit-vector and Boolean variables
receive fixed values.
- Bug fixes
- many
- Notes
- the new arithmetic theory is turned on by default. It _does_ introduce regressions on
several scenarios, but has its own advantages. Users can turn on the old solver by setting smt.arith.solver=2.
Depending on feedback, we may turn toggle this default setting again back to smt.arith.solver=2.
Version 4.8.8
=============
- New features
- rewritten NIA (non-linear integer arithmetic) core solver
It is enabled in selected theories as default.
The legacy arithmetic solver remains the overall default in this release
as the rewritten solver shows regressions (on mainly NRA problems).
- recursive function representation without hoisting ite expressions. Issue #2601
- model-based interpolation for quantifier-free UF, arithmetic
- Julia bindings over the C++ API, thanks to ahumenberger
- Bug fixes
- numerous, many based on extensive fuzz testing.
Thanks to 5hadowblad3, muchang, numairmansur, rainoftime, wintered
- Notes
- recursive functions are unfolded with separate increments based on unsat core
analysis of blocking literals that are separate for different recursive functions.
- the seq (string) solver has been revised in several ways and likely shows some
regressions in this release.
Version 4.8.7
=============
- New features
- setting parameter on solver over the API by
solver.smtlib2_log=<filename>
enables tracing calls into the solver as SMTLIB2 commands.
It traces, assert, push, pop, check_sat, get_consequences.
- Notes
- various bug fixes
- remove model_compress. Use model.compact
- print weights with quantifiers when weight is != 1
Version 4.8.6
=============
- Notes
- various bug fixes
- built in support for PIP, thanks to Audrey Dutcher
- VS compilation mode including misc flags for managed packages
Version 4.8.5
=============
- Notes
- various bug fixes
Version 4.8.4
=============
- Notes
- fixes bugs
- a substantial update to how the seq theory solver handles regular
expressions. Other performance improvements to the seq solver.
- Managed .NET DLLs include dotnet standard 1.4 on supported platforms.
- Windows Managed DLLs are strong signed in the released binaries.
Version 4.8.3
=============
- New features
- Native handling of recursive function definitions, thanks to Simon Cruanes
- PB rounding based option for conflict resolution when reasoning about PB constraints.
- Access to numeral constants as a double from the native API.
- Notes
- fixes several bugs discovered since the 4.8.1 release.
Version 4.8.2
=============
- Post-Release.
Version 4.8.1
=============
- Release. Bug-fix for 4.8.0
Version 4.8.0
=============
- New requirements:
- A breaking change to the API is that parsers for SMT-LIB2 formulas return a vector of
formulas as opposed to a conjunction of formulas. The vector of formulas correspond to
the set of "assert" instructions in the SMT-LIB input.
- New features
- A parallel mode is available for select theories, including QF_BV.
By setting parallel.enable=true Z3 will spawn a number of worker threads proportional to the
number of available CPU cores to apply cube and conquer solving on the goal.
- The SAT solver by default handle cardinality and PB constraints using a custom plugin
that operates directly on cardinality and PB constraints.
- A "cube" interface is exposed over the solver API.
- Model conversion is first class over the textual API, such that subgoals created from running a
solver can be passed in text files and a model for the original formula can be recreated from the result.
- This has also led to changes in how models are tracked over tactic subgoals. The API for
extracting models from apply_result have been replaced.
- An optional mode handles xor constraints using a custom xor propagator.
It is off by default and its value not demonstrated.
- The SAT solver includes new inprocessing techniques that are available during simplification.
It performs asymmetric tautology elimination by default, and one can turn on more powerful inprocessing techniques
(known as ACCE, ABCE, CCE). Asymmetric branching also uses features introduced in Lingeling by exploiting binary implication graphs.
Use sat.acce=true to enable the full repertoire of inprocessing methods. By default, clauses that are "eliminated" by acce are tagged
as lemmas (redundant) and are garbage collected if their glue level is high.
- Substantial overhaul of the spacer horn clause engine.
- Added basic features to support Lambda bindings.
- Added model compression to eliminate local function definitions in models when
inlining them does not incur substantial overhead. The old behavior, where models are left
uncompressed can be replayed by setting the top-level parameter model_compress=false.
- Integration of a new solver for linear integer arithmetic and mixed linear integer arithmetic by Lev Nachmanson.
It incorporates several improvements to QF_LIA solving based on
. using a better LP engine, which is already the foundation for QF_LRA
. including cuts based on Hermite Normal Form (thanks to approaches described
in "cuts from proofs" and "cutting the mix").
. extracting integer solutions from LP solutions by tightening bounds selectively.
We use a generalization of Bromberger and Weidenbach that allows avoiding selected
bounds tightenings (https://easychair.org/publications/paper/qGfG).
It solves significantly more problems in the QF_LIA category and may at this point also
be the best solver for your problem as well.
The new solver is enabled only for select SMT-LIB logics. These include QF_LIA, QF_IDL, and QF_UFLIA.
Other theories (still) use the legacy solver for arithmetic. You can enable the new solver by setting
the parameter smt.arith.solver=6 to give it a spin.
- Removed features:
- interpolation API
- duality engine for constrained Horn clauses.
- pdr engine for constrained Horn clauses. The engine's functionality has been
folded into spacer as one of optional strategies.
- long deprecated API functions have been removed from z3_api.h
Version 4.7.1
=============
- New requirements:
- uses stdbool and stdint as part of z3.
- New features:
- none
- Removed features:
- none
- Notes:
This is a minor release prior to a set of planned major updates.
It uses minor version 7 to indicate that the use of stdbool and
stdint are breaking changes to consumers of the C-based API.
Version 4.6.0
=============
- New requirements:
- C++11 capable compiler to build Z3.
- C++ API now requires C++11 or newer.
- New features (including):
- A new string solver from University of Waterloo
- A new linear real arithmetic solver
- Changed behavior for optimization commands from the SMT2 command-line interface.
Objective values are no longer printed by default. They can be retrieved by
issuing the command (get-objectives). Pareto front objectives are accessed by
issuing multiple (check-sat) calls until it returns unsat.
- Removed features:
- Removed support for SMT-LIB 1.x
b003ba9f29