search

exo-lang / exo

Exocompilation for productive programming of hardware accelerators
https://exo-lang.dev
MIT License
307 stars 28 forks source link

Bump z3-solver from 4.13.2.0 to 4.13.3.0 #722

Closed dependabot[bot] closed 1 month ago

dependabot[bot] commented 1 month ago

Bumps z3-solver from 4.13.2.0 to 4.13.3.0.

Release notes

Sourced from z3-solver's releases.

Nightly

nightly build

Changes:

  • 3a8195b9c3875cbce4fe6a89c6874923d34479a9 #7419
  • 7a0b58bcd5e28ce819a58832b8a2a61e6ad26595 increment minor version number
  • efde65603622ae54ef82050b0ade3f3218b2d54b fix recursive self call for slice_solver check-sat-cc method

This list of changes was auto generated.

z3-4.13.3

4.13.3 release

Changes:

  • 54d30f26f72ce62f5dcb5a5258f632f84858714f add _0 to platform tag for pypi
  • 6e3b99fb9ee02cbc37c6fb3ba289a5fd0fb59134 downgrade to macos13 in builds until fully supported by pypi
  • b268b56519f09828cc3b41d989b89377fae178cc update release notes
  • 00f1f1b83da7c583d0290280b1b3bbb6097a6be8 fix typo in setup.py
  • fe71b75ffdaaa775b8ff931b3d411aee7dcc13ff remove : from setup.py
  • 5dc1b1acd4dfb0b6db110251883853f4b1274b14 remove hard-wired osx=11.0
  • 48aa2f6988f62466ecfed284587357d4ca0722f2 setup python dist to remove internal build suffix for macos
  • da614c65e58b8e97d6d0c7aaf3a1294bac8e6097 remove m_level attribute, use s->get_scope_level directly
  • 6bd46b0922a0c02dbf142c4ac3dd7b9cca6d0b4c fix #7363. Replay relevancy on unit literals that are re-asserted during backtracking.
  • cfd00ad672dbe1334976c35867001e3f96f63692 add slice solver option to command context
  • 8a95dd4d65d0a4d9eaf760ebcd5ddf5456a17780 A slice solver option for interactive use case
  • 0fec7efc7ba75de1292b78fe334a87a884a2187f micro-tuning
  • c6cd25c822a552d0caf813d33b89e086d05750d9 mico-tuning
  • 24d7b05c0d4e1eb07b2c6b11dd19c0aba4f9a603 refactor and optimize git operations for commit messages and failure analysis (#7412)
  • 2ae4ac8d0a24b6542306737501bcc2679e34fcd2 fix build
  • b60e1a2ed22111fefa328cfcbdc3fa1cdd2b1555 fixup variables
  • 969511ac00830a97f49be9d9585540f33b8aaa7e fixup std-order / inv-order
  • 66bb3109662ff2ff1c25de128b5e3ebc270334eb reset before manager is deallocated
  • a98c9250690f82a67e27b5d8ae84d61550ffdfd7 optimize var_subst
  • f5db6bf92b88a9648ae73de38d7a9989233a0922 install Julia for macos build
  • e58eb9f3029a7055b9070a235aced7241d4ee5c3 fix indentation for mbp
  • 3586b613f7e0cdd404d9c44e51d27d01be08019e remove default destructors
  • b170f101481c51e4d753212b484bc5a48191f6ed reorder template definition
  • 6dec943b297f455b178b2f0369544e99b0d79779 Bump docker/build-push-action from 6.7.0 to 6.9.0 (#7408)
  • d686e92bfa48eac2c980b103a7c121387e83d851 disambiguate
  • 93ff89bf9807ca305b49faae77f379f0bfab36ac add == for const_ref and ref to disambiguate equality.
  • c7af97364a55394396b69feb04c449aa3fe60f1f fixes for #7402
  • 328616b8b28feddca2fdb55b2865ca525d584e91 fix build warnings
  • 8c39863019f32c12ae11869a38598849c2c2b404 fix typo in arch for setup.py
  • 4cefc513eb24e6077ec77d6282a5cbfd212c886d add sequoia to os versions #7407
  • 19f63cd6e336e5795c3a65fd0af1254e78a3ded2 add sequoia to os versions #7407
  • 86b97186b0a4b3a8f8a041f2443b540952a5c530 fix build warnings

... (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.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.

Version 4.13.0

  • add ARM64 wheels for Python, thanks to Steven Moy, smoy

Version 4.12.6

  • remove expensive rewrite that coalesces adjacent stores

... (truncated)

Commits
  • 54d30f2 add _0 to platform tag for pypi
  • 6e3b99f downgrade to macos13 in builds until fully supported by pypi
  • b268b56 update release notes
  • 00f1f1b fix typo in setup.py
  • fe71b75 remove : from setup.py
  • 5dc1b1a remove hard-wired osx=11.0
  • 48aa2f6 setup python dist to remove internal build suffix for macos
  • da614c6 remove m_level attribute, use s->get_scope_level directly
  • 6bd46b0 fix #7363. Replay relevancy on unit literals that are re-asserted during back...
  • cfd00ad add slice solver option to command context
  • Additional commits viewable in compare view


Dependabot compatibility score

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 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)