Revisions of z3
Dominique Leuenberger (dimstar_suse)
accepted
request 1153113
from
Factory Maintainer (factory-maintainer)
(revision 39)
Automatic submission by obs-autosubmit
Dominique Leuenberger (dimstar_suse)
accepted
request 1093226
from
Jiri Slaby (jirislaby)
(revision 38)
- 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
Dominique Leuenberger (dimstar_suse)
accepted
request 1060326
from
Jiri Slaby (jirislaby)
(revision 37)
Dominique Leuenberger (dimstar_suse)
accepted
request 1059321
from
Jiri Slaby (jirislaby)
(revision 36)
Dominique Leuenberger (dimstar_suse)
accepted
request 1003077
from
Jiri Slaby (jirislaby)
(revision 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 (forwarded request 1003043 from dirkmueller)
Dominique Leuenberger (dimstar_suse)
accepted
request 999781
from
Jiri Slaby (jirislaby)
(revision 34)
Dominique Leuenberger (dimstar_suse)
accepted
request 992706
from
Jiri Slaby (jirislaby)
(revision 33)
Dominique Leuenberger (dimstar_suse)
accepted
request 975667
from
Jiri Slaby (jirislaby)
(revision 32)
Dominique Leuenberger (dimstar_suse)
accepted
request 970659
from
Jiri Slaby (jirislaby)
(revision 31)
Dominique Leuenberger (dimstar_suse)
accepted
request 961806
from
Jiri Slaby (jirislaby)
(revision 30)
Dominique Leuenberger (dimstar_suse)
accepted
request 948353
from
Martin Pluskal (pluskalm)
(revision 29)
Dominique Leuenberger (dimstar_suse)
accepted
request 934483
from
Jiri Slaby (jirislaby)
(revision 28)
Dominique Leuenberger (dimstar_suse)
accepted
request 925964
from
Jiri Slaby (jirislaby)
(revision 27)
Dominique Leuenberger (dimstar_suse)
accepted
request 899409
from
Jiri Slaby (jirislaby)
(revision 26)
Dominique Leuenberger (dimstar_suse)
accepted
request 868100
from
Jiri Slaby (jirislaby)
(revision 25)
- update to 4.8.10: - rewritten arithmetic solver replacing legacy arithmetic solver and on by default (forwarded request 867815 from dirkmueller)
Dominique Leuenberger (dimstar_suse)
accepted
request 835112
from
Jiri Slaby (jirislaby)
(revision 24)
Dominique Leuenberger (dimstar_suse)
accepted
request 821644
from
Jiri Slaby (jirislaby)
(revision 23)
- Backport pkg-config support from upstream * add 5a42a000e938a295feb1a7070dd74b192796db4e.patch
Dominique Leuenberger (dimstar_suse)
accepted
request 821247
from
Martin Pluskal (pluskalm)
(revision 22)
Dominique Leuenberger (dimstar_suse)
accepted
request 810759
from
Factory Maintainer (factory-maintainer)
(revision 21)
Automatic submission by obs-autosubmit
Displaying revisions 1 - 20 of 40