Revisions of z3
buildservice-autocommit
accepted
request 1060179
from
Dirk Mueller (dirkmueller)
(revision 12)
baserev update by copy to link target
Dirk Mueller (dirkmueller)
committed
(revision 11)
* 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.
Dirk Mueller (dirkmueller)
committed
(revision 10)
- 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 1003043
from
Dirk Mueller (dirkmueller)
(revision 9)
baserev update by copy to link target
Dirk Mueller (dirkmueller)
committed
(revision 8)
- 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 992650
from
Dirk Mueller (dirkmueller)
(revision 7)
baserev update by copy to link target
Dirk Mueller (dirkmueller)
committed
(revision 6)
- 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 934414
from
Dirk Mueller (dirkmueller)
(revision 5)
baserev update by copy to link target
Dirk Mueller (dirkmueller)
committed
(revision 4)
- update to 4.8.13: The release integrates various bug fixes and tuning.
buildservice-autocommit
accepted
request 925728
from
Dirk Mueller (dirkmueller)
(revision 3)
baserev update by copy to link target
Dirk Mueller (dirkmueller)
committed
(revision 2)
- update to 4.8.12: Release provided to fix git tag discrepancy issues with 4.8.11
Dirk Mueller (dirkmueller)
committed
(revision 1)
Displaying all 12 revisions