Nightly

Z3Prover/z3

版本发布时间: 2023-12-25 11:44:31

Z3Prover/z3最新发布版本:z3-4.13.0(2024-03-08 03:21:18)

nightly build

Changes:

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

See More

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