z3-4.12.5
版本发布时间: 2024-01-22 04:13:55
Z3Prover/z3最新发布版本:z3-4.13.0(2024-03-08 03:21:18)
4.12.5 release
Changes:
- a7b564cafe3b96c8a868388bc4b96b319facea44 update release scripts and notes
- 7486e8724f234b648de9efa92d5508f1d2672866 track quantifier instantiation method in proof hint #7080
- 302ebff70492fc70788f6d1c5b05defd0d1a617b prepare for release
- e722dc77773f595800a3393ee0b39e8388f90b90 add status badge for windows build, remove windows build from Azure pipelines
- 2dd45f8c1967ecbae85b7e5eb771d29697bf13f1 add Windows build
- 910b3023c22d32469b0a780280132d3bcb148ec0 free memory the clean way
- d32dcfc4a4512f61e9c4aa3c97a9dabe5050f7ea free memory the clean way
- 17545233e6354d9822efada84a48ca19bdfda69f encapsulate anum functionality
- 548be4c1f92447fa45e283c2903bb3ea939909bb add explicit move constructor to deal with unit test regression test-z3 algebraic on Windows/debug -
- a2993f7457923ecfa1a7bdcaa5057b81f900a01b encapsulate mpz a bit more
See More
- d2706bab649b966170189d25090284c21cce7186 Fixes in Java's User Propagator (#7088)
- 2c55aa5466197ad5ee92c732fa14305a9ba69f3e remove unused code
- d084a19630a7c21018cb298258ac165e52f7fa2f take care of strategy undecided, Nikolaj's comments
- 6e9a93853312346e5f055e21672393301636beac Merge branch 'master' of https://github.com/z3prover/z3
- c591a7a3e78dfd5f7b9923f2e95cf5922a475236 force int bound on int columns, call term_is_int() after subst
- fef1596c813f0016a22f0febe335da52f61aea98 pin expression passed to validate_eq
- 4f75153186f0ceb3a1f8ba3aeee842514e51a3e7 Update z3_api.h
- c340233df6bbe98b6225176aed2ba3697236b545 fix #7081
- afba43a5a732afa18f361686e5e68135d0a5e02a fix #7085
- 4ff352fcace8880e3607f643683ca6e9c88c87fd fix #7084
- 91ca55e5ad159abcc6c90c5576af57076c7b52bc change the definition of Gomory row
- d8df203622a519a7e54a72b22a479e7be9e02318 remove an unused declaration
- e2fb4fbd387f06bd670146163df11ee650eb50cd fix dependencies for Gomory polarity
- 2eadcf0872b6feab9ff42db552b1df4740d4f34b avoid duplicate explanations
- 7d7fef061f2ac296835f23e22e8be70bdd9eeef3 add explanations and fix polarity
- ddf2eb57d629eb702fcdf30edd963645ed0d3da1 deleted parameter
- 3381fd2b52615189895a2704a474b9a5ba7637a4 spell check from https://github.com/microsoft/z3guide/pull/165
- 27171591d1d6c94978f5d7f7122b0b8b2f0bc321 Update sat_params.pyg
- 59b18d4a14eeec6bd887b8135e34677f373e9f02 create as_bin as_hex wrappers for display
- 999e67df0db670d86275acee572f4f89ccf0c505 address Nikolaj's comments in Gomory cut
- 2d2443658287c54cdad4dd712839ed0d1c2dc467 remove a blank line
- 2b974a0f1dacd465fc4d2345348295f081892c8b do not delay update for the polar case
- 2ac866a8d088b73d5310051ffc31ca909fa1162a take the coefficient from cut_result, not lia
- 1b3929099b445359aa1982940be3da75a8d060e6 try to remove version spec
- b23937126571cf9cd774e58f26d5f26b499d36f3 try to remove version spec
- aa4e1b34bb2ce3d945a25d1bce05874a43efa44f update Julia versions
- 955c80e98bbda9df668eef218705f218d44a3850 import updates from poly branch
- 2ca1187b3ad5308c824d37dab5dfe310eacc1029 fix a bug in polarity
- 75005d907725f0c2d4e2f6cf1ebe15ab9d6352c7 add validation option for debugging regressions
- 2934618c50bc85d94f6f201e62c1581e1a9fce01 remove simplify_inequality from gomory.cpp
- 696b70fddbf5017f3c883f9d874ba78ff1e71da7 fix
- 239d68ed9cb439fe8c8f6501151bbf6543525224 return conflict on an empty term in Gomory cuts
- b75367ffc70ae6a950ba51c0f40d822ec42bc4e3 port improvements to arith rewriter
- a7bfdcd0ea4d9d4b6b080e3140e6e01836212806 readd big cuts
- 84997f8b21ec6d4c63d6b3fad21953ff22624b46 move a TRACE statement
- fd2b6c62d1e909317d786611bfb2d24d615ae4a2 bug fix in gomory polarity
- d66df2616f7523e991e779dc7896a482bb4d3482 Fix some typos. (#7075)
- ec2b8eb4ca914f7d73457744e9cbf0531c4018f1 Merge shared parts from polysat branch (#7063)
- 53c95e3627325dcae5a01cd3e01ec3f2c301a7e4 cleanup
- 0728b81e9e272848abcef628c965f9c8ee1f408e add parameter lp_settings.m_gomory_simplify
- 5796e8899f6c17051e565c26e67834701e6a2cce use vector instead of unordered_map in gomory
- a3529a0046e4c0bcc3e500183d8770c750eafa64 create bounds for gomory cuts with big numbers
- af7691224e6fd6dae8ea9b3356e051d445e523f0 adding the polarity bound
- d7931b93425e5db3dbd0366f1dbdb843313f3fb4 Bump microsoft/setup-msbuild from 1.1 to 1.3 (#7071)
- ebe5ebf0ae63bf520839b4d34d7b19e0af87fe36 Add branch and bound solver, for fun
- ad07e0e18d9806c4461beac7670faf4431727af7 add sub and super-slice functionality directory to euf-bv-plugin
- cd331b8a56bfb76208c0e27e8daef6e2db2a4694 remove reference to tactic.h
- 7adb402a3fa9fbbf66d7ed18f0431d5061281b66 add missing dependencies
- 5f451182f771975796e67093cc1fbbdd6750c18d missing cmake list
- e321643bf5d66e4be6dd71c41e20fd17b6a3c277 move sls core functionality to be independent of tactic
- 606a9a7409df8b31301b9ebd8fedfc357098a6a5 fix test build
- cab3c45863d5e64a79b22a841d265dd4122cffe5 remove unnecessary parameter copies
- ab22e763d72a94937c7b56a3b986444b860c160a some code simplifications in mpn
- 4fe423482a1644ea54965768ce332cbb4c20a21c bugfix on slack
- 766f5f04c0d86cf6fb1ed1ef2da07eab3487a797 reduce memory allocs in params
- ae1d9270b55e6e35d132c9f1cb9c43541da60fe3 improve add bin/item functions
- b09c23777549529e6f5d89f001e1ff40ce6dc197 rudimentary bin cover solver using the user propagator
- 68a2c08d5eeb1ef406acd810c62c559339b65f12 Add Z3_get_estimated_alloc_size to OCaml API (#7068)
- 19f3ad46ce0d41a55c3119c9ed4e70ea79f972d3 fix the build
- e9fa7db96cc927d92dfc58ac26a79a717e9288f8 revert smt_enode
- a00eb08dddf5597328f11ef5dfc19d6fd0045a9e Merge branch 'master' of https://github.com/z3prover/z3
- 4317d134bfc82e3326b34d519b8a5eb0359c17e4 refactor: move gomory functionaly from int_solver to gomory
- c4fa719751bf867fb9ad61bb60d94eac11e13291 revert last two commits; MSVC doesn't like to statically allocate flexible arrays
- 6246c6517d8743185d8e0b73b7e1a799351ba176 fix debug build
- c9c53b7c6501c7ccd4657353061fbef05aa411b7 tmp_enode: don't heap allocate an app. store it inline instead.
- 4898a156d8fcc2a627e82778fae6b55437f829f7 shrink ast's app by 8 bytes on 64-bit platforms when number of args > 0
- b2d5c24c1df440b653bd6a31955849545a8bf6ad remove a few string copies
- e28b644a67d44cc39c5ec33456957226c9a9ce1c remove an empty line
- d6365610d54087f2167c8e05423e6a7b3089df2c change some TRACE statements
- db5a1a7604bfe06299d4273ee4affb2132d24851 Bump actions/upload-artifact from 3 to 4 (#7065)
- 97d450868ed06f06874c73210b90c3373075f110 Vector updates from polysat branch (#7066)
- 4c9f705cd18054c36f8afd4e13b42ec8b85bf01e tptr: add pointer tagging templates (#7067)
- fcc7b25c191519990b9710db9a86b222e6be8521 remove a few string copies
- e5f52e213146c6fc3d3a60bbaee6cdfaef93cb85 Update Windows.yml
- d088fe9c439b88743f040342734ebd34d130d78b Merge branch 'master' of https://github.com/z3prover/z3
- 9a18628b17d2704ada69f05774fa4849db70e219 remove unnecessary assignments
- 5cafda1fad936148d023b6eafe8d49e0f83dedc7 remove reference to matrix bindings to see if it works
- 2602fc2eb56b55cdb5d5b38fb997341fc76ccde2 remove reference to matrix bindings to see if it works
- 1b7550483e2ce2f3153654bd7497fe0df983b935 add path n prefix
- 00965cbdf2be02a55b62ae35dd7639a037debd82 fix string
- 394a355b19b6f88b593c54e6d1b01570ba1570d8 fix string
- 9469f7574a60ec7185afc6665978387e29d60ee2 Update Windows.yml
- ea03b558c6549cdfbf70f55915182c1b6e89d7b6 Update Windows.yml
- bb8ed43cdb07e9d88319ea89199693c7ce776bdb Update Windows.yml
- ea44c110bb5c81d4c190c0c601c5aeafa20f2b91 gc expressions in the scope of updates, not old expressions
- 842385a7d7c59800810aee32a01d2d89bee0278c Update Windows.yml
- 62ae9a0b7264ebf252cc38263dcf08a9eb44e930 Update Windows.yml
- 91ba893d7b4ca6c8fc46a89246d421960c6550f5 Update Windows.yml
- ee073be3f01490638f1515afb5d8a10263529f57 Update Windows.yml
- c7c007c2c66e28f584927ceee359e6b8e2832b24 Update Windows.yml
- 9e3a489a6c2cf03b4556ddcca51b2283a84d5277 Update Windows.yml
- 0dc851132ea75cff932146beaa22427977f31b18 Create Windows.yml
- 13be3c3fbb75e62cba56f55aa8ba1f0d073525b2 reset model converter between rounds to elim-unconstrained.
- 0daa05aab224dd6e506ca65e2de501f2b703945a add ability to log selected bv rewrites
- dff419a7cb5cadc46fc29b99cb4b9d748ad7621f pin expressions to fix unsound behavior
- 5d4c18dde27f6e81711bdcabe23e84cf43d8e8bf fixes
- 6d23847482e8ae9f9b68f0bc6e2ff9e371a33ae2 fix typos
- d008dbe50adc47d776b477158b0beb4238562668 port Jakob's update to bv_internalize
- 085b5e2588f048d6ff2bfec9776e0cf2cb724f3c port Jakob's update to union_find from polysat branch
- 2f2bf749b9d3fb71f2ae49ffaafde5b6e370f96c fixes to intblast encoding and more arithmetic rewriters
- bb99f442147bf87cc2cd437e6edfdf2ae7e9a068 fix bugs in elim-unconstr2 and fix bugs in intblast_solver
- 4867073290378ec4a31eb06b4df507c815a12473 remove windowsArm64 from nightly
- d0a59f37404c7ccf0d2e13eda40dd8da3f6884d5 intblast with lazy expansion of shl, ashr, lshr
- 50e0fd3ba66e4e2910a081e21671be2429a48ac5 Use
noexcept
more. (#7058) - b44ab2f6204b12d338cccdfa28449cc5c0993553 add rewriters for and
- 4778f27b46aba4171a05c385ed2bb1cf0694cc95 revert to standard solver
- 9293923b8adb69f9775e7cce53ed17b032730fb6 Add intblast solver
- 0520558fc0e18979d79935c3630ad5bde09a1dae port updated pdd from polysat
- 2e83352d425f8fc8b357a48ae536fafb4edc6417 Fix bug in fp.round_to_integral (#7060)
- e90a84450859038ce5c97d51dca833de03f19ae6 Use
override
more. (#7059) - f6e69d43a361012b0a53a252425b8d5f3a963695 Merge branch 'master' of https://github.com/z3prover/z3
- a2b490baa6f092be60d9797e7ddbeabe37b2671f Disable Python compilation cache during build (#7057)
- 7c2e4f2f9c546ee0b8ed241c7ea85a903b2b7c38 fiddle with what gets added to win-arm64
- f7d9a5ba935163ddefd3e1883878556d713d6fee Revert "Disable Python compilation cache during build (#7052)" (#7054)
- b40e3015efe5092e072a85cc41770e3a946e06ae fix #7053
- c20b8cb9788bc445600c637e763c9c37e0fb6c57 nightly
- 995b40865b868511f8e627b7728c07b9d35520c9 remove readme reference, add arm64 build to nightly
- 8293be859f0b8eb4c2b818f245c912864e79bde0 Disable Python compilation cache during build (#7052)
- 3ebec56880ec7e1b55993ea80ef44a71d2dbf3d8 tptr.h: Include
<cstdint>
once rather than twice. (#7051) - 536f4f84bb5e42c882512012102df0bc08f26018 Merge branch 'master' of https://github.com/z3prover/z3
- 0f4e96ac5d76bbf860ee80a6d0943e0a5589db1b fix character
- 5fc039d6ea60e12bb319fa01c4b76e9818949596 nuget spec: does this work?
- 5732c3c98031e51eb803839b637f5aba4aed25a9 add readme under content
- 91837c3aeeafb5a0d1c4a7e3225f572f99d17e39 try adding readme again
- 70d4f32ffd56b2508bb2c2ae8bc37a8452561d5b port updates from poly/polysat
- e580c384b89c89f6536cc3e2e6a72471b0139bbe import updates to rational from polysat
- 575538d32580a7d0b2ef8f721a817abfd6e8afc6 follow error message to put dependencies in setup args
- 4123405d176fb49e8e304a70405ae55448bc8ee4 add version
- 6282f402550e53766f28ed9354772209b93cb098 try add name to project
- 7e716f7cfe75b7da51167b0c4545c3506760351c try fix suggested in #7041
- 8e26c2af17f33439b20c90fc865152de67cfb2df fix #7049
- 6cd619d377d829a81249cef93279afebcd945b44 kludge to fixup osver in python for Mac
- 4d1d067d42c3ea9d2928448b39695389c0e38552 fix divergence reported by Guido Martinez
- 6afed0819c3c1ab515d7606bc4b703a4d8f9d405 update minor version number
- fc23a498c4da724746263f25432f639de2b5c213 a simple version of choosing a column for gomory cut
This list of changes was auto generated.
1、 CodeSignSummary-4050837d-b405-45bf-a0e4-8f6a5ee6929e.md 386B
2、 CodeSignSummary-4657c960-ebc3-401c-9e15-24be3a24912e.md 386B
3、 CodeSignSummary-65009740-62d9-4c22-a182-fc5e7b3c229f.md 386B
4、 CodeSignSummary-c0050cb3-1d10-4001-ab04-b0cd51324ca4.md 386B
5、 Microsoft.Z3.4.12.5.nupkg 29.29MB
6、 Microsoft.Z3.4.12.5.snupkg 41.77MB
7、 Microsoft.Z3.x86.4.12.5.nupkg 5.78MB
8、 Microsoft.Z3.x86.4.12.5.snupkg 38.28MB
9、 z3-4.12.5-arm64-glibc-2.35.zip 46.02MB
10、 z3-4.12.5-arm64-osx-11.0.zip 32.94MB
11、 z3-4.12.5-x64-glibc-2.31.zip 45.9MB
12、 z3-4.12.5-x64-glibc-2.35.zip 46.01MB
13、 z3-4.12.5-x64-osx-11.7.10.zip 35.59MB
14、 z3-4.12.5-x64-win.zip 55.11MB
15、 z3-4.12.5-x86-win.zip 49.1MB
16、 z3-solver-4.12.5.0.tar.gz 4.6MB
17、 z3doc.zip 9.94MB
18、 z3_solver-4.12.5.0-py2.py3-none-macosx_11_0_arm64.whl 25.71MB
19、 z3_solver-4.12.5.0-py2.py3-none-macosx_11_0_x86_64.whl 28.5MB
20、 z3_solver-4.12.5.0-py2.py3-none-manylinux2014_x86_64.whl 54.29MB
21、 z3_solver-4.12.5.0-py2.py3-none-win32.whl 53.68MB
22、 z3_solver-4.12.5.0-py2.py3-none-win_amd64.whl 56.46MB