openSUSE Build Service

buildservice-autocommit accepted request 1170694 from

Jiri Slaby (jirislaby) 2 days ago (revision 101)

baserev update by copy to link target

Jiri Slaby (jirislaby) accepted request 1170557 from

Andreas Stieger (AndreasStieger) 3 days ago (revision 100)

z3 4.13.0

buildservice-autocommit accepted request 1153113 from

Factory Maintainer (factory-maintainer) 2 months ago (revision 99)

baserev update by copy to link target

Jiri Slaby (jirislaby) committed 2 months ago (revision 98)

up to 4.12.5

buildservice-autocommit accepted request 1093226 from

Jiri Slaby (jirislaby) 11 months ago (revision 97)

baserev update by copy to link target

Jiri Slaby (jirislaby) committed 11 months ago (revision 96)

up to 4.12.2

buildservice-autocommit accepted request 1060326 from

Jiri Slaby (jirislaby) over 1 year ago (revision 95)

baserev update by copy to link target

Jiri Slaby (jirislaby) accepted request 1060179 from

Dirk Mueller (dirkmueller) over 1 year ago (revision 94)

- 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.

buildservice-autocommit accepted request 1059321 from

Jiri Slaby (jirislaby) over 1 year ago (revision 93)

baserev update by copy to link target

Jiri Slaby (jirislaby) accepted request 1059018 from

Andrea Manzini (amanzini) over 1 year ago (revision 92)

- 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

buildservice-autocommit accepted request 1003077 from

Jiri Slaby (jirislaby) over 1 year ago (revision 91)

baserev update by copy to link target

Jiri Slaby (jirislaby) accepted request 1003043 from

Dirk Mueller (dirkmueller) over 1 year ago (revision 90)

- 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

buildservice-autocommit accepted request 999781 from

Jiri Slaby (jirislaby) over 1 year ago (revision 89)

baserev update by copy to link target

Jiri Slaby (jirislaby) accepted request 999657 from

Matthias Eliasson (elimat) over 1 year ago (revision 88)

- 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.

buildservice-autocommit accepted request 992706 from

Jiri Slaby (jirislaby) over 1 year ago (revision 87)

baserev update by copy to link target

Jiri Slaby (jirislaby) accepted request 992650 from

Dirk Mueller (dirkmueller) over 1 year ago (revision 86)

- 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

buildservice-autocommit accepted request 975667 from

Jiri Slaby (jirislaby) almost 2 years ago (revision 85)

baserev update by copy to link target

Jiri Slaby (jirislaby) accepted request 975376 from

Ferdinand Thiessen (susnux) almost 2 years ago (revision 84)

Update to 4.8.17

buildservice-autocommit accepted request 970659 from

Jiri Slaby (jirislaby) about 2 years ago (revision 83)

baserev update by copy to link target

Jiri Slaby (jirislaby) accepted request 970179 from

Ferdinand Thiessen (susnux) about 2 years ago (revision 82)

- Update to 4.8.15:
  * Fix solution soundness bug on QF_ABV formula undetected by
    model validator
  * Various other bug fixes

Places

Revisions of z3

Places