Script 'mail_helper' called by obssrc Hello community, here is the log from the commit of package z3 for openSUSE:Factory checked in at 2022-08-04 13:23:54 ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Comparing /work/SRC/openSUSE:Factory/z3 (Old) and /work/SRC/openSUSE:Factory/.z3.new.1521 (New) ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Package is "z3" Thu Aug 4 13:23:54 2022 rev:33 rq:992706 version:4.10.2 Changes: -------- --- /work/SRC/openSUSE:Factory/z3/z3.changes 2022-05-09 18:44:22.800226935 +0200 +++ /work/SRC/openSUSE:Factory/.z3.new.1521/z3.changes 2022-08-04 13:24:18.308641933 +0200 @@ -1,0 +2,66 @@ +Wed Aug 3 21:27:44 UTC 2022 - Dirk M??ller <[email protected]> + +- 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. + +------------------------------------------------------------------- Old: ---- z3-4.8.17.tar.gz New: ---- z3-4.10.2.tar.gz ++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++ Other differences: ------------------ ++++++ z3.spec ++++++ --- /var/tmp/diff_new_pack.R2FODj/_old 2022-08-04 13:24:18.904643624 +0200 +++ /var/tmp/diff_new_pack.R2FODj/_new 2022-08-04 13:24:18.908643636 +0200 @@ -16,9 +16,9 @@ # -%define sover 4_8 +%define sover 4_10 Name: z3 -Version: 4.8.17 +Version: 4.10.2 Release: 0 Summary: Theorem prover from Microsoft Research License: MIT @@ -93,7 +93,7 @@ %files %license LICENSE.txt -%doc README.md RELEASE_NOTES +%doc README.md RELEASE_NOTES.md %{_bindir}/z3 %files -n libz3-%{sover} ++++++ z3-4.8.17.tar.gz -> z3-4.10.2.tar.gz ++++++ ++++ 42909 lines of diff (skipped)
