| Index | index by Group | index by Distribution | index by Vendor | index by creation date | index by Name | Mirrors | Help | Search |
| Name: z3 | Distribution: openSUSE Tumbleweed |
| Version: 4.13.0 | Vendor: openSUSE |
| Release: 1.1 | Build date: Fri Apr 12 21:53:36 2024 |
| Group: Productivity/Scientific/Other | Build host: reproducible |
| Size: 15831884 | Source RPM: z3-4.13.0-1.1.src.rpm |
| Packager: http://bugs.opensuse.org | |
| Url: https://github.com/Z3Prover/z3/wiki | |
| Summary: Theorem prover from Microsoft Research | |
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.
MIT
* Fri Apr 12 2024 Andreas Stieger <andreas.stieger@gmx.de>
- includes changes from 4.13.0:
* remove expensive rewrite that coalesces adjacent stores
* improved Java use of reference queues
* fixes to conditional import of python library
* include universe for constants that get removed during
pre-processing
* code improvements
* fix nested callback handling for user propagators
* added Julia API
* Thu Feb 22 2024 Jiri Slaby <jslaby@suse.cz>
- update to 4.12.5
* track quantifier instantiation method in proof hint #7080
* prepare for release
* free memory the clean way
* encapsulate anum functionality
* encapsulate mpz a bit more
* Fixes in Java's User Propagator (#7088)
* remove unused code
* take care of strategy undecided, Nikolaj's comments
* Merge branch 'master' of https://github.com/z3prover/z3
* force int bound on int columns, call term_is_int() after subst
* pin expression passed to validate_eq
* Update z3_api.h
* fix #7081
* fix #7085
* fix #7084
* change the definition of Gomory row
* and more
- remove 0001-Fix-building-with-gcc-13-6723.patch (upstream)
* Thu Jun 15 2023 Jiri Slaby <jslaby@suse.cz>
- update to 4.12.2
* remove MSF (Microsoft Solver Foundation) plugin.
* updated propagate-ineqs tactic and implementing it as a simplifier,
bound_simplifier.
* add API function Z3_mk_real_int64 to take two int64 as arguments. The
Z3_mk_real function takes integers.
* Add _simplifiers_ as optional incremental pre-processing to solvers.
* Optimize added to JS API.
* SMTLIB2 proposal for bit-vector overflow predicates added.
* bug fixes.
- add 0001-Fix-building-with-gcc-13-6723.patch
* Sat Jan 21 2023 Dirk Müller <dmueller@suse.com>
- update to 4.12.1:
* change macos build to use explicit reference to Macos version 11. Hosted
builds are migrating to macos-12 and it broke a user Issue #6539.
* Tue Jan 17 2023 Andrea Manzini <andrea.manzini@suse.com>
- update to 4.12.0
* move bound_manager to simplifiers, add bound manager to extract_eqs for solve-eqs
* fix memory leak on proof justifications
* expose parameters to control behavior for
* many bugfixes, see https://github.com/Z3Prover/z3/releases
* Mon Sep 12 2022 Dirk Müller <dmueller@suse.com>
- update to 4.11.2:
* add error handling to fromString method in JavaScript
* fix regression in default parameters for CDCL, thanks to Nuno Lopes
* fix model evaluation bugs for as-array nested under functions (data-type constructors)
* add rewrite simplifications for datatypes with a single constructor
* add "Global Guidance" capability to SPACER, thanks to Arie Gurfinkel and Hari Gorvind.
* change proof logging format for the new core to use SMTLIB commands.
The format was so far an extension of DRAT used by SAT solvers, but not well compatible
with SMT format that is extensible. The resulting format is a mild extension of SMTLIB with
three extra commands assume, learn, del. They track input clauses, generated clauses and deleted clauses.
They are optionally augmented by proof hints. Two proof hints are used in the current version: "rup" and "farkas".
"rup" is used whent the generated clause can be justified by reverse unit propagation. "farkas" is used when
the clause can be justified by a combination of Farkas cutting planes. There is a built-in proof checker for the
format. Quantifier instantiations are also tracked as proof hints.
Other proof hints are to be added as the feature set is tested and developed. The fallback, buit-in,
self-checker uses z3 to check that the generated clause is a consequence. Note that this is generally
insufficient as generated clauses are in principle required to only be satisfiability preserving.
Proof checking and tranformation operations is overall open ended.
The log for the first commit introducing this change contains further information on the format.
* fix to re-entrancy bug in user propagator (thanks to Clemens Eisenhofer).
* handle _toExpr for quantified formulas in JS bindings
* Sun Aug 28 2022 Matthias Eliasson <elimat@opensuse.org>
- update to 4.11.0:
* remove Z3_bool, Z3_TRUE, Z3_FALSE from the API. Use bool, true, false instead.
* z3++.h no longer includes <sstream> as it did not use it.
* add solver.axioms2files
- prints negated theory axioms to files. Each file should be unsat
* add solver.lemmas2console
- prints lemmas to the console.
* remove option smt.arith.dump_lemmas. It is replaced by solver.axioms2files
* add option smt.bv.reduce_size.
- it allows to apply incremental pre-processing of bit-vectors by identifying ranges that are known to be constant.
This rewrite is beneficial, for instance, when bit-vectors are constrained to have many high-level bits set to 0.
* add feature to model-based projection for arithmetic to handle integer division.
* add fromString method to JavaScript solver object.
* Wed Aug 03 2022 Dirk Müller <dmueller@suse.com>
- 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
form x*y*p = 0 where x, are variables, p is linear.
* Added support for declaring algebraic datatypes from the C++ interface.
* Bugfix release to ensure npm package works
* Native M1 (Mac ARM64) binaries and pypi distribution.
- thanks to Isabel Garcia Contreras and Arie Gurfinkel for testing and fixes
* API for incremental parsing of assertions.
A description of the feature is given by example here: https://github.com/Z3Prover/z3/commit/815518dc026e900392bf0d08ed859e5ec42d1e43
It also allows incrementality at the level of adding assertions to the
solver object.
* Fold/map for sequences:
https://microsoft.github.io/z3guide/docs/guide/Sequences#map-and-fold
At this point these functions are only exposed over the SMTLIB2 interface (and not programmatic API)
maxdiff/mindiff on arrays are more likely to be deprecated
* User Propagator:
- Add functions and callbacks for external control over branching thanks to Clemens Eisenhofer
- A functioning dotnet API for the User Propagator
https://github.com/Z3Prover/z3/blob/master/src/api/dotnet/UserPropagator.cs
* Java Script API
- higher level object wrappers are available thanks to Kevin Gibbons and Olaf Tomalka
* Totalizers and RC2
- The MaxSAT engine now allows to run RC2 with totalizer encoding.
Totalizers are on by default as preliminary tests suggest this solves already 10% more problems on
standard benchmarks. The option opt.rc2.totalizer (which by default is true) is used to control whether to use
totalizer encoding or built-in cardinality constraints.
The default engine is still maxres, so you have to set opt.maxsat_engine=rc2 to
enable the rc2 option at this point. The engines maxres-bin and rc2bin are experimental should not be used
(they are inferior to default options).
* Incremental constraints during optimization set option opt.incremental = true
- The interface `Z3_optimize_register_model_eh` allows to monitor incremental results during optimization.
It is now possible to also add constraints to the optimization context during search.
You have to set the option opt.incremental=true to be able to add constraints. The option
disables some pre-processing functionality that removes variables from the constraints.
* Fri May 06 2022 Ferdinand Thiessen <rpm@fthiessen.de>
- Update to 4.8.17
* fix breaking bug in python interface for user propagator pop
* Various fixes for z3str3
* Initial support for nested algebraic datatypes with sequences
* Initiate map/fold operators on sequences
* Initiate maxdiff/mindiff on arrays
- Update to version 4.8.16
* Initial support for Darwin Arm64 (for M1, M2, .. users)
* Added functionality to user propagator decisions.
* Added options for rc2 and maxres-bin to maxsat
* Improved search for mutex constraints (at-most-1 constraints)
among soft constraints for maxsat derived from approach used
in rc2 sample.
* Various other bugfixes
* Thu Apr 14 2022 Ferdinand Thiessen <rpm@fthiessen.de>
- Update to 4.8.15:
* Fix solution soundness bug on QF_ABV formula undetected by
model validator
* Various other bug fixes
* Tue Mar 15 2022 Shung-Hsi Yu <shung-hsi.yu@suse.com>
- fix python3-z3 requirement
* Fri Jan 21 2022 Avinesh Kumar <avinesh.kumar@suse.com>
- update to 4.8.14:
* fixes Antimirov derivatives for intersections and unions required
required for solving non-emptiness constraints.
* includes x86 dll in nuget package for Windows.
* exposes additional user propagator functionality
* Sun Nov 28 2021 Dirk Müller <dmueller@suse.com>
- update to 4.8.13:
The release integrates various bug fixes and tuning.
* Sat Oct 16 2021 Dirk Müller <dmueller@suse.com>
- update to 4.8.12:
Release provided to fix git tag discrepancy issues with 4.8.11
* Fri Jun 11 2021 Paolo Stivanin <info@paolostivanin.com>
- update to 4.8.11:
* fix soundness issues, invalid models, and crashes for options
"tactic.default_tactic=smt sat.euf=true"
* centos -> glibc
* updated ref to esrp
* undo cxx hoist
* hoist c++ flags
* Fri Jan 29 2021 Dirk Müller <dmueller@suse.com>
- update to 4.8.10:
- rewritten arithmetic solver replacing legacy arithmetic solver and on by default
/usr/bin/z3 /usr/share/doc/packages/z3 /usr/share/doc/packages/z3/README.md /usr/share/doc/packages/z3/RELEASE_NOTES.md /usr/share/licenses/z3 /usr/share/licenses/z3/LICENSE.txt
Generated by rpm2html 1.8.1
Fabrice Bellet, Wed Oct 9 00:49:13 2024