deps(python)(deps-dev): update z3-solver requirement from <5,>=4.16 to >=4.16,<6 in /python

[dependabot]

Updates the requirements on z3-solver to permit the latest version.

Changelog

Sourced from z3-solver's changelog.

RELEASE NOTES

Version 5.0.0

• A FiniteSets theory solver FiniteSets is a theory with a sort (FiniteSet S) for base sort S. Inhabitants of (FiniteSet S) are finite sets of elements over S. The main operations are creating empty sets, singleton sets, union, intersection, set difference, ranges of integers, subset modulo a predicate. Constraints are: membership, subset. The size of a set is obtained using set.size. It is possible to map a function over elements of a set using set.map. Support for set.range, set.map is partial. Support for set.size exists, but is without any optimization. The source code contains comments on ways to make it more efficient. File a GitHub issue if you want to contribute.s
• Add Python API convenience methods for improved usability. Thanks to Daniel Tang.
  • Solver.solutions(t) method for finding all solutions to constraints, Z3Prover/z3#8633
  • ArithRef.abs alias to integrate with Python's abs() builtin, Z3Prover/z3#8623
  • Improved error message in ModelRef.getitem to suggest using eval(), Z3Prover/z3#8626
  • Documentation example for Solver.sexpr(), Z3Prover/z3#8631
• Performance improvements by replacing unnecessary copy operations with std::move semantics for better efficiency. Thanks to Nuno Lopes, Z3Prover/z3#8583
• Fix spurious sort error with nested quantifiers in model finder. Fixes [#8563](https://github.com/Z3Prover/z3/issues/8563)
• NLSAT optimizations including improvements to handle_nullified_poly and levelwise algorithm. Thanks to Lev Nachmanson.
• Add ASan/UBSan memory safety CI workflow for continuous runtime safety checking. Thanks to Angelica Moreira. Z3Prover/z3#8856
• Add missing API bindings across multiple languages:
  • Python: BvNand, BvNor, BvXnor operations, Optimize.translate()
  • Go: MkAsArray, MkRecFuncDecl, AddRecDef, Model.Translate, MkBVRotateLeft, MkBVRotateRight, MkRepeat, and 8 BV overflow/underflow check functions
  • TypeScript: Array.fromFunc, Model.translate
  • OCaml: Model.translate, mk_re_allchar (thanks to Filipe Marques, Z3Prover/z3#8785)
  • Java: as-array method (thanks to Ruijie Fang, Z3Prover/z3#8762)
• Fix #7507: simplify (>= product_of_consecutive_ints 0) to true
• Fix #7951: add cancellation checks to polynomial gcd_prs and HNF computation
• Fix #7677: treat FC_CONTINUE from check_nla as FEASIBLE in maximize
• Fix assertion violation in q_mbi diagnostic output
• Fix memory leaks in model_based_opt def ref-counting
• Fix NoSuchFieldError in JNI for BoolPtr: use Z field descriptor and SetBooleanField
• Fix TypeScript Array.fromFunc to use f.ptr instead of f.ast for Z3_func_decl type
• Fix intblast ubv_to_int bug: add bv2int axioms for compound expressions
• Fix static analysis findings: uninitialized variables, bitwise shift undefined behavior, and null pointer dereferences
• Convert bv1-blast and blast-term-ite tactics to also expose as simplifiers for more flexible integration
• Change default of param lws_subs_witness_disc to true for improved NLSAT performance. Thanks to Lev Nachmanson.
• Nl2Lin integrates a linear under-approximation of a CAD cell by Valentin Promies for improved NLSAT performance on nonlinear arithmetic problems. Z3Prover/z3#8982
• Fix incorrect optimization of mod in box mode. Fixes #9012
• Fix inconsistent optimization with scaled objectives in the LP optimizer when nonlinear constraints prevent exploration of the full feasible region. Z3Prover/z3#8998
• Fix NLA optimization regression and improve LP restore_x handling. Z3Prover/z3#8944
• Enable sum of monomials simplification in the optimizer for improved nonlinear arithmetic optimization.

... (truncated)

Commits

• See full diff in compare view

[dependabot]

Labels

The following labels could not be found: dependencies, python. Please create them before Dependabot can add them to a pull request.

Please fix the above issues or remove invalid values from dependabot.yml.