Bump z3-solver from 4.13.3.0 to 4.13.4.0

[dependabot]

Bumps z3-solver from 4.13.3.0 to 4.13.4.0.

Release notes

Sourced from z3-solver's releases.

Nightly

nightly build

Changes:

• 31ee56c1cab652bf7b8d63224594c7578f0d1842 wip - incremental edit distance algorithm
• 538f74d64c7feac3e259b4e0ffbbbebee3bbd4cb extract stats with finalize for parallel mode
• b4295620b35082c3a9651b7f13ad36a04acc0ddb Add enter and exit methods on Optimize class (#7477)
• 1e5c59a06f46fb80f5f98738f922c73d196f3e43 add repair step for str.replace
• e8c23600433674646c33e374d061a5db46f4d7a0 fix #7461
• 8f5658b77d8c728c58e958f28f4f1cdf5f9af48a add another baseline heuristic for string equalities, add cases for array axioms.
• e5f8327483739cd802b68c02c5c17616660133b9 Update emscripten (#7473)
• 4fbf54afd06b2353555939c249bd60784aa58e8b fixes to regex membership and edit updates
• 1ab0962d43f97c61e4420425fda035a1ea2ba040 partial fix to make computed term integer well-formed for solve_for functionality
• bcb61ee12c573b6e7da08eefa6c7bf89b6125651 v0 of edit distance repair

• 4be4067f75830edde261b6f5230296ea1f7c261f Typescript high-level api for Sets (#7471)
• a17d4e68eb483145ed27a29e6a74cfb7cf47a7d4 bugfix to elim_uncnstr to ensure nodes are created. Prepare smt_internalizer to replay unit literals
• 6ea4110b303c7e5015ee591f47a188db00c53e27 Bump docker/build-push-action from 6.9.0 to 6.10.0 (#7469)
• aec867586a67b5153677a47f2cd554c8da79ef42 updates to equality solving search
• e6feb8423a397da44eb352402a3d26f70489f1e9 sls: fix bug where unsat remains empty after a literal is flipped. The new satisfiable subset should be checked
• 24c3cd38d1ce7f961b38183676b01f16525ce750 add v0 of equality solver
• 05e053247dabdbd2231e5b97986d70293f5ab737 add facility to solve for a linear term over API
• d2411567b5d02cd5581e3d9e7b502b6c0dc5058e add projection with witnesses
• b7b611d84baed948e2b606a8a9b875359aba378f inherit from std::exception
• ab1be5c06e5d32a7fe83fcf9e7910803d2065699 internalize the reduce_args_tactic to reduce the number of heap allocations
• 1ccfba6a91b0fff2278644ef152dea3a598b3c1d remove unreachble code
• 1e62029413f7828b4fa90b429c42da12c40bcbb8 use ztring
• fce377e1d777406b014cf7801bf75011886ed40c add basic regex functions
• b143a954c5d98e0c85292ab4d579835b4d48c8e7 add notes and additional functions to sls-seq
• aed3279d7dabe4e9730f69b3f9257ad266d601cd add missing new_value_eh when repaired up
• 1e839e5ac25e37b02e0ea9bebf67f2f6ac5474b5 add missing new_value_eh when repaired up
• 7ed185aa9e3c3170b2c68bda9fb34fa0014d02e5 add comments
• 4559b23caf8c0db4644719ceeae00e94bea1c842 add local search functionality to sls_seq_plugin
• b4e768cfb0ac2ccd26d00d99d3c7ab478c415a64 adding plugin for local search strings
• 36725758ebde12c404427be68fb392dd81dcc2bf fix typos POLING -> POLLING in setup.py and remove unused CFLAGS
• 71bad7159b1f821c61196b8a7c010f08a5119442 #7418 - circumvent use of timer threads to make WASM integration of z3 easier
• 94f0aff47fe3ecfe5c3ad82af90dbc276485e49c remove the use-pthread
• 76795a44e40673e14d3e46602e0009c391d293dd remove -pthread from options
• 8965123c0d3f55197c7df5754d3cb65f6a7a2b8f fix type in setup.py
• 10d9c81957f2a0d3fad4417690abc9fd928806e7 adapt for pyodide built
• 012fc1b72b5b8245d0dff98b150bb9e4fb51a7b2 more detailed tracing of where unmaterialized exceptions happen
• 7de0c29f12886f20f8d7fb1e60f5b38297f89fe5 Update pyodide.yml
• e855a50d9bc4d9c321836bad98b9a89cb2b88cf6 add exception handling to easier diagnose #7418
• 5168a13efacf2ecd39654be04d6b577424b9b8b0 track exceptions in reason-unknown
• a8a50695c90d2de93794a4d40fb296d9e0c65e71 Update README.md
• 15f954ec3bbafbd7e2a5ebf4fdb76457ed70cb0f add picture of z3guide
• 24dfc179209bc223414872fc6b2cc88785c5e228 Update README.md
• 4b72e517b7b37affe410390b242fc6d56032e855 SLS: log clause , allow more frequent export of SLS state to SMT

... (truncated)

Changelog

Sourced from z3-solver's changelog.

RELEASE NOTES

Version 4.next

• Planned features
  • sat.euf
    • a new CDCL core for SMT queries. It extends the SAT engine with theory solver plugins. the current state is unstable. It lacks efficient ematching.
  • polysat
    • native word level bit-vector solving.
  • introduction of simple induction lemmas to handle a limited repertoire of induction proofs.

Version 4.13.4

• several updates to emscripten including #7473
• add preliminary pyodie build
• address issues with Java bindings
• Include start of sls-smt functionality SLS modulo theories as co-processor to SMT core and stand-alone tactic.

Version 4.13.3

• Fixes, including #7363
• Fix paths to Java binaries in release
• Remove internal build names from pypi wheels

Version 4.13.2

• Performance regression fix. #7404

Version 4.13.1

• single-sample cell projection in nlsat was designed by Haokun Li and Bican Xia.

• using simple-checker together with and variable ordering supported by qfnra_tactic was developed by Mengyu Zhao (Linxi) and Shaowei Cai.

  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. Supply these functions with a Boolean or numeric variable, and a value. The solver will then attempt to use these values in the initial phase of search. The feature is aimed at resolving nearly similar problems, or problems with a predicted model and the intent is that restarting the solver based on a near solution can avoid prune the space of constraints that are initially infeasible. The SMTLIB front-end contains the new command (set-initial-value var value). For example, (declare-const x Int) (set-initial-value x 10) (push) (assert (> x 0)) (check-sat) (get-model) produces a model where x = 10. We use (push) to ensure that z3 doesn't run a specialized pre-processor that eliminates x, which renders the initialization without effect.

... (truncated)

Commits

• See full diff in compare view

Dependabot will resolve any conflicts with this PR as long as you don't alter it yourself. You can also trigger a rebase manually by commenting @dependabot rebase.

---

Dependabot commands and options

You can trigger Dependabot actions by commenting on this PR:

• @dependabot rebase will rebase this PR
• @dependabot recreate will recreate this PR, overwriting any edits that have been made to it
• @dependabot merge will merge this PR after your CI passes on it
• @dependabot squash and merge will squash and merge this PR after your CI passes on it
• @dependabot cancel merge will cancel a previously requested merge and block automerging
• @dependabot reopen will reopen this PR if it is closed
• @dependabot close will close this PR and stop Dependabot recreating it. You can achieve the same result by closing it manually
• @dependabot show <dependency name> ignore conditions will show all of the ignore conditions of the specified dependency
• @dependabot ignore this major version will close this PR and stop Dependabot creating any more for this major version (unless you reopen the PR or upgrade to it yourself)
• @dependabot ignore this minor version will close this PR and stop Dependabot creating any more for this minor version (unless you reopen the PR or upgrade to it yourself)
• @dependabot ignore this dependency will close this PR and stop Dependabot creating any more for this dependency (unless you reopen the PR or upgrade to it yourself)

[codspeed-hq]

CodSpeed Performance Report

Merging #271 will improve performances by ×2.2

_{Comparing dependabot/pip/z3-solver-4.13.4.0 (de9e870) with main (5ba5ea6)}

Summary

⚡ 1 improvements
✅ 20 untouched benchmarks

Benchmarks breakdown

	Benchmark	main	dependabot/pip/z3-solver-4.13.4.0	Change
⚡	test_bench_crossover[StackGP]	69.1 s	32.1 s	×2.2