This release introduces the following features:
- F# Quotation utilities. The release contains a new directory 'utils'. It contains utilities built on top of Z3. The main one is support for translating F# quoted expressions into Z3 formulas.
- QUANT_ARITH configuration. Complete quantifier-elimination simplification for linear real and linear integer arithmetic. QUANT_ARITH=1 uses Ferrante/Rackhoff for reals and Cooper's method for integers. QUANT_ARITH=2 uses Fourier-Motzkin for reals and the Omega test for integers.
It fixes the following bugs:
- Incorrect simplification of map over store in the extendted array theory. Reported by Catalin Hritcu.
- Incomplete handling of equality propagation with constant arrays. Reported by Catalin Hritcu.
- Crash in bit-vector theory.
- Incorrectness in proof reconstruction for quantifier manipulation.
Thanks to Catalin Hritcu, Nikolai Tillmann and Sascha Boehme.
This release fixes minor bugs. It introduces some additional features in the SMT-LIB front-end to make it easier to parse new operators in the theory of arrays. These are described in
SMT-LIB Extensions.
This is a bug fix release. Many thanks to Robert Brummayer, Carine Pascal, François Remy, Rajesh K Karmani, Roberto Lublinerman and numerous others for their feedback and bug reports.
- Parallel Z3. Thanks to Christoph Wintersteiger there is a binary supporting running multiple instances of Z3 from different threads, but more interestingly, also making use of multiple cores for a single formula.
- Check Assumptions. The binary API exposes a new call Z3_check_assumptions, which allows passing in additional assumptions while checking for consistency of the already asserted formulas. The API function returns a subset of the assumptions that were used in an unsatisfiable core. It also returns an optional proof object.
- Proof Objects. The Z3_check_assumptions retuns a proof object if the configuration flag PROOF_MODE is set to 1 or 2.
- Partial support for non-linear arithmetic. The support uses support for computing Groebner bases. It allows solving some, but far from all, formulas using polynomials over the reals. Uses should be aware that the support for non-linear arithmetic (over the reals) is not complete in Z3.
- Recursive data-types. The theory of well-founded recursive data-types is supported over the binary APIs. It supports ground satisfiability checking for tuples, enumeration types (scalars), lists and mututally recursive data-types.
- The names of the basic objects exposed by Z3 have been renamed from
type to sort. - The managed API uses the type-safe context by default. Using the type-safe context, every term, sort and function declaration is managed in a .NET object. The non-type safe version (RawContext) uses integer pointers for these different types.
- When using the CheckAssumptions Z3_check_assumptions feature you will need to explicitly push/pop a context around the calls to undo the additional assumptions that are passed in.
To Wolfgang Grieskamp, Sascha Boehme, Yannick Moy, Christoph Wintersteiger, Yeting Ge, Ruzica Piskac, Grant Passmore, Aditya Nori, and numerous others for trying out preliminary versions of Z3 2.0.
An Efficient SMT Solver