search

alcides / GeneticEngine

A Hybrid between Grammar-Guided and Strongly-Typed Genetic Programming in Python
33 stars 6 forks source link

Bump z3-solver from 4.12.1.0 to 4.13.0.0 #169

Closed dependabot[bot] closed 6 months ago

dependabot[bot] commented 6 months ago

Bumps z3-solver from 4.12.1.0 to 4.13.0.0.

Release notes

Sourced from z3-solver's releases.

Nightly

nightly build

Changes:

  • e873664fe804ac5bc3831340928fa40d4816887a Downgrade arm cross compile toolchain to glibc 2.34 (#7153)
  • 364da191223cf49e5b18fd4cb30ac9193e23555b remove test
  • 620efbb67b6c43457620daebcce7faac92baaa26 add aacrhc
  • aad8cbdd9d26b3c2b73b376bf8da7c78420f6cb1 Add LinuxBuildsArm64 ci azure-pipelines for testing (#7152)
  • 017367d7af4b834c5062ceeba95668abbbcf2fa7 Handle cross compile within manylinux (#7150)
  • e8c8d8aa7dca9cfa48b3c9b51cd2508d17fc9931 Put in workaround to rename manylinux_arm64 to manylinux_aarch64 (#7149)
  • d6f522e205a03f5d6c59fa415cf59d182e2b3e84 na
  • 531bda39ac7f97656c831b1b6ed18f1ceb232ad5 fix alias bug
  • 657aaf9a0fd9d6e427aca3f8228e77fd3472927a na
  • 8679c08010fa180e165dbdf658ed09e8a5304898 fix test
  • 22616da63bdb2c43d8dd9644ba1fb1f09a8a54fc updates
  • 5be8872d6a90e6a4133fab4f25f5d880eff8ee11 na
  • dfd5c27fec205f9fd939e6a208dac7ffab73cad4 na
  • 803f0f0c65d1be10d684d69f8c36b70e73e59d64 na
  • 5455603910da128969dda0fd533806da758db1e4 na
  • 9888d87294eb91ace7dee171fd5ab3bbaefb37fc na
  • f46c3782d69be9384dab169c0dfcd0786f045aaf bugfixes
  • d774f07eb3a2f20e9fb58423aeb66b8b217d0cc9 add eval field to sls-valuation to track temporary values.
  • 8f139e862c5a22d59ebc8f0127e1105c7ba04e0f updates to multiplication
  • 2590d672f464d96c5777331237e8dcc8dc5c537c na
  • 58474df4381b0102a68d778a8a9e1dd0c6253883 na
  • 0e5b504c309f189af0840c3bce3071046396df71 remove bw setting
  • a328366c7d0a533ac964080660b58ee63cbc1e1b move to single path mode for search
  • 8f85df05edd24df573f108b27e6d888a4b270481 fb
  • c451e4e50bfc6e1bbd5fd9f61b070463d1a7732a na
  • 63804c52962837d33e1fe633ec68e6b0a30d603d na
  • 74e73f2b8468ce2e43e9684b7f883f07d3e5a769 reorg to use datatypes
  • 48026edd7fe21cdc3bb707b9246cde1e121f77bd move to hide bits
  • acc9c21653f438676fb0294ad1133f3e5f001dc2 move to hide bits
  • cfa6bd45347ca9b9047dae718e0ca4c91525e9af update python build dependencies
  • 5379fabf9de6856b9ce716589a0c189dd0a6d11a include thread
  • b14499f2301cba4c47e7d8574ad094b148dc0282 prepare for sls experiment
  • cf72a916f8d7c8703aa45605588c0be387c3ec26 bugfixes, adding plugin solver
  • 659e384ee716d3d9f70e7730684141b05439950d bugfixes
  • cd6382f1c86eb3f785443baca643867a95f629fc fix alias bug
  • 9cde4f7e05bfedd8e467044206820d91c0588d4d bugfixes
  • d7e419b7ed2ea4df65334767db0ac48ef5ba4424 fixes and checks
  • ab0459e5aa8d2b3389813ce5b656c9355f536951 bugfixes
  • 7dc4ce8259b6352445601b8103ab121adcbb1ee2 use tuned gcd to compute mult inverse
  • 4391c909609d0b03d3ad540e66338cc21fd2e43e na
  • 991537836b1ee8b96a00850f6554b4c5a881a0a1 fixes based on unit tests
  • 046db662f9ccb1706bae4180931e482f8b9aa879 na
  • 388b2f5eec9c08155ef0947ca26d53479cd96739 n/a

... (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.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
  • added Julia API, Thanks to Yisu Remy Yang #7108

Version 4.12.5

  • Fixes to pypi setup and build for MacOS distributions
  • A new theory solver "int-blast" enabled by using:
    • sat.smt=true smt.bv.solver=2
    • It solves a few bit-vector problems not handled by bit-blasting, especially if the bit-widths are large.
    • It is based on encoding bit-vector constraints to non-linear integer arithmetic.
  • Optimizations to the arithmetic solver. Description: https://github.com/Z3Prover/doc/tree/master/arithmetic

Version 4.12.4

  • Re-release fixing a few issues with 4.12:
    • Python dependency on importlib.resources vs importlib_resources break automatic pypi installations. Supposedly fixed by conditioning dependency on Python 3.9 where the feature is built-in.
    • Missing release of arm64 for Ubuntu.
    • Futile attempt to streamline adding readme.md file as part of Nuget distribution. Nuget.org now requires a readme file. I was able to integrate the readme with the cmake build, but the cross-platform repackage in scripts/mk_nuget_task.py does not ingest a similar readme file with the CI pipelines.

Version 4.12.3

  • Alpha support for polymorphism.
    • SMTLIB3-ish, C, Python It adds the new command (declare-type-var A) that declares a symbol (in this case A) globally as a polymorphic type variable. The C API contains a new function Z3_mk_type_variable and a new enumeration case Z3_TYPE_VAR as a kind associated with sorts. All occurrences of A are treated as type variables. A function declaration whose signature uses A is treated as a shorthand

... (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 6 months ago

Codecov Report

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

Project coverage is 86.40%. Comparing base (c7a3085) to head (e35fdaa).

Additional details and impacted files ```diff @@ Coverage Diff @@ ## main #169 +/- ## ======================================= Coverage 86.40% 86.40% ======================================= Files 83 83 Lines 4193 4193 ======================================= Hits 3623 3623 Misses 570 570 ```

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