z3
Z3 is a Satisfiability Modulo Theories (SMT) solver and integrates several decision procedures: Linear real and integer arithmetic, fixed-size bit vectors, uninterpreted functions, extensional arrays, quantifiers and model generation.
- Devel package for openSUSE:Factory
-
1
derived packages
- Links to openSUSE:Factory / z3
- Download package
-
Checkout Package
osc -A https://api.opensuse.org checkout devel:tools:statica/z3 && cd $_
- Create Badge
Refresh
Refresh
Source Files
Filename | Size | Changed |
---|---|---|
_link | 0000000124 124 Bytes | |
z3-4.10.2.tar.gz | 0005367336 5.12 MB | |
z3.changes | 0000064162 62.7 KB | |
z3.spec | 0000003166 3.09 KB |
Revision 86 (latest revision is 101)
- update to 4.10.2: * fix regression #6194. It broke mod/rem/div reasoning. * fix user propagator scope management for equality callbacks. * fix implementation of mk_fresh in user propagator for Python API * Added API Z3_enable_concurrent_dec_ref to be set by interfaces that use concurrent GC to manage reference counts. This feature is integrated with the OCaml bindings and fixes a regression introduced when OCaml transitioned to concurrent GC. Use of this feature for .Net and Java bindings is not integrated for this release. They use external queues that are unnecessarily complicated. * Added pre-declared abstract datatype declarations to the context so that Z3_eval_smtlib2_string works with List examples. * Fixed Java linking for MacOS Arm64. * Added missing callback handlers in tactics for user-propagator, Thanks to Clemens Eisenhofer * Tuning to Grobner arithmetic reasoning for smt.arith.solver=6 (currently the default in most cases). The check for consistency modulo multiplication was updated in the following way: - polynomial equalities are extracted from Simplex tableau rows using a cone of influence algorithm. Rows where the basic variables were unbounded were previously included. Following the legacy implementation such rows are not included when building polynomial equations. - equations are pre-solved if they are linear and can be split into two groups one containing a single variable that has a lower (upper) bound, the other with more than two variables with upper (lower) bounds. This avoids losing bounds information during completion. - After (partial) completion, perform constant propagation for equalities of the form x = 0 - After (partial) completion, perform factorization for factors of the
Comments 0