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.0.0 to 4.13.2.0 #707

Closed dependabot[bot] closed 1 month ago

dependabot[bot] commented 1 month ago

Bumps z3-solver from 4.13.0.0 to 4.13.2.0.

Release notes

Sourced from z3-solver's releases.

Nightly

nightly build

Changes:

  • 77aa5280dfd4960f615e98b669ff411c774598c5 wasm: increase timeout in tests (#7401)
  • 103c5ad71c4526bfc0b7580bce3383940f953c8f wasm: attempt to GC in tests (#7400)
  • 82eb18674b446f3a90992fc57cbb690ccd4cfa08 remove ubuntu build 20 from nightly
  • eb5d036786d1c1571067f656ef9c42afa4a828b7 fix #7392
  • 2655301afcdab4d98f2844f0a69d8ca2ff7aba38 comment out simple proofs unit test
  • 8b81bda46959e82c7e333f5838f4a424f4289f92 Julia now used the C API. (#7388)
  • 994056f347a637bfe90b224d4ffdeb2fde43b469 C API now used by Julia. (#7387)
  • 716a815ce169492837f95bb7613f8ff6cb183b98 update lock file
  • a831fe9609488a98ac53fba725bb54707ae27942 fix some build warnings
  • afaa48d72af0bfad47a3b3b4cf745c3a6f7f1714 sample fix script
  • fa1a2cdc1e5e808c59f6f70647eef4415e405bd5 disable simple check in nlsat
  • c34c8477f3d10444f8142e6917a752f06af1e246 Add .gitattributes for genaiscript and update git commit flow script. (#7396)
  • ec14ef765e20a1280d956c57458d3bda52e6ff5b Update Ubuntu job name in Azure pipeline and add string variable creation in C API example
  • 95d2e009ef93fbcd07d531fc4360249a0afc13fa Update OCaml jobs to use Ubuntu-latest in Azure Pipelines configuration
  • 0604d23c570970155ed56d58f545b8533d336be1 Check if model_converter is non-null before initializing values in sat_tactic
  • 5a6dc18d0d7843a6b8583be193056fee467995f6 Override convert_initialize_value method in bit_blaster_model_converter.cpp
  • 5c583299f1983bcd7300f82d96b1b81e5634baee Remove unnecessary const qualifiers from comparison operator overloads in z3++.h
  • ee347735be8246d7150fa90b1e35cfc5f02bb835 remove junk
  • eb8c63080a9f37e023fce58caf76e82e4497c406 Refactor and fix uninitialized variables and improve function consistency across multiple modules
  • 499ed5d8445607c03c4bd11e5cba27a91dfec578 remove unneeded iterator functions
  • 737c2208fad6c006a391897663adba71215f066f delete more default constructors
  • 4b4a28239f9a06e9e10049f73f65e9859268b0a6 Add const qualifiers to comparison operators and update iterator equality checks in various classes
  • a62fede64ba641cb6158f3bfdd22fd86f87d55f9 remove a few default constructors
  • 22d9bfad358eefaa2f7aa490983463f6b0dd022f fix warning with iterators due to non-const comparator
  • 11218154391d5137ab35a3281fb6283587c08ba0 Standardize C++20 flag across different platforms in build script
  • 1e580a7f12cb1cbba6aed4d3484bae4988e06806 update to c++20, remove debug output
  • 96c13757864c3fb5ec91e811fb4b4186fcd4ce91 #7391
  • a9f8ec1bcb997ab7d386e67ff4825450b110728a updated handling of value initialization for bit-vectors
  • ba5cec77045720d9cb81edbf102e473762762f37 additional rewrites for bv2int
  • fa7fc8ef5ed98849f1a1408130f61a1b98bf58ca Refactor bv_rewriter functions using unified variable assignment and early break logic
  • d66609ea14e8d329bb1ab730c93c98f3f67250be fix #7389
  • 0c48a50d59f207e3f1dee38a02391fd21f038d5b Add support for initializing variable values in solver and optimize contexts in Z3
  • 342dccdc0223b10f03369b037d529b396f70843b correctly process cancellation in gomory cuts
  • b99c4a47a4097cc6a671808f1e8abafcfd54bd06 Add override specifiers to methods in set_initial_value_cmd class for clarity and consistency
  • 8349ee006936f8088e2cbba66504bd2c8fc458a4 Add support for const array in all logics as per issue #7383
  • 4896edfb042a44c05b57770d4f77298723071c28 Add tracking of values size in scoped_state push method in opt_context
  • a3f35b6830fb9639a3e1d0dc23250e91973cb244 Add command to set initial value hints for solver in various components
  • 1c163dbad2d2d9716a6a9eb7654a6a4387104ee3 remove output
  • 0f896503a9ffe875936ec4f80094ea0e587e833a Add initial value setting API for solver and optimize contexts and update related function signatures
  • 48712b4f60e090b3e95bb71063cbfe37c1c1d353 Add initial value setting for variables in Z3 API, solver, and optimize modules
  • 0ba306e7b320901540162bfd7cf70c7b7399be17 y
  • 99a9a4af03ed34fd4bd13b9881ca5910646d4c54 fix #7372
  • 1ace3d0cf3f1a0f1c1c4a39a581674ebe7fa5306 fix #7372

... (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.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
  • improved Java use of reference queues thanks to Thomas Haas #7131
  • fixes to conditional import of python library thanks to Cal Jacobson #7116
  • include universe for constants that get removed during pre-processing #7121
  • code improvements, Bruce Mitchener #7119
  • fix nested callback handling for user propagators
  • include ARM64 binaries in distribution

... (truncated)

Commits


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)
codecov[bot] commented 1 month ago

Codecov Report

All modified and coverable lines are covered by tests :white_check_mark:

Project coverage is 87.78%. Comparing base (60a4ef5) to head (afa24a7). Report is 1 commits behind head on main.

Additional details and impacted files ```diff @@ Coverage Diff @@ ## main #707 +/- ## ======================================= Coverage 87.78% 87.78% ======================================= Files 84 84 Lines 20721 20721 ======================================= Hits 18190 18190 Misses 2531 2531 ```

:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.