Bump z3-solver from 4.13.4.0 to 4.14.0.0

[dependabot]

Bumps z3-solver from 4.13.4.0 to 4.14.0.0.

Release notes

Sourced from z3-solver's releases.

Nightly

nightly build

Changes:

• be8febedc3dedc35d86568399f2e77526d0955b2 add throttle, fixup bp.init() for proper initialization
• c79967b2b61c13d75e9131d45c223f52ef20bd6b using iterators
• 17f239c2cb7063ca4536eb9c67fab535cabc3639 base line specbot
• 589fb1b04f3ec07b1f12fc1b93d6371fa86670d4 base line specbot
• 67d77e26d2b348833bcc7ce710733e05f4ba7234 remove a parameter when calling bound_analyzer_on_row
• b985838112e01585b89df6d52354d9931994e310 do not pass row index to bound_analyzer_on_row
• 10c2af85c1b4e0f26afb2e57d908ae6b4682a737 try for mixed-mode
• ead8478046da39f8d87404fa8035ce443c6b8149 fix build per new API for analyze_row
• 1a3d1ad69dccc332d118191ec2c6e0ac81496b63 add base line bounds tightening utility
• 7044bb8485398ee26218d89ad83da8ed0a737387 remove an unused parameter in bound_analyzer_on_row

• fbfbfa5d76d3d9e5e4614d9af1aeda714d099ef6 print column value
• f50f21198e636e7f4b7a913139102f6562173887 Fix #7505 (#7565)
• bd3d288a085b1543e8130983be7e1bc1d1becb9f tighten only core constrants
• 45ad61438a4dfd980ee12bbfbcc0f8831ebe8ec6 added logging
• 1fec0fa35bda08af519c688cfd7bfaf538a2d5e0 remove verbose output
• 01fbc0e8e7e683a24674ace74b2598657e919e5d fix #7563
• 712231dcda4eb6b6fe37927f304df48d7595ffe5 fix #7560
• 075773e51970f854d923a47359802ef59c0eb083 remove proviso for single index arrays
• 3e5abef14524419805a1d38b51aa698076b1aa5d fix #7549
• e0945f57bb550208802a3884ac6ece633bc5ed3f fix #7554
• 28f3f8046e2f1a034e7b68d977af875810fdc44e #7559
• 11066486d750ffbfa16370721112c87711990979 #7559
• 991cffb51990b0c88f8a64a0096d5526b103593a handle multi-arity arrays
• 674e1b8f981042c6d2f5fe9c94fefe67db64ff31 remove equality check on container
• ce69b54b5fbd28ce878dbbe367017e664f76b630 adjust select/store rule for n-ary arrays
• 42f6e1300a94adf094125f7795bb40b5a38a8888 more review of mbp_arrays
• a4a84ed083bc7d40e4f53f90d054060e82b0b5b0 arrays are not necessarily unary
• a5e5a35755d51ac49319b662be4e9220ce35708c code simplification
• a143ed3bff01bccecde97b52c178381057478f6f taking a look at mbp_qel for arrays
• dda60737dc94a1e7b4d7aaffdd0c24cd43286bc7 updated release notes
• fb6ec7d5e7eb5db27e35f6a3b5bcbbe929e725c5 increase version number
• 30dba9bde73fb0eefd55c08ed1d2b9040679a87a use down-level setup tools on hosted machines to avoid https://stackoverflow.com/questions/79252233/canonicalize-versionversion-strip-trailing-zero-false-while-doing-colcon-buil

This list of changes was auto generated.

z3-4.14.0

4.14.0 release

Changes:

• 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 bump timeout for jobs
• 2e008a97452bf7e47f64d9e623d428d9abd4293e Update release.yml for Azure Pipelines
• d1575af5d267b4758189484aab3d7945cf76fa95 Update nightly.yaml for Azure Pipelines

... (truncated)

Changelog

Sourced from z3-solver's changelog.

RELEASE NOTES

Version 4.next

• Planned features
  • sat.euf
    • CDCL core for SMT queries. It extends the SAT engine with theory solver plugins.
  • add global incremental pre-processing for the legacy core.

Version 4.14.1

• Improved integer cut algorithms for linear integer arithmetic.

Version 4.14.0

• SLS modulo theories engine v1 release.
• API for accessing term depth and groundness.
• Two fixes to relevancy propagation thanks to Can Cebeci. Two instacnes where literals lemmas and axioms were not marked relevant and therefore not propagated to other theories. Theory lemmas are replayed during backjumping and have are now by default marked relevant.
• A new API for solving LRA variables modulo constraints.
• Performance and bug fixes.

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)

... (truncated)

Commits

• 3c47fd9 bump timeout for jobs
• 2e008a9 Update release.yml for Azure Pipelines
• d1575af Update nightly.yaml for Azure Pipelines
• 96e3233 Update azure-pipelines.yml for Azure Pipelines
• 813da35 fix unit test
• f8f2678 convert def into expression tree
• f977b48 adjust solve_for to handle rationals
• 528efbb fixes to failure conditions for unification
• fe27ca1 remove verbose output
• 50f9fdd Add unification based projection function
• Additional commits viewable 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)

[codecov]

Codecov Report

All modified and coverable lines are covered by tests ✅

Project coverage is 88.34%. Comparing base (b51c861) to head (cd2ad7a).
Report is 1 commits behind head on main.

Additional details and impacted files

@@           Coverage Diff           @@
##             main     #765   +/-   ##
=======================================
  Coverage   88.34%   88.34%           
=======================================
  Files          93       93           
  Lines       21716    21716           
=======================================
  Hits        19185    19185           
  Misses       2531     2531           

☔ View full report in Codecov by Sentry.
📢 Have feedback on the report? Share it here.