- update to 4.14.1
* Add ubv_to_int, sbv_to_int, int_to_bv to SMTLIB2 API.
* Fix nuget package regression omitting Microsoft.Z3.* files
* SLS modulo theories engine v1 release.
* API for accessing term depth and groundness.
* Two fixes to relevancy propagation.
* A new API for solving LRA variables modulo constraints.
* Performance and bug fixes.
* several updates to emscripten including #7473
* add preliminary pyodie build
* address issues with Java bindings
* Include start of sls-smt functionality SLS modulo theories
OBS-URL: https://build.opensuse.org/request/show/1266082
OBS-URL: https://build.opensuse.org/package/show/openSUSE:Factory/z3?expand=0&rev=43
* Fixes, including #7363
* Fix paths to Java binaries in release
* Remove internal build names from pypi wheels
* Performance regression fix. #7404
* single-sample cell projection in nlsat
* using simple-checker together with and variable ordering
The projection is described in paper by Haokun Li and Bican Xia,
Solving Satisfiability of Polynomial Formulas By Sample - Cell Projection.
The code ported from https://github.com/hybridSMT/hybridSMT.git
* Add API for providing hints for the solver/optimize contexts for which
initial values to attempt to use for variables. The new API function are
Z3_solver_set_initial_value and Z3_optimize_set_initial_value, respectively.
OBS-URL: https://build.opensuse.org/package/show/devel:tools:statica/z3?expand=0&rev=102
- 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
OBS-URL: https://build.opensuse.org/request/show/1093226
OBS-URL: https://build.opensuse.org/package/show/openSUSE:Factory/z3?expand=0&rev=38
- 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 (forwarded request 1003043 from dirkmueller)
OBS-URL: https://build.opensuse.org/request/show/1003077
OBS-URL: https://build.opensuse.org/package/show/openSUSE:Factory/z3?expand=0&rev=35
- 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
OBS-URL: https://build.opensuse.org/request/show/1003043
OBS-URL: https://build.opensuse.org/package/show/devel:tools:statica/z3?expand=0&rev=90
- 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.
OBS-URL: https://build.opensuse.org/request/show/999657
OBS-URL: https://build.opensuse.org/package/show/devel:tools:statica/z3?expand=0&rev=88
- 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
OBS-URL: https://build.opensuse.org/request/show/992650
OBS-URL: https://build.opensuse.org/package/show/devel:tools:statica/z3?expand=0&rev=86
- update to 4.8.9:
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.
- many
- 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.
- remove remove-timestamp.patch, 5a42a000e938a295feb1a7070dd74b192796db4e.patch (upstream)
OBS-URL: https://build.opensuse.org/request/show/835098
OBS-URL: https://build.opensuse.org/package/show/devel:tools:statica/z3?expand=0&rev=71
- Update to version 4.8.7+git.20200407:
* work on random_updates
* fill columns to fill in random update as in theory_arith_aux.h
* block selected configurations from HORN tactic
* set arith.solver=6 by default
* revert the default arith.solver=2
* simplify patch_blocker()
* redirect to the new solver
* fix the patch of real vars
* change lar_terms to use column indices
* change lar_terms to use column indices
* fix#3713: too much caching in dom-simplify for OR expressions
* fix#3739 - dependencies may be valid even if they are null
* [spacer] fix ugly bug in ground refutation generation (i.e., cex)
* Replace is_null with is_non_empty_string in spacer params
* [spacer] fixedpoint.get_answer() returns ground refutation for SAT
* reduce_invertible: fix mk_diagonal for BV 0 switch from -x to ~x
* minor code simplification in bv rewriter
* reduce_invertible: recognize (* x -1) as the same as (- x)
* roll back in maximize_term if the integrality is broken
* remove output from normalize bounds
* and plenty of other chanes
- Use cmake_build macro
OBS-URL: https://build.opensuse.org/request/show/792386
OBS-URL: https://build.opensuse.org/package/show/devel:tools:statica/z3?expand=0&rev=62
